Weighing the positions

Nine parties are heard. One holds only what all of them hold: salvation is by grace, from Romans 11:6. Then Dort; Trent, on the Molinist reading of its fourth canon; the Thomists, on theirs; the Remonstrants; the Lutherans of the Formula of Concord; Wesley; the third way as it was put to this argument; and the objection from the Spirit's resistance, with its three routes to the claim that the grace that saves can be finally refused. Who defeats whom is computed from their premises and checked by the kernel.

How to read the verdicts

  • Weakest link. A position is only as strong as its least-supported premise or step. What every party holds rests on Romans 11:6 and a step rated consensus, accepted across traditions. Every other position rests on at least one reading or step rated disputed, the lowest rating, so no rating breaks a standoff between them.
  • Defeats. One position contradicts another (it denies one of the other's premises, its conclusion, or a claim it derives on the way), and its weakest link is not rated below the other's. A defeat that runs both ways is a standoff.
  • Settled before any choice. What prevails once every unanswered attack is taken into account, before any standoff is decided either way.
  • Can be defended. Held by some consistent group of positions that answers every attack on its members, by itself or through an ally. Such a group that no further party can join is a maximal defensible position.
  • Forced. Held in every maximal defensible position, however the standoffs are resolved. A party is shown not forced by naming a maximal defensible position that does not hold it.

Dort's position here does not carry faith alone: the Reformed case is stated from Ephesians 2 and Romans 9, and sola fide is an argument of its own. So Dort and Trent are never set against each other over it; they stand off over the will's passivity and grace effectual of itself.

What the weighing found

Only what every party holds is settled before any choice: salvation is by grace (only_grace_prevails). Everything else is in a standoff with something.

  • Dort stands off against every party that denies part of sola gratia: Trent, the Remonstrants, the Lutherans, Wesley and the objection. Each of them defeats Dort, and Dort defeats each back.
  • Neither Dort nor the Thomists defeats the other (dort_stands_with_the_thomists), because the Thomist position weighed here takes no side on the will's passivity: it holds that the will is "not merely passive" and draws nothing from it. So this does not show that the Thomists hold the third part of sola gratia. In the Molinists' sense the phrase cannot be held with Dort; in Garrigou-Lagrange's it can (the chapter on Aquinas). On faith alone and perseverance, on which they part, Dort's position here carries nothing. So the Thomists can be defended with Dort (thomist_defensible).
  • The Thomists stand off against every party but Dort and what every party holds. Against the Remonstrants, the Lutherans, Wesley and the objection, the standoff is over grace effectual of itself, which the claim that the grace that saves can be finally refused excludes. Against the third way, the Lutherans and Wesley, it is also over faith alone. Against Trent on the Molinist reading, it is the question Rome left open in 1607.
  • Trent stands off against Dort, the Thomists, the Lutherans, Wesley and the third way. With the Thomists the standoff is over grace effectual of itself, the question of the two Catholic schools that Rome left open in 1607 (thomist_not_forced); with the Lutherans, Wesley and the third way it is over faith alone, which Trent's ninth canon condemns; with the Lutherans also over the will's passivity.
  • The Remonstrants, the Lutherans, Wesley and the objection do not defeat one another. They agree that the grace that saves can be finally refused. The Lutherans also hold the will passive; the Remonstrants and Wesley are not encoded with a view on that, so nothing here sets them against each other.
  • The third way is attacked only over faith alone, by Trent and by the Thomists. It takes no side between Dort and Wesley, and so it can be defended with either: with Dort, against Trent (third_way_defensible_with_dort); and with the Remonstrants, the Lutherans and Wesley, against both Dort and Trent (third_way_defensible_with_wesley). The dilemma found the same thing: until the third way says which kind of help God gives, it has taken neither side.
  • Trent can be defended with the Remonstrants and the objection, which agree with it that grace can be resisted, against Dort.

Every party can be defended, and only the first is forced: each of the others is left out of some maximal defensible position. Each standoff rests on readings and steps rated disputed, so the verdict moves only if a new, cited argument moves one of those ratings.

How this is checked

The positions, steps and results behind this chapter, each with the formula or the Lean that checks it

The dispute

partyNode

The package each party argues from.

def partyNode : Party → ArgumentPackage Claim :=
  fun x =>
    match x with
    | Party.grace => graceCase
    | Party.reformed => reformed
    | Party.trent => tridentinePosition
    | Party.remonstrant => remonstrantPosition
    | Party.lutheran => lutheranPosition
    | Party.wesleyan => wesleyanPosition
    | Party.thirdWay => thirdWay
    | Party.objection => objection
    | Party.thomist => thomistPosition

solaGratiaDispute

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

def solaGratiaDispute : Dispute Claim Party :=
  { node := partyNode,
    consistent := solaGratiaDispute._proof_1,
    sound := solaGratiaDispute._proof_2,
    rated := solaGratiaDispute._proof_12 }

solaGratiaDispute_defeats

Who defeats whom, all 81 pairs: twenty-eight defeats, every one of them half of a standoff. Dort stands off against Trent, the Remonstrants, the Lutherans, Wesley and the objection; Trent against Dort, the Lutherans, Wesley, the third way and the Thomists; the Thomists against every party but Dort and what every party holds. Dort and the Thomists defeat neither each other. Nothing attacks what every party holds. Every cell is checked by the kernel.

theorem solaGratiaDispute_defeats : ∀ (i j : Party), solaGratiaDispute.defeats
    i j ↔ (i, j) ∈ [(Party.reformed, Party.trent), (Party.reformed,
    Party.remonstrant), (Party.reformed, Party.lutheran), (Party.reformed,
    Party.wesleyan), (Party.reformed, Party.objection), (Party.trent,
    Party.reformed), (Party.trent, Party.lutheran), (Party.trent,
    Party.wesleyan), (Party.trent, Party.thirdWay), (Party.trent,
    Party.thomist), (Party.remonstrant, Party.reformed), (Party.remonstrant,
    Party.thomist), (Party.lutheran, Party.reformed), (Party.lutheran,
    Party.trent), (Party.lutheran, Party.thomist), (Party.wesleyan,
    Party.reformed), (Party.wesleyan, Party.trent), (Party.wesleyan,
    Party.thomist), (Party.thirdWay, Party.trent), (Party.thirdWay,
    Party.thomist), (Party.objection, Party.reformed), (Party.objection,
    Party.thomist), (Party.thomist, Party.trent), (Party.thomist,
    Party.remonstrant), (Party.thomist, Party.lutheran), (Party.thomist,
    Party.wesleyan), (Party.thomist, Party.thirdWay), (Party.thomist,
    Party.objection)]
-- axioms: propext, Classical.choice, Quot.sound

What the dispute decides

graceUnanswered

How far the dispute is settled before any choice. Nothing defeats what every party holds, so it is settled first; and nothing is settled with it, because every other party has a defeater that what every party holds does not answer.

What the dispute forces is exactly Romans 11:6 (by grace, so not by works).

  • Stage 1: Romans 11:6 (by grace, so not by works).
    • Romans 11:6 (by grace, so not by works) is defeated by nothing.
  • Nothing else is forced:
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort), and nothing forced defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading), and nothing forced defeats Reformed (the Canons of Dort).
    • Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610), and nothing forced defeats Reformed (the Canons of Dort).
    • Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord), and nothing forced defeats Reformed (the Canons of Dort).
    • Reformed (the Canons of Dort) defeats Wesleyan (preventing grace), and nothing forced defeats Reformed (the Canons of Dort).
    • Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith), and nothing forced defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance, and nothing forced defeats Reformed (the Canons of Dort).
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Thomist (Aquinas; Garrigou-Lagrange), and nothing forced defeats Trent (Session VI, canon 4, on the Molinist reading).

