orderPartyNode

The package each party argues from.

def orderPartyNode : OrderParty → ArgumentPackage Claim :=
  fun x =>
    match x with
    | OrderParty.lst => lstOrderCase
    | OrderParty.arian => arianCase
    | OrderParty.augustine => augustineCase
    | OrderParty.athanasius => athanasiusCase
    | OrderParty.calvin => calvinCase
    | OrderParty.eternal => eternalAuthorityCase
    | OrderParty.equal => equalAuthorityCase

orderDispute

The dispute over the order texts: every party can be held without contradiction, delivers its conclusion, and has its steps rated.

def orderDispute : Dispute Claim OrderParty :=
  { node := orderPartyNode, consistent := orderDispute._proof_1,
    sound := orderDispute._proof_2,
    rated := orderDispute._proof_10 }

orderDispute_defeats

Who defeats whom, all 49 pairs. The Arians and each of Augustine, Athanasius and Calvin defeat each other. Calvin and Augustine defeat each other as well: Calvin denies that John 14:28 speaks of the Son's human nature, which is Augustine's reading. Grudem and Ware and Giles defeat each other. Nothing attacks LST. Every cell is checked by the kernel.

theorem orderDispute_defeats : ∀ (i j : OrderParty), orderDispute.defeats i j
    ↔ (i, j) ∈ [(OrderParty.arian, OrderParty.augustine),
    (OrderParty.augustine, OrderParty.arian), (OrderParty.arian,
    OrderParty.athanasius), (OrderParty.athanasius, OrderParty.arian),
    (OrderParty.arian, OrderParty.calvin), (OrderParty.calvin,
    OrderParty.arian), (OrderParty.augustine, OrderParty.calvin),
    (OrderParty.calvin, OrderParty.augustine), (OrderParty.eternal,
    OrderParty.equal), (OrderParty.equal, OrderParty.eternal)]
-- axioms: propext, Classical.choice, Quot.sound

orderDispute_supports

Nothing supports anything, in all 49 pairs. Every cell is checked by the kernel.

theorem orderDispute_supports : ∀ (i j : OrderParty), ¬orderDispute.supports i
    j
-- axioms: propext, Classical.choice, Quot.sound

orderDispute_partOf

LST's case is part of every other party's, since each holds the order texts and the order drawn from them. Every cell is checked by the kernel.

theorem orderDispute_partOf : ∀ (i j : OrderParty), orderDispute.partOf i j ↔
    i = j ∨ (i, j) ∈ [(OrderParty.lst, OrderParty.arian), (OrderParty.lst,
    OrderParty.augustine), (OrderParty.lst, OrderParty.athanasius),
    (OrderParty.lst, OrderParty.calvin), (OrderParty.lst, OrderParty.eternal),
    (OrderParty.lst, OrderParty.equal)]
-- axioms: propext, Classical.choice, Quot.sound

orderMap

The dispute over the order texts drawn: who defeats whom, and whose case is part of whose.

Solid red: defeats. Dashed green: supports. Dotted blue: one party's case is part of another's.

The defeats are the cells of orderDispute_defeats, the supports the cells of orderDispute_supports and the parts the cells of orderDispute_partOf, each computed from the parties' premises and checked by the kernel. The attacks derived through support and through parts are reported, not counted: every verdict is computed from the defeats alone. Every derived attack is already a defeat.

nicene_readings_stand_with_the_eternal_order

Augustine's and Athanasius's readings can be held with Grudem and Ware's eternal order: nothing in the two forms, or in "greater" as the one the Son is from, rules it out. This does not say that Augustine or Athanasius held it. Giles reads them as denying it, and Augustine writes that the Son "was not sent in virtue of some disparity of power or substance" (On the Trinity IV.20.27, as Grudem quotes it).

theorem nicene_readings_stand_with_the_eternal_order :
    orderDispute.StandTogether [OrderParty.lst, OrderParty.augustine,
    OrderParty.athanasius, OrderParty.eternal]
-- axioms: propext, Classical.choice, Quot.sound

nicene_readings_stand_with_giles

They can be held with Giles's denial of it too. So the two Nicene readings of John 14:28 take no side in the second question.

theorem nicene_readings_stand_with_giles : orderDispute.StandTogether
    [OrderParty.lst, OrderParty.augustine, OrderParty.athanasius,
    OrderParty.equal]
-- axioms: propext, Classical.choice, Quot.sound

What the dispute decides

orderUnanswered

LST's position is accepted at once, because nothing defeats it. No other position can be added to it, because each is defeated by a rival that nothing already accepted answers.

What the dispute forces is exactly The order texts: the Son sent, obedient, and subject at the end.

• Stage 1: The order texts: the Son sent, obedient, and subject at the end.
  • The order texts: the Son sent, obedient, and subject at the end is defeated by nothing.
