The conclusion

solaGratia

Sola gratia, stated sharply enough that the rivals divide from it. Salvation is by grace and not earned; the grace that saves brings about the consent it seeks; and in being made alive the will contributes nothing. The three parts are separate claims so that a rival can be shown holding the first and denying one or both of the others: Trent's premises deny both, the Remonstrants' the second.

The steps

graceStep

Romans 11:6: if salvation is by grace it is not by works, so it is by grace and not earned.

ephesiansStep

Ephesians 2:8–9, with "this" read as pointing to the whole of being saved by grace through faith: so faith, part of that whole, is God's gift. Rated disputed: Robertson reads the pronoun the same way and calls the whole "conditioned on faith on our part", and Calvin, on the next verse, writes "not that faith is the gift of God, but that salvation is given to us by God".

giftStep

The step Arminius refuses. If faith is God's gift, and it is given to those who were dead until God made them alive (Ephesians 2:1–5), then conversion is God's work alone. Rated disputed: Arminius grants both grounds and denies that the gift cannot be refused. Dort's answer is its article on faith: God's gift "not on account of its being offered by God to man, to be accepted or rejected at his pleasure, but because it is in reality conferred" (III/IV, article 14).

romansStep

Romans 9:16, read as being about salvation: if God's saving mercy "depends not on human will or exertion", conversion is God's work alone. Rated disputed: Arminius grants that the verse is about salvation and reads its willing and running as seeking salvation by the works of the law, so that the mercy goes to believers and can be refused.

passiveStep

From God's work alone to the third part of the conclusion: the will is passive in being made alive. Rated wellSupported: the Lutherans, who part from Dort on the next step, grant this one. It is taken as what Dort means by the phrase: the new life is "a making alive, which God works in us without our aid" (III/IV, article 12). "Passive" here means that the will is not the agent of its new life. Garrigou-Lagrange grants God's work alone and holds the will "does not remain passive" under operating grace, but in another sense: its consent follows grace "in the genus or order of formal, efficient, and final cause". The dilemma over the Thomists' claim sets the two senses apart (whatNotMerelyPassiveMeans).

operatingGraceStep

Aquinas on operating grace. In converting grace God is the sole mover of the will, so God alone is the one who regenerates.

efficacyStep

Aquinas on God's intention. If God moves the will intending that it attain grace, the grace brings about what it is given for. Rated disputed: the Molinists grant the intention and the infallible result, and ascribe it to the consent God foreknows, not to the grace.

effectualStep

From God's work alone to the second part of the conclusion: the grace that saves cannot be finally refused. Rated disputed: the Formula of Concord holds conversion to be the Spirit's work alone, with the will "purely passive", and holds grace resistible all the same.

textsOfResistanceStep

What the texts of resistance say together: the Spirit's work is resisted. Acts 7:51 says so of Stephen's hearers, and Paul's commands not to grieve the Spirit (Ephesians 4:30) or quench him (1 Thessalonians 5:19) presuppose it of believers.

resistanceStep

From resistance to final refusal. If the Spirit is resisted, and what is resisted is the grace that saves, that grace can be finally refused. The Remonstrants' fourth article, made explicit.

griefStep

From grieving the Spirit to final refusal. If the Spirit is resisted, and those who obstinately resist him can grieve and lose him, the grace that saves can be finally refused. The Formula of Concord's reading of Ephesians 4:30.

blasphemyStep

From the unforgivable sin to final refusal. If the blasphemy against the Spirit is never forgiven (Matthew 12:31–32), and it is the final refusal of the grace offered, then that grace can be finally refused.

cooperationStep

Trent's fourth canon, first half. The will, moved by God, cooperates by assenting, as "Return to me" calls on it to; so it is not passive. Rated disputed: Aquinas grants that grace cooperates with a will that moves and holds that in grace's first effect the mind "is moved and does not move".

dissentStep

Trent's fourth canon, second half. The will, moved by God, can refuse if it wishes; so grace is not effectual of itself. Rated disputed: Aquinas grants that a will God moves could, taken simply, fail to be moved, and still holds that the man God moves to grace attains it infallibly.

The lines

graceLine — Romans 11:6 (by grace, so not by works)

Romans 11:6, the line every party walks. It delivers the first part of the conclusion and nothing more.

ephesiansLine — Ephesians 2:8–9 ("this is not your own doing")