What this rests on. The reasons state 8 defeats and 11 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

only_grace_prevails

Only what every party holds prevails: salvation is by grace. What the dispute settles before any choice between rivals is that, and nothing more. Nothing defeats it, because every party holds every premise it holds.

What this does not claim: that sola gratia is false, or that any rival is right. Every other position is in a standoff, and none is forced.

theorem only_grace_prevails : Framework.grounded solaGratiaDispute.defeats =
    Solver.toSet [Party.grace]
-- axioms: propext, Classical.choice, Quot.sound

dortDefended

Why Dort can be defended: with what every party holds and the third way, it answers every attacker itself.

Reformed (the Canons of Dort) is accepted on some resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) can be held.
  • None of Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) defeats another, and each attack on them is answered from among them:
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610).
    • Lutheran (the Formula of Concord) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord).
    • Wesleyan (preventing grace) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Wesleyan (preventing grace).
    • The objection from the Spirit's resistance defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance.
    • Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The third way (an ability given, received by faith), and The third way (an ability given, received by faith) defeats Thomist (Aquinas; Garrigou-Lagrange).

What this rests on. The reasons state 13 defeats and 20 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

reformed_defensible

Dort can be defended, together with what every party holds and the third way: some maximal defensible position, one no other party can join, holds all three.