• Nothing else is forced:
  • Equal in nature, less in the form of a servant (Augustine) defeats The Son less in divinity (the Arians), and nothing forced defeats Equal in nature, less in the form of a servant (Augustine).
  • The Son less in divinity (the Arians) defeats Equal in nature, less in the form of a servant (Augustine), and nothing forced defeats The Son less in divinity (the Arians).
  • The Son less in divinity (the Arians) defeats Greater as the one he is from (Athanasius), and nothing forced defeats The Son less in divinity (the Arians).
  • The Son less in divinity (the Arians) defeats The Mediator's state, not his natures (Calvin), and nothing forced defeats The Son less in divinity (the Arians).
  • No eternal subordination in authority (Giles) defeats Eternal authority and submission (Grudem, Ware), and nothing forced defeats No eternal subordination in authority (Giles).
  • Eternal authority and submission (Grudem, Ware) defeats No eternal subordination in authority (Giles), and nothing forced defeats Eternal authority and submission (Grudem, Ware).

What this rests on. The reasons state 6 defeats and 11 absences of defeat, each a cell of the defeat table, orderDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

• The order texts: the Son sent, obedient, and subject at the end, weakest at well supported:
  • an inference step — Kibbey 2026, §3, The Triune God
• The Son less in divinity (the Arians), weakest at disputed:
  • In John 14:28 "greater" means the Son is less in his divinity — Schaff and Wace 1892, §De Synodis 28; Schaff 1887, §On the Trinity I.7.14; Calvin 1847, p. 102
• Equal in nature, less in the form of a servant (Augustine), weakest at disputed:
  • In John 14:28 the Son is less in the form of a servant, not in the form of God — Schaff 1887, §On the Trinity I.7.14
• Greater as the one he is from (Athanasius), weakest at disputed:
  • The Father is "greater" as the one the Son is begotten from — Schaff and Wace 1892, §Against the Arians I.13.58
• The Mediator's state, not his natures (Calvin), weakest at disputed:
  • In John 14:28 Christ compares his humbled state as Mediator with his glory — Calvin 1847, pp. 102–103
• Eternal authority and submission (Grudem, Ware), weakest at disputed:
  • The sending and obeying are the outworking of an eternal authority and submission — Grudem 2015, p. 40; Grudem 2016; Ware 2005
• No eternal subordination in authority (Giles), weakest at disputed:
  • Eternal subordination in authority would deny the Son's equality in power — Giles 2008, p. 323; Giles 2006

the_order_prevails

What the order texts establish is forced, and nothing more: a real order of Father and Son in the work of salvation. Nothing defeats it, because every party holds every premise it holds. It says nothing about the Son's divinity or about whether the order is eternal; on both, every position is in a tie.

theorem the_order_prevails : Framework.grounded orderDispute.defeats =
    Solver.toSet [OrderParty.lst]
-- axioms: propext, Classical.choice, Quot.sound

arianWithTheOrder

Held with LST's position, the Arian reading defeats each Nicene reading that defeats it.

The Son less in divinity (the Arians) is accepted on some resolution.

• A position holding The order texts: the Son sent, obedient, and subject at the end, The Son less in divinity (the Arians) can be held.
• None of The order texts: the Son sent, obedient, and subject at the end, The Son less in divinity (the Arians) defeats another, and each attack on them is answered from among them:
  • Equal in nature, less in the form of a servant (Augustine) defeats The Son less in divinity (the Arians), and The Son less in divinity (the Arians) defeats Equal in nature, less in the form of a servant (Augustine).
  • Greater as the one he is from (Athanasius) defeats The Son less in divinity (the Arians), and The Son less in divinity (the Arians) defeats Greater as the one he is from (Athanasius).
  • The Mediator's state, not his natures (Calvin) defeats The Son less in divinity (the Arians), and The Son less in divinity (the Arians) defeats The Mediator's state, not his natures (Calvin).

What this rests on. The reasons state 6 defeats and 11 absences of defeat, each a cell of the defeat table, orderDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

• The order texts: the Son sent, obedient, and subject at the end, weakest at well supported:
  • an inference step — Kibbey 2026, §3, The Triune God
• The Son less in divinity (the Arians), weakest at disputed:
  • In John 14:28 "greater" means the Son is less in his divinity — Schaff and Wace 1892, §De Synodis 28; Schaff 1887, §On the Trinity I.7.14; Calvin 1847, p. 102
• Equal in nature, less in the form of a servant (Augustine), weakest at disputed:
  • In John 14:28 the Son is less in the form of a servant, not in the form of God — Schaff 1887, §On the Trinity I.7.14
• Greater as the one he is from (Athanasius), weakest at disputed:
  • The Father is "greater" as the one the Son is begotten from — Schaff and Wace 1892, §Against the Arians I.13.58
• The Mediator's state, not his natures (Calvin), weakest at disputed:
  • In John 14:28 Christ compares his humbled state as Mediator with his glory — Calvin 1847, pp. 102–103
• Eternal authority and submission (Grudem, Ware), weakest at disputed:
  • The sending and obeying are the outworking of an eternal authority and submission — Grudem 2015, p. 40; Grudem 2016; Ware 2005
• No eternal subordination in authority (Giles), weakest at disputed:
  • Eternal subordination in authority would deny the Son's equality in power — Giles 2008, p. 323; Giles 2006

arian_reading_defensible

On the order texts alone, the Arian reading can be defended: some consistent way of settling the dispute accepts it. That is because the readings that answer it, Augustine's, Athanasius's and Calvin's, are rated no higher than it, so each answers the other and none is chosen. It does not say the reading is likely, or that the Son is less than the Father. The texts that say the Son is God, John 1:1 and 20:28 among them, are not heard here.