Ephesians 2:8–9, read with "this" pointing to the whole of being saved by grace through faith. It delivers that faith is God's gift, which is not yet the conclusion.

giftLine — From faith given to the dead, to God's work alone (Ephesians 2:1–5)

From faith given to the dead, to God's work alone. Its ground is Ephesians 2:1–5; that faith is God's gift comes from the Ephesians line above.

romansLine — Romans 9:16 ("not on human will or exertion")

Romans 9:16, read as being about salvation. It reaches God's work alone without the Ephesians grammar.

cooperationLine — Trent, canon 4: the will cooperates by assenting

Trent on cooperation: Zechariah 1:3 with Lamentations 5:21, and the first half of canon 4.

dissentLine — Trent, canon 4: the will can refuse if it wishes

Trent on dissent: the second half of canon 4.

textsOfResistanceLine — The texts of resistance (Acts 7:51; Ephesians 4:30; 1 Thessalonians 5:19)

The texts of resistance: Acts 7:51, Ephesians 4:30 and 1 Thessalonians 5:19, delivering that the Spirit's work is resisted. Every party walks this line.

resistanceLine — Remonstrance, article 4: grace is not irresistible (Acts 7:51)

The Remonstrants on resistance: what Stephen's hearers resisted was the grace that saves, so that grace can be finally refused.

griefLine — Grieving the Spirit (Ephesians 4:30), as able to lose him

Grieving the Spirit, read as able to end in losing him.

blasphemyLine — The sin against the Spirit (Matthew 12:31–32), as final refusal

The unforgivable sin, read as the final refusal of grace.

operatingGraceLine — Operating grace: the mind is moved and does not move (Aquinas)

Operating grace (Aquinas, I-II q.111 a.2): God alone is the one who regenerates.

efficacyLine — God's intention in moving: grace attained infallibly (Aquinas)

God's intention in moving (Aquinas, I-II q.112 a.3): the grace that saves brings about the consent it seeks.

Shared grounds

reformedShared

What the Reformed packages rest on beyond any one line: the Reformed answer to Acts 7:51, from Dort's account of those who refuse the call. What Stephen's hearers resisted was the outward call of the preached word, not the grace that saves. The texts of resistance themselves are a line the Reformed walk too.

closingSteps

The steps that close every Reformed package: God's work alone, unpacked into the conclusion's last two parts, one step each.

closingInferences

The ratings of the closing steps, which belong to no line.

def closingInferences : List Source :=
  [passiveInference, effectualInference]

The rivals

tridentine — Trent (Session VI, canon 4, on the Molinist reading)

Trent, from the sixth session (1547). Romans 11:6, which its eighth chapter quotes; Zechariah 1:3 read with Lamentations 5:21, as its fifth chapter reads them; and canon 4, on the will that cooperates by assenting and can refuse if it wishes.

Grounded in scripture alone: Romans 11:6 — if it is by grace, it is no longer on the basis of works.

remonstrant — Remonstrant (the Five Articles, 1610)

The Remonstrants, from their articles of 1610 and from Arminius. Romans 11:6; the texts of resistance, which every party grants; the fourth article, that grace is not irresistible, read from Acts 7:51; and what Arminius grants of the Reformed case: the texts of Ephesians 2, that faith is God's gift, and that Romans 9:16 is about salvation. What is left out is the two steps from those to God's work alone, which are the steps he refuses.

Grounded in scripture alone: Romans 11:6 — if it is by grace, it is no longer on the basis of works, Acts 7:51 — you always resist the Holy Spirit, Ephesians 4:30 — do not grieve the Holy Spirit of God, by whom you were sealed, 1 Thessalonians 5:19 — do not quench the Spirit, Ephesians 2:1–5 — dead in trespasses, God made us alive together with Christ, Ephesians 2:8–9 — by grace you have been saved through faith, and this is not your own doing; it is the gift of God, Romans 9:16 — it depends not on human will or exertion, but on God, who has mercy.

lutheran — Lutheran (the Formula of Concord)

The Lutherans, from the Formula of Concord (1577) and the Augsburg Confession (1530). Conversion is the Holy Spirit's work alone, and in it the will is "purely passive"; yet those who obstinately resist the Spirit "grieve and lose" him, so the grace that saves can be finally refused, and where it is, the fault is the person's own. Grace is received by faith alone.