theorem reformed_defensible : Framework.CredulouslyAccepted
    solaGratiaDispute.defeats Party.reformed
-- axioms: propext, Classical.choice, Quot.sound

dortAnsweredByTheRemonstrants

Why Dort is not forced: a defensible position holds the Remonstrants, and they defeat Dort.

Reformed (the Canons of Dort) is not accepted on every resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Remonstrant (the Five Articles, 1610), Lutheran (the Formula of Concord), Wesleyan (preventing grace), The third way (an ability given, received by faith), The objection from the Spirit's resistance can be held, and it holds Remonstrant (the Five Articles, 1610); Remonstrant (the Five Articles, 1610) conflicts with Reformed (the Canons of Dort): Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610).
  • None of Romans 11:6 (by grace, so not by works), Remonstrant (the Five Articles, 1610), Lutheran (the Formula of Concord), Wesleyan (preventing grace), The third way (an ability given, received by faith), The objection from the Spirit's resistance defeats another, and each attack on them is answered from among them:
    • Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610), and Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Remonstrant (the Five Articles, 1610), and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord), and Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort).
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Lutheran (the Formula of Concord), and Lutheran (the Formula of Concord) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Lutheran (the Formula of Concord), and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats Wesleyan (preventing grace), and Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort).
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Wesleyan (preventing grace), and Lutheran (the Formula of Concord) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Wesleyan (preventing grace), and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith), and Lutheran (the Formula of Concord) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The third way (an ability given, received by faith), and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance, and Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The objection from the Spirit's resistance, and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).

What this rests on. The reasons state 15 defeats and 42 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

reformed_not_forced

Nor is Dort forced. A maximal defensible position holds the Remonstrants, the Lutherans, Wesley, the third way and the objection, and cannot hold Dort with them.

theorem reformed_not_forced : ¬Framework.SkepticallyAccepted
    solaGratiaDispute.defeats Party.reformed
-- axioms: propext, Classical.choice, Quot.sound

lutheransDefended

Why the Lutherans can be defended: with the Remonstrants and Wesley they answer both Dort and Trent.

Lutheran (the Formula of Concord) is accepted on some resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Remonstrant (the Five Articles, 1610), Lutheran (the Formula of Concord), Wesleyan (preventing grace), The third way (an ability given, received by faith), The objection from the Spirit's resistance can be held.
  • None of Romans 11:6 (by grace, so not by works), Remonstrant (the Five Articles, 1610), Lutheran (the Formula of Concord), Wesleyan (preventing grace), The third way (an ability given, received by faith), The objection from the Spirit's resistance defeats another, and each attack on them is answered from among them:
    • Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610), and Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Remonstrant (the Five Articles, 1610), and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord), and Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort).
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Lutheran (the Formula of Concord), and Lutheran (the Formula of Concord) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Lutheran (the Formula of Concord), and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats Wesleyan (preventing grace), and Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort).
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Wesleyan (preventing grace), and Lutheran (the Formula of Concord) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Wesleyan (preventing grace), and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith), and Lutheran (the Formula of Concord) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The third way (an ability given, received by faith), and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance, and Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The objection from the Spirit's resistance, and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).

What this rests on. The reasons state 15 defeats and 42 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

lutheran_defensible

The Lutheran position can be defended, with the Remonstrants, Wesley, the third way and the objection.

theorem lutheran_defensible : Framework.CredulouslyAccepted
    solaGratiaDispute.defeats Party.lutheran
-- axioms: propext, Classical.choice, Quot.sound

trentDefended

Why Trent can be defended: it answers every attacker of its group itself.