theorem arian_reading_defensible : Framework.CredulouslyAccepted
    orderDispute.defeats OrderParty.arian
-- axioms: propext, Classical.choice, Quot.sound

arianAnsweredByAugustine

Augustine's and Athanasius's readings, held together, each defeat the Arian one.

The Son less in divinity (the Arians) is not accepted on every resolution.

• A position holding The order texts: the Son sent, obedient, and subject at the end, Equal in nature, less in the form of a servant (Augustine), Greater as the one he is from (Athanasius) can be held, and it holds Equal in nature, less in the form of a servant (Augustine); Equal in nature, less in the form of a servant (Augustine) conflicts with The Son less in divinity (the Arians): Equal in nature, less in the form of a servant (Augustine) defeats The Son less in divinity (the Arians), and The Son less in divinity (the Arians) defeats Equal in nature, less in the form of a servant (Augustine).
• None of The order texts: the Son sent, obedient, and subject at the end, Equal in nature, less in the form of a servant (Augustine), Greater as the one he is from (Athanasius) defeats another, and each attack on them is answered from among them:
  • The Son less in divinity (the Arians) defeats Equal in nature, less in the form of a servant (Augustine), and Equal in nature, less in the form of a servant (Augustine) defeats The Son less in divinity (the Arians).
  • The Mediator's state, not his natures (Calvin) defeats Equal in nature, less in the form of a servant (Augustine), and Equal in nature, less in the form of a servant (Augustine) defeats The Mediator's state, not his natures (Calvin).
  • The Son less in divinity (the Arians) defeats Greater as the one he is from (Athanasius), and Equal in nature, less in the form of a servant (Augustine) defeats The Son less in divinity (the Arians).

What this rests on. The reasons state 5 defeats and 18 absences of defeat, each a cell of the defeat table, orderDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

• Equal in nature, less in the form of a servant (Augustine), weakest at disputed:
  • In John 14:28 the Son is less in the form of a servant, not in the form of God — Schaff 1887, §On the Trinity I.7.14
• The Son less in divinity (the Arians), weakest at disputed:
  • In John 14:28 "greater" means the Son is less in his divinity — Schaff and Wace 1892, §De Synodis 28; Schaff 1887, §On the Trinity I.7.14; Calvin 1847, p. 102
• The order texts: the Son sent, obedient, and subject at the end, weakest at well supported:
  • an inference step — Kibbey 2026, §3, The Triune God
• Greater as the one he is from (Athanasius), weakest at disputed:
  • The Father is "greater" as the one the Son is begotten from — Schaff and Wace 1892, §Against the Arians I.13.58
• The Mediator's state, not his natures (Calvin), weakest at disputed:
  • In John 14:28 Christ compares his humbled state as Mediator with his glory — Calvin 1847, pp. 102–103
• Eternal authority and submission (Grudem, Ware), weakest at disputed:
  • The sending and obeying are the outworking of an eternal authority and submission — Grudem 2015, p. 40; Grudem 2016; Ware 2005
• No eternal subordination in authority (Giles), weakest at disputed:
  • Eternal subordination in authority would deny the Son's equality in power — Giles 2008, p. 323; Giles 2006

arian_reading_not_forced

The Arian reading is not forced. One consistent way of settling the dispute, which can take in no further position, holds Augustine's and Athanasius's readings, and the Arian one cannot join them.

theorem arian_reading_not_forced : ¬Framework.SkepticallyAccepted
    orderDispute.defeats OrderParty.arian
-- axioms: propext, Classical.choice, Quot.sound

augustineWithAthanasius

Held with Athanasius's, Augustine's reading defeats both the Arian reading and Calvin's, the two that defeat it.

Equal in nature, less in the form of a servant (Augustine) is accepted on some resolution.

• A position holding The order texts: the Son sent, obedient, and subject at the end, Equal in nature, less in the form of a servant (Augustine), Greater as the one he is from (Athanasius) can be held.
• None of The order texts: the Son sent, obedient, and subject at the end, Equal in nature, less in the form of a servant (Augustine), Greater as the one he is from (Athanasius) defeats another, and each attack on them is answered from among them:
  • The Son less in divinity (the Arians) defeats Equal in nature, less in the form of a servant (Augustine), and Equal in nature, less in the form of a servant (Augustine) defeats The Son less in divinity (the Arians).
  • The Mediator's state, not his natures (Calvin) defeats Equal in nature, less in the form of a servant (Augustine), and Equal in nature, less in the form of a servant (Augustine) defeats The Mediator's state, not his natures (Calvin).
  • The Son less in divinity (the Arians) defeats Greater as the one he is from (Athanasius), and Equal in nature, less in the form of a servant (Augustine) defeats The Son less in divinity (the Arians).

What this rests on. The reasons state 5 defeats and 18 absences of defeat, each a cell of the defeat table, orderDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

• The order texts: the Son sent, obedient, and subject at the end, weakest at well supported:
  • an inference step — Kibbey 2026, §3, The Triune God
• Equal in nature, less in the form of a servant (Augustine), weakest at disputed:
  • In John 14:28 the Son is less in the form of a servant, not in the form of God — Schaff 1887, §On the Trinity I.7.14