Grounded in scripture alone: Romans 11:6 — if it is by grace, it is no longer on the basis of works, Acts 7:51 — you always resist the Holy Spirit, Ephesians 4:30 — do not grieve the Holy Spirit of God, by whom you were sealed, 1 Thessalonians 5:19 — do not quench the Spirit.

wesleyan — Wesleyan (preventing grace)

Wesley. God restores to every person a measure of free will, by the grace that goes before ("preventing grace"), so that each is able to believe; that grace can be resisted or yielded to; and it is received by faith alone.

Grounded in scripture alone: Romans 11:6 — if it is by grace, it is no longer on the basis of works, Acts 7:51 — you always resist the Holy Spirit, Ephesians 4:30 — do not grieve the Holy Spirit of God, by whom you were sealed, 1 Thessalonians 5:19 — do not quench the Spirit.

thirdWay — The third way (an ability given, received by faith)

The third way, as it was put to this argument. As Adam was made able to stand or to fall (Genesis 2:16–17), so God gives the one who hears the gospel the ability to believe, and grace is received by faith alone. That the offer is real is part of the third way too, and is not encoded as a premise, because no party here denies it. Stated this way it does not say what kind of help the ability is, whether one that makes believing possible or one that brings it about, and it carries nothing that would decide whether the grace that saves can be finally refused.

Grounded in scripture alone: Romans 11:6 — if it is by grace, it is no longer on the basis of works, Genesis 2:16–17 — of the tree of the knowledge of good and evil you shall not eat.

objection — The objection from the Spirit's resistance

The objection from the Spirit's resistance, strengthened. Three routes to the claim that the grace that saves can be finally refused. Two run from the texts of resistance: with the Remonstrants' reading of what Stephen's hearers resisted, and with the Formula of Concord's reading of grieving the Spirit, that it can end in losing him. The third runs from the sin that is never forgiven, read with Augustine as impenitence to the end. It concludes that the grace that saves can be finally refused. That this denies the second part of sola gratia is not a premise of the objection: it is what the two claims mean, and the meanings join them (TestimonyArguments.Meanings.SolaGratia).

Grounded in scripture alone: Acts 7:51 — you always resist the Holy Spirit, Ephesians 4:30 — do not grieve the Holy Spirit of God, by whom you were sealed, 1 Thessalonians 5:19 — do not quench the Spirit, Matthew 12:31–32 — the blasphemy against the Spirit will not be forgiven.

The position argued for

reformed — Reformed (the Canons of Dort)

The Reformed position, as the Synod of Dort (1619) and the Westminster Confession (1647) state it. Two routes to God's work alone, one through Ephesians 2 and one through Romans 9:16, with Romans 11:6 for the first part of the conclusion, and the Reformed answer to Acts 7:51.

Grounded in scripture alone: Romans 11:6 — if it is by grace, it is no longer on the basis of works, Ephesians 2:8–9 — by grace you have been saved through faith, and this is not your own doing; it is the gift of God, Ephesians 2:1–5 — dead in trespasses, God made us alive together with Christ, Romans 9:16 — it depends not on human will or exertion, but on God, who has mercy, Acts 7:51 — you always resist the Holy Spirit, Ephesians 4:30 — do not grieve the Holy Spirit of God, by whom you were sealed, 1 Thessalonians 5:19 — do not quench the Spirit.

Each strand alone

ephesiansStrand — Reformed, the Ephesians strand alone

The Ephesians strand alone: Romans 11:6, Ephesians 2 with its reading of "this", and the step from the gift to God's work alone.

Grounded in scripture alone: Romans 11:6 — if it is by grace, it is no longer on the basis of works, Ephesians 2:8–9 — by grace you have been saved through faith, and this is not your own doing; it is the gift of God, Ephesians 2:1–5 — dead in trespasses, God made us alive together with Christ.

romansStrand — Reformed, the Romans strand alone

The Romans strand alone: Romans 11:6, and Romans 9:16 read as being about salvation.

Grounded in scripture alone: Romans 11:6 — if it is by grace, it is no longer on the basis of works, Romans 9:16 — it depends not on human will or exertion, but on God, who has mercy.

ephesiansWithoutTheGiftStep — Reformed, the Ephesians strand without the step from the gift