Trent (Session VI, canon 4, on the Molinist reading) is accepted on some resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Trent (Session VI, canon 4, on the Molinist reading), Remonstrant (the Five Articles, 1610), The objection from the Spirit's resistance can be held.
  • None of Romans 11:6 (by grace, so not by works), Trent (Session VI, canon 4, on the Molinist reading), Remonstrant (the Five Articles, 1610), The objection from the Spirit's resistance defeats another, and each attack on them is answered from among them:
    • Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort).
    • Lutheran (the Formula of Concord) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats Lutheran (the Formula of Concord).
    • Wesleyan (preventing grace) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats Wesleyan (preventing grace).
    • The third way (an ability given, received by faith) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610), and Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Remonstrant (the Five Articles, 1610), and Trent (Session VI, canon 4, on the Molinist reading) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance, and Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The objection from the Spirit's resistance, and Trent (Session VI, canon 4, on the Molinist reading) defeats Thomist (Aquinas; Garrigou-Lagrange).

What this rests on. The reasons state 14 defeats and 27 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

tridentine_defensible

Trent can be defended, with what every party holds, the Remonstrants and the objection, which agree with it that grace can be resisted. Only Dort attacks the Remonstrants and the objection, and Trent answers Dort.

theorem tridentine_defensible : Framework.CredulouslyAccepted
    solaGratiaDispute.defeats Party.trent
-- axioms: propext, Classical.choice, Quot.sound

trentAnsweredByDort

Why Trent is not forced: a maximal defensible position holds Dort, and Dort defeats Trent.

Trent (Session VI, canon 4, on the Molinist reading) is not accepted on every resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) can be held, and it holds Reformed (the Canons of Dort); Reformed (the Canons of Dort) conflicts with Trent (Session VI, canon 4, on the Molinist reading): Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort).
  • None of Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) defeats another, and each attack on them is answered from among them:
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610).
    • Lutheran (the Formula of Concord) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord).
    • Wesleyan (preventing grace) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Wesleyan (preventing grace).
    • The objection from the Spirit's resistance defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance.
    • Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The third way (an ability given, received by faith), and The third way (an ability given, received by faith) defeats Thomist (Aquinas; Garrigou-Lagrange).

What this rests on. The reasons state 13 defeats and 20 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

tridentine_not_forced

Nor is Trent forced. The maximal defensible position that holds Dort and the third way cannot hold Trent with them.

theorem tridentine_not_forced : ¬Framework.SkepticallyAccepted
    solaGratiaDispute.defeats Party.trent
-- axioms: propext, Classical.choice, Quot.sound

remonstrantsAnsweredByDort

Why the Remonstrants are not forced: Dort's position defeats them.

Remonstrant (the Five Articles, 1610) is not accepted on every resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) can be held, and it holds Reformed (the Canons of Dort); Reformed (the Canons of Dort) conflicts with Remonstrant (the Five Articles, 1610): Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610), and Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort).
  • None of Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) defeats another, and each attack on them is answered from among them:
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610).
    • Lutheran (the Formula of Concord) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord).
    • Wesleyan (preventing grace) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Wesleyan (preventing grace).
    • The objection from the Spirit's resistance defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance.
    • Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The third way (an ability given, received by faith), and The third way (an ability given, received by faith) defeats Thomist (Aquinas; Garrigou-Lagrange).

What this rests on. The reasons state 13 defeats and 20 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

remonstrant_not_forced

The Remonstrants can be defended (with the Lutherans and Wesley, as lutheran_defensible shows), and are not forced: the maximal defensible position that holds Dort cannot hold them.

theorem remonstrant_not_forced : ¬Framework.SkepticallyAccepted
    solaGratiaDispute.defeats Party.remonstrant
-- axioms: propext, Classical.choice, Quot.sound

lutheransAnsweredByDort

Why the Lutherans are not forced: Dort's position defeats them.

Lutheran (the Formula of Concord) is not accepted on every resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) can be held, and it holds Reformed (the Canons of Dort); Reformed (the Canons of Dort) conflicts with Lutheran (the Formula of Concord): Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord), and Lutheran (the Formula of Concord) defeats Reformed (the Canons of Dort).
  • None of Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) defeats another, and each attack on them is answered from among them:
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610).
    • Lutheran (the Formula of Concord) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord).
    • Wesleyan (preventing grace) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Wesleyan (preventing grace).
    • The objection from the Spirit's resistance defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance.
    • Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The third way (an ability given, received by faith), and The third way (an ability given, received by faith) defeats Thomist (Aquinas; Garrigou-Lagrange).