• Greater as the one he is from (Athanasius), weakest at disputed:
  • The Father is "greater" as the one the Son is begotten from — Schaff and Wace 1892, §Against the Arians I.13.58
• The Son less in divinity (the Arians), weakest at disputed:
  • In John 14:28 "greater" means the Son is less in his divinity — Schaff and Wace 1892, §De Synodis 28; Schaff 1887, §On the Trinity I.7.14; Calvin 1847, p. 102
• The Mediator's state, not his natures (Calvin), weakest at disputed:
  • In John 14:28 Christ compares his humbled state as Mediator with his glory — Calvin 1847, pp. 102–103
• Eternal authority and submission (Grudem, Ware), weakest at disputed:
  • The sending and obeying are the outworking of an eternal authority and submission — Grudem 2015, p. 40; Grudem 2016; Ware 2005
• No eternal subordination in authority (Giles), weakest at disputed:
  • Eternal subordination in authority would deny the Son's equality in power — Giles 2008, p. 323; Giles 2006

augustine_reading_defensible

Augustine's reading can be defended, with Athanasius's.

theorem augustine_reading_defensible : Framework.CredulouslyAccepted
    orderDispute.defeats OrderParty.augustine
-- axioms: propext, Classical.choice, Quot.sound

augustineAnsweredByArius

Held with LST's position, the Arian reading defeats Augustine's.

Equal in nature, less in the form of a servant (Augustine) is not accepted on every resolution.

• A position holding The order texts: the Son sent, obedient, and subject at the end, The Son less in divinity (the Arians) can be held, and it holds The Son less in divinity (the Arians); The Son less in divinity (the Arians) conflicts with Equal in nature, less in the form of a servant (Augustine): The Son less in divinity (the Arians) defeats Equal in nature, less in the form of a servant (Augustine), and Equal in nature, less in the form of a servant (Augustine) defeats The Son less in divinity (the Arians).
• None of The order texts: the Son sent, obedient, and subject at the end, The Son less in divinity (the Arians) defeats another, and each attack on them is answered from among them:
  • Equal in nature, less in the form of a servant (Augustine) defeats The Son less in divinity (the Arians), and The Son less in divinity (the Arians) defeats Equal in nature, less in the form of a servant (Augustine).
  • Greater as the one he is from (Athanasius) defeats The Son less in divinity (the Arians), and The Son less in divinity (the Arians) defeats Greater as the one he is from (Athanasius).
  • The Mediator's state, not his natures (Calvin) defeats The Son less in divinity (the Arians), and The Son less in divinity (the Arians) defeats The Mediator's state, not his natures (Calvin).

What this rests on. The reasons state 6 defeats and 11 absences of defeat, each a cell of the defeat table, orderDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

• The Son less in divinity (the Arians), weakest at disputed:
  • In John 14:28 "greater" means the Son is less in his divinity — Schaff and Wace 1892, §De Synodis 28; Schaff 1887, §On the Trinity I.7.14; Calvin 1847, p. 102
• Equal in nature, less in the form of a servant (Augustine), weakest at disputed:
  • In John 14:28 the Son is less in the form of a servant, not in the form of God — Schaff 1887, §On the Trinity I.7.14
• The order texts: the Son sent, obedient, and subject at the end, weakest at well supported:
  • an inference step — Kibbey 2026, §3, The Triune God
• Greater as the one he is from (Athanasius), weakest at disputed:
  • The Father is "greater" as the one the Son is begotten from — Schaff and Wace 1892, §Against the Arians I.13.58
• The Mediator's state, not his natures (Calvin), weakest at disputed:
  • In John 14:28 Christ compares his humbled state as Mediator with his glory — Calvin 1847, pp. 102–103
• Eternal authority and submission (Grudem, Ware), weakest at disputed:
  • The sending and obeying are the outworking of an eternal authority and submission — Grudem 2015, p. 40; Grudem 2016; Ware 2005
• No eternal subordination in authority (Giles), weakest at disputed:
  • Eternal subordination in authority would deny the Son's equality in power — Giles 2008, p. 323; Giles 2006

augustine_reading_not_forced

Augustine's reading is not forced: the Arian reading, rated no lower, leaves it out of one consistent settlement.

theorem augustine_reading_not_forced : ¬Framework.SkepticallyAccepted
    orderDispute.defeats OrderParty.augustine
-- axioms: propext, Classical.choice, Quot.sound

athanasiusWithTheOrder

Athanasius's reading defeats the Arian one, the only reading that defeats it.

Greater as the one he is from (Athanasius) is accepted on some resolution.

• A position holding The order texts: the Son sent, obedient, and subject at the end, Greater as the one he is from (Athanasius) can be held.
• None of The order texts: the Son sent, obedient, and subject at the end, Greater as the one he is from (Athanasius) defeats another, and each attack on them is answered from among them:
  • The Son less in divinity (the Arians) defeats Greater as the one he is from (Athanasius), and Greater as the one he is from (Athanasius) defeats The Son less in divinity (the Arians).

What this rests on. The reasons state 2 defeats and 13 absences of defeat, each a cell of the defeat table, orderDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

• The order texts: the Son sent, obedient, and subject at the end, weakest at well supported:
  • an inference step — Kibbey 2026, §3, The Triune God