The Ephesians strand without the step Arminius refuses: every text and reading it rests on, and the step to faith as God's gift, with only the step from the gift to God's work alone left out. The Reformed answer to Acts 7:51 is not part of the strand, and is left out with the rest of what the strand does not read.

Grounded in scripture alone: Romans 11:6 — if it is by grace, it is no longer on the basis of works, Ephesians 2:8–9 — by grace you have been saved through faith, and this is not your own doing; it is the gift of God, Ephesians 2:1–5 — dead in trespasses, God made us alive together with Christ.

The readings, removed

reformedWithoutTouto — Reformed, minus its reading of "this" in Ephesians 2:8

The Reformed position without its reading of "this" in Ephesians 2:8. The Romans strand is untouched.

Grounded in scripture alone: Romans 11:6 — if it is by grace, it is no longer on the basis of works, Ephesians 2:8–9 — by grace you have been saved through faith, and this is not your own doing; it is the gift of God, Ephesians 2:1–5 — dead in trespasses, God made us alive together with Christ, Romans 9:16 — it depends not on human will or exertion, but on God, who has mercy, Acts 7:51 — you always resist the Holy Spirit, Ephesians 4:30 — do not grieve the Holy Spirit of God, by whom you were sealed, 1 Thessalonians 5:19 — do not quench the Spirit.

reformedWithoutRomansReading — Reformed, minus Romans 9:16 as being about salvation

The Reformed position without the reading of Romans 9:16 as being about salvation. The Ephesians strand is untouched.

Grounded in scripture alone: Romans 11:6 — if it is by grace, it is no longer on the basis of works, Ephesians 2:8–9 — by grace you have been saved through faith, and this is not your own doing; it is the gift of God, Ephesians 2:1–5 — dead in trespasses, God made us alive together with Christ, Romans 9:16 — it depends not on human will or exertion, but on God, who has mercy, Acts 7:51 — you always resist the Holy Spirit, Ephesians 4:30 — do not grieve the Holy Spirit of God, by whom you were sealed, 1 Thessalonians 5:19 — do not quench the Spirit.

reformedWithoutEitherReading — Reformed, minus both readings

The Reformed position without either reading. Every text is kept, and every step.

Grounded in scripture alone: Romans 11:6 — if it is by grace, it is no longer on the basis of works, Ephesians 2:8–9 — by grace you have been saved through faith, and this is not your own doing; it is the gift of God, Ephesians 2:1–5 — dead in trespasses, God made us alive together with Christ, Romans 9:16 — it depends not on human will or exertion, but on God, who has mercy, Acts 7:51 — you always resist the Holy Spirit, Ephesians 4:30 — do not grieve the Holy Spirit of God, by whom you were sealed, 1 Thessalonians 5:19 — do not quench the Spirit.

The positions

reformed_establishes

Grant the Reformed premises, and sola gratia follows. The premises are Romans 11:6; Ephesians 2, with "this" pointing to the whole of being saved by grace through faith; Romans 9:16, read as being about salvation; the steps from each of those to God's work alone; and the Reformed answer to Acts 7:51. The result does not say that the readings or the steps are right, only that the conclusion follows from them. Four of the steps are rated disputed, each on a reader who grants its grounds and denies its conclusion: the step from "this" to faith as a gift (Robertson), the steps from each strand to God's work alone (Arminius), and the step from God's work alone to grace that cannot be finally refused (the Formula of Concord).

theorem reformed_establishes : Establishes reformed
-- axioms: propext, Quot.sound

trentsReading

Trent's reading, written down: salvation is by grace, the will cooperates and can refuse, so grace is not effectual of itself and the will is not passive in being made alive, and grace is not received by faith alone (canon 9). Claims Trent's documents do not address, such as the readings of Ephesians 2 and Romans 9, are set true; nothing turns on them. On these sixteen claims Trent's reading and Arminius's coincide; the two positions differ in which premises they hold and whom they cite.

def trentsReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.faithAloneReceivesGrace => False
    | Claim.conversionIsGodsWorkAlone => False
    | Claim.graceIsEffectualOfItself => False
    | Claim.willIsPassiveInRegeneration => False
    | x => True

tridentine_not_establishes