What this rests on. The reasons state 13 defeats and 20 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

lutheran_not_forced

Nor are the Lutherans forced: the maximal defensible position that holds Dort cannot hold them.

theorem lutheran_not_forced : ¬Framework.SkepticallyAccepted
    solaGratiaDispute.defeats Party.lutheran
-- axioms: propext, Classical.choice, Quot.sound

wesleyAnsweredByDort

Why Wesley is not forced: Dort's position defeats him.

Wesleyan (preventing grace) is not accepted on every resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) can be held, and it holds Reformed (the Canons of Dort); Reformed (the Canons of Dort) conflicts with Wesleyan (preventing grace): Reformed (the Canons of Dort) defeats Wesleyan (preventing grace), and Wesleyan (preventing grace) defeats Reformed (the Canons of Dort).
  • None of Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) defeats another, and each attack on them is answered from among them:
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610).
    • Lutheran (the Formula of Concord) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord).
    • Wesleyan (preventing grace) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Wesleyan (preventing grace).
    • The objection from the Spirit's resistance defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance.
    • Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The third way (an ability given, received by faith), and The third way (an ability given, received by faith) defeats Thomist (Aquinas; Garrigou-Lagrange).

What this rests on. The reasons state 13 defeats and 20 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

wesleyan_not_forced

Nor is Wesley's position forced: the maximal defensible position that holds Dort cannot hold it.

theorem wesleyan_not_forced : ¬Framework.SkepticallyAccepted
    solaGratiaDispute.defeats Party.wesleyan
-- axioms: propext, Classical.choice, Quot.sound

objectionAnsweredByDort

Why the objection is not forced: Dort's position defeats it.

The objection from the Spirit's resistance is not accepted on every resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) can be held, and it holds Reformed (the Canons of Dort); Reformed (the Canons of Dort) conflicts with The objection from the Spirit's resistance: Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance, and The objection from the Spirit's resistance defeats Reformed (the Canons of Dort).
  • None of Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) defeats another, and each attack on them is answered from among them:
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610).
    • Lutheran (the Formula of Concord) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord).
    • Wesleyan (preventing grace) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Wesleyan (preventing grace).
    • The objection from the Spirit's resistance defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance.
    • Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The third way (an ability given, received by faith), and The third way (an ability given, received by faith) defeats Thomist (Aquinas; Garrigou-Lagrange).

What this rests on. The reasons state 13 defeats and 20 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

objection_not_forced

Nor is the objection from the Spirit's resistance forced: the maximal defensible position that holds Dort cannot hold it.

theorem objection_not_forced : ¬Framework.SkepticallyAccepted
    solaGratiaDispute.defeats Party.objection
-- axioms: propext, Classical.choice, Quot.sound

thirdWayWithDort

The third way, defended with Dort.

The third way (an ability given, received by faith) is accepted on some resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) can be held.
  • None of Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), The third way (an ability given, received by faith) defeats another, and each attack on them is answered from among them:
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610).
    • Lutheran (the Formula of Concord) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord).
    • Wesleyan (preventing grace) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Wesleyan (preventing grace).
    • The objection from the Spirit's resistance defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance.
    • Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The third way (an ability given, received by faith), and The third way (an ability given, received by faith) defeats Thomist (Aquinas; Garrigou-Lagrange).

What this rests on. The reasons state 13 defeats and 20 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

third_way_defensible_with_dort

The third way can be defended with Dort, against Trent, by the position shown above. Trent attacks the third way over faith alone; Dort, which defeats Trent over the will and grace, answers that attack; and nothing in the third way contradicts Dort.

theorem third_way_defensible_with_dort : Framework.CredulouslyAccepted
    solaGratiaDispute.defeats Party.thirdWay
-- axioms: propext, Classical.choice, Quot.sound

thirdWayWithWesley

The third way, defended with Wesley.