• Greater as the one he is from (Athanasius), weakest at disputed:
  • The Father is "greater" as the one the Son is begotten from — Schaff and Wace 1892, §Against the Arians I.13.58
• The Son less in divinity (the Arians), weakest at disputed:
  • In John 14:28 "greater" means the Son is less in his divinity — Schaff and Wace 1892, §De Synodis 28; Schaff 1887, §On the Trinity I.7.14; Calvin 1847, p. 102
• Equal in nature, less in the form of a servant (Augustine), weakest at disputed:
  • In John 14:28 the Son is less in the form of a servant, not in the form of God — Schaff 1887, §On the Trinity I.7.14
• The Mediator's state, not his natures (Calvin), weakest at disputed:
  • In John 14:28 Christ compares his humbled state as Mediator with his glory — Calvin 1847, pp. 102–103
• Eternal authority and submission (Grudem, Ware), weakest at disputed:
  • The sending and obeying are the outworking of an eternal authority and submission — Grudem 2015, p. 40; Grudem 2016; Ware 2005
• No eternal subordination in authority (Giles), weakest at disputed:
  • Eternal subordination in authority would deny the Son's equality in power — Giles 2008, p. 323; Giles 2006

athanasius_reading_defensible

Athanasius's reading can be defended. It can be held with Augustine's and with Calvin's, which cannot be held with each other.

theorem athanasius_reading_defensible : Framework.CredulouslyAccepted
    orderDispute.defeats OrderParty.athanasius
-- axioms: propext, Classical.choice, Quot.sound

athanasiusAnsweredByArius

Held with LST's position, the Arian reading defeats Athanasius's.

Greater as the one he is from (Athanasius) is not accepted on every resolution.

• A position holding The order texts: the Son sent, obedient, and subject at the end, The Son less in divinity (the Arians) can be held, and it holds The Son less in divinity (the Arians); The Son less in divinity (the Arians) conflicts with Greater as the one he is from (Athanasius): The Son less in divinity (the Arians) defeats Greater as the one he is from (Athanasius), and Greater as the one he is from (Athanasius) defeats The Son less in divinity (the Arians).
• None of The order texts: the Son sent, obedient, and subject at the end, The Son less in divinity (the Arians) defeats another, and each attack on them is answered from among them:
  • Equal in nature, less in the form of a servant (Augustine) defeats The Son less in divinity (the Arians), and The Son less in divinity (the Arians) defeats Equal in nature, less in the form of a servant (Augustine).
  • Greater as the one he is from (Athanasius) defeats The Son less in divinity (the Arians), and The Son less in divinity (the Arians) defeats Greater as the one he is from (Athanasius).
  • The Mediator's state, not his natures (Calvin) defeats The Son less in divinity (the Arians), and The Son less in divinity (the Arians) defeats The Mediator's state, not his natures (Calvin).

What this rests on. The reasons state 6 defeats and 11 absences of defeat, each a cell of the defeat table, orderDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

• The Son less in divinity (the Arians), weakest at disputed:
  • In John 14:28 "greater" means the Son is less in his divinity — Schaff and Wace 1892, §De Synodis 28; Schaff 1887, §On the Trinity I.7.14; Calvin 1847, p. 102
• Greater as the one he is from (Athanasius), weakest at disputed:
  • The Father is "greater" as the one the Son is begotten from — Schaff and Wace 1892, §Against the Arians I.13.58
• The order texts: the Son sent, obedient, and subject at the end, weakest at well supported:
  • an inference step — Kibbey 2026, §3, The Triune God
• Equal in nature, less in the form of a servant (Augustine), weakest at disputed:
  • In John 14:28 the Son is less in the form of a servant, not in the form of God — Schaff 1887, §On the Trinity I.7.14
• The Mediator's state, not his natures (Calvin), weakest at disputed:
  • In John 14:28 Christ compares his humbled state as Mediator with his glory — Calvin 1847, pp. 102–103
• Eternal authority and submission (Grudem, Ware), weakest at disputed:
  • The sending and obeying are the outworking of an eternal authority and submission — Grudem 2015, p. 40; Grudem 2016; Ware 2005
• No eternal subordination in authority (Giles), weakest at disputed:
  • Eternal subordination in authority would deny the Son's equality in power — Giles 2008, p. 323; Giles 2006

athanasius_reading_not_forced

Athanasius's reading is not forced, for the same reason as Augustine's.

theorem athanasius_reading_not_forced : ¬Framework.SkepticallyAccepted
    orderDispute.defeats OrderParty.athanasius
-- axioms: propext, Classical.choice, Quot.sound

calvinWithAthanasius

Held with Athanasius's, Calvin's reading defeats both the Arian reading and Augustine's, the two that defeat it.

The Mediator's state, not his natures (Calvin) is accepted on some resolution.