Trent's premises do not lead to sola gratia. A countermodel shows it: a way of holding every one of Trent's premises while denying the conclusion. On Trent's account the will, moved by God, cooperates by assenting and can refuse its consent; so the second and third parts of the conclusion fail. Whether canon 4 really denies the second part is itself disputed, because Aquinas holds both that the will can refuse, taken simply, and that the man God moves to grace attains it infallibly; that dispute is in the rating of the canon's step, not in this result.

theorem tridentine_not_establishes : ¬Establishes tridentine
-- axioms: propext, Quot.sound

arminiusReading

Arminius's reading, written down: salvation is by grace, faith is God's gift, Romans 9:16 is about salvation, and the grace that saves can be refused. It also sets the will's passivity false. The Remonstrants denied that too, but their denial of it is not encoded, and nothing in their package turns on it. The reading of "this" in Ephesians 2:8 is set true, as Hoehner and Robertson hold it; no reading of the pronoun is cited to Arminius.

def arminiusReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.conversionIsGodsWorkAlone => False
    | Claim.graceIsEffectualOfItself => False
    | Claim.willIsPassiveInRegeneration => False
    | x => True

remonstrant_not_establishes

The Remonstrants' premises do not lead to sola gratia either, though they grant much of what the Reformed case rests on: that faith is God's gift, given to those dead in sin, and that Romans 9:16 is about salvation. What they add is their fourth article, that grace is not irresistible, read from Acts 7:51; what they leave out is the two steps from those grants to God's work alone.

theorem remonstrant_not_establishes : ¬Establishes remonstrant
-- axioms: propext, Quot.sound

rivals_hold_salvation_by_grace

Both rivals reach the first part, that salvation is by grace. Trent's premises deliver it, and so do the Remonstrants', by the same line from Romans 11:6. A conclusion stated only as "salvation is by grace" would be established by all three positions and would divide none of them, which is why the conclusion here has two further parts.

theorem rivals_hold_salvation_by_grace : Entails tridentine.premises (p
    Claim.salvationIsByGrace) ∧ Entails remonstrant.premises (p
    Claim.salvationIsByGrace)
-- axioms: propext, Quot.sound

trent_denies_passivity

Trent's premises deny the third part, that the will is passive. Canon 4 condemns anyone who says the will "is merely passive", and the premises deliver the denial outright. The step is rated disputed, because the canon speaks of the will preparing itself for justification and the Reformed claim is about the moment of being made alive.

theorem trent_denies_passivity : Entails tridentine.premises (notP
    Claim.willIsPassiveInRegeneration)
-- axioms: propext, Quot.sound

trent_denies_effectual_grace

Trent's premises deny the second part too, that grace is effectual of itself. Canon 4 condemns anyone who says the will "cannot refuse its consent, if it would", and the premises deliver the denial. The step is rated disputed: Aquinas grants that the will moved by God could, taken simply, refuse, and holds that the man God moves to grace "will infallibly attain to it". So a Catholic reader in his school grants the canon and not this conclusion.

theorem trent_denies_effectual_grace : Entails tridentine.premises (notP
    Claim.graceIsEffectualOfItself)
-- axioms: propext, Quot.sound

remonstrants_deny_effectual_grace

The Remonstrants deny the second part: grace can be resisted. Their fourth article reads Acts 7:51 so, and their premises deliver that the grace that saves can be finally refused. That this is the denial of grace effectual of itself is not a premise of theirs but what the two claims mean: the meanings join them, and the theorem is stated over the premises together with that join.

theorem remonstrants_deny_effectual_grace : Entails remonstrant.held (notP
    Claim.graceIsEffectualOfItself)
-- axioms: propext, Quot.sound

Which reading the Reformed case depends on

touto_not_load_bearing

The case does not depend on the reading of "this". Remove the reading on which "this" in Ephesians 2:8 points to the whole of being saved by grace through faith, keep everything else, and sola gratia still follows by Romans 9:16, which does not use the Ephesians grammar. The reading itself is well supported: Hoehner and Robertson both hold it.

theorem touto_not_load_bearing : Establishes reformedWithoutTouto
-- axioms: propext, Quot.sound

romans_reading_not_load_bearing

Nor does it depend on the reading of Romans 9:16. Remove the reading on which the verse is about salvation, keep everything else, and sola gratia still follows by Ephesians 2.

theorem romans_reading_not_load_bearing : Establishes
    reformedWithoutRomansReading
-- axioms: propext, Quot.sound

neitherReadingGranted