The third way (an ability given, received by faith) is accepted on some resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Remonstrant (the Five Articles, 1610), Lutheran (the Formula of Concord), Wesleyan (preventing grace), The third way (an ability given, received by faith), The objection from the Spirit's resistance can be held.
  • None of Romans 11:6 (by grace, so not by works), Remonstrant (the Five Articles, 1610), Lutheran (the Formula of Concord), Wesleyan (preventing grace), The third way (an ability given, received by faith), The objection from the Spirit's resistance defeats another, and each attack on them is answered from among them:
    • Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610), and Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Remonstrant (the Five Articles, 1610), and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord), and Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort).
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Lutheran (the Formula of Concord), and Lutheran (the Formula of Concord) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Lutheran (the Formula of Concord), and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats Wesleyan (preventing grace), and Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort).
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Wesleyan (preventing grace), and Lutheran (the Formula of Concord) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Wesleyan (preventing grace), and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith), and Lutheran (the Formula of Concord) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The third way (an ability given, received by faith), and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance, and Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The objection from the Spirit's resistance, and Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange).

What this rests on. The reasons state 15 defeats and 42 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

third_way_defensible_with_wesley

It can also be defended with Wesley, the Lutherans and the Remonstrants, against both Dort and Trent, by the position shown above. The third way, as stated, takes no side between Dort and Wesley.

theorem third_way_defensible_with_wesley : Framework.CredulouslyAccepted
    solaGratiaDispute.defeats Party.thirdWay
-- axioms: propext, Classical.choice, Quot.sound

thirdWayAnsweredByTrent

Why the third way is not forced: a defensible position holds Trent, and Trent defeats it.

The third way (an ability given, received by faith) is not accepted on every resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Trent (Session VI, canon 4, on the Molinist reading), Remonstrant (the Five Articles, 1610), The objection from the Spirit's resistance can be held, and it holds Trent (Session VI, canon 4, on the Molinist reading); Trent (Session VI, canon 4, on the Molinist reading) conflicts with The third way (an ability given, received by faith): Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith), and The third way (an ability given, received by faith) defeats Trent (Session VI, canon 4, on the Molinist reading).
  • None of Romans 11:6 (by grace, so not by works), Trent (Session VI, canon 4, on the Molinist reading), Remonstrant (the Five Articles, 1610), The objection from the Spirit's resistance defeats another, and each attack on them is answered from among them:
    • Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort).
    • Lutheran (the Formula of Concord) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats Lutheran (the Formula of Concord).
    • Wesleyan (preventing grace) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats Wesleyan (preventing grace).
    • The third way (an ability given, received by faith) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610), and Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Remonstrant (the Five Articles, 1610), and Trent (Session VI, canon 4, on the Molinist reading) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance, and Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The objection from the Spirit's resistance, and Trent (Session VI, canon 4, on the Molinist reading) defeats Thomist (Aquinas; Garrigou-Lagrange).

What this rests on. The reasons state 14 defeats and 27 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

third_way_not_forced

Nor is the third way forced. A maximal defensible position holds Trent, which condemns faith alone, and cannot hold the third way with it.

theorem third_way_not_forced : ¬Framework.SkepticallyAccepted
    solaGratiaDispute.defeats Party.thirdWay
-- axioms: propext, Classical.choice, Quot.sound

dort_stands_with_the_thomists

Dort and the Thomists stand together: one reading satisfies every premise and every conclusion of both, so neither defeats the other. The Thomist position weighed here takes no side on the will's passivity. It holds that the will is "not merely passive" and draws nothing from it, so this result does not show that the Thomists hold the third part of sola gratia. Read in the Molinists' sense, the phrase cannot be held with Dort (whereTheAgentReadingFalls); read in Garrigou-Lagrange's, it can (dort_holds_with_garrigou_lagrange). They differ on faith alone and on perseverance, which this dispute does not weigh between them.

theorem dort_stands_with_the_thomists : solaGratiaDispute.StandTogether
    [Party.reformed, Party.thomist]
-- axioms: propext, Classical.choice, Quot.sound

thomistsWithDort

The Thomists, defended with Dort.