• A position holding The order texts: the Son sent, obedient, and subject at the end, The Mediator's state, not his natures (Calvin), Greater as the one he is from (Athanasius) can be held.
• None of The order texts: the Son sent, obedient, and subject at the end, The Mediator's state, not his natures (Calvin), Greater as the one he is from (Athanasius) defeats another, and each attack on them is answered from among them:
  • The Son less in divinity (the Arians) defeats The Mediator's state, not his natures (Calvin), and The Mediator's state, not his natures (Calvin) defeats The Son less in divinity (the Arians).
  • Equal in nature, less in the form of a servant (Augustine) defeats The Mediator's state, not his natures (Calvin), and The Mediator's state, not his natures (Calvin) defeats Equal in nature, less in the form of a servant (Augustine).
  • The Son less in divinity (the Arians) defeats Greater as the one he is from (Athanasius), and The Mediator's state, not his natures (Calvin) defeats The Son less in divinity (the Arians).

What this rests on. The reasons state 5 defeats and 18 absences of defeat, each a cell of the defeat table, orderDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

• The order texts: the Son sent, obedient, and subject at the end, weakest at well supported:
  • an inference step — Kibbey 2026, §3, The Triune God
• The Mediator's state, not his natures (Calvin), weakest at disputed:
  • In John 14:28 Christ compares his humbled state as Mediator with his glory — Calvin 1847, pp. 102–103
• Greater as the one he is from (Athanasius), weakest at disputed:
  • The Father is "greater" as the one the Son is begotten from — Schaff and Wace 1892, §Against the Arians I.13.58
• The Son less in divinity (the Arians), weakest at disputed:
  • In John 14:28 "greater" means the Son is less in his divinity — Schaff and Wace 1892, §De Synodis 28; Schaff 1887, §On the Trinity I.7.14; Calvin 1847, p. 102
• Equal in nature, less in the form of a servant (Augustine), weakest at disputed:
  • In John 14:28 the Son is less in the form of a servant, not in the form of God — Schaff 1887, §On the Trinity I.7.14
• Eternal authority and submission (Grudem, Ware), weakest at disputed:
  • The sending and obeying are the outworking of an eternal authority and submission — Grudem 2015, p. 40; Grudem 2016; Ware 2005
• No eternal subordination in authority (Giles), weakest at disputed:
  • Eternal subordination in authority would deny the Son's equality in power — Giles 2008, p. 323; Giles 2006

calvin_reading_defensible

Calvin's reading can be defended, with Athanasius's, and not with Augustine's, whose reading of the verse it denies.

theorem calvin_reading_defensible : Framework.CredulouslyAccepted
    orderDispute.defeats OrderParty.calvin
-- axioms: propext, Classical.choice, Quot.sound

calvinAnsweredByArius

Held with LST's position, the Arian reading defeats Calvin's.

The Mediator's state, not his natures (Calvin) is not accepted on every resolution.

• A position holding The order texts: the Son sent, obedient, and subject at the end, The Son less in divinity (the Arians) can be held, and it holds The Son less in divinity (the Arians); The Son less in divinity (the Arians) conflicts with The Mediator's state, not his natures (Calvin): The Son less in divinity (the Arians) defeats The Mediator's state, not his natures (Calvin), and The Mediator's state, not his natures (Calvin) defeats The Son less in divinity (the Arians).
• None of The order texts: the Son sent, obedient, and subject at the end, The Son less in divinity (the Arians) defeats another, and each attack on them is answered from among them:
  • Equal in nature, less in the form of a servant (Augustine) defeats The Son less in divinity (the Arians), and The Son less in divinity (the Arians) defeats Equal in nature, less in the form of a servant (Augustine).
  • Greater as the one he is from (Athanasius) defeats The Son less in divinity (the Arians), and The Son less in divinity (the Arians) defeats Greater as the one he is from (Athanasius).
  • The Mediator's state, not his natures (Calvin) defeats The Son less in divinity (the Arians), and The Son less in divinity (the Arians) defeats The Mediator's state, not his natures (Calvin).

What this rests on. The reasons state 6 defeats and 11 absences of defeat, each a cell of the defeat table, orderDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

• The Son less in divinity (the Arians), weakest at disputed:
  • In John 14:28 "greater" means the Son is less in his divinity — Schaff and Wace 1892, §De Synodis 28; Schaff 1887, §On the Trinity I.7.14; Calvin 1847, p. 102
• The Mediator's state, not his natures (Calvin), weakest at disputed:
  • In John 14:28 Christ compares his humbled state as Mediator with his glory — Calvin 1847, pp. 102–103
• The order texts: the Son sent, obedient, and subject at the end, weakest at well supported:
  • an inference step — Kibbey 2026, §3, The Triune God
• Equal in nature, less in the form of a servant (Augustine), weakest at disputed:
  • In John 14:28 the Son is less in the form of a servant, not in the form of God — Schaff 1887, §On the Trinity I.7.14
• Greater as the one he is from (Athanasius), weakest at disputed:
  • The Father is "greater" as the one the Son is begotten from — Schaff and Wace 1892, §Against the Arians I.13.58
• Eternal authority and submission (Grudem, Ware), weakest at disputed:
  • The sending and obeying are the outworking of an eternal authority and submission — Grudem 2015, p. 40; Grudem 2016; Ware 2005
• No eternal subordination in authority (Giles), weakest at disputed:
  • Eternal subordination in authority would deny the Son's equality in power — Giles 2008, p. 323; Giles 2006

calvin_reading_not_forced

Calvin's reading is not forced: the Arian reading leaves it out of one consistent settlement, and so does Augustine's.