The reading on which neither of the two readings holds: "this" in Ephesians 2:8 does not point to the whole, and Romans 9:16 is about God's choice of a people for a part in history alone. No reader is cited who holds both denials; the countermodel shows what follows if both readings go, not that anyone has given them up. Everything else the Reformed position grants is kept, the Reformed answer to Acts 7:51 included.

def neitherReadingGranted : Valuation Claim :=
  fun a =>
    match a with
    | Claim.toutoRefersToTheWhole => False
    | Claim.romans9_16ConcernsSalvation => False
    | Claim.faithIsGodsGift => False
    | Claim.conversionIsGodsWorkAlone => False
    | Claim.graceIsEffectualOfItself => False
    | Claim.willIsPassiveInRegeneration => False
    | Claim.acts7_51ResistsSavingGrace => False
    | x => True

readings_jointly_load_bearing

The two readings together carry it. Remove both, keep every text and every step, and sola gratia no longer follows, because nothing is left that reaches God's work alone. So the Reformed case needs at least one of the two readings, and either will do. A reading whose removal stops the conclusion following is called load-bearing; here only the pair is.

theorem readings_jointly_load_bearing : ¬Establishes
    reformedWithoutEitherReading
-- axioms: propext, Quot.sound

ephesians_strand_establishes

The Ephesians strand, argued alone, reaches sola gratia. It rests on two steps, both rated disputed: from "this" to faith as God's gift, and from the gift to God's work alone.

theorem ephesians_strand_establishes : Establishes ephesiansStrand
-- axioms: propext, Quot.sound

romans_strand_establishes

So does the Romans strand, on one step rated disputed.

theorem romans_strand_establishes : Establishes romansStrand
-- axioms: propext, Quot.sound

Where Arminius parts from the Ephesians strand

gift_of_faith_does_not_settle_resistibility

That faith is God's gift does not settle whether grace can be refused. Grant everything the Ephesians strand rests on short of its last step: the texts, "this" pointing to the whole, and so faith as God's gift, given to those who were dead in sin. Leave out only the step from that gift to God's work alone, and sola gratia does not follow.

Arminius grants the texts and that faith is God's gift; the reading of "this" is Hoehner's and Robertson's, not cited to him. On a reading that grants all of these, his, the conclusion fails. So where he parts from the strand is the step from the gift to God's work alone. The encoding writes "faith is God's gift" as one claim, and Dort and Arminius mean different things by it: for Dort a gift "in reality conferred", for Arminius one that can be refused. The difference shows here as Arminius refusing the step.

theorem gift_of_faith_does_not_settle_resistibility : ¬Establishes
    ephesiansWithoutTheGiftStep
-- axioms: propext, Quot.sound

dortReading

Dort's reading: every claim of the Reformed position holds. What Stephen's hearers resisted was the preached word, not the grace that saves; grieving the Spirit does not end in losing him; the unforgivable sin is not the final refusal of saving grace; and that grace cannot be finally refused.

def dortReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.acts7_51ResistsSavingGrace => False
    | Claim.savingGraceCanBeFinallyRefused => False
    | Claim.grievingCanLoseTheSpirit => False
    | Claim.blasphemyIsFinalRefusalOfGrace => False
    | x => True

reformed_is_satisfiable

The Reformed package has a model.

theorem reformed_is_satisfiable : Satisfiable reformed.premises
-- axioms: propext, Quot.sound

reformedWithoutTouto_is_satisfiable

The Reformed package without its reading of "this" has a model.

theorem reformedWithoutTouto_is_satisfiable : Satisfiable
    reformedWithoutTouto.premises
-- axioms: propext, Quot.sound

reformedWithoutRomansReading_is_satisfiable

The Reformed package without its reading of Romans 9:16 has a model.

theorem reformedWithoutRomansReading_is_satisfiable : Satisfiable
    reformedWithoutRomansReading.premises
-- axioms: propext, Quot.sound

ephesiansStrand_is_satisfiable

The Ephesians strand alone has a model.

theorem ephesiansStrand_is_satisfiable : Satisfiable ephesiansStrand.premises
-- axioms: propext, Quot.sound

romansStrand_is_satisfiable

The Romans strand alone has a model.

theorem romansStrand_is_satisfiable : Satisfiable romansStrand.premises
-- axioms: propext, Quot.sound