Thomist (Aquinas; Garrigou-Lagrange) is accepted on some resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), Thomist (Aquinas; Garrigou-Lagrange) can be held.
  • None of Romans 11:6 (by grace, so not by works), Reformed (the Canons of Dort), Thomist (Aquinas; Garrigou-Lagrange) defeats another, and each attack on them is answered from among them:
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Remonstrant (the Five Articles, 1610) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610).
    • Lutheran (the Formula of Concord) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord).
    • Wesleyan (preventing grace) defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats Wesleyan (preventing grace).
    • The objection from the Spirit's resistance defeats Reformed (the Canons of Dort), and Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance.
    • Trent (Session VI, canon 4, on the Molinist reading) defeats Thomist (Aquinas; Garrigou-Lagrange), and Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading).
    • Remonstrant (the Five Articles, 1610) defeats Thomist (Aquinas; Garrigou-Lagrange), and Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610).
    • Lutheran (the Formula of Concord) defeats Thomist (Aquinas; Garrigou-Lagrange), and Reformed (the Canons of Dort) defeats Lutheran (the Formula of Concord).
    • Wesleyan (preventing grace) defeats Thomist (Aquinas; Garrigou-Lagrange), and Reformed (the Canons of Dort) defeats Wesleyan (preventing grace).
    • The third way (an ability given, received by faith) defeats Thomist (Aquinas; Garrigou-Lagrange), and Thomist (Aquinas; Garrigou-Lagrange) defeats The third way (an ability given, received by faith).
    • The objection from the Spirit's resistance defeats Thomist (Aquinas; Garrigou-Lagrange), and Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance.

What this rests on. The reasons state 17 defeats and 16 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

thomist_defensible

The Thomists can be defended, with Dort: some maximal defensible position holds both, with what every party holds. Between them they answer every attack on either.

theorem thomist_defensible : Framework.CredulouslyAccepted
    solaGratiaDispute.defeats Party.thomist
-- axioms: propext, Classical.choice, Quot.sound

thomistsAnsweredByTrent

Why the Thomists are not forced: a maximal defensible position holds Trent on the Molinist reading, and Trent defeats them.

Thomist (Aquinas; Garrigou-Lagrange) is not accepted on every resolution.

  • A position holding Romans 11:6 (by grace, so not by works), Trent (Session VI, canon 4, on the Molinist reading), Remonstrant (the Five Articles, 1610), The objection from the Spirit's resistance can be held, and it holds Trent (Session VI, canon 4, on the Molinist reading); Trent (Session VI, canon 4, on the Molinist reading) conflicts with Thomist (Aquinas; Garrigou-Lagrange): Trent (Session VI, canon 4, on the Molinist reading) defeats Thomist (Aquinas; Garrigou-Lagrange), and Thomist (Aquinas; Garrigou-Lagrange) defeats Trent (Session VI, canon 4, on the Molinist reading).
  • None of Romans 11:6 (by grace, so not by works), Trent (Session VI, canon 4, on the Molinist reading), Remonstrant (the Five Articles, 1610), The objection from the Spirit's resistance defeats another, and each attack on them is answered from among them:
    • Reformed (the Canons of Dort) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort).
    • Lutheran (the Formula of Concord) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats Lutheran (the Formula of Concord).
    • Wesleyan (preventing grace) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats Wesleyan (preventing grace).
    • The third way (an ability given, received by faith) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats The third way (an ability given, received by faith).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Trent (Session VI, canon 4, on the Molinist reading), and Trent (Session VI, canon 4, on the Molinist reading) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats Remonstrant (the Five Articles, 1610), and Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats Remonstrant (the Five Articles, 1610), and Trent (Session VI, canon 4, on the Molinist reading) defeats Thomist (Aquinas; Garrigou-Lagrange).
    • Reformed (the Canons of Dort) defeats The objection from the Spirit's resistance, and Trent (Session VI, canon 4, on the Molinist reading) defeats Reformed (the Canons of Dort).
    • Thomist (Aquinas; Garrigou-Lagrange) defeats The objection from the Spirit's resistance, and Trent (Session VI, canon 4, on the Molinist reading) defeats Thomist (Aquinas; Garrigou-Lagrange).

What this rests on. The reasons state 14 defeats and 27 absences of defeat, each a cell of the defeat table, solaGratiaDispute_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:

thomist_not_forced

Nor are the Thomists forced. A maximal defensible position holds Trent on the Molinist reading, with the Remonstrants and the objection, and cannot hold the Thomists with them: the dispute between the two Catholic schools, which Rome left open in 1607, is a standoff here too.

theorem thomist_not_forced : ¬Framework.SkepticallyAccepted
    solaGratiaDispute.defeats Party.thomist
-- axioms: propext, Classical.choice, Quot.sound