theorem calvin_reading_not_forced : ¬Framework.SkepticallyAccepted
    orderDispute.defeats OrderParty.calvin
-- axioms: propext, Classical.choice, Quot.sound

eternalWithTheOrder

Held with LST's position, the eternal order defeats Giles's denial of it, the one position that defeats it.

Eternal authority and submission (Grudem, Ware) is accepted on some resolution.

• A position holding The order texts: the Son sent, obedient, and subject at the end, Eternal authority and submission (Grudem, Ware) can be held.
• None of The order texts: the Son sent, obedient, and subject at the end, Eternal authority and submission (Grudem, Ware) defeats another, and each attack on them is answered from among them:
  • No eternal subordination in authority (Giles) defeats Eternal authority and submission (Grudem, Ware), and Eternal authority and submission (Grudem, Ware) defeats No eternal subordination in authority (Giles).

What this rests on. The reasons state 2 defeats and 13 absences of defeat, each a cell of the defeat table, orderDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

• The order texts: the Son sent, obedient, and subject at the end, weakest at well supported:
  • an inference step — Kibbey 2026, §3, The Triune God
• Eternal authority and submission (Grudem, Ware), weakest at disputed:
  • The sending and obeying are the outworking of an eternal authority and submission — Grudem 2015, p. 40; Grudem 2016; Ware 2005
• The Son less in divinity (the Arians), weakest at disputed:
  • In John 14:28 "greater" means the Son is less in his divinity — Schaff and Wace 1892, §De Synodis 28; Schaff 1887, §On the Trinity I.7.14; Calvin 1847, p. 102
• Equal in nature, less in the form of a servant (Augustine), weakest at disputed:
  • In John 14:28 the Son is less in the form of a servant, not in the form of God — Schaff 1887, §On the Trinity I.7.14
• Greater as the one he is from (Athanasius), weakest at disputed:
  • The Father is "greater" as the one the Son is begotten from — Schaff and Wace 1892, §Against the Arians I.13.58
• The Mediator's state, not his natures (Calvin), weakest at disputed:
  • In John 14:28 Christ compares his humbled state as Mediator with his glory — Calvin 1847, pp. 102–103
• No eternal subordination in authority (Giles), weakest at disputed:
  • Eternal subordination in authority would deny the Son's equality in power — Giles 2008, p. 323; Giles 2006

eternal_order_defensible

Grudem and Ware's eternal order can be defended.

theorem eternal_order_defensible : Framework.CredulouslyAccepted
    orderDispute.defeats OrderParty.eternal
-- axioms: propext, Classical.choice, Quot.sound

eternalAnsweredByGiles

Held with LST's position, Giles's denial defeats the eternal order.

Eternal authority and submission (Grudem, Ware) is not accepted on every resolution.

• A position holding The order texts: the Son sent, obedient, and subject at the end, No eternal subordination in authority (Giles) can be held, and it holds No eternal subordination in authority (Giles); No eternal subordination in authority (Giles) conflicts with Eternal authority and submission (Grudem, Ware): No eternal subordination in authority (Giles) defeats Eternal authority and submission (Grudem, Ware), and Eternal authority and submission (Grudem, Ware) defeats No eternal subordination in authority (Giles).
• None of The order texts: the Son sent, obedient, and subject at the end, No eternal subordination in authority (Giles) defeats another, and each attack on them is answered from among them:
  • Eternal authority and submission (Grudem, Ware) defeats No eternal subordination in authority (Giles), and No eternal subordination in authority (Giles) defeats Eternal authority and submission (Grudem, Ware).

What this rests on. The reasons state 2 defeats and 13 absences of defeat, each a cell of the defeat table, orderDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

• No eternal subordination in authority (Giles), weakest at disputed:
  • Eternal subordination in authority would deny the Son's equality in power — Giles 2008, p. 323; Giles 2006
• Eternal authority and submission (Grudem, Ware), weakest at disputed:
  • The sending and obeying are the outworking of an eternal authority and submission — Grudem 2015, p. 40; Grudem 2016; Ware 2005
• The order texts: the Son sent, obedient, and subject at the end, weakest at well supported:
  • an inference step — Kibbey 2026, §3, The Triune God
• The Son less in divinity (the Arians), weakest at disputed:
  • In John 14:28 "greater" means the Son is less in his divinity — Schaff and Wace 1892, §De Synodis 28; Schaff 1887, §On the Trinity I.7.14; Calvin 1847, p. 102
• Equal in nature, less in the form of a servant (Augustine), weakest at disputed:
  • In John 14:28 the Son is less in the form of a servant, not in the form of God — Schaff 1887, §On the Trinity I.7.14
• Greater as the one he is from (Athanasius), weakest at disputed:
  • The Father is "greater" as the one the Son is begotten from — Schaff and Wace 1892, §Against the Arians I.13.58
• The Mediator's state, not his natures (Calvin), weakest at disputed:
  • In John 14:28 Christ compares his humbled state as Mediator with his glory — Calvin 1847, pp. 102–103

eternal_order_not_forced

The eternal order is not forced: Giles's position can be held with LST's, and it rules the eternal order out.

theorem eternal_order_not_forced : ¬Framework.SkepticallyAccepted
    orderDispute.defeats OrderParty.eternal
-- axioms: propext, Classical.choice, Quot.sound

equalWithTheOrder

Held with LST's position, Giles's denial defeats the eternal order, the one position that defeats it.

No eternal subordination in authority (Giles) is accepted on some resolution.

• A position holding The order texts: the Son sent, obedient, and subject at the end, No eternal subordination in authority (Giles) can be held.
• None of The order texts: the Son sent, obedient, and subject at the end, No eternal subordination in authority (Giles) defeats another, and each attack on them is answered from among them:
  • Eternal authority and submission (Grudem, Ware) defeats No eternal subordination in authority (Giles), and No eternal subordination in authority (Giles) defeats Eternal authority and submission (Grudem, Ware).

What this rests on. The reasons state 2 defeats and 13 absences of defeat, each a cell of the defeat table, orderDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

• The order texts: the Son sent, obedient, and subject at the end, weakest at well supported:
  • an inference step — Kibbey 2026, §3, The Triune God
• No eternal subordination in authority (Giles), weakest at disputed:
  • Eternal subordination in authority would deny the Son's equality in power — Giles 2008, p. 323; Giles 2006
• The Son less in divinity (the Arians), weakest at disputed:
  • In John 14:28 "greater" means the Son is less in his divinity — Schaff and Wace 1892, §De Synodis 28; Schaff 1887, §On the Trinity I.7.14; Calvin 1847, p. 102
• Equal in nature, less in the form of a servant (Augustine), weakest at disputed:
  • In John 14:28 the Son is less in the form of a servant, not in the form of God — Schaff 1887, §On the Trinity I.7.14
• Greater as the one he is from (Athanasius), weakest at disputed:
  • The Father is "greater" as the one the Son is begotten from — Schaff and Wace 1892, §Against the Arians I.13.58
• The Mediator's state, not his natures (Calvin), weakest at disputed:
  • In John 14:28 Christ compares his humbled state as Mediator with his glory — Calvin 1847, pp. 102–103
• Eternal authority and submission (Grudem, Ware), weakest at disputed:
  • The sending and obeying are the outworking of an eternal authority and submission — Grudem 2015, p. 40; Grudem 2016; Ware 2005

equal_authority_defensible

Giles's position can be defended: held with LST's, it answers Grudem and Ware's position, which is the only one that attacks it.

theorem equal_authority_defensible : Framework.CredulouslyAccepted
    orderDispute.defeats OrderParty.equal
-- axioms: propext, Classical.choice, Quot.sound

equalAnsweredByTheEternalOrder

Held with LST's position, the eternal order defeats Giles's denial.

No eternal subordination in authority (Giles) is not accepted on every resolution.

• A position holding The order texts: the Son sent, obedient, and subject at the end, Eternal authority and submission (Grudem, Ware) can be held, and it holds Eternal authority and submission (Grudem, Ware); Eternal authority and submission (Grudem, Ware) conflicts with No eternal subordination in authority (Giles): Eternal authority and submission (Grudem, Ware) defeats No eternal subordination in authority (Giles), and No eternal subordination in authority (Giles) defeats Eternal authority and submission (Grudem, Ware).
• None of The order texts: the Son sent, obedient, and subject at the end, Eternal authority and submission (Grudem, Ware) defeats another, and each attack on them is answered from among them:
  • No eternal subordination in authority (Giles) defeats Eternal authority and submission (Grudem, Ware), and Eternal authority and submission (Grudem, Ware) defeats No eternal subordination in authority (Giles).

What this rests on. The reasons state 2 defeats and 13 absences of defeat, each a cell of the defeat table, orderDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

• Eternal authority and submission (Grudem, Ware), weakest at disputed:
  • The sending and obeying are the outworking of an eternal authority and submission — Grudem 2015, p. 40; Grudem 2016; Ware 2005
• No eternal subordination in authority (Giles), weakest at disputed:
  • Eternal subordination in authority would deny the Son's equality in power — Giles 2008, p. 323; Giles 2006
• The order texts: the Son sent, obedient, and subject at the end, weakest at well supported:
  • an inference step — Kibbey 2026, §3, The Triune God
• The Son less in divinity (the Arians), weakest at disputed:
  • In John 14:28 "greater" means the Son is less in his divinity — Schaff and Wace 1892, §De Synodis 28; Schaff 1887, §On the Trinity I.7.14; Calvin 1847, p. 102
• Equal in nature, less in the form of a servant (Augustine), weakest at disputed:
  • In John 14:28 the Son is less in the form of a servant, not in the form of God — Schaff 1887, §On the Trinity I.7.14
• Greater as the one he is from (Athanasius), weakest at disputed:
  • The Father is "greater" as the one the Son is begotten from — Schaff and Wace 1892, §Against the Arians I.13.58
• The Mediator's state, not his natures (Calvin), weakest at disputed:
  • In John 14:28 Christ compares his humbled state as Mediator with his glory — Calvin 1847, pp. 102–103

equal_authority_not_forced

Giles's position is not forced either. Between it and the eternal order the dispute chooses neither, as LST says the texts do not.

theorem equal_authority_not_forced : ¬Framework.SkepticallyAccepted
    orderDispute.defeats OrderParty.equal
-- axioms: propext, Classical.choice, Quot.sound