Sola fide

This page is generated from arguments/TestimonyArguments/SolaFide. Every heading and paragraph below is a docstring in those files; every formula is rendered from the encoding they check. If the page and the source disagree, the page is the one that is wrong, and regenerating it is the fix.

Atoms are numbered propositional variables, numbered once for the whole page, so the same variable means the same claim in every position below. Reading the logic is the short version of what the notation means. A result marked ⚗ is one this library constructs rather than reports.

TestimonyArguments.SolaFide — justification by grace through faith, not works

The Reformation's material principle, encoded so that its premises are visible and its disputed step is identified mechanically.

The argument runs on three independent strands, and that is the point.

The Pauline strand reads Galatians 2:16 as the centre of a polemic. The Teachers in Galatia required believers to be circumcised as well as to believe, and Paul answers that a person is justified "not by works of the law but through faith in Jesus Christ". It rests on two disputed readings of that verse.

The first is worksOfLawMeansWorksGenerally: whether ἔργα νόμου denotes human works in general, or specifically the covenant boundary markers — circumcision, food laws, sabbath — that marked Jews off from gentiles, as Dunn and Wright argue, building on Sanders' account of Second Temple Judaism. Only on the first reading does refusing circumcision mean refusing every work as a requirement.

The second is pistisChristouObjective: whether πίστις Χριστοῦ is faith in Christ, as Dunn holds, or Christ's own faithfulness, as Hays holds. Only on the first does the verse name the believer's faith as the means of justification. Excluding works is not yet faith alone.

The genitive dispute is a premise inside the Pauline strand, not a third strand. Every πίστις Χριστοῦ text sets it against νόμος, so no route through the genitive avoids the question of what ἔργα νόμου denotes. Nor does it follow the Old/New Perspective line: the New Perspective package keeps the objective genitive, because Dunn does.

The dominical strand rests on Jesus' own words rather than Paul's. ἡ πίστις σου σέσωκέν σε — "your faith has saved you" — occurs four times in Luke (7:50, 8:48, 17:19, 18:42). It is not a free win: σῴζω means both save and heal, and in 8:48, 17:19 and 18:42 the context is physical healing, which is why most translations render "made you well" there. The argument therefore rests on Luke 7:50, where the saying follows "your sins are forgiven" rather than a healing, and carries sozoIsSoteriological as its own premise. It is a second bet, on a different word — rated wellSupported, because no scholar found argues the healing sense at 7:50. It also carries its answer to "she loved much" (7:47): luke7_47LoveIsEvidence, that her love is the evidence of her forgiveness and not its ground, as 7:47b and the parable of the two debtors (7:41–43) read it. The reading of 7:47 is cited to Osvaldo Padilla's narrative-critical study of the episode: her actions "stem from the fact that she loves much because she has been forgiven much". Both premises are also Melanchthon's, in the Apology of the Augsburg Confession, which answers "she loved much" with Jesus' own words: "Christ interprets Himself when He adds: Thy faith hath saved thee". Neither argues σῴζω against the healing sense word by word; Marshall's commentary at 7:50 is named as the philological study to check.

The apostolic strand rests on Peter as Luke reports him. At the Jerusalem council (Acts 15) the demand Galatians answers is made again — "unless you are circumcised according to the custom of Moses, you cannot be saved" (15:1) — and Peter answers that God cleansed the gentiles' hearts by faith, that Jew and gentile alike are saved through grace, and that the law is "a yoke… that neither our fathers nor we have been able to bear" (15:9–11). James concurs (15:19). It carries acts15YokeIsLawAsCondition as its disputed premise: that the yoke is the whole law as a condition of salvation, and not Israel's law laid on gentiles as a mark of belonging, as Jervell reads Luke. The two premises are about different texts, and logically independent; they are not dialectically independent, since a reader who takes ἔργα νόμου as boundary markers will read the yoke the same way.

Each strand delivers only what its texts say. Paul argues for alone: the Galatians already believed, adding circumcision to their faith is what severs them from Christ, and 2:16 names faith as the one means (ἐὰν μή, "except through faith"). Luke 7:50 and Acts 15 say less: that her faith saved her, and that the gentiles are saved without the yoke — that faith suffices (faithIsSufficient), not that nothing else could be a condition. "Through faith", the part of the conclusion the strands are needed for, needs only that. The difference is not pedantry. A case is attacked on what it claims, and a Luke credited with alone would be attacked by the apocalyptic reading on a claim Luke never made.

A Johannine strand is encoded alongside, but not yet inside, the Reformed case (Johannine.lean). Asked what they must do "to be doing the works of God", the crowd is told: "This is the work of God, that you believe in him whom he has sent" (John 6:28–29). Calvin reads that believing as trust, which "brings nothing to God"; Aquinas as faith living through charity, the principle of good works. John alone delivers sola fide on Calvin's reading (johannine_strand_establishes) and not on Aquinas's (johannine_strand_rests_on_believing_as_trust). Luther answers Aquinas from Galatians 3:11–12: the law commands love, and the law is not of faith, so a faith formed by charity would justify by the law (luther_answers_aquinas_from_galatians) — an answer that rests on his step, which Aquinas denies (luther_answer_rests_on_his_step). The strand is not yet one of the strands of reformed, so what follows about three strands is still exact.

Encoding three strands yields a result no single strand could: no disputed premise is load-bearing on its own, because any strand carries the conclusion without the others. What is load-bearing is a disjunction — both Pauline readings, or the dominical one, or the apostolic one. Defeating Paul's reading and Luke's together, which defeated the two-strand version, no longer does. A reader who wins the ἔργα νόμου argument outright does not thereby defeat sola fide, and the New Perspective, which accepts justification by faith while rejecting the traditional reading of Paul's phrase, turns out to establish the conclusion too. Nor does winning the genitive for Hays: that costs the Reformed case its Pauline route, and not its conclusion.

The conclusion has three parts — salvation is by grace, not by works, and through faith — and they are separate atoms, because the rivals divide over different parts. The Tridentine position denies the second: works done in grace merit an increase of justification. The apocalyptic reading of Martyn and Campbell does not reach the third: taking the genitive as subjective and δικαιοσύνη θεοῦ as God's act of deliverance, it denies that faith is the condition of justification, and so has no ground for "through faith" of its own, while establishing grace and "not by works" by its own route (apocalyptic_establishes_grace_not_works). The split also shows which part the strands are needed for. Grace and "not by works" follow from the texts that say so in terms, given an answer to James, with every lexical premise removed (grace_and_works_rest_on_no_lexical_premise). The lexical disputes decide through faith. And each part has its own closing step, which shows what the answer to James is for: grace follows without it (grace_needs_no_answer_to_james), "not by works" does not (james_harmonisation_is_load_bearing).

The New Perspective's reading of ἔργα νόμου has a reason, and its critics answer the reason. Sanders' covenantal nomism — in by grace, staying in by works — is the ground, and Dunn's inference from it to the boundary-marker reading is the step, cited as his (sandersLine). Gathercole and the Variegated Nomism volume deny the ground: Second Temple Judaism also held final vindication according to works, so the demand Galatians refuses is a demand for obedience, and the Reformed reading follows (criticsLine). On the critics' history Paul alone carries sola fide (critics_carry_the_pauline_strand); on Sanders' he does not (sanders_costs_the_pauline_strand). The ἔργα νόμου dispute is a dispute about Second Temple Judaism before it is one about Paul's Greek.

What justification is is a separate question, and the encoding keeps it separate. The Reformed account is forensic: pardon and imputation, not infusion (Westminster XI.1). Trent denies it — justification is "not remission of sins merely, but also the sanctification and renewal of the inward man" — and so does Mannermaa's Finnish reading of Luther, for which Christ himself is present in faith. The Finnish package denies the forensic account and establishes sola fide (forensic_justification_not_load_bearing); Trent denies it and does not. So denying the forensic account is not enough to deny sola fide. What Trent's objection needs is its fuller definition: justification includes the renewal of the inward man, and that renewal grows through good works, so works increase justification. Both sides grant the growth; the Reformed call it sanctification, distinct from justification and following it (Westminster XIII.1; Calvin, Institutes III.xi.6). Put the distinction in place of Trent's definition and Trent's case no longer denies "not by works" (trent_objection_rests_on_its_definition). The dispute over merit is a dispute over what justification is — but over sanctification, not over infusion as such.

Authorship. Ephesians, Titus and 1 and 2 Peter are each disputed, and each dispute is catalogued from both sides — Hoehner and Lincoln on Ephesians, Mounce, Dibelius–Conzelmann and Marshall on the Pastorals, Jobes and Achtemeier on 1 Peter, Schreiner and Bauckham on 2 Peter, and Ehrman across all four. Granting every critical conclusion costs the argument nothing, because it reads these letters as canonical scripture rather than as an apostle's testimony. It does cost them their use as evidence of what Paul meant by "works", which is why that premise is argued from Romans 4, 9 and 11, where the law is not in view and the authorship is not in doubt.

James 2:24 — "a person is justified by works and not by faith alone", the only occurrence of faith alone in the New Testament — is no longer assumed away. Its compatibility with Paul is now derived from two cited premises: that James's target is a barren faith, mere assent ("even the demons believe", Jas 2:19), and that works are the fruit and evidence of saving faith rather than a ground of justification. Moo and Johnson for the exegesis; Westminster XI.2 for the confessional form — faith "is not alone in the person justified, but is ever accompanied with all other saving graces, and is no dead faith, but worketh by love". james_harmonisation_is_load_bearing shows the argument genuinely depends on this: drop it and sola fide does not follow.

Weighed as a dispute, with each strand, Trent, the apocalyptic reading, Sanders, the critics, Jervell, Paul's gospel, Paul's word (lexically, and from Romans 4) and Trent read as a claim about that word as parties, one thing prevails outright: Paul's word — δικαιόω does not denote the renewal of the inward man. Its two routes are the only parties whose every link is rated above disputed, and each defeats Trent read as a claim about the word, which cannot be defended at all. Everything else ties. Every other party's weakest link is disputed, and every attack between Trent and a Reformed party runs both ways: Luke's case, Paul's gospel and Trent are each defensible, and none is accepted on every resolution. Luke's case, holding only Luke's words, meets Trent over faith's sufficiency, and the apocalyptic reading not at all — Luke says faith saved her, not that faith alone does — so the dispute between Campbell and the Reformed reading is between Campbell and Paul, over the genitive.

Where Trent parts from Paul (Gospel.lean). Paul's answer to anything added to the gospel is Galatians — another gospel, accursed (1:6–9); if righteousness came by the law, Christ died for nothing (2:21) — and the gospel is that Christ died for our sins (1 Corinthians 15:3). Read with the forensic sense of δικαιόω, it denies Trent's definition of justification as renewal. Trent grants every text, and — with the Joint Declaration (§22) and New Testament scholarship across traditions — the forensic sense of the verb. A checked Because finds where they part: one step, that a verdict on a finished work excludes the renewal wrought in us.

What Trent's definition claims (Definition.lean). The definition can be read as a claim about Paul's word or about what God does in justifying, and a checked Dilemma answers both. Read as a claim about the word, it cannot be held with the lexical case — the forensic sense, Paul's own words for renewal, and the rule of least meaning (Joos, Silva; Barr's "illegitimate totality transfer") — at a step rated wellSupported; nor can the step from the Latin gloss Trent rests that reading on (Augustine: "being justified" is "being made righteous") to what the Greek word denotes. Read as a claim about what God does, nothing about the word reaches it, and it conflicts with Paul twice — with his gospel in Galatians and with Romans 4:5–8, "God justifies the ungodly" — each at a disputed step: Augustine grants Romans 4 and reads it the other way. Romans 4 thus does two things: read for the word, it is a second route, rated wellSupported, to the lexical conclusion; read for the reality, it meets Trent where Galatians does, and no higher.

Heard narrower (Hearings.lean). Two questions a reader asks, answered by hearing the same dispute with some parties set aside. What did the Reformation itself decide? Heard as Rome and the Reformers alone, only Paul's word is forced; Trent's definition, as a claim about what God does, and the Reformed strands tie. Without Trent, would Scripture establish sola fide? Four things are then forced — Luke's "faith suffices", Paul's gospel, and Paul's word by both routes — but faith alone is still not: Campbell on πίστις Χριστοῦ, Sanders and Dunn on ἔργα νόμου, and Jervell on the yoke each still stand against it. The obstacle then is modern exegesis, not Rome.

Jesus' own words (JesusWords.lean). What does Jesus himself say? Luke 18:9–14 — the tax collector "went down to his house justified" — is his own teaching on justification and works, in Paul's word for it. Trent's case is consistent with every word of the parable, and with the tax collector bringing no meriting works. Trent never cites Luke 18; applied to it, its dispositions (Session VI, ch. 6) and canon 9 deny the step to "faith suffices". So Luke 18 meets Trent where Luke 7:50 does, at Trent's definition. Matthew 7:21–23 and 19:16–22 are read both ways, each reading cited and disputed, and neither text settles its question alone. Heard together, Jesus' words force nothing; heard without Trent, Luke's two sayings are forced (that faith sufficed, not that faith alone saves) and Matthew is not. This is a dispute of its own, kept apart from the one above for the reason the Johannine strand is.

Baptism (Baptism.lean). Trent makes water baptism the instrumental cause of justification, and qualifies it in its own words: "or the desire thereof". Water, the Spirit and "fire" are kept as separate atoms, so no argument passes from one sense of "baptism" to another. Read so that the washing itself is necessary for salvation — Feeney's reading — Trent's claim cannot be held with the thief read as Augustine reads him, nor with Rome's own teaching on the desire. Read in Trent's own words, the thief does not reach it; what it meets is the Reformed argument from the desire — where only the desire is present, what justifies is not the washing — at a step Aquinas contests. John 3:5 is a dilemma of its own: of the four readings of its "water" on record, only the baptismal one leaves Trent's step from the verse standing, and even then the step is disputed. And that Acts gives the Spirit both before the water and after it is common ground: Rome says God "is not bound by his sacraments".

Where things are

TestimonyArguments.SolaFide.Atoms — the atomic claims

The prooftexts of the three strands, their four disputed premises, the reading of Galatians as a polemic, the authorship of the disputed letters, the rivals' premises — covenantal nomism, forensic justification, the apocalyptic reading — the James premises, and the three parts of the conclusion. See TestimonyArguments.SolaFide for the dispute this encodes.

TestimonyArguments.SolaFide.Sources — a citation for every atom

Several cite functions, not one. The atoms are shared across the positions; the citation of a disputed premise is not, because each side of a dispute is cited to its own scholarship. The Reformed tradition and the New Perspective part over what Paul's ἔργα νόμου denotes; Dunn and Hays part over the genitive in πίστις Χριστοῦ; the apocalyptic reading parts from both.

baseCite carries the default citation of every atom; reformedCite, newPerspectiveCite, subjectiveGenitiveCite, apocalypticCite and lawObservantLukeCite each override the one atom where their position parts from it, and criticalAuthorshipCite the four atoms on who wrote the disputed letters. That is the disagreement made mechanical: it shows up as a difference in the generated manifest rather than as a remark in a docstring.

Rated inferences

A dispute weighs a position's inference steps as well as its premises (see Testimony.Logic.Dispute), and a step is rated disputed when a cited source grants its grounds and denies its conclusion. These are the ratings the positions in SolaFide.Dispute carry.

The claims, numbered

※ grounded in scripture alone: the reading is assumed, not argued for.

trentAgainstFaithAlone

Every Reformed strand's step is contested, by Trent. Trent grants what each strand reads — Romans 3:28 and Galatians 2:16, that Jesus' words save, that salvation is through grace — and anathematises the conclusion each draws: justification by faith alone (Session VI, canon 9).

def trentAgainstFaithAlone : Source :=
  {
    primary :=
      Reference.work tannerDecrees
        (Bib.Locus.sectionRef "Trent, Session VI (1547), canon 9"),
    tradition := Tradition.romanCatholic, confidence := Confidence.disputed }

trentOnMerit

Trent's own step, from merit to the denial of "not by works". Rated consensus: the step is conceded on both sides — it is why the Reformed deny merit — and the dispute is over its premise, not its inference.

def trentOnMerit : Source :=
  {
    primary :=
      Reference.work tannerDecrees
        (Bib.Locus.sectionRef
          "Trent, Session VI (1547), Decree on Justification, ch. 16"),
    tradition := Tradition.romanCatholic, confidence := Confidence.consensus }

trentAgainstThePleaAlone

The step from Luke 18 is contested, by Trent applied to it. Trent never cites Luke 18, and grants that nothing before justification, "whether faith or works", merits it (ch. 8). But it requires the dispositions it lists — fear, hope, beginning to love God, penitence (ch. 6) — and anathematises whoever says "nothing else is required to co-operate" (canon 9). Read by those chapters, the tax collector's humility and contrition are dispositions his justification required, not a plea that sufficed alone. So the step from the plea to "faith suffices" is disputed.

def trentAgainstThePleaAlone : Source :=
  { primary := Reference.work waterworthTrent (Bib.Locus.page 45),
    supporting := [Reference.work waterworthTrent (Bib.Locus.pages 33 34)],
    tradition := Tradition.romanCatholic, confidence := Confidence.disputed }

calvinAgainstObedienceAsGround

The Catholic step from Matthew 7:21 is contested, by Calvin. He grants the text, and that entry requires doing the Father's will, and denies that the doing is more than the fruit of faith: "These words, therefore, do not exclude faith, but presuppose it as the principle from which other good works flow."

def calvinAgainstObedienceAsGround : Source :=
  { primary := Reference.work calvinHarmony1 (Bib.Locus.pages 367 368),
    tradition := Tradition.reformedProtestant,
    confidence := Confidence.disputed }

catechismAgainstDoingAsBelieving

The Reformed step from Matthew 7:21 is contested, by the Catechism. It grants the text and reads it the other way: "one enters the kingdom of heaven not by speaking words, but by doing 'the will of my Father in heaven'" (§2826).

def catechismAgainstDoingAsBelieving : Source :=
  {
    primary :=
      Reference.work catechismCatholicChurch (Bib.Locus.sectionRef "2826"),
    tradition := Tradition.romanCatholic, confidence := Confidence.disputed }

calvinAgainstTheCommandmentsAsTheWay

The Catholic step from Matthew 19:17 is contested, by Calvin. He grants the text — "we have no right, therefore, to deny that the keeping of the law is righteousness" — and denies that it is the way to life for any sinner: "this passage was erroneously interpreted by some of the ancients, whom the Papists have followed, as if Christ taught that, by keeping the law, we may merit eternal life." Calvin answers the claim to merit; the reading encoded here claims less — the way made possible by grace — and he denies that too, since for him no sinner keeps the law.

def calvinAgainstTheCommandmentsAsTheWay : Source :=
  { primary := Reference.work calvinHarmony2 (Bib.Locus.page 394),
    tradition := Tradition.reformedProtestant,
    confidence := Confidence.disputed }

veritatisSplendorAgainstTheLegalReply

The Reformed step from Matthew 19:17 is contested, by John Paul II. He grants the text and reads it as the real path: Jesus "proposes them to us as the way and condition of salvation" (Veritatis Splendor 12).

def veritatisSplendorAgainstTheLegalReply : Source :=
  { primary := Reference.work veritatisSplendor (Bib.Locus.sectionRef "12"),
    tradition := Tradition.romanCatholic, confidence := Confidence.disputed }

calvinAgainstBaptismInJohnThreeFive

Trent's step from John 3:5 is contested, by Calvin. He grants the verse and denies that it requires water baptism: "I cannot bring myself to believe that Christ speaks of baptism" (on John 3:5, 110).

def calvinAgainstBaptismInJohnThreeFive : Source :=
  { primary := Reference.work calvinJohn (Bib.Locus.page 110),
    tradition := Tradition.reformedProtestant,
    confidence := Confidence.disputed }

readingsWithoutTheWater

The steps from each non-baptismal reading of John 3:5 are well supported. If the water is natural birth, or Ezekiel's cleansing and not baptism, or the Spirit's own cleansing, the verse does not require water baptism: no reader was found who holds one of these readings and still requires baptism from the verse. Those who require it deny the reading instead (Trent, Session VII, On Baptism, canon 2).

def readingsWithoutTheWater : Source :=
  { primary := Reference.work oliverWaterJohn,
    supporting :=
      [Reference.work Bib.calvinInstitutes (Bib.Locus.sectionRef "IV.xvi.25")],
    tradition := Tradition.christianHistoricalGrammatical,
    confidence := Confidence.wellSupported }

augustineOnTheThief

The step from the thief is well supported. Grant that he was promised paradise unbaptised, and that his case bears on salvation under the Gospel, and the washing itself is not necessary for salvation: "as in the thief, to whom the material administration of the sacrament was necessarily wanting, the salvation was complete" (Augustine, On Baptism IV.23.31), a passage Aquinas quotes with approval (III q.66 a.11). Feeney denies the conclusion; how he answers the thief could not be verified here.

def augustineOnTheThief : Source :=
  {
    primary :=
      Reference.work npnfAugustineManichaeans
        (Bib.Locus.sectionRef "On Baptism IV.23.31"),
    supporting :=
      [Reference.work aquinasSumma (Bib.Locus.sectionRef "III q.66 a.11")],
    tradition := Tradition.christianHistoricalGrammatical,
    confidence := Confidence.wellSupported }

catechismOnDesire

The step from the desire to the salvation it assures is well supported. If the desire for baptism brings about its fruits, the washing itself is not necessary for salvation: the Catechism says it "assures them the salvation that they were not able to receive through the sacrament" (1259). Feeney grants that the desire justifies; he denies that it saves. It is this saving fruit, as the Catechism states it, that he denies — the ground, not the step.

def catechismOnDesire : Source :=
  {
    primary :=
      Reference.work catechismCatholicChurch (Bib.Locus.sectionRef "1259"),
    tradition := Tradition.romanCatholic,
    confidence := Confidence.wellSupported }

westminsterOnTheDesire

The Reformed step from the desire, as Westminster holds it: grace and salvation "are not so inseparably annexed unto it, as that no person can be regenerated, or saved, without it" (XXVIII.5), and faith is "the alone instrument of justification" (XI.2).

def westminsterOnTheDesire : Source :=
  {
    primary :=
      Reference.work westminsterConfession (Bib.Locus.sectionRef "XXVIII.5"),
    supporting :=
      [Reference.work westminsterConfession (Bib.Locus.sectionRef "XI.2")],
    tradition := Tradition.reformedProtestant,
    confidence := Confidence.disputed }

aquinasOnTheDesire

The Reformed step from the desire is contested, by Aquinas. He grants that Cornelius and others "receive grace and virtues through their faith in Christ and their desire for Baptism", and denies that the sacrament is therefore not the instrument: the desire is for the sacrament, and "when baptized, they receive a yet greater fulness of grace and virtues" (III q.69 a.4 ad 2).

def aquinasOnTheDesire : Source :=
  {
    primary :=
      Reference.work aquinasSumma (Bib.Locus.sectionRef "III q.69 a.4 ad 2"),
    tradition := Tradition.romanCatholic, confidence := Confidence.disputed }

calvinOnActsTen

Where the Spirit comes before the water, and after it: common ground. Both grant that God is not bound to the water: the Catechism, that God "himself is not bound by his sacraments" (1257). Calvin's own sentence on Acts 10:47 goes further — "the Spirit is not included in baptism" — and that further claim is not what is granted here.

def calvinOnActsTen : Source :=
  { primary := Reference.work calvinActs1 (Bib.Locus.page 454),
    supporting :=
      [Reference.work catechismCatholicChurch (Bib.Locus.sectionRef "1257")],
    tradition := Tradition.christianHistoricalGrammatical,
    confidence := Confidence.consensus }

melanchthonOnLuke7

Where Melanchthon reads Luke 7:47 by 7:50, in the Apology of the Augsburg Confession (1531): the part of Article IV on love and the fulfilling of the law. The Concordia Triglotta numbers it Article III, 31–34; the reference is given by article and topic because paragraph numbers differ between editions.

def melanchthonOnLuke7 : Bib.Locus :=
  Bib.Locus.sectionRef
    "Apology IV, on love and the fulfilling of the law: Luke 7:47–50"

campbellOnDeliverance

The apocalyptic reading's step, from Christ's faithfulness and God's deliverance to the denial that faith is the condition. Rated plausible: no source cited here grants both grounds and affirms faith as the condition of justification.

def campbellOnDeliverance : Source :=
  { primary := Reference.work campbellDeliveranceOfGod,
    supporting := [Reference.work martynGalatians],
    tradition := Tradition.criticalScholarship,
    confidence := Confidence.plausible }

reformedWorksOfLawSource

The Reformed reading of ἔργα νόμου, cited to the tradition that holds it and to its modern defenders against the New Perspective. Disputed precisely because the New Perspective denies it; see newPerspectiveCite.

def reformedWorksOfLawSource : Source

baseCite

Citations shared by every package: the prooftexts and the hermeneutical premises, which none of the three positions disputes the wording of.

def baseCite : Claim → AtomMeta

reformedCite

The Reformed reading of the disputed premise.

def reformedCite : Claim → AtomMeta :=
  fun x =>
    match x with
    | Claim.worksOfLawMeansWorksGenerally =>
      {
        label :=
          "Paul's ἔργα νόμου denotes human works in general, not boundary markers",
        kind := PremiseKind.linguistic,
        source := reformedWorksOfLawSource }
    | c => baseCite c

newPerspectiveCite

The New Perspective's reading of the disputed premise: ἔργα νόμου denotes the covenant boundary markers, so Paul is not addressing human effort in general.

def newPerspectiveCite : Claim → AtomMeta :=
  fun x =>
    match x with
    | Claim.worksOfLawMeansWorksGenerally =>
      {
        label :=
          "Paul's ἔργα νόμου denotes Jewish covenant boundary markers, not works in general",
        kind := PremiseKind.linguistic,
        source :=
          { primary := Reference.work dunnNewPerspective,
            supporting :=
              [Reference.work sandersPaulPalestinianJudaism,
                Reference.work wrightWhatPaulSaid,
                Reference.work wrightJustification],
            tradition := Tradition.criticalScholarship,
            confidence := Confidence.disputed } }
    | c => baseCite c

subjectiveGenitiveCite

Hays's reading of the genitive: πίστις Χριστοῦ is Christ's own faithfulness. Everything else as baseCite.

def subjectiveGenitiveCite : Claim → AtomMeta

lawObservantLukeCite

Jervell's reading of Luke-Acts: what Acts 15 withholds from gentiles is Israel's law as a mark of belonging, and the law is not refused as a means of salvation. Everything else as baseCite.

def lawObservantLukeCite : Claim → AtomMeta

criticalAuthorshipCite

The critical view of authorship: Ephesians and Titus are not by Paul, and 1 and 2 Peter not by Peter. Each atom is cited to a scholar who holds that view of that letter, with Ehrman for the case across all four. Marshall's mediating view of the Pastorals — written by Paul's circle after his death, without intent to deceive — is cited with the critical side, because it too denies that Paul wrote Titus.

def criticalAuthorshipCite : Claim → AtomMeta

criticsCite

The New Perspective's critics: Second Temple Judaism was not uniformly covenantal nomism, because final vindication according to works was widely held. Gathercole primary, the Variegated Nomism volume in support.

def criticsCite : Claim → AtomMeta :=
  fun x =>
    match x with
    | Claim.secondTempleCovenantalNomism =>
      {
        label :=
          "Second Temple Judaism also held final vindication according to works",
        kind := PremiseKind.historical,
        source :=
          { primary := Reference.work gathercoleWhereIsBoasting,
            supporting := [Reference.work carsonVariegatedNomism1],
            tradition := Tradition.reformedProtestant,
            confidence := Confidence.disputed } }
    | c => reformedCite c

tridentineCite

The Tridentine reading of what justification is: "not remission of sins merely, but also the sanctification and renewal of the inward man". Everything else as baseCite.

def tridentineCite : Claim → AtomMeta :=
  fun x =>
    match x with
    | Claim.justificationIsForensicOnly =>
      { label := "Justification is not forensic only: it renews the inward man",
        kind := PremiseKind.theological,
        source :=
          {
            primary :=
              Reference.work tannerDecrees
                (Bib.Locus.sectionRef
                  "Trent, Session VI (1547), Decree on Justification, ch. 7"),
            tradition := Tradition.romanCatholic,
            confidence := Confidence.wellSupported } }
    | c => baseCite c

finnishCite

The Finnish reading of Luther: justification is not forensic only, because Christ himself is present in faith and is the believer's righteousness. Everything else as reformedCite.

def finnishCite : Claim → AtomMeta :=
  fun x =>
    match x with
    | Claim.justificationIsForensicOnly =>
      {
        label :=
          "Justification is not forensic only: Christ is present in faith",
        kind := PremiseKind.theological,
        source :=
          { primary := Reference.work mannermaaChristPresentInFaith,
            tradition := Tradition.criticalScholarship,
            confidence := Confidence.disputed } }
    | c => reformedCite c

apocalypticCite

The apocalyptic reading: the genitive is subjective, and it is Campbell's reason for reading it so that the citation records.

def apocalypticCite : Claim → AtomMeta

TestimonyArguments.SolaFide.Lines — the strands, and what they share

Three strands deliver the conclusion, by different words from different speakers: Paul, Jesus, and Peter at Jerusalem. Each delivers only what its own texts say. Paul's says justification is by faith alone; Jesus' words at Luke 7:50 and Peter's at Jerusalem say that faith suffices, which is weaker, and is all the conclusion's "through faith" needs. A fourth line answers James, and a fifth — the apocalyptic reading — denies what Paul delivers. What every package holds in common is collected here too, so that a variant package is a named difference rather than a retyped list.

Lines of reason

Three strands deliver the conclusion, and a fourth line answers James. They do not all deliver the same thing. Paul argues for alone: the polemic refuses circumcision added to faith, and Galatians 2:16 names faith as the one means (ἐὰν μή, "except through faith"). Luke 7:50 and Acts 15 say that faith saves, and that the woman's love and the law's yoke are not what does; they do not say that nothing else could. So they deliver faithIsSufficient. The difference matters in a dispute, where a case is attacked on what it derives as well as on what it assumes: credit Luke with alone, and a reading that denies faith alone — the apocalyptic reading — attacks Luke's case on a claim Luke never made. The James harmonisation is deliberately not a strand: it does not reach justificationByFaithAlone by an independent route, it supplies a premise the closing step needs. So it contributes its grounds and its step to the case without being one of the lines caseOf treats as converging.

paulineToFaithAlone

The Pauline strand. From Romans and Galatians to justification by faith alone, read from Galatians 2:16 as the centre of the letter's polemic.

Each premise does its own work. Galatians 2:16 excludes works of the law; read as an objective genitive, it also names faith in Christ as the means of justification. The polemic says what is being refused: circumcision added to faith as a requirement. That is where alone comes from. The Galatians already believed, and adding a work to their faith is what Paul says severs them from Christ (5:4). Only the ἔργα νόμου premise lets circumcision stand for works in general rather than for one ethnic marker.

dominicalToSufficiency

The dominical strand. From Jesus' own words at Luke 7:50 to the sufficiency of faith, by way of the lexical premise about σῴζω and the reading of 7:47 that answers "she loved much": her love shows her forgiveness and does not earn it, so what Jesus names as saving her is her faith. It says her faith saved her, and no more — not that nothing else could have. Independent of Paul, and of the ἔργα νόμου dispute.

apostolicToSufficiency

The apostolic strand. From Peter's speech at the Jerusalem council to the sufficiency of faith, by way of the disputed premise about the yoke.

The council answers the same demand Galatians answers: circumcision and the law of Moses as a condition of salvation (Acts 15:1, 15:5). Peter's reply names faith as what cleansed the gentiles' hearts and grace as how Jew and gentile alike are saved, and refuses the yoke. If the yoke is the whole law as a condition of salvation, the gentiles are saved without it, by faith: faith suffices.

jamesHarmonisation

The harmonisation of James: because James's target is barren faith, and works are the fruit of saving faith rather than its ground, James 2:24 does not contradict Paul. Derived rather than assumed.

solaFide

The conclusion, in its three parts: salvation is by grace, not by works, and through faith. Stated as three atoms rather than one so that a position can be shown to hold some parts and deny another — which the apocalyptic reading and the Tridentine position each do, over different parts.

graceNotWorks

The first two parts: by grace, and not by works. What the apocalyptic reading keeps.

toGrace

By grace, from the texts that say so: a gift through faith (Ephesians 2:8), a gift and not wages (Romans 4:4–5), mercy (Titus 3:5). Neither a strand nor the answer to James is needed for this part.

toNotByWorks

Not by works, from the same texts, which say "not of works" in terms — provided James 2:24 is answered, and scripture does not contradict itself. No strand is needed for this part either; what it needs, and grace does not, is an answer to James.

faithAloneSuffices

Faith alone is at least faith sufficient: if nothing but faith is the condition, faith is enough. How Paul's strand, which argues the stronger claim, reaches the part of the conclusion the others reach directly.

toThroughFaith

Through faith, from the sufficiency of faith and Ephesians 2:8 (διὰ πίστεως: faith as the means). This is the only part of the conclusion the three strands are needed for, and it needs only what each of them says.

paulineLine — Pauline strand (ἔργα νόμου, πίστις Χριστοῦ)

The Pauline line. Its grounds are the reading of Galatians as a polemic and the two disputed lexical premises, about ἔργα νόμου and about πίστις Χριστοῦ. The prooftexts its step reads are shared with every other package, which is exactly why denying a lexical premise does not cost the argument its prooftexts.

The genitive dispute is a premise inside this strand, not a third strand. Every πίστις Χριστοῦ text sets it against νόμος, so a route through the genitive still passes through what ἔργα νόμου denotes. A line on the genitive whose grounds omitted the ἔργα νόμου premise would misdescribe Paul.

dominicalLine — Dominical strand (σῴζω at Luke 7:50)

The dominical line, resting on Jesus' words rather than Paul's. Its distinctive grounds are the other lexical premise, and the reading of 7:47 that keeps the woman's love from being the ground of her forgiveness.

apostolicLine — Apostolic strand (Acts 15:7–11)

The apostolic line, resting on Peter as Luke reports him rather than on Paul or on Jesus. Its distinctive ground is the premise about the yoke.

It is logically independent of the Pauline strand: no premise is shared. It is not dialectically independent. A reader who takes ἔργα νόμου as Israel's boundary markers will read Peter's yoke the same way, as Jervell does, so the two premises tend to be won or lost together. What the encoding shows is that they are two premises about two texts, and an opponent has to answer both.

jamesLine — Harmonisation of James 2:24

The James line: not a route to the conclusion but the answer to the one text that stands against it.

deliveranceNotFaithAlone

The apocalyptic reading (Martyn, Campbell). If πίστις Χριστοῦ is Christ's own faithfulness, and δικαιοσύνη θεοῦ is God's act of deliverance, then faith is not the condition on which justification is granted. So justification by faith alone, in the sense the Reformed and New Perspective packages share, is denied. Grace and "not by works" are not denied: the reading rejects the condition, not the gift.

deliveranceIsGrace

What the apocalyptic reading keeps. If δικαιοσύνη θεοῦ is God's act of deliverance, it is sheer gift, conditioned on nothing a person does: by grace, and not by works. Campbell's inference, and his reason for calling the reading more gracious than the one it replaces.

apocalypticLine — Apocalyptic reading (δικαιοσύνη θεοῦ as deliverance)

The apocalyptic line: a rival route from Paul, delivering the denial of what the Pauline strand delivers.

sandersLine — Covenantal nomism (Sanders, Dunn)

The New Perspective's reason for its reading of ἔργα νόμου. If Second Temple Judaism was covenantal nomism — in by grace, staying in by works — then Paul's opponents were not seeking to earn salvation, and what he refuses is not works as such but the marks that kept gentiles out: the boundary markers. The ground is Sanders'; the inference is Dunn's, and is cited as his.

criticsLine — Variegated nomism (Gathercole, Carson et al.)

The critics' reply. If Second Temple Judaism also held final vindication according to works, then the demand Galatians refuses — circumcision added to faith as a requirement — is a demand for obedience, and what Paul refuses in refusing it is works as such. So the Reformed reading of ἔργα νόμου is not assumed but derived: from the reading of Galatians as a polemic, and from a historical claim about Judaism that is argued on the evidence.

jervellLine — Law-observant Luke (Jervell)

Jervell's reading of the yoke. If Luke presents the Jewish believers as keeping the law (Acts 21:20–24), and the decree as laying part of it on gentiles (Acts 15:20–21), then what Peter refuses at 15:10 is not the law as a condition of salvation but the whole of Israel's law laid on gentiles. The step is contested: Bruce grants both texts and reads the yoke as the law taken as a condition of salvation.

trentOnIncrease

Trent's step from its definition to merit: if justification is the renewal of the inward man, and that renewal grows through good works, then good works increase justification (Session VI, ch. 10 and canon 24). Rated consensus, as trentOnMerit is: the Reformed deny the definition, not the inference, and canon 24 condemns the Reformed alternative by name — that works are "merely the fruits and signs of Justification obtained".

def trentOnIncrease : Source :=
  {
    primary :=
      Reference.work tannerDecrees
        (Bib.Locus.sectionRef "Trent, Session VI (1547), canon 24"),
    supporting :=
      [Reference.work tannerDecrees
          (Bib.Locus.sectionRef
            "Trent, Session VI (1547), Decree on Justification, ch. 10")],
    tradition := Tradition.romanCatholic, confidence := Confidence.consensus }

tridentineLine — Trent (justification as renewal)

Trent's line. From its definition of justification — the renewal of the inward man, not remission of sins only — and the growth of that renewal through good works, to merit: good works increase justification (Session VI, ch. 10, canon 24). The Reformed grant the growth and deny the definition, so the step carries the objection only as far as the definition does.

trentDefinitionSteps

What Trent's definition rules out: justification as forensic only (canon 11); justification as distinct from the sanctification that follows it; and faith as sufficient. If justification is the renewal of the inward man by infused charity, then faith "unless hope and charity be added thereto" does not unite a person perfectly with Christ (ch. 7), and whoever says that "nothing else is required to cooperate" is anathema (canon 9). Trent's denial of sufficiency is not a separate thesis: it follows from what Trent says justification is.

prooftexts

The prooftexts the strands read. Shared by every Reformed package, and by the New Perspective.

sharedGrounds

Everything the strands share: the prooftexts, the grounds of the James harmonisation, and scripture's self-consistency.

sharedGroundsWithoutJames

The same, with James unanswered.

conclusionSteps

The steps to the three parts of the conclusion, one each, and the step by which faith alone gives faith sufficient.

closingSteps

The steps that close the argument: the James harmonisation, then the steps to the parts of the conclusion.

Paul's gospel, against justification as renewal

Galatians is a letter about another gospel. The Teachers did not deny Christ; they added circumcision to him, and Paul calls that addition a different gospel and its preachers accursed (1:6–9). What he sets against it is what he received: Christ died for our sins (1 Corinthians 15:3); if righteousness came by the law, Christ died for nothing (Galatians 2:21); whoever would be justified by the law is severed from Christ (5:2–4).

This line reads those texts as one claim — Christ's work is the whole ground of justification — and carries it, with the forensic sense of Paul's verb, to the denial of Trent's definition: if justification is God's verdict on the ground of a finished work, the renewal wrought in us is no part of it.

galatianGospelReadingSource

Paul's reading of the gospel in Galatians: Christ's death is the whole ground, and adding a ground is another gospel. Cited to Moo on Galatians and to the Westminster Confession, and rated disputed: Trent grants every text and that Christ's passion merited justification (ch. 7), and denies that nothing is added (canons 24, 32).

def galatianGospelReadingSource : Source :=
  {
    primary :=
      Reference.work mooGalatians
        (Bib.Locus.adLoc { book := Book.galatians, chapter := 1, verse := 6 }),
    supporting :=
      [Reference.work westminsterConfession (Bib.Locus.sectionRef "XI.1")],
    tradition := Tradition.reformedProtestant,
    confidence := Confidence.disputed }

verdictNotRenewalSource

The step from a verdict on a finished work to "renewal is no part of justification": Westminster XI.1, God justifies "not by infusing righteousness into them, but by pardoning their sins, and by accounting and accepting their persons as righteous; not for anything wrought in them". Rated disputed, and the source that makes it so is Rome's own: the Joint Declaration (§22) grants the ground — God "no longer imputes to them their sin" — and denies the step: forgiveness and the love the Spirit effects "are not to be separated". Among New Testament scholars, Gorman takes the same side: the verdict is an effective word that transforms.

def verdictNotRenewalSource : Source :=
  {
    primary :=
      Reference.work westminsterConfession (Bib.Locus.sectionRef "XI.1"),
    supporting :=
      [Reference.work Bib.calvinInstitutes (Bib.Locus.sectionRef "III.xi.2"),
        Reference.work morrisApostolicPreaching],
    tradition := Tradition.reformedProtestant,
    confidence := Confidence.disputed }

galatianGospelLine — Paul's gospel (Galatians 1:6–9; 2:21; 5:2–4; 1 Corinthians 15:3)

Paul's gospel, as Galatians states it and 1 Corinthians summarises it.

verdictExcludesRenewal

The step where Trent parts from Paul. If justification is God's verdict — δικαιόω is forensic, the opposite of condemning (Romans 8:33–34) — and its ground is Christ's finished work alone, then the renewal of the inward man is no part of it.

What Paul's word means

Trent's definition can be read as a claim about Paul's word — that δικαιόω, in Paul, denotes the renewal of the inward man — and this line answers it on lexical ground alone. δικαιόω is forensic: its opposite is condemn. Paul has other words for renewal, and sets them beside it. And a word contributes the least meaning its context requires: nothing in a verdict's context requires a second, inward sense, and to supply one from the doctrine is what Barr called illegitimate totality transfer. So Paul's δικαιόω does not denote renewal.

The line says nothing about what God does when he justifies. That is the other reading of Trent's definition, and this line does not reach it (TestimonyArguments.SolaFide.Definition).

leastMeaningSource

The step from the forensic sense, Paul's own vocabulary for renewal, and the rule of least meaning to "δικαιόω does not denote renewal". Silva's method, applied as Moo applies it to Romans. Rated wellSupported: no source cited here grants the three grounds and denies the conclusion. Those who hold that δικαιόω means "make righteous" — VanLandingham, and the Latin tradition from Augustine — deny the forensic sense itself, and are weighed in that premise's rating; those who hold that God's verdict renews — Gorman, the Joint Declaration — make a claim about what God does, not about the word.

def leastMeaningSource : Source :=
  { primary := Reference.work silvaBiblicalWords,
    supporting :=
      [Reference.work mooRomans (Bib.Locus.sectionRef "p. 80"),
        Reference.work barrSemantics],
    tradition := Tradition.christianHistoricalGrammatical,
    confidence := Confidence.wellSupported }

lexicalLine — Paul's word (δικαιόω, by the rule of least meaning)

Paul's word, read by the rule of least meaning.

Romans 4: the ungodly, justified

An exegetical case, in two steps. The first is about Paul's argument: God "justifies the ungodly" (4:5), and what he counts to them is described in the psalm Paul quotes — lawless deeds forgiven, sin not counted (4:6–8). λογίζομαι is the language of reckoning, set against wages owed (4:4). So, in Paul's own argument, the righteousness counted to the ungodly is sin not counted. No source cited here grants the texts and the sense of the verb and denies that gloss.

The second step is where the exegesis is put to work, and it goes two ways.

• Against a claim about Paul's word. With the rule of least meaning, the verb Paul glosses so does not also denote the renewal of the inward man. Rated wellSupported, as the lexical case is.
• Against a claim about what God does. That what is counted is sin not counted, and that the verdict is forensic, excludes renewal from justification. Augustine grants every word of Romans 4 and reads the verse the other way — God "justifies the ungodly man, that he may become a godly one" (On the Spirit and the Letter 26.45) — and Trent makes the justice "whereby He maketh us just" justification's formal cause (ch. 7). So that step is disputed, as the step from Galatians is.

romansFourExegesisSource

The exegesis of Romans 4:3–8: reckoning language, set against wages, and the psalm's gloss on what is counted. Cited to Moo on Romans, and rated wellSupported: Augustine and Trent grant the texts and dispute what follows from them, not what Paul says the counting is.

def romansFourExegesisSource : Source :=
  {
    primary :=
      Reference.work mooRomans
        (Bib.Locus.adLoc { book := Book.romans, chapter := 4, verse := 6 }),
    supporting := [Reference.work bdag (Bib.Locus.sectionRef "s.v. λογίζομαι")],
    tradition := Tradition.christianHistoricalGrammatical,
    confidence := Confidence.wellSupported }

romansFourReadingSource

The step from Paul's gloss, with the forensic sense of the verb, to "renewal is no part of justification". Cited to Moo on Romans 4:5 and Westminster XI.1, and rated disputed: Augustine grants the texts and reads "justifies the ungodly" as making the ungodly godly, and Trent's chapter 7 makes the justice "whereby He maketh us just" justification's formal cause.

def romansFourReadingSource : Source :=
  {
    primary :=
      Reference.work mooRomans
        (Bib.Locus.adLoc { book := Book.romans, chapter := 4, verse := 5 }),
    supporting :=
      [Reference.work westminsterConfession (Bib.Locus.sectionRef "XI.1")],
    tradition := Tradition.reformedProtestant,
    confidence := Confidence.disputed }

romansFourExegesisLine — Romans 4:3–8 (the ungodly, justified)

Romans 4:3–8, read: God justifies the ungodly, and the righteousness he counts to them is, in Paul's own gloss, sin not counted.

glossByLeastMeaning

From Paul's gloss, by the rule of least meaning: the verb he glosses so does not also denote renewal.

countedExcludesRenewal

From Paul's gloss, with the forensic sense of the verb: renewal is no part of justification. The step Augustine denies.

TestimonyArguments.SolaFide.Packages — the positions, and the variants

The positions — Reformed, New Perspective, subjective genitive, law-observant Luke, Finnish, critical authorship, apocalyptic, Tridentine — and reduced Reformed packages, each missing a named premise. Whether a premise is load-bearing is shown by removing it and then either establishing the conclusion anyway or naming a countermodel.

Packages

reformed — Reformed (sola fide)

The classical Protestant position: all three strands, and every disputed premise they rest on — ἔργα νόμου and πίστις Χριστοῦ in Paul, σῴζω in Luke, the yoke in Acts.

No premise here rests on scripture alone.

dominicalWithoutSozo — Dominical strand (σῴζω at Luke 7:50)

The dominical line without the σῴζω premise. The reading of 7:47 stays: it is not the premise being tested.

paulineWithoutWorksOfLaw — Pauline strand (ἔργα νόμου, πίστις Χριστοῦ)

The Pauline line without the ἔργα νόμου premise.

paulineWithoutPistisChristou — Pauline strand (ἔργα νόμου, πίστις Χριστοῦ)

The Pauline line without the objective genitive.

newPerspective — New Perspective on Paul

The New Perspective on Paul: it denies the traditional reading of ἔργα νόμου while accepting justification by faith, which is what Dunn and Wright actually hold. It keeps the objective genitive, as Dunn does, so the one Pauline ground it denies is the ἔργα νόμου premise.

The denial is not assumed: sandersLine derives it from covenantal nomism, so the package rests on Sanders' account of Judaism and Dunn's inference from it, which is where its critics engage it.

It takes no position on the yoke of Acts 15:10: the apostolic line keeps its step and loses its ground, so the package neither grants nor denies the premise on the New Perspective's behalf.

No premise here rests on scripture alone.

finnish — Finnish reading of Luther (Mannermaa)

The Finnish reading of Luther (Mannermaa): the Reformed case, with the forensic account of justification denied. Christ himself is present in faith and is the believer's righteousness, so justification is not a declaration only.

On what justification is, this sides with Trent against the Reformed account; on sola fide it sides with the Reformed. The encoding shows both, and shows that the two questions are independent.

No premise here rests on scripture alone.

subjectiveGenitive — Subjective genitive (πίστις Χριστοῦ as Christ's faithfulness)

The subjective genitive (Hays): πίστις Χριστοῦ in Galatians 2:16 is Christ's own faithfulness, so the verse does not name the believer's faith as the means of justification. Everything else in the Reformed case is granted.

No premise here rests on scripture alone.

lawObservantLuke — Law-observant Luke (the yoke as Israel's law for gentiles)

Luke as law-observant (Jervell): the yoke Acts 15:10 refuses is Israel's law laid on gentiles as a mark of belonging, not the law as a condition of salvation. Everything else in the Reformed case is granted. The rival the apostolic strand was written against.

No premise here rests on scripture alone.

criticalAuthorship — Reformed, with the critical view of authorship

The Reformed case granted every critical conclusion about authorship: Ephesians and Titus not by Paul, 1 and 2 Peter not by Peter.

Nothing else changes, and that is the point. The case reads these letters as canonical scripture, bound together by scriptureSelfConsistent, not as the testimony of a named apostle. So conceding their authorship costs the argument nothing — while it would cost an argument that cited Ephesians 2:9 as evidence of what Paul meant by "works", which is why worksOfLawMeansWorksGenerally leans on Romans instead.

No premise here rests on scripture alone.

apocalyptic — Apocalyptic reading of Paul (Martyn, Campbell)

The apocalyptic reading of Paul (Martyn, Campbell). It rejects the traditional reading's framing of justification and also the New Perspective's. The question is neither how an individual is accepted nor how Jew and gentile are related, but God's deliverance of the world in Christ.

It shares Galatians with the Reformed reading — the text of 2:16 and the circumcision polemic — and closes with the same step to salvation. It does not share the dominical or apostolic strands, which neither Martyn nor Campbell argues from; to grant it Luke 7:50 or Acts 15 would be to encode a position nobody holds.

No premise here rests on scripture alone.

apocalypticOnGraceAndWorks — Apocalyptic reading, on grace and works only

The apocalyptic reading, asked only about the first two parts of the conclusion: by grace, and not by works.

No premise here rests on scripture alone.

tridentinePremises

Trent's premises, given the line that carries its definition to merit: four prooftexts it shares with the Reformed, scripture's self-consistency, what its definition rules out, and the step from merit to the denial of "not by works" (ch. 16).

Not built from the Reformed lines, and that is the point: it shares four prooftexts with them and nothing else, so caseOf would misdescribe it.

def tridentinePremises : Line Claim → List (Formula Claim) :=
  fun line =>
    [p Claim.ephesians2_8_9, p Claim.romans3_28,
            p Claim.galatians2_16,
            p Claim.titus3_5,
            p Claim.scriptureSelfConsistent] ++
          line.premises ++
        trentDefinitionSteps ++
      [p Claim.worksMeritIncreaseOfJustification 🡒
          notP Claim.salvationNotByWorks]

tridentine — Tridentine (Council of Trent, Session VI)

The Tridentine position: justification is the renewal of the inward man, that renewal grows through good works, so works performed in grace merit an increase of justification — which denies the second part of the conclusion, salvation not by works. The same definition denies that justification is forensic only.

No premise here rests on scripture alone.

Variants

Each removes named premises from reformed and keeps the rest. The Pauline strand has two lexical premises, so it has two reduced forms.

reformedWithoutWorksOfLaw — Reformed, minus the ἔργα νόμου premise

The Reformed package without the ἔργα νόμου premise.

No premise here rests on scripture alone.

reformedWithoutSozo — Reformed, minus the dominical lexical premise

The Reformed package without the dominical lexical premise.

No premise here rests on scripture alone.

reformedWithoutWorksOfLawOrSozo — Reformed, minus the ἔργα νόμου and σῴζω premises

The Reformed package with the ἔργα νόμου premise and the dominical premise removed: the two disputes the argument was first built to survive. The apostolic strand is untouched.

No premise here rests on scripture alone.

reformedWithoutEveryStrandsPremise — Reformed, minus the ἔργα νόμου, σῴζω and yoke premises

The Reformed package with a disputed premise removed from every strand: ἔργα νόμου from Paul, σῴζω from Luke, the yoke from Acts. The objective genitive stays.

No premise here rests on scripture alone.

reformedWithoutPistisChristouSozoOrYoke — Reformed, minus the πίστις Χριστοῦ, σῴζω and yoke premises

The same with the objective genitive removed in place of ἔργα νόμου: the Pauline strand loses its other lexical premise, and the other two strands theirs.

No premise here rests on scripture alone.

graceAndWorksWithoutAnyLexicalPremise — Grace and works, minus every lexical premise

The Reformed package with every lexical premise removed — both of Paul's, Luke's σῴζω and the yoke of Acts 15 — asked only about grace and works. The reading of Galatians as a polemic stays, and so does the answer to James.

No premise here rests on scripture alone.

paulineStrandOnTheCritics — Pauline strand alone, on variegated nomism

The New Perspective's critics (Gathercole, the Variegated Nomism volume), on the Pauline strand alone: the ἔργα νόμου premise derived from a denial of covenantal nomism rather than assumed, and the other two strands left out. Does Paul alone carry sola fide on Gathercole's history?

No premise here rests on scripture alone.

paulineStrandOnSanders — Pauline strand alone, on covenantal nomism

The same on Sanders' reading of Judaism.

No premise here rests on scripture alone.

reformedWithoutJamesHarmonisation — Reformed, minus the James harmonisation

The Reformed package without the premises that harmonise James.

No premise here rests on scripture alone.

graceWithoutJamesHarmonisation — Grace alone, minus the James harmonisation

The same, asked only about the first part of the conclusion: is salvation by grace, with James 2:24 left unanswered?

No premise here rests on scripture alone.

tridentineCase — Trent, against 'not by works'

Trent, as the argument it makes in a dispute: justification is the renewal of the inward man, that renewal grows through good works, so works done in grace merit an increase of justification, and salvation is not apart from works. The same premises as tridentine, concluding what Trent denies.

No premise here rests on scripture alone.

Paul's gospel, against Trent's definition

galatianGospel — Paul's gospel (Galatians 1), against justification as renewal

Paul's gospel, against justification as renewal. Galatians and 1 Corinthians read as one claim — Christ's work is the whole ground — with the forensic sense of δικαιόω and Romans 8:33–34, concluding that justification is not the renewal of the inward man: the direct denial of Trent's definition (Session VI, ch. 7).

Grounded in scripture alone: 1 Corinthians 15:3: the gospel of first importance — Christ died for our sins, Romans 8:33–34: it is God who justifies — who is to condemn?.

romansFourOnTheWord — Romans 4:3–8, on Paul's word (by the rule of least meaning)

Romans 4, on what Paul's word means. Paul glosses the righteousness God counts to the ungodly as sin not counted; by the rule of least meaning, the verb he glosses so does not also denote the renewal of the inward man. An exegetical route to what the lexical case reaches lexically.

No premise here rests on scripture alone.

romansFourCase — Romans 4:3–8, against justification as renewal

Romans 4, against justification as renewal. Paul glosses the righteousness God counts to the ungodly as sin not counted; with the forensic sense of the verb, justification is not the renewal of the inward man.

No premise here rests on scripture alone.

Paul's word, against justification as renewal

lexicalCase — Paul's word (δικαιόω, by the rule of least meaning)

Paul's word. δικαιόω is forensic, Paul names renewal with words of its own, and a word contributes the least meaning its context requires: so Paul's δικαιόω does not denote the renewal of the inward man.

Grounded in scripture alone: Paul names renewal with other words (ἀνακαίνωσις, ἁγιασμός) and sets them beside δικαιόω.

TestimonyArguments.SolaFide.Results — what does and does not follow

Entailments are established with establish; refutations name a countermodel — the rival's own reading, written down as a valuation — and use refute_with.

lexical_premises_jointly_load_bearing is the result the encoding exists to make possible: no strand's disputed premise carries the argument, and only removing one from every strand defeats it. apostolic_strand_survives_paul_and_luke records what the third strand changed: the two disputes that used to be jointly decisive are no longer enough.

Results

reformed_establishes

Given the Reformed premises, the conclusion follows.

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

newPerspective_establishes

The New Perspective establishes it too. Dunn and Wright reject the traditional reading of ἔργα νόμου; they do not reject justification by faith. Once Jesus' words at Luke 7:50 are in view, denying the Pauline lexical premise no longer blocks the conclusion.

Winning the ἔργα νόμου argument outright is therefore not a defeat of sola fide, and this library says so in a form either side can check. The critics of the New Perspective dispute its premise, not this result.

theorem newPerspective_establishes : Establishes newPerspective
-- axioms: propext, Quot.sound

tridentineReading

The Tridentine reading, as a valuation: works merit an increase of justification, so salvation is not apart from works; and justification renews the inward man, so it is not forensic only, not distinct from sanctification, and not had by faith alone — faith without charity does not suffice.

def tridentineReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.salvationNotByWorks => False
    | Claim.justificationIsForensicOnly => False
    | Claim.justificationDistinctFromSanctification => False
    | Claim.faithIsSufficient => False
    | Claim.justificationByFaithAlone => False
    | x => True

tridentine_not_establishes

The Tridentine premises do not establish the conclusion — they entail the negation of its second part, that salvation is not by works.

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

worksOfLaw_not_load_bearing

The ἔργα νόμου premise is not load-bearing on its own: strip it and the other strands still carry the argument.

theorem worksOfLaw_not_load_bearing : Establishes reformedWithoutWorksOfLaw
-- axioms: propext, Quot.sound

sozo_not_load_bearing

Nor is the dominical lexical premise: strip it and the other strands still carry the argument.

theorem sozo_not_load_bearing : Establishes reformedWithoutSozo
-- axioms: propext, Quot.sound

apostolic_strand_survives_paul_and_luke

The two disputes that used to decide the argument no longer do. Deny both the ἔργα νόμου premise and the dominical premise — the pair whose joint removal defeated sola fide before Acts 15 was encoded — and the conclusion still follows, by Peter's speech at Jerusalem.

This is the change the third strand makes, stated as a result rather than left to be inferred from the absence of an old one.

theorem apostolic_strand_survives_paul_and_luke : Establishes
    reformedWithoutWorksOfLawOrSozo
-- axioms: propext, Quot.sound

pistisChristou_not_load_bearing

The objective genitive is not load-bearing for sola fide as a whole. Grant Hays that πίστις Χριστοῦ is Christ's own faithfulness, keep everything else, and the conclusion still follows.

The genitive is the hinge of the Pauline strand, as pistisChristou_jointly_load_bearing shows. It is not the hinge of the argument. A reader who wins the genitive for Hays has cost the Reformed case its Pauline route, and not its conclusion.

theorem pistisChristou_not_load_bearing : Establishes subjectiveGenitive
-- axioms: propext, Quot.sound

acts15Yoke_not_load_bearing

Nor is the yoke. Grant Jervell that the yoke of Acts 15:10 is Israel's law laid on gentiles, not the law as a condition of salvation, keep everything else, and the conclusion still follows by Paul and by Luke 7:50.

theorem acts15Yoke_not_load_bearing : Establishes lawObservantLuke
-- axioms: propext, Quot.sound

neitherLexicalReading

A reading on which no strand's disputed premise holds: Paul's phrase is about boundary markers, Jesus' σέσωκέν σε is about healing, and Peter's yoke is Israel's law for gentiles.

def neitherLexicalReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.worksOfLawMeansWorksGenerally => False
    | Claim.sozoIsSoteriological => False
    | Claim.acts15YokeIsLawAsCondition => False
    | Claim.justificationByFaithAlone => False
    | Claim.faithIsSufficient => False
    | Claim.salvationThroughFaith => False
    | x => True

lexical_premises_jointly_load_bearing

The result worth having. No strand's disputed premise carries the argument alone, but together they do: remove the ἔργα νόμου premise from Paul, σῴζω from Luke and the yoke from Acts, and sola fide no longer follows, with everything else retained.

So the Reformation's material principle, as encoded here, does not hang on the sense of Paul's ἔργα νόμου. It hangs on that, or on the sense of Jesus' σέσωκέν σε, or on Peter's yoke — and an opponent must defeat all three. The same holds with the πίστις Χριστοῦ premise in place of ἔργα νόμου; see pistisChristou_jointly_load_bearing.

theorem lexical_premises_jointly_load_bearing : ¬Establishes
    reformedWithoutEveryStrandsPremise
-- axioms: propext, Quot.sound

neitherPistisNorSozoReading

A reading on which Galatians 2:16 names Christ's faithfulness rather than faith in Christ, Jesus' σέσωκέν σε is about healing, and Peter's yoke is Israel's law for gentiles.

def neitherPistisNorSozoReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.pistisChristouObjective => False
    | Claim.sozoIsSoteriological => False
    | Claim.acts15YokeIsLawAsCondition => False
    | Claim.justificationByFaithAlone => False
    | Claim.faithIsSufficient => False
    | Claim.salvationThroughFaith => False
    | x => True

pistisChristou_jointly_load_bearing

Within the Pauline strand, faith in Christ is load-bearing. Deny the objective genitive, and the disputed premise of each other strand, keep the ἔργα νόμου premise and the reading of Galatians as a polemic against circumcision, and sola fide no longer follows.

Excluding works is not enough to reach faith alone. Galatians 2:16 must also name the believer's faith as the means, and on the subjective genitive it does not. So the Pauline strand rests on two disputed readings of one verse, either of which costs it the conclusion.

theorem pistisChristou_jointly_load_bearing : ¬Establishes
    reformedWithoutPistisChristouSozoOrYoke
-- axioms: propext, Quot.sound

authorship_not_load_bearing

Authorship is not load-bearing. Grant every critical conclusion — that Ephesians and Titus are not by Paul, and 1 and 2 Peter not by Peter — and the conclusion still follows.

The case reads these letters as canonical scripture rather than as an apostle's testimony, so their authorship is no premise of it — which is why this is proved by weakening (entails_of_subset) from reformed_establishes: the premises added are ones no step reads. What that costs is stated in criticalAuthorship: the letters cannot then serve as evidence of what Paul meant, and the ἔργα νόμου premise rests on Romans instead.

theorem authorship_not_load_bearing : Establishes criticalAuthorship
-- axioms: propext, Quot.sound

apocalypticReading

The apocalyptic reading, as a valuation: πίστις Χριστοῦ is Christ's faithfulness, δικαιοσύνη θεοῦ is God's deliverance, and faith is not the condition of justification. Everything else it grants.

def apocalypticReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.pistisChristouObjective => False
    | Claim.justificationByFaithAlone => False
    | Claim.faithIsSufficient => False
    | Claim.salvationThroughFaith => False
    | x => True

apocalyptic_not_establishes

The apocalyptic reading does not establish sola fide. It does not reach the conclusion's third part, "through faith": nothing it holds says that faith suffices, and the faith alone from which Paul's strand derives it, it denies.

What it keeps is stated as its own result, apocalyptic_establishes_grace_not_works.

theorem apocalyptic_not_establishes : ¬Establishes apocalyptic
-- axioms: propext, Quot.sound

apocalyptic_establishes_grace_not_works

What the apocalyptic reading keeps: grace, and not by works. If δικαιοσύνη θεοῦ is God's act of deliverance, salvation is sheer gift, conditioned on nothing a person does. The reading establishes the first two parts of the conclusion by its own route, and denies the third.

So the dispute between the apocalyptic and Reformed readings is located exactly: it is over through faith, and not over grace or works.

theorem apocalyptic_establishes_grace_not_works : Establishes
    apocalypticOnGraceAndWorks
-- axioms: propext, Quot.sound

grace_and_works_rest_on_no_lexical_premise

Grace, and not by works, rest on no lexical premise. Remove every one — ἔργα νόμου and πίστις Χριστοῦ from Paul, σῴζω from Luke, the yoke from Acts — and the first two parts of the conclusion still follow, from the texts that say "not of works" in terms and the answer to James.

The lexical disputes decide through faith: whether the texts that exclude works also name faith as the means. They do not decide whether works are excluded.

theorem grace_and_works_rest_on_no_lexical_premise : Establishes
    graceAndWorksWithoutAnyLexicalPremise
-- axioms: propext, Quot.sound

forensic_justification_not_load_bearing

Forensic justification is not load-bearing. Grant the Finnish reading of Luther that justification is not a declaration only — Christ himself is present in faith — and sola fide still follows. Proved by weakening, like authorship_not_load_bearing: no step reads the forensic premise.

On what justification is, Mannermaa sides with Trent against the Reformed account, and on sola fide with the Reformed against Trent. This result and tridentine_not_establishes together show that denying the forensic account does not by itself deny sola fide. What Trent's denial rests on is narrower: that justification includes the sanctification that grows through works (trent_objection_rests_on_its_definition).

theorem forensic_justification_not_load_bearing : Establishes finnish
-- axioms: propext, Quot.sound

critics_carry_the_pauline_strand

The critics carry the Pauline strand. Deny covenantal nomism with Gathercole, keep the reading of Galatians as a polemic, leave Luke and Acts out, and sola fide follows from Paul alone — with the ἔργα νόμου premise derived rather than assumed.

theorem critics_carry_the_pauline_strand : Establishes
    paulineStrandOnTheCritics
-- axioms: propext, Quot.sound

sandersReading

Sanders' world, with only Paul to go on: covenantal nomism, so the ἔργα νόμου premise fails and Paul does not reach faith alone.

def sandersReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.worksOfLawMeansWorksGenerally => False
    | Claim.sozoIsSoteriological => False
    | Claim.acts15YokeIsLawAsCondition => False
    | Claim.justificationByFaithAlone => False
    | Claim.faithIsSufficient => False
    | Claim.salvationThroughFaith => False
    | x => True

sanders_costs_the_pauline_strand

And Sanders costs it. Grant covenantal nomism, and with Dunn's inference the ἔργα νόμου premise is denied; leave Luke and Acts out, and sola fide does not follow from Paul.

Between them, this and critics_carry_the_pauline_strand locate the ἔργα νόμου dispute where the literature has it: in a historical question about Second Temple Judaism, before any question about Paul's Greek.

theorem sanders_costs_the_pauline_strand : ¬Establishes paulineStrandOnSanders
-- axioms: propext, Quot.sound

jamesUnharmonisedReading

A reading on which James 2:24 stands unharmonised against Paul.

def jamesUnharmonisedReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.james2_24Compatible => False
    | Claim.salvationNotByWorks => False
    | x => True

james_harmonisation_is_load_bearing

The argument genuinely depends on answering James. Remove the two premises that harmonise James 2:24 with Paul and sola fide no longer follows, however much of the rest is retained.

An argument for sola fide that does not engage James 2:24 is not merely impolite; it is invalid.

theorem james_harmonisation_is_load_bearing : ¬Establishes
    reformedWithoutJamesHarmonisation
-- axioms: propext, Quot.sound

grace_needs_no_answer_to_james

But grace does not need it. Remove the answer to James and salvation by grace still follows, from Ephesians 2:8, Romans 4:4–5 and Titus 3:5 alone. James 2:24 is load-bearing for not by works, the part it appears to contradict, and for nothing else — which the single closing step this argument once had could not show.

theorem grace_needs_no_answer_to_james : Establishes
    graceWithoutJamesHarmonisation
-- axioms: propext, Quot.sound

Satisfiability

Entails is vacuously true over a premise set with no model, so a package built from contradictory premises would establish its conclusion and every gate would pass. Only packages carrying a positive Establishes result need checking: one with a ¬ Establishes result is satisfiable already, because its countermodel satisfies every premise.

Not tagged @[headline] — these are claims about the health of the encoding rather than about justification.

everythingHoldsReading

The reading on which every claim in this argument holds at once: the witness that the packages built from positive grounds are coherent.

def everythingHoldsReading : Valuation Claim :=
  fun x => True

reformed_is_satisfiable

The Reformed package has a model, so reformed_establishes is not vacuous.

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

newPerspectiveOwnReading

The New Perspective's own world: Paul's ἔργα νόμου denotes the covenant boundary markers rather than works in general, and justification is by faith regardless. The all-holds reading cannot serve here — this package denies a premise, which is the whole point of it. Faith the only means and justification forensic only, it denies Trent's baptism as the instrument and justification as including sanctification.

def newPerspectiveOwnReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | Claim.rev22_11BeJustifiedStill => False
    | Claim.sir18_22BeJustifiedToDeath => False
    | Claim.jamesUsesDikaioAsPaul => False
    | Claim.worksOfLawMeansWorksGenerally => False
    | Claim.baptismIsInstrumentalCause => False
    | Claim.justificationIncludesSanctification => False
    | x => True

newPerspective_is_satisfiable

The New Perspective package has a model.

theorem newPerspective_is_satisfiable : Satisfiable newPerspective.premises
-- axioms: propext, Quot.sound

subjectiveGenitiveReading

Hays's own world: πίστις Χριστοῦ is Christ's faithfulness, and everything else in the Reformed case holds.

def subjectiveGenitiveReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.pistisChristouObjective => False
    | x => True

subjectiveGenitive_is_satisfiable

The subjective-genitive package has a model, so pistisChristou_not_load_bearing is not vacuous.

theorem subjectiveGenitive_is_satisfiable : Satisfiable
    subjectiveGenitive.premises
-- axioms: propext, Quot.sound

lawObservantLukeReading

Jervell's world: the yoke is Israel's law for gentiles, and everything else in the Reformed case holds.

def lawObservantLukeReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.acts15YokeIsLawAsCondition => False
    | x => True

lawObservantLuke_is_satisfiable

The law-observant package has a model, so acts15Yoke_not_load_bearing is not vacuous.

theorem lawObservantLuke_is_satisfiable : Satisfiable
    lawObservantLuke.premises
-- axioms: propext, Quot.sound

criticalAuthorshipReading

The critics' world: none of the four disputed letters is by the apostle whose name it bears, and everything else holds.

def criticalAuthorshipReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.ephesiansIsPauline => False
    | Claim.titusIsPauline => False
    | Claim.firstPeterIsPetrine => False
    | Claim.secondPeterIsPetrine => False
    | x => True

criticalAuthorship_is_satisfiable

The critical-authorship package has a model, so authorship_not_load_bearing is not vacuous.

theorem criticalAuthorship_is_satisfiable : Satisfiable
    criticalAuthorship.premises
-- axioms: propext, Quot.sound

reformedWithoutWorksOfLaw_is_satisfiable

The Reformed package minus the ἔργα νόμου premise has a model, so worksOfLaw_not_load_bearing is not vacuous. A load-bearing result that held only because its premises could not all be true would be exactly backwards.

theorem reformedWithoutWorksOfLaw_is_satisfiable : Satisfiable
    reformedWithoutWorksOfLaw.premises
-- axioms: propext, Quot.sound

reformedWithoutSozo_is_satisfiable

And the same minus the dominical lexical premise.

theorem reformedWithoutSozo_is_satisfiable : Satisfiable
    reformedWithoutSozo.premises
-- axioms: propext, Quot.sound

reformedWithoutWorksOfLawOrSozo_is_satisfiable

And the same minus both, so apostolic_strand_survives_paul_and_luke is not vacuous.

theorem reformedWithoutWorksOfLawOrSozo_is_satisfiable : Satisfiable
    reformedWithoutWorksOfLawOrSozo.premises
-- axioms: propext, Quot.sound

apocalypticOnGraceAndWorks_is_satisfiable

The apocalyptic package, asked about grace and works, has a model.

theorem apocalypticOnGraceAndWorks_is_satisfiable : Satisfiable
    apocalypticOnGraceAndWorks.premises
-- axioms: propext, Quot.sound

graceAndWorksWithoutAnyLexicalPremise_is_satisfiable

With every lexical premise removed, the package still has a model.

theorem graceAndWorksWithoutAnyLexicalPremise_is_satisfiable : Satisfiable
    graceAndWorksWithoutAnyLexicalPremise.premises
-- axioms: propext, Quot.sound

finnishReading

Mannermaa's world: justification is not forensic only, and everything else holds.

def finnishReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.justificationIsForensicOnly => False
    | x => True

finnish_is_satisfiable

The Finnish package has a model, so forensic_justification_not_load_bearing is not vacuous.

theorem finnish_is_satisfiable : Satisfiable finnish.premises
-- axioms: propext, Quot.sound

criticsReading

Gathercole's world: Second Temple Judaism was not uniformly covenantal nomism, and everything else holds. Faith the only means and justification forensic only, it denies Trent's baptism as the instrument and justification as including sanctification.

def criticsReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | Claim.rev22_11BeJustifiedStill => False
    | Claim.sir18_22BeJustifiedToDeath => False
    | Claim.jamesUsesDikaioAsPaul => False
    | Claim.secondTempleCovenantalNomism => False
    | Claim.baptismIsInstrumentalCause => False
    | Claim.justificationIncludesSanctification => False
    | x => True

paulineStrandOnTheCritics_is_satisfiable

The critics' Pauline package has a model, so critics_carry_the_pauline_strand is not vacuous.

theorem paulineStrandOnTheCritics_is_satisfiable : Satisfiable
    paulineStrandOnTheCritics.premises
-- axioms: propext, Quot.sound

graceWithoutJamesHarmonisation_is_satisfiable

With the answer to James removed, the package asked about grace still has a model, so grace_needs_no_answer_to_james is not vacuous.

theorem graceWithoutJamesHarmonisation_is_satisfiable : Satisfiable
    graceWithoutJamesHarmonisation.premises
-- axioms: propext, Quot.sound

TestimonyArguments.SolaFide.Gospel — where Trent parts from Paul

Paul's direct answer to anything added to the gospel is Galatians: another gospel, whoever preaches it accursed (1:6–9); if righteousness came by the law, Christ died for nothing (2:21); whoever would be justified by the law is severed from Christ (5:2–4). The gospel itself is that Christ died for our sins (1 Corinthians 15:3).

Set against Trent's definition of justification — "not remission of sins merely, but also the sanctification and renewal of the inward man" (Session VI, ch. 7) — the question is exactly where the two part. This module answers it in three steps, each checked.

What Trent grants. Every text of the line. And the forensic sense of Paul's verb: the Joint Declaration (1999), signed by the Catholic Church, confesses that God "no longer imputes to them their sin" (§22), and modern Greek scholarship across traditions reads δικαιόω as a verdict — the standard lexicon, Morris, Moo, Irons, Wright, and the Catholic exegete Fitzmyer (dikaioIsForensic, rated wellSupported).

What Trent denies. One step: that a verdict on the ground of a finished work excludes the renewal wrought in us. The same paragraph of the Joint Declaration holds forgiveness and the love the Spirit effects "not to be separated", and Gorman reads the verdict as an effective word that transforms.

Where they part. whereTrentPartsFromPaul finds it mechanically: the crux is that step, and what it breaks in Trent is its definition, and nothing else.

What this does not show is that the step is true. It shows that it is the whole of the disagreement: grant it, and Trent's definition cannot stand; deny it, and Paul's gospel as encoded here does not reach Trent's definition at all.

The gospel line holds

galatianGospelReading

The world of Paul's gospel as this line reads it: every text true, Christ's work the whole ground, the verdict forensic — and justification not the renewal of the inward man.

def galatianGospelReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.justificationIncludesSanctification => False
    | x => True

galatianGospel_establishes

Paul's gospel denies Trent's definition. From Galatians 1:6–9, 2:21, 5:2–4 and 1 Corinthians 15:3, read as one claim, with the forensic sense of δικαιόω: justification is not the renewal of the inward man.

theorem galatianGospel_establishes : Establishes galatianGospel
-- axioms: propext, Quot.sound

galatianGospel_is_satisfiable

The gospel line's premises have a model.

theorem galatianGospel_is_satisfiable : Satisfiable galatianGospel.premises
-- axioms: propext, Quot.sound

What Trent grants

jointDeclarationReading

Trent's world, with the Joint Declaration's confession added: God no longer imputes sin — the verb is forensic — and every text of the gospel line holds. Justification still includes renewal, faith without charity does not suffice, and justification is not by faith alone. Having granted that the verb is forensic, it does not also hold that Paul's verb denotes renewal: the meanings exclude the two (TestimonyArguments.Meanings.SolaFide.joins). Of the other pairs the meanings exclude, it holds the Greek of Revelation 22:11 and Sirach 18:22, and that James's δικαιόω is Paul's.

def jointDeclarationReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | Claim.rev22_11BeJustifiedStill => False
    | Claim.sir18_22BeJustifiedToDeath => False
    | Claim.james2_24Compatible => False
    | Claim.salvationNotByWorks => False
    | Claim.justificationIsForensicOnly => False
    | Claim.justificationDistinctFromSanctification => False
    | Claim.faithIsSufficient => False
    | Claim.justificationByFaithAlone => False
    | x => True

trent_grants_the_gospel_texts

Trent can grant every text of the gospel line. Nothing Trent holds denies that Christ died for our sins, that righteousness by the law would make his death needless, or that another gospel is accursed.

theorem trent_grants_the_gospel_texts : Grants tridentineCase (⋀[p
    Claim.galatians1_6_9, p Claim.firstCorinthians15_3, p Claim.galatians2_21,
    p Claim.galatians5_2_4, p Claim.romans8_33_34])
-- axioms: propext, Quot.sound

trent_grants_the_forensic_sense

Trent can grant that Paul's verb is forensic, as the Joint Declaration does: God no longer imputes sin. The lexical question is not where they part.

theorem trent_grants_the_forensic_sense : Grants tridentineCase (p
    Claim.dikaioIsForensic)
-- axioms: propext, Quot.sound

Where Trent parts from Paul

whereTrentPartsFromPaul

Where Trent parts from Paul. The crux is one step: if justification is God's verdict on the ground of Christ's finished work, the renewal of the inward man is no part of it (verdictExcludesRenewal; Westminster XI.1). What it breaks in Trent is its definition — justification "not remission of sins merely, but also the sanctification and renewal of the inward man" (Session VI, ch. 7) — and nothing else in Trent's case: not its account of merit, not its reading of works.

The break needs the gospel line's grounds as well, and says so: the four texts, Paul's reading of them, Romans 8:33–34 and the forensic sense of the verb. Trent can grant every one of those (trent_grants_the_gospel_texts, trent_grants_the_forensic_sense); it is the step that it denies, with the Joint Declaration: forgiveness and renewal are "not to be separated".

Why Paul's gospel (Galatians 1), against justification as renewal stands against Trent, against 'not by works'.

• The crux: \((P_{56} \land P_{47} \land P_{46}) \rightarrow \lnot P_{33}\), a premise of Paul's gospel (Galatians 1), against justification as renewal.
• What it does: its conclusion does not follow without it.
• Granted: \(P_{42}\), \(P_{43}\), \(P_{44}\), \(P_{45}\), \((P_{42} \land P_{43} \land P_{44} \land P_{45}) \rightarrow P_{56}\), \(P_{46}\), \(P_{47}\), which the break also needs.
• Where the rival breaks: \(P_{33}\) cannot be held together with \((P_{56} \land P_{47} \land P_{46}) \rightarrow \lnot P_{33}\) and \(P_{42}\), \(P_{43}\), \(P_{44}\), \(P_{45}\), \((P_{42} \land P_{43} \land P_{44} \land P_{45}) \rightarrow P_{56}\), \(P_{46}\), \(P_{47}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{42}\) Galatians 1:6–9: whoever preaches a gospel contrary to the one received is accursed — consensus: Gal 1:6-9; moo-galatians-2013, ad loc. Gal 1:6
  • \(P_{43}\) 1 Corinthians 15:3: the gospel of first importance — Christ died for our sins — consensus: 1 Cor 15:3
  • \(P_{44}\) Galatians 2:21: if righteousness were through the law, Christ died for no purpose — consensus: Gal 2:21; moo-galatians-2013, ad loc. Gal 2:21
  • \(P_{45}\) Galatians 5:2–4: you who would be justified by the law are severed from Christ — consensus: Gal 5:2-4; moo-galatians-2013, ad loc. Gal 5:2
  • \(P_{56}\) Christ's death for our sins is the whole ground of justification; to add to it is another gospel — disputed: westminster-confession-1647, §XI.1; Gal 2:21; moo-galatians-2013, ad loc. Gal 2:21; roberts-ante-nicene-fathers-1-1885, §Epistle to Diognetus 9
  • \(P_{46}\) Romans 8:33–34: it is God who justifies — who is to condemn? — consensus: Rom 8:33-34
  • \(P_{47}\) In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — well supported: bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • the step itself — disputed: moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1; disputed: westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965

TestimonyArguments.SolaFide.Definition — what Trent's definition claims

Trent defines justification as "not remission of sins merely, but also the sanctification and renewal of the inward man" (Session VI, ch. 7). The Reformed deny it, and whereTrentPartsFromPaul locates the denial at one step. But the definition can be read two ways, and the two readings meet different objections.

Read as a claim about Paul's word, it says that δικαιόω, in Paul, denotes the renewal of the inward man. Trent invites the reading: chapter 8 sets out how "the Apostle's" words — justified "by faith and freely" — are to be understood, and chapter 7 says that the justified "are not only reputed, but are truly called, and are, just". Read so, the definition is a lexical claim, and it meets a lexical answer: δικαιόω is forensic, Paul names renewal with words of its own and sets them beside it (Titus 3:5–7; 1 Corinthians 6:11), and a word contributes the least meaning its context requires (Joos; Silva). To read renewal into the verdict from the doctrine is what Barr called illegitimate totality transfer. Every link of that answer is rated above disputed.

Why Trent would read it so is not left to the magisterium. The council read Paul in the Latin it had declared "authentic" (Session IV), and in Latin iustificare had meant "to make righteous" since Augustine: "what else does the phrase 'being justified' signify than being made righteous" (On the Spirit and the Letter 26.45). McGrath traces that inheritance through the medieval West. So this reading rests on a ground of its own — that Augustine glossed the word so, rated consensus, because he did — and a step from the Latin gloss to the Greek word. That step is where the reading breaks: a gloss in one language does not fix what a word denotes in another, and the lexical case says what δικαιόω denotes in Paul (whereTheLatinReadingFalls).

Read as a claim about what God does, it says that when God justifies he also renews — pardon and renewal given together, "not to be separated", as the Joint Declaration (§22) confesses. Read so, no lexical argument reaches it: it can be held with every word the lexical case says about δικαιόω, and Calvin himself grants that justification and sanctification are inseparable. What still divides Trent from Paul, on this reading, is the step whereTrentPartsFromPaul names — that a verdict on a finished work excludes renewal from justification — and that step is disputed.

Romans 4 is a second route to the same place, and it does not lift the rating. God "justifies the ungodly" (4:5), and the blessing of righteousness counted apart from works is sin not counted (4:6–8): read with the forensic verb, what is counted to the ungodly is not a righteousness wrought in them. Trent can grant every word (trent_grants_romans_four), and Augustine reads the same verse the other way — God justifies the ungodly "that he may become a godly one". So the step is disputed, as the step from Galatians is. What Romans 4 adds is not strength but a second route: on this reading, Paul meets Trent from Galatians and from Romans 4, and each must be answered on its own (whereRomansFourMeetsWhatGodDoes). The two routes are not wholly independent: both rest on the forensic sense of the verb, so a reader who denies that sense denies both.

whatTrentsDefinitionClaims is the dilemma, checked: each reading is fair — Trent read that way still has a model — and each is answered. The first cannot be held with Paul's word, three times over and each time at a step rated wellSupported: against the lexical case, as Trent states it and as it rests on the Latin gloss, and against Romans 4 read for the word. The second is untouched by anything about the word, and conflicts with Paul's gospel and with Romans 4, each time at a step rated disputed — so whoever grants that step rejects this reading, and whoever denies it need not. Which reading Trent means is not something the dilemma decides. What it shows is what each reading costs.

paulNamesRenewalOtherwise is grounded in scripture alone — what the texts say, and no more — and the manifest lists it so.

The lexical case holds

lexicalReading

The world of the lexical case: every word as it reads it, and δικαιόω denoting the verdict and not renewal.

def lexicalReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | x => True

lexicalCase_establishes

Paul's δικαιόω does not denote the renewal of the inward man, from the forensic sense, Paul's own words for renewal, and the rule of least meaning.

theorem lexicalCase_establishes : Establishes lexicalCase
-- axioms: propext, Quot.sound

lexicalCase_is_satisfiable

The lexical case's premises have a model.

theorem lexicalCase_is_satisfiable : Satisfiable lexicalCase.premises
-- axioms: propext, Quot.sound

Two readings of Trent's definition

trentReadsPaulsWord

Reading Trent's definition as a claim about Paul's word, and reading Paul's word as the Latin West did. Trent's chapter 8 sets out how "the Apostle's" words are to be understood, and chapter 7 says the justified are "not only reputed, but are truly called, and are, just". The council read Paul in the Latin it had declared "authentic" (Session IV), where iustificare had meant "to make righteous" since Augustine; McGrath traces that inheritance. Rated disputed: whether the council defines the word or the reality is itself argued, and the step from the Latin gloss to the Greek word is what the lexical case denies.

def trentReadsPaulsWord : Source :=
  {
    primary :=
      Reference.work tannerDecrees
        (Bib.Locus.sectionRef
          "Trent, Session VI (1547), Decree on Justification, ch. 8"),
    supporting :=
      [Reference.work tannerDecrees
          (Bib.Locus.sectionRef
            "Trent, Session VI (1547), Decree on Justification, ch. 7"),
        Reference.work npnfAugustineAntiPelagian
          (Bib.Locus.sectionRef "On the Spirit and the Letter, ch. 45 (26.45)"),
        Reference.work mcgrathIustitiaDei],
    tradition := Tradition.romanCatholic, confidence := Confidence.disputed }

trentReadsGrace

Reading Trent's definition as a claim about what God does in justifying: in the Joint Declaration, forgiveness and the renewal the Spirit effects are two aspects of God's gracious action, "not to be separated" (§22). Rated disputed, for the same reason as the other reading.

def trentReadsGrace : Source :=
  {
    primary :=
      Reference.work jointDeclarationJustification (Bib.Locus.sectionRef "§22"),
    supporting :=
      [Reference.work tannerDecrees
          (Bib.Locus.sectionRef
            "Trent, Session VI (1547), Decree on Justification, ch. 7")],
    tradition := Tradition.romanCatholic, confidence := Confidence.disputed }

trentOnPaulsWord

Trent's definition, read as a claim about what Paul's word means — and resting that reading, as the Latin West did, on Augustine's gloss: "being justified" is "being made righteous".

def trentOnPaulsWord : Reading Claim :=
  { name := "as what Paul's word means",
    commits := p Claim.paulsJustifyDenotesRenewal,
    grounds :=
      [p Claim.augustineReadsJustifyAsMakeRighteous,
        p Claim.augustineReadsJustifyAsMakeRighteous 🡒
          p Claim.paulsJustifyDenotesRenewal],
    source := trentReadsPaulsWord }

trentOnWhatGodDoes

Trent's definition, read as a claim about what God does in justifying.

def trentOnWhatGodDoes : Reading Claim :=
  { name := "as what God does in justifying",
    commits := p Claim.justifyingGraceRenews,
    source := trentReadsGrace }

tridentineOnPaulsWord — Trent, against 'not by works', read as what Paul's word means

Trent, with its definition read as a claim about Paul's word.

No premise here rests on scripture alone.

tridentineOnWhatGodDoes — Trent, against 'not by works', read as what God does in justifying

Trent, with its definition read as a claim about what God does.

No premise here rests on scripture alone.

tridentineOnPaulsWord_establishes

Trent, read as a claim about Paul's word, still concludes what Trent concludes: a reading only adds premises.

theorem tridentineOnPaulsWord_establishes : Establishes tridentineOnPaulsWord
-- axioms: propext, Quot.sound

trentOnPaulsWordReading

Trent's world, reading Paul's word as it does: δικαιόω denotes making just, and not a verdict only; justification includes renewal, faith without charity does not suffice, and justification is not by faith alone.

def trentOnPaulsWordReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.salvationNotByWorks => False
    | Claim.justificationIsForensicOnly => False
    | Claim.justificationDistinctFromSanctification => False
    | Claim.faithIsSufficient => False
    | Claim.justificationByFaithAlone => False
    | Claim.dikaioIsForensic => False
    | x => True

tridentineOnPaulsWord_is_satisfiable

Trent, read as a claim about Paul's word, holds together. The horn is fair: it does not fall to itself.

theorem tridentineOnPaulsWord_is_satisfiable : Satisfiable
    tridentineOnPaulsWord.premises
-- axioms: propext, Quot.sound

trentGrantsTheWordReading

Trent read as a claim about what God does, with every word of the lexical case granted: δικαιόω forensic, Paul's own words for renewal, the rule of least meaning, and δικαιόω not denoting renewal. God, in justifying, also renews.

def trentGrantsTheWordReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.salvationNotByWorks => False
    | Claim.justificationIsForensicOnly => False
    | Claim.justificationDistinctFromSanctification => False
    | Claim.faithIsSufficient => False
    | Claim.justificationByFaithAlone => False
    | Claim.paulsJustifyDenotesRenewal => False
    | x => True

tridentineOnWhatGodDoes_is_satisfiable

Trent, read as a claim about what God does, holds together.

theorem tridentineOnWhatGodDoes_is_satisfiable : Satisfiable
    tridentineOnWhatGodDoes.premises
-- axioms: propext, Quot.sound

lexical_case_does_not_reach_what_god_does

The lexical case does not reach the second reading. Trent, read as a claim about what God does, can be held with every premise of the lexical case: the rule of least meaning governs what Paul's word says, and this reading says nothing about the word.

theorem lexical_case_does_not_reach_what_god_does : Satisfiable
    (lexicalCase.premises ++ tridentineOnWhatGodDoes.premises)
-- axioms: propext, Quot.sound

Where each reading falls

whereTrentsWordReadingFalls

Why Paul's word stands against Trent, read as a claim about it. The crux is the lexical step: with the forensic sense, Paul's own words for renewal and the rule of least meaning, δικαιόω does not denote renewal. What it breaks is Trent's definition together with the reading — nothing else in Trent — and every link of the break is rated above disputed.

Why Paul's word (δικαιόω, by the rule of least meaning) stands against Trent, against 'not by works', read as what Paul's word means.

• The crux: \((P_{47} \land P_{48} \land P_{49}) \rightarrow \lnot P_{50}\), a premise of Paul's word (δικαιόω, by the rule of least meaning).
• What it does: its conclusion does not follow without it.
• Granted: \(P_{47}\), \(P_{48}\), \(P_{49}\), which the break also needs.
• Where the rival breaks: \(P_{33}\), \(P_{33} \rightarrow P_{50}\) cannot be held together with \((P_{47} \land P_{48} \land P_{49}) \rightarrow \lnot P_{50}\) and \(P_{47}\), \(P_{48}\), \(P_{49}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{47}\) In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — well supported: bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • \(P_{48}\) Paul names renewal with other words (ἀνακαίνωσις, ἁγιασμός) and sets them beside δικαιόω — consensus: Titus 3:5-7; Rom 12:2; Rom 6:19-22; 1 Cor 6:11
  • \(P_{49}\) A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — well supported: silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • the step itself — well supported: silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

whereTheLatinReadingFalls

Why Paul's word stands against the Latin reading of it. The same crux, and a second break in the same horn: Trent rests its reading of Paul's word on Augustine's gloss, and the step from that gloss to what the Greek word means is what breaks. That Augustine glossed it so is not in question — it is rated consensus — but a Latin gloss does not fix what δικαιόω denotes in Paul, and the forensic sense, Paul's own words for renewal and the rule of least meaning say it does not.

Why Paul's word (δικαιόω, by the rule of least meaning) stands against Trent, against 'not by works', read as what Paul's word means.

• The crux: \((P_{47} \land P_{48} \land P_{49}) \rightarrow \lnot P_{50}\), a premise of Paul's word (δικαιόω, by the rule of least meaning).
• What it does: its conclusion does not follow without it.
• Granted: \(P_{47}\), \(P_{48}\), \(P_{49}\), which the break also needs.
• Where the rival breaks: \(P_{52}\), \(P_{52} \rightarrow P_{50}\) cannot be held together with \((P_{47} \land P_{48} \land P_{49}) \rightarrow \lnot P_{50}\) and \(P_{47}\), \(P_{48}\), \(P_{49}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{47}\) In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — well supported: bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • \(P_{48}\) Paul names renewal with other words (ἀνακαίνωσις, ἁγιασμός) and sets them beside δικαιόω — consensus: Titus 3:5-7; Rom 12:2; Rom 6:19-22; 1 Cor 6:11
  • \(P_{49}\) A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — well supported: silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • the step itself — well supported: silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

whereTrentsGraceReadingFalls

Why Paul's gospel stands against Trent, read as a claim about what God does. The same crux as whereTrentPartsFromPaul, and the same break: the step from a verdict on a finished work to "renewal is no part of justification", against Trent's definition. On this reading that step is all that divides them, and it is rated disputed.

Why Paul's gospel (Galatians 1), against justification as renewal stands against Trent, against 'not by works', read as what God does in justifying.

• The crux: \((P_{56} \land P_{47} \land P_{46}) \rightarrow \lnot P_{33}\), a premise of Paul's gospel (Galatians 1), against justification as renewal.
• What it does: its conclusion does not follow without it.
• Granted: \(P_{42}\), \(P_{43}\), \(P_{44}\), \(P_{45}\), \((P_{42} \land P_{43} \land P_{44} \land P_{45}) \rightarrow P_{56}\), \(P_{46}\), \(P_{47}\), which the break also needs.
• Where the rival breaks: \(P_{33}\) cannot be held together with \((P_{56} \land P_{47} \land P_{46}) \rightarrow \lnot P_{33}\) and \(P_{42}\), \(P_{43}\), \(P_{44}\), \(P_{45}\), \((P_{42} \land P_{43} \land P_{44} \land P_{45}) \rightarrow P_{56}\), \(P_{46}\), \(P_{47}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{42}\) Galatians 1:6–9: whoever preaches a gospel contrary to the one received is accursed — consensus: Gal 1:6-9; moo-galatians-2013, ad loc. Gal 1:6
  • \(P_{43}\) 1 Corinthians 15:3: the gospel of first importance — Christ died for our sins — consensus: 1 Cor 15:3
  • \(P_{44}\) Galatians 2:21: if righteousness were through the law, Christ died for no purpose — consensus: Gal 2:21; moo-galatians-2013, ad loc. Gal 2:21
  • \(P_{45}\) Galatians 5:2–4: you who would be justified by the law are severed from Christ — consensus: Gal 5:2-4; moo-galatians-2013, ad loc. Gal 5:2
  • \(P_{56}\) Christ's death for our sins is the whole ground of justification; to add to it is another gospel — disputed: westminster-confession-1647, §XI.1; Gal 2:21; moo-galatians-2013, ad loc. Gal 2:21; roberts-ante-nicene-fathers-1-1885, §Epistle to Diognetus 9
  • \(P_{46}\) Romans 8:33–34: it is God who justifies — who is to condemn? — consensus: Rom 8:33-34
  • \(P_{47}\) In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — well supported: bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • the step itself — disputed: moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1; disputed: westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965

Romans 4

romansFourCase_establishes

Romans 4 denies Trent's definition: Paul glosses the righteousness God counts to the ungodly as sin not counted, and with the forensic sense of the verb, renewal is no part of justification.

theorem romansFourCase_establishes : Establishes romansFourCase
-- axioms: propext, Quot.sound

romansFourCase_is_satisfiable

Romans 4's case has a model: Paul's gospel's world.

theorem romansFourCase_is_satisfiable : Satisfiable romansFourCase.premises
-- axioms: propext, Quot.sound

romansFourOnTheWord_establishes

Romans 4, read by the rule of least meaning, says what Paul's word means: the verb Paul glosses as sin not counted does not also denote the renewal of the inward man.

theorem romansFourOnTheWord_establishes : Establishes romansFourOnTheWord
-- axioms: propext, Quot.sound

romansFourOnTheWord_is_satisfiable

The exegetical route to Paul's word has a model: the lexical case's world.

theorem romansFourOnTheWord_is_satisfiable : Satisfiable
    romansFourOnTheWord.premises
-- axioms: propext, Quot.sound

trent_grants_romans_four

Trent can grant every word of Romans 4:5–8, as Augustine does: God justifies the ungodly, and the blessing is sin not counted. The texts are common ground; the reading is not.

theorem trent_grants_romans_four : Grants tridentineCase (⋀[p
    Claim.romans4_4_5, p Claim.romans4_6_8])
-- axioms: propext, Quot.sound

romans_four_on_the_word_does_not_reach_what_god_does

Romans 4, read for Paul's word, does not reach the second reading either. Trent, read as a claim about what God does, can be held with every premise of it: the exegesis says what the counting is, and this reading says nothing about the word.

theorem romans_four_on_the_word_does_not_reach_what_god_does : Satisfiable
    (romansFourOnTheWord.premises ++ tridentineOnWhatGodDoes.premises)
-- axioms: propext, Quot.sound

whereRomansFourMeetsTheWordReading

Why Romans 4 stands against Trent, read as a claim about Paul's word. The crux is the step from Paul's gloss — the righteousness counted to the ungodly is sin not counted — by the rule of least meaning, to "the verb does not also denote renewal". What it breaks is Trent's definition with the reading, and every link of the break is rated wellSupported or better: an exegetical route to where the lexical case arrives lexically.

Why Romans 4:3–8, on Paul's word (by the rule of least meaning) stands against Trent, against 'not by works', read as what Paul's word means.

• The crux: \((P_{55} \land P_{49}) \rightarrow \lnot P_{50}\), a premise of Romans 4:3–8, on Paul's word (by the rule of least meaning).
• What it does: its conclusion does not follow without it.
• Granted: \(P_{4}\), \(P_{53}\), \(P_{54}\), \(P_{49}\), \((P_{4} \land P_{53} \land P_{54}) \rightarrow P_{55}\), which the break also needs.
• Where the rival breaks: \(P_{33}\), \(P_{33} \rightarrow P_{50}\) cannot be held together with \((P_{55} \land P_{49}) \rightarrow \lnot P_{50}\) and \(P_{4}\), \(P_{53}\), \(P_{54}\), \(P_{49}\), \((P_{4} \land P_{53} \land P_{54}) \rightarrow P_{55}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{4}\) Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — well supported: Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • \(P_{53}\) Romans 4:6–8: righteousness counted apart from works — sins forgiven, sin not counted — consensus: Rom 4:6-8; moo-romans-1996, ad loc. Rom 4:6
  • \(P_{54}\) λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — well supported: bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • \(P_{49}\) A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — well supported: silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • \(P_{55}\) In Romans 4:6–8 Paul glosses righteousness counted apart from works as sin not counted — well supported: moo-romans-1996, ad loc. Rom 4:6; Rom 4:6-8
  • the step itself — well supported: moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι; well supported: silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

whereRomansFourMeetsWhatGodDoes

Why Romans 4 stands against Trent, read as a claim about what God does. The crux is the step from Paul's gloss, with the forensic sense of the verb, to "renewal is no part of justification". It breaks Trent's definition and nothing else. It is rated disputed, as the step from Galatians is — Augustine grants the same verses and reads them the other way, God justifying the ungodly "that he may become a godly one" — so on this reading of Trent, Paul meets it by two routes, from Galatians and from Romans 4, each at a disputed step. The routes share one ground, the forensic sense of the verb.

Why Romans 4:3–8, against justification as renewal stands against Trent, against 'not by works', read as what God does in justifying.

• The crux: \((P_{55} \land P_{47}) \rightarrow \lnot P_{33}\), a premise of Romans 4:3–8, against justification as renewal.
• What it does: its conclusion does not follow without it.
• Granted: \(P_{4}\), \(P_{53}\), \(P_{54}\), \(P_{47}\), \((P_{4} \land P_{53} \land P_{54}) \rightarrow P_{55}\), which the break also needs.
• Where the rival breaks: \(P_{33}\) cannot be held together with \((P_{55} \land P_{47}) \rightarrow \lnot P_{33}\) and \(P_{4}\), \(P_{53}\), \(P_{54}\), \(P_{47}\), \((P_{4} \land P_{53} \land P_{54}) \rightarrow P_{55}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{4}\) Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — well supported: Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • \(P_{53}\) Romans 4:6–8: righteousness counted apart from works — sins forgiven, sin not counted — consensus: Rom 4:6-8; moo-romans-1996, ad loc. Rom 4:6
  • \(P_{54}\) λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — well supported: bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • \(P_{47}\) In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — well supported: bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • \(P_{55}\) In Romans 4:6–8 Paul glosses righteousness counted apart from works as sin not counted — well supported: moo-romans-1996, ad loc. Rom 4:6; Rom 4:6-8
  • the step itself — well supported: moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι; disputed: moo-romans-1996, ad loc. Rom 4:5; westminster-confession-1647, §XI.1

The dilemma

whatTrentsDefinitionClaims

What Trent's definition claims, read both ways. The claim is Trent's definition — justification is the sanctification and renewal of the inward man.

Read as a claim about what Paul's word means (δικαιόω denotes that renewal), it cannot be held with Paul's word, three times over, each at a step rated wellSupported: the lexical case against the definition as Trent states it; the lexical case against the Latin gloss the reading rests on ("being justified" as "being made righteous"); and Romans 4 read for the word.

Read as a claim about what God does in justifying (he also renews), nothing about the word reaches it: neither the lexical case nor Romans 4 read for the word. It conflicts with Paul twice, each time at a step rated disputed: with his gospel in Galatians, at the step whereTrentPartsFromPaul names, and with Romans 4, at his reading of the ungodly justified. A reader who grants those steps rejects this reading; one who denies them, as Augustine and the Joint Declaration do, need not.

Each reading is fair: Trent read either way still has a model.

Every reading of \(P_{33}\), answered. Trent, against 'not by works' holds \(P_{33}\). It is read 2 ways here, and each reading is checked; none can be left out.

1. Read as what Paul's word means. The claim commits Trent, against 'not by works' to \(P_{50}\) — so read by tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 8; tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; npnf1-05-1887, §On the Spirit and the Letter, ch. 45 (26.45); mcgrath-iustitia-dei-2005 (disputed). It rests the reading on \(P_{52}\), \(P_{52} \rightarrow P_{50}\).

Against Paul's word (δικαιόω, by the rule of least meaning), it cannot be held. Where it breaks:

Why Paul's word (δικαιόω, by the rule of least meaning) stands against Trent, against 'not by works', read as what Paul's word means.

• The crux: \((P_{47} \land P_{48} \land P_{49}) \rightarrow \lnot P_{50}\), a premise of Paul's word (δικαιόω, by the rule of least meaning).
• What it does: its conclusion does not follow without it.
• Granted: \(P_{47}\), \(P_{48}\), \(P_{49}\), which the break also needs.
• Where the rival breaks: \(P_{33}\), \(P_{33} \rightarrow P_{50}\) cannot be held together with \((P_{47} \land P_{48} \land P_{49}) \rightarrow \lnot P_{50}\) and \(P_{47}\), \(P_{48}\), \(P_{49}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{47}\) In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — well supported: bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • \(P_{48}\) Paul names renewal with other words (ἀνακαίνωσις, ἁγιασμός) and sets them beside δικαιόω — consensus: Titus 3:5-7; Rom 12:2; Rom 6:19-22; 1 Cor 6:11
  • \(P_{49}\) A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — well supported: silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • the step itself — well supported: silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

Against Paul's word (δικαιόω, by the rule of least meaning), it cannot be held. Where it breaks:

Why Paul's word (δικαιόω, by the rule of least meaning) stands against Trent, against 'not by works', read as what Paul's word means.

• The crux: \((P_{47} \land P_{48} \land P_{49}) \rightarrow \lnot P_{50}\), a premise of Paul's word (δικαιόω, by the rule of least meaning).
• What it does: its conclusion does not follow without it.
• Granted: \(P_{47}\), \(P_{48}\), \(P_{49}\), which the break also needs.
• Where the rival breaks: \(P_{52}\), \(P_{52} \rightarrow P_{50}\) cannot be held together with \((P_{47} \land P_{48} \land P_{49}) \rightarrow \lnot P_{50}\) and \(P_{47}\), \(P_{48}\), \(P_{49}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{47}\) In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — well supported: bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • \(P_{48}\) Paul names renewal with other words (ἀνακαίνωσις, ἁγιασμός) and sets them beside δικαιόω — consensus: Titus 3:5-7; Rom 12:2; Rom 6:19-22; 1 Cor 6:11
  • \(P_{49}\) A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — well supported: silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • the step itself — well supported: silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

Against Romans 4:3–8, on Paul's word (by the rule of least meaning), it cannot be held. Where it breaks:

Why Romans 4:3–8, on Paul's word (by the rule of least meaning) stands against Trent, against 'not by works', read as what Paul's word means.

• The crux: \((P_{55} \land P_{49}) \rightarrow \lnot P_{50}\), a premise of Romans 4:3–8, on Paul's word (by the rule of least meaning).
• What it does: its conclusion does not follow without it.
• Granted: \(P_{4}\), \(P_{53}\), \(P_{54}\), \(P_{49}\), \((P_{4} \land P_{53} \land P_{54}) \rightarrow P_{55}\), which the break also needs.
• Where the rival breaks: \(P_{33}\), \(P_{33} \rightarrow P_{50}\) cannot be held together with \((P_{55} \land P_{49}) \rightarrow \lnot P_{50}\) and \(P_{4}\), \(P_{53}\), \(P_{54}\), \(P_{49}\), \((P_{4} \land P_{53} \land P_{54}) \rightarrow P_{55}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{4}\) Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — well supported: Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • \(P_{53}\) Romans 4:6–8: righteousness counted apart from works — sins forgiven, sin not counted — consensus: Rom 4:6-8; moo-romans-1996, ad loc. Rom 4:6
  • \(P_{54}\) λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — well supported: bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • \(P_{49}\) A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — well supported: silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • \(P_{55}\) In Romans 4:6–8 Paul glosses righteousness counted apart from works as sin not counted — well supported: moo-romans-1996, ad loc. Rom 4:6; Rom 4:6-8
  • the step itself — well supported: moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι; well supported: silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

2. Read as what God does in justifying. The claim commits Trent, against 'not by works' to \(P_{51}\) — so read by lwf-catholic-joint-declaration-2000, §§22; tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7 (disputed).

Against Paul's word (δικαιόω, by the rule of least meaning), it is not reached: Paul's word (δικαιόω, by the rule of least meaning) holds, and can be held together with it.

Against Romans 4:3–8, on Paul's word (by the rule of least meaning), it is not reached: Romans 4:3–8, on Paul's word (by the rule of least meaning) holds, and can be held together with it.

Against Paul's gospel (Galatians 1), against justification as renewal, it cannot be held. Where it breaks:

Why Paul's gospel (Galatians 1), against justification as renewal stands against Trent, against 'not by works', read as what God does in justifying.

• The crux: \((P_{56} \land P_{47} \land P_{46}) \rightarrow \lnot P_{33}\), a premise of Paul's gospel (Galatians 1), against justification as renewal.
• What it does: its conclusion does not follow without it.
• Granted: \(P_{42}\), \(P_{43}\), \(P_{44}\), \(P_{45}\), \((P_{42} \land P_{43} \land P_{44} \land P_{45}) \rightarrow P_{56}\), \(P_{46}\), \(P_{47}\), which the break also needs.
• Where the rival breaks: \(P_{33}\) cannot be held together with \((P_{56} \land P_{47} \land P_{46}) \rightarrow \lnot P_{33}\) and \(P_{42}\), \(P_{43}\), \(P_{44}\), \(P_{45}\), \((P_{42} \land P_{43} \land P_{44} \land P_{45}) \rightarrow P_{56}\), \(P_{46}\), \(P_{47}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{42}\) Galatians 1:6–9: whoever preaches a gospel contrary to the one received is accursed — consensus: Gal 1:6-9; moo-galatians-2013, ad loc. Gal 1:6
  • \(P_{43}\) 1 Corinthians 15:3: the gospel of first importance — Christ died for our sins — consensus: 1 Cor 15:3
  • \(P_{44}\) Galatians 2:21: if righteousness were through the law, Christ died for no purpose — consensus: Gal 2:21; moo-galatians-2013, ad loc. Gal 2:21
  • \(P_{45}\) Galatians 5:2–4: you who would be justified by the law are severed from Christ — consensus: Gal 5:2-4; moo-galatians-2013, ad loc. Gal 5:2
  • \(P_{56}\) Christ's death for our sins is the whole ground of justification; to add to it is another gospel — disputed: westminster-confession-1647, §XI.1; Gal 2:21; moo-galatians-2013, ad loc. Gal 2:21; roberts-ante-nicene-fathers-1-1885, §Epistle to Diognetus 9
  • \(P_{46}\) Romans 8:33–34: it is God who justifies — who is to condemn? — consensus: Rom 8:33-34
  • \(P_{47}\) In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — well supported: bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • the step itself — disputed: moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1; disputed: westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965

Against Romans 4:3–8, against justification as renewal, it cannot be held. Where it breaks:

Why Romans 4:3–8, against justification as renewal stands against Trent, against 'not by works', read as what God does in justifying.

• The crux: \((P_{55} \land P_{47}) \rightarrow \lnot P_{33}\), a premise of Romans 4:3–8, against justification as renewal.
• What it does: its conclusion does not follow without it.
• Granted: \(P_{4}\), \(P_{53}\), \(P_{54}\), \(P_{47}\), \((P_{4} \land P_{53} \land P_{54}) \rightarrow P_{55}\), which the break also needs.
• Where the rival breaks: \(P_{33}\) cannot be held together with \((P_{55} \land P_{47}) \rightarrow \lnot P_{33}\) and \(P_{4}\), \(P_{53}\), \(P_{54}\), \(P_{47}\), \((P_{4} \land P_{53} \land P_{54}) \rightarrow P_{55}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{4}\) Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — well supported: Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • \(P_{53}\) Romans 4:6–8: righteousness counted apart from works — sins forgiven, sin not counted — consensus: Rom 4:6-8; moo-romans-1996, ad loc. Rom 4:6
  • \(P_{54}\) λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — well supported: bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • \(P_{47}\) In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — well supported: bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • \(P_{55}\) In Romans 4:6–8 Paul glosses righteousness counted apart from works as sin not counted — well supported: moo-romans-1996, ad loc. Rom 4:6; Rom 4:6-8
  • the step itself — well supported: moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι; disputed: moo-romans-1996, ad loc. Rom 4:5; westminster-confession-1647, §XI.1

TestimonyArguments.SolaFide.Dispute — who prevails over sola fide

The results in Results.lean ask what each package entails. This module asks what happens when the positions meet: the three Reformed strands, each argued alone; Trent; the apocalyptic reading of Martyn and Campbell; Sanders and Dunn on covenantal nomism, and the critics who answer them; Jervell on the yoke of Acts 15; Paul's gospel in Galatians, against Trent's definition; Paul's word, read by the rule of least meaning, lexically and from Romans 4; and Trent with its definition read as a claim about that word. Who defeats whom is not stipulated — each defeat, and each absence of one, is a theorem about the positions' premises (see Testimony.Logic.Dispute).

The ratings decide one thing here

Every party's weakest link but two is disputed: each Reformed strand's inference is rated at Trent's canon 9, which denies it; Paul's and Peter's cases hold the Reformed distinction between justification and sanctification, which Trent anathematises; Trent rests on its own definition of justification, which Westminster denies; the apocalyptic reading denies an atom (and a denial ranks at the bottom); and so on. Between those parties no rating blocks any attack, and the outcome is fixed by who contradicts whom.

The exceptions are the two routes to Paul's word. The lexical case (lexicalCase): δικαιόω is forensic, Paul names renewal with words of its own, and a word contributes the least meaning its context requires. And the exegetical case from Romans 4 (romansFourOnTheWord): Paul glosses the righteousness God counts to the ungodly as sin not counted, and by the same rule the verb he glosses so does not also denote renewal. Every link of each is rated wellSupported or better. Each contradicts one party, Trent read as a claim about Paul's word, and those are the attacks in the dispute the ratings decide.

How to read the verdicts

A few words recur, and each has a plain meaning.

• Defeats. One position contradicts another — denies one of its premises, its conclusion, or a claim it derives on the way — and is not the weaker of the two. Many defeats run both ways: a standoff.
• Weakest link. A position is only as strong as its least-supported premise or step. Ratings run from disputed, the lowest, through plausible and wellSupported, to consensus. Denying a claim counts as disputed.
• Forced (prevails outright, the grounded positions). Accepted however every standoff is resolved: nothing attacks it that it cannot rule out.
• Can be defended (credulously accepted). Held by some consistent position that answers every attack on its members, itself or through an ally.
• Not forced. Some consistent position leaves it out. Not forced is not false: it means the dispute, as argued, cannot make a reader accept it.
• Cannot be defended. No consistent position can hold it and answer its attackers.

Who defeats whom

• Trent and each Reformed strand defeat each other. Paul's and Peter's cases conclude "not by works", which Trent denies; and Trent's definition of justification — the renewal of the inward man — contradicts the distinction between justification and sanctification they hold. That is where the objection comes from: with the distinction in place of the definition, Trent's case no longer denies "not by works" (trent_objection_rests_on_its_definition). Luke's case holds only Luke's words, and meets Trent over faith's sufficiency: Trent's definition, with canon 9, denies that faith without charity suffices, and "your faith has saved you" says hers did.
• The apocalyptic reading and Paul defeat each other: it denies the objective genitive, and Paul concludes faith alone. Luke and Acts do not conflict with it either way. They say that faith saves, which it grants; it says that faith is not the condition, which they do not deny.
• The apocalyptic reading and Trent defeat each other. They agree that justification is not by faith alone; but the apocalyptic reading derives "not by works" — God's deliverance is conditioned on nothing a person does — and Trent denies it. Each attacks what the other holds.
• Sanders defeats Paul, by denying the ἔργα νόμου premise; Paul and the critics each defeat Sanders back.
• Jervell and Acts defeat each other, over the yoke.
• Paul's gospel and Trent defeat each other, over Trent's definition: the gospel line concludes that justification is not the renewal of the inward man, and both rest on something rated disputed.
• Paul's word defeats Trent read as a claim about it, and not the reverse (lexical_defeats_trent_on_pauls_word, trent_on_pauls_word_does_not_defeat_lexical). Read that way, Trent's case derives that δικαιόω denotes renewal; Paul's word denies it, and Trent's reply, from a definition rated disputed, fails against a case rated wellSupported. Romans 4, read for Paul's word, does the same, by exegesis rather than lexicography. Neither conflicts with anything else — in particular not with Trent's case as Trent states it, whose definition, taken at face value, says nothing about the word.

What follows

Only Paul's word prevails outright (only_pauls_word_prevails): the grounded extension is exactly its two routes, the lexical case and Romans 4 read for the word. Every other party is attacked by someone the dispute cannot rule out: some lose outright, and others stand off against a rival the dispute cannot choose between. And Trent read as a claim about Paul's word cannot be defended at all (trent_on_pauls_word_indefensible): both routes defeat it, and nothing answers either.

Beyond that, nothing wins on every resolution. Luke's case, Paul's gospel and Trent — as Trent states it, tied to neither reading — are each defensible, and none is forced (dominical_case_defensible, dominical_case_not_forced, gospel_defensible, gospel_not_forced, trent_defensible, trent_not_forced). Every attack between Trent and a Reformed party runs both ways, with every rating at the bottom, and the dispute has no ground to choose between them.

Between Paul and the apocalyptic reading, the dispute chooses neither. Each defeats the other over πίστις Χριστοῦ; each is defensible, and neither is forced (apocalyptic_defensible, apocalyptic_not_forced). The apocalyptic reading stands with Luke's case and Peter's, which claim that faith saves and not that faith alone does.

What the verdict rests on

Three things, each stated as a result or a limitation rather than left implicit.

What Trent's definition claims. Trent's definition can be read two ways, and the dilemma whatTrentsDefinitionClaims (Definition.lean) answers both. Read as a claim about Paul's word, it cannot be held with Paul's word, and in this dispute it cannot be defended. Read as a claim about what God does in justifying, the lexical case does not reach it, and what divides it from Paul is one step, that a verdict on a finished work excludes the renewal wrought in us (whereTrentPartsFromPaul) — rated disputed. Trent's case as Trent states it stands for that second reading here: the reading adds a commitment no party denies. So the dispute does not settle between Trent and the Reformed; it shows that Trent can keep its definition only as a claim about the reality and not about Paul's word, and it names the one step on which that claim turns.

An absence. The dominical case is attacked by no one but Trent, because no source cited here argues that σῴζω at Luke 7:50 means healing. That absence is now also its rating: the premise is wellSupported, not disputed, because a search for a scholar arguing the healing sense at 7:50 found none, and at 7:50 there is no illness — the saying follows "your sins are forgiven". It is not consensus, because the same formula means "made you well" at Luke 8:48, 17:19 and 18:42. A cited argument for the healing reading would attack the dominical case and lower the rating.

An objection answered in advance. "Her sins are forgiven, for she loved much" (7:47) is the text a rival would use to make love, not faith, the ground of her forgiveness. The dominical case does not leave that open: it carries luke7_47LoveIsEvidence — her love is the evidence of forgiveness, not its ground, as 7:47b and the parable of 7:41–43 read it — as a premise of its own. It is Padilla's reading — she "loves much because she has been forgiven much" — and Melanchthon's in the Apology of the Augsburg Confession: "Christ interprets Himself when He adds: Thy faith hath saved thee", so the woman did not merit forgiveness "by that work of love". It is rated plausible, because Trent counts beginning to love God among the dispositions to justification (Session VI, ch. 6); but no party here argues that reading of 7:47.

The parties chosen. A dispute is over the arguments put into it. Hays's subjective genitive is represented through the apocalyptic reading, which holds it; a Hays party of its own, the Joint Declaration, and a party for the Finnish reading would each be new arguments to weigh. So would a cited argument that Paul's δικαιόω, granted forensic, still denotes renewal: none was found, and the lexical case's rating says so. Romans 4 (romansFourCase) is answered in the dilemma, not added here: it meets Trent exactly where Paul's gospel does — at Trent's definition, from a step rated disputed — and a party of its own would be a second argument to weigh.

The positions

Each party is an argument in its own right: premises that can hold together, a conclusion they deliver, and an inference someone has rated. The Reformed case enters as three parties, one per strand, because a dispute weighs arguments whole: one package holding all three strands would be defeated by a contradiction of any one of them, and the redundancy the results prove would count for nothing.

reformedOntology

What the Reformed hold about what justification is, where Trent is heard: justification and sanctification are distinct, and sanctification follows. It carries no strand's conclusion — the strands reach sola fide without it — but it is the premise Trent's definition contradicts, so it belongs to each Reformed party, and Trent's attack on each lands on it as well as on "not by works". Not added to reformed, because the other packages built from it, the Finnish reading among them, would then hold it on their authors' behalf.

paulineCase — Sola fide from Paul (Galatians 2:16)

The Pauline strand, argued alone: sola fide from Galatians 2:16.

Its ἔργα νόμου premise is derived, not assumed: it rests on the critics' line, which denies covenantal nomism and reads Galatians as a polemic against circumcision as a requirement. That is where the literature puts the dispute (critics_carry_the_pauline_strand, sanders_costs_the_pauline_strand), and so Sanders meets Paul here on the history of Second Temple Judaism, not on Paul's Greek. The critics' inference is rated with the rest, as Gathercole's.

No premise here rests on scripture alone.

dominicalCase — Luke 7:50: "your faith has saved you"

Luke's case: what Jesus says at Luke 7:50, and no more. "Your faith has saved you", read with σῴζω as salvation and the woman's love (7:47) as the evidence of her forgiveness rather than its ground: her faith sufficed.

It carries nothing Luke does not say — not Paul's texts, not the answer to James, not the Reformed account of what justification is — and it does not claim what Paul argues, that faith alone saves. So it is attacked only by what denies Luke's own claim.

No premise here rests on scripture alone.

apostolicCase — Sola fide from Peter (Acts 15:9–11)

The apostolic strand, argued alone: sola fide from Peter at Jerusalem.

No premise here rests on scripture alone.

apocalypticCase — Apocalyptic reading, against faith as the condition

The apocalyptic reading, as the argument it makes: faith is not the condition of justification. It keeps grace and "not by works", by its own step.

No premise here rests on scripture alone.

sandersCase — Covenantal nomism (Sanders, Dunn)

Sanders and Dunn: covenantal nomism, so ἔργα νόμου are the boundary markers.

No premise here rests on scripture alone.

criticsCase — Variegated nomism (Gathercole, Carson et al.)

Gathercole and Variegated Nomism: not covenantal nomism, so ἔργα νόμου are works in general.

No premise here rests on scripture alone.

jervellCase — Law-observant Luke (Jervell)

Jervell: Luke is law-observant, so the yoke is not the law as a condition of salvation.

No premise here rests on scripture alone.

Each position holds together and delivers its conclusion

paulineCase_establishes

The Pauline case delivers sola fide.

theorem paulineCase_establishes : Establishes paulineCase
-- axioms: propext, Quot.sound

paulineCase_is_satisfiable

The Pauline case has a model.

theorem paulineCase_is_satisfiable : Satisfiable paulineCase.premises
-- axioms: propext, Quot.sound

dominicalCase_establishes

The dominical case delivers sola fide.

theorem dominicalCase_establishes : Establishes dominicalCase
-- axioms: propext, Quot.sound

dominicalCase_is_satisfiable

The dominical case has a model.

theorem dominicalCase_is_satisfiable : Satisfiable dominicalCase.premises
-- axioms: propext, Quot.sound

apostolicCase_establishes

The apostolic case delivers sola fide.

theorem apostolicCase_establishes : Establishes apostolicCase
-- axioms: propext, Quot.sound

apostolicCase_is_satisfiable

The apostolic case has a model.

theorem apostolicCase_is_satisfiable : Satisfiable apostolicCase.premises
-- axioms: propext, Quot.sound

tridentineCase_establishes

Trent's case delivers its conclusion: salvation is not apart from works.

theorem tridentineCase_establishes : Establishes tridentineCase
-- axioms: propext, Quot.sound

tridentineCase_is_satisfiable

Trent's case has a model.

theorem tridentineCase_is_satisfiable : Satisfiable tridentineCase.premises
-- axioms: propext, Quot.sound

Where Trent's objection comes from

Trent's objection to "not by works" is not a separate thesis about works. It follows from what Trent says justification is: the renewal of the inward man, not remission of sins only (ch. 7). Grant that, grant that the renewal grows as the justified do good works (ch. 10), and good works increase justification (canon 24), which denies "not by works" (ch. 16). The Reformed grant the growth — Westminster XIII.1 calls it sanctification — and deny the definition.

tridentineCaseOnTheReformedDistinction — Trent, on the Reformed distinction

Trent's case with its definition of justification exchanged for the Reformed distinction: everything else Trent holds, including that the renewal grows through good works, and justification and sanctification distinct.

No premise here rests on scripture alone.

reformedDistinctionReading

Trent's world, with the Reformed distinction in place of its definition: the renewal grows, but it is sanctification, so it increases nothing called justification, and salvation is not by works.

def reformedDistinctionReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.justificationIncludesSanctification => False
    | Claim.worksMeritIncreaseOfJustification => False
    | x => True

trent_objection_rests_on_its_definition

Trent's objection rests on its definition of justification. Keep all of Trent's case except its definition, grant the Reformed distinction instead, and "not apart from works" no longer follows — though both sides still hold that the renewal of the justified grows through good works. So the dispute over works is, at bottom, a dispute over what justification is: whether the renewal that grows is justification or the sanctification that follows it.

theorem trent_objection_rests_on_its_definition : ¬Establishes
    tridentineCaseOnTheReformedDistinction
-- axioms: propext, Quot.sound

apocalypticCase_establishes

The apocalyptic case delivers its conclusion.

theorem apocalypticCase_establishes : Establishes apocalypticCase
-- axioms: propext, Quot.sound

apocalypticCase_is_satisfiable

The apocalyptic case has a model.

theorem apocalypticCase_is_satisfiable : Satisfiable apocalypticCase.premises
-- axioms: propext, Quot.sound

sandersCase_establishes

Sanders' case delivers its conclusion.

theorem sandersCase_establishes : Establishes sandersCase
-- axioms: propext, Quot.sound

sandersCase_is_satisfiable

Sanders' case has a model.

theorem sandersCase_is_satisfiable : Satisfiable sandersCase.premises
-- axioms: propext, Quot.sound

criticsCase_establishes

The critics' case delivers its conclusion.

theorem criticsCase_establishes : Establishes criticsCase
-- axioms: propext, Quot.sound

criticsCase_is_satisfiable

The critics' case has a model.

theorem criticsCase_is_satisfiable : Satisfiable criticsCase.premises
-- axioms: propext, Quot.sound

jervellCase_establishes

Jervell's case delivers its conclusion.

theorem jervellCase_establishes : Establishes jervellCase
-- axioms: propext, Quot.sound

jervellCase_is_satisfiable

Jervell's case has a model.

theorem jervellCase_is_satisfiable : Satisfiable jervellCase.premises
-- axioms: propext, Quot.sound

Strength: every weakest link is disputed, but two

Every party but two rests on something cited disputed, or denies an atom, which ranks at the bottom; so its strength is 0, and no rating blocks an attack between two of them. The exceptions are the two routes to Paul's word, the lexical case and Romans 4 read for the word: every link of each is rated wellSupported or better. So an attack on either from a party at the bottom does not defeat it, and its attack on such a party does.

paulineCase_strength

The Pauline case rests on its lexical premises, cited disputed, as well as on the Reformed distinction.

theorem paulineCase_strength : paulineCase.strength = 0
-- axioms: propext

dominicalCase_strength

The dominical case rests on the Reformed distinction, cited disputed, and on an inference Trent's canon 9 denies. Its own two premises rank higher: σῴζω wellSupported, and the reading of 7:47 plausible.

theorem dominicalCase_strength : dominicalCase.strength = 0
-- axioms: propext

apostolicCase_strength

The apostolic case rests on the yoke premise, cited disputed.

theorem apostolicCase_strength : apostolicCase.strength = 0
-- axioms: propext

tridentineCase_strength

Trent rests on its definition of justification, cited disputed.

theorem tridentineCase_strength : tridentineCase.strength = 0
-- axioms: propext

apocalypticCase_strength

The apocalyptic case denies the objective genitive.

theorem apocalypticCase_strength : apocalypticCase.strength = 0
-- axioms: propext

sandersCase_strength

Sanders' case rests on covenantal nomism, cited disputed.

theorem sandersCase_strength : sandersCase.strength = 0
-- axioms: propext

criticsCase_strength

The critics' case denies covenantal nomism.

theorem criticsCase_strength : criticsCase.strength = 0
-- axioms: propext

jervellCase_strength

Jervell's step is contested, by Bruce.

theorem jervellCase_strength : jervellCase.strength = 0
-- axioms: propext

galatianGospel_strength

Paul's gospel rests on its reading of Galatians and on the step from a verdict to "renewal is no part of justification", both cited disputed.

theorem galatianGospel_strength : galatianGospel.strength = 0
-- axioms: propext

lexicalCase_strength

Paul's word does not rest on anything disputed. The forensic sense and the rule of least meaning are wellSupported, Paul's own words for renewal are consensus, and so is no step: the step from them is wellSupported. Its weakest link ranks 2, above the bottom.

theorem lexicalCase_strength : lexicalCase.strength = 2
-- axioms: propext

tridentineOnPaulsWord_strength

Trent read as a claim about Paul's word rests on everything Trent does.

theorem tridentineOnPaulsWord_strength : tridentineOnPaulsWord.strength = 0
-- axioms: propext

romansFourOnTheWord_strength

Nor does Romans 4, read for Paul's word. Its texts are rated wellSupported or better, and so are the sense of λογίζομαι, Paul's gloss, the rule of least meaning and both steps. Its weakest link ranks 2.

theorem romansFourOnTheWord_strength : romansFourOnTheWord.strength = 2
-- axioms: propext

The defeats

Each is decided from the two packages' premises by Horn.defeats? and checked by the kernel: the attack, and the comparison of strengths.

trent_defeats_pauline

Trent defeats the Pauline case. It entails the denial of "not by works", so it rebuts sola fide.

theorem trent_defeats_pauline : Defeats tridentineCase paulineCase
-- axioms: propext, Classical.choice, Quot.sound

trent_defeats_dominical

Trent defeats the dominical case, on the same rebuttal.

theorem trent_defeats_dominical : Defeats tridentineCase dominicalCase
-- axioms: propext, Classical.choice, Quot.sound

trent_defeats_apostolic

Trent defeats the apostolic case, on the same rebuttal.

theorem trent_defeats_apostolic : Defeats tridentineCase apostolicCase
-- axioms: propext, Classical.choice, Quot.sound

pauline_defeats_trent

The Pauline case defeats Trent back. It entails "not by works", which Trent denies.

theorem pauline_defeats_trent : Defeats paulineCase tridentineCase
-- axioms: propext, Classical.choice, Quot.sound

dominical_defeats_trent

The dominical case defeats Trent back.

theorem dominical_defeats_trent : Defeats dominicalCase tridentineCase
-- axioms: propext, Classical.choice, Quot.sound

apostolic_defeats_trent

The apostolic case defeats Trent back.

theorem apostolic_defeats_trent : Defeats apostolicCase tridentineCase
-- axioms: propext, Classical.choice, Quot.sound

apocalyptic_defeats_trent

The apocalyptic reading defeats Trent. It holds "not by works" by its own step — God's deliverance is conditioned on nothing a person does — and Trent denies it.

theorem apocalyptic_defeats_trent : Defeats apocalypticCase tridentineCase
-- axioms: propext, Classical.choice, Quot.sound

apocalyptic_defeats_pauline

The apocalyptic reading defeats the Pauline case. It denies the objective genitive, a premise of Paul's strand cited disputed.

theorem apocalyptic_defeats_pauline : Defeats apocalypticCase paulineCase
-- axioms: propext, Classical.choice, Quot.sound

pauline_defeats_apocalyptic

The Pauline case defeats the apocalyptic reading back. It entails justification by faith alone.

theorem pauline_defeats_apocalyptic : Defeats paulineCase apocalypticCase
-- axioms: propext, Classical.choice, Quot.sound

dominical_does_not_defeat_apocalyptic

The dominical case does not defeat the apocalyptic reading. Luke 7:50 says that faith saved her, not that faith alone does; the apocalyptic reading grants that faith saves, and denies only that faith is the condition. So Luke's case entails nothing the apocalyptic reading denies (luke_grants_the_apocalyptic_conclusion).

theorem dominical_does_not_defeat_apocalyptic : ¬Defeats dominicalCase
    apocalypticCase
-- axioms: propext, Classical.choice, Quot.sound

apostolic_does_not_defeat_apocalyptic

Nor does the apostolic case, for the same reason: Peter at Jerusalem says faith suffices, not that it alone does (peter_grants_the_apocalyptic_conclusion).

theorem apostolic_does_not_defeat_apocalyptic : ¬Defeats apostolicCase
    apocalypticCase
-- axioms: propext, Classical.choice, Quot.sound

sanders_defeats_pauline

Sanders defeats the Pauline case. Covenantal nomism, with Dunn's inference, denies the ἔργα νόμου premise.

theorem sanders_defeats_pauline : Defeats sandersCase paulineCase
-- axioms: propext, Classical.choice, Quot.sound

pauline_defeats_sanders

The Pauline case defeats Sanders back. It holds the premise Sanders' conclusion denies.

theorem pauline_defeats_sanders : Defeats paulineCase sandersCase
-- axioms: propext, Classical.choice, Quot.sound

sanders_defeats_critics

Sanders defeats the critics. Their conclusions contradict.

theorem sanders_defeats_critics : Defeats sandersCase criticsCase
-- axioms: propext, Classical.choice, Quot.sound

critics_defeat_sanders

The critics defeat Sanders. They deny covenantal nomism, his ground.

theorem critics_defeat_sanders : Defeats criticsCase sandersCase
-- axioms: propext, Classical.choice, Quot.sound

jervell_defeats_apostolic

Jervell defeats the apostolic case. He denies the yoke premise.

theorem jervell_defeats_apostolic : Defeats jervellCase apostolicCase
-- axioms: propext, Classical.choice, Quot.sound

apostolic_defeats_jervell

The apostolic case defeats Jervell back. It holds the premise his conclusion denies.

theorem apostolic_defeats_jervell : Defeats apostolicCase jervellCase
-- axioms: propext, Classical.choice, Quot.sound

What does not defeat

Most pairs of parties are compatible: some world holds both, and seven such worlds are named below (Dispute.StandTogether) — the readings on which whole groups of positions can be held at once. Three pairs conflict in one direction only. All of them, like every cell of the table, are decided by Horn.defeats? from the premises.

criticsJervellReading

The critics' world with Jervell's: covenantal nomism fails, and the yoke is Israel's law for gentiles. The Pauline and dominical cases hold in it. Faith the only means and justification forensic only, it denies Trent's baptism as the instrument and justification as including sanctification.

def criticsJervellReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | Claim.rev22_11BeJustifiedStill => False
    | Claim.sir18_22BeJustifiedToDeath => False
    | Claim.jamesUsesDikaioAsPaul => False
    | Claim.secondTempleCovenantalNomism => False
    | Claim.acts15YokeIsLawAsCondition => False
    | Claim.baptismIsInstrumentalCause => False
    | Claim.justificationIncludesSanctification => False
    | x => True

trentSandersJervellReading

Trent's world with Sanders' and Jervell's. With Trent, it denies that faith is the only means of justification.

def trentSandersJervellReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | Claim.rev22_11BeJustifiedStill => False
    | Claim.sir18_22BeJustifiedToDeath => False
    | Claim.jamesUsesDikaioAsPaul => False
    | Claim.salvationNotByWorks => False
    | Claim.justificationIsForensicOnly => False
    | Claim.worksOfLawMeansWorksGenerally => False
    | Claim.acts15YokeIsLawAsCondition => False
    | Claim.justificationDistinctFromSanctification => False
    | Claim.faithIsSufficient => False
    | Claim.justificationByFaithAlone => False
    | x => True

trentCriticsJervellReading

Trent's world with the critics' and Jervell's. With Trent, it denies that faith is the only means of justification.

def trentCriticsJervellReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | Claim.rev22_11BeJustifiedStill => False
    | Claim.sir18_22BeJustifiedToDeath => False
    | Claim.jamesUsesDikaioAsPaul => False
    | Claim.salvationNotByWorks => False
    | Claim.justificationIsForensicOnly => False
    | Claim.secondTempleCovenantalNomism => False
    | Claim.acts15YokeIsLawAsCondition => False
    | Claim.justificationDistinctFromSanctification => False
    | Claim.faithIsSufficient => False
    | Claim.justificationByFaithAlone => False
    | x => True

apocalypticSandersJervellReading

The apocalyptic world with Sanders' and Jervell's. Justification is forensic only here, as in every world but Trent's, so it does not include sanctification.

def apocalypticSandersJervellReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | Claim.rev22_11BeJustifiedStill => False
    | Claim.sir18_22BeJustifiedToDeath => False
    | Claim.jamesUsesDikaioAsPaul => False
    | Claim.pistisChristouObjective => False
    | Claim.justificationByFaithAlone => False
    | Claim.worksOfLawMeansWorksGenerally => False
    | Claim.acts15YokeIsLawAsCondition => False
    | Claim.justificationIncludesSanctification => False
    | x => True

apocalypticCriticsJervellReading

The apocalyptic world with the critics' and Jervell's. Justification is forensic only here, as in every world but Trent's, so it does not include sanctification.

def apocalypticCriticsJervellReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | Claim.rev22_11BeJustifiedStill => False
    | Claim.sir18_22BeJustifiedToDeath => False
    | Claim.jamesUsesDikaioAsPaul => False
    | Claim.pistisChristouObjective => False
    | Claim.justificationByFaithAlone => False
    | Claim.secondTempleCovenantalNomism => False
    | Claim.acts15YokeIsLawAsCondition => False
    | Claim.justificationIncludesSanctification => False
    | x => True

apocalyptic_does_not_defeat_dominical

The apocalyptic reading does not defeat the dominical case. It contradicts nothing the dominical case rests on — not Luke 7:50, not σῴζω, not the reading of 7:47 — and it does not deny its conclusion: it grants grace and "not by works", and it can grant that salvation is received through faith while denying that faith is its condition. Why, premise by premise: apocalyptic_grants_sola_fide_as_stated and apocalyptic_grants_the_dominical_step.

theorem apocalyptic_does_not_defeat_dominical : ¬Defeats apocalypticCase
    dominicalCase
-- axioms: propext, Classical.choice, Quot.sound

apocalyptic_does_not_defeat_apostolic

Nor the apostolic case, for the same reasons (apocalyptic_grants_the_apostolic_step).

theorem apocalyptic_does_not_defeat_apostolic : ¬Defeats apocalypticCase
    apostolicCase
-- axioms: propext, Classical.choice, Quot.sound

trent_defeats_apocalyptic

Trent defeats the apocalyptic reading. They agree on its conclusion — justification is not by faith alone — but the apocalyptic reading derives "not by works" on the way (God's deliverance is sheer gift, conditioned on nothing a person does), and Trent denies it: works done in grace merit an increase of justification. So Trent rebuts the apocalyptic reading on a claim it derives (RebutsStep).

theorem trent_defeats_apocalyptic : Defeats tridentineCase apocalypticCase
-- axioms: propext, Classical.choice, Quot.sound

gospel_defeats_trent

Paul's gospel defeats Trent. It entails the denial of Trent's definition — justification is not the renewal of the inward man — and so undermines Trent at that premise (whereTrentPartsFromPaul says where).

theorem gospel_defeats_trent : Defeats galatianGospel tridentineCase
-- axioms: propext, Classical.choice, Quot.sound

trent_defeats_gospel

Trent defeats Paul's gospel back, by the same contradiction from the other side: its definition rebuts the gospel line's conclusion, and both rest on something rated disputed.

theorem trent_defeats_gospel : Defeats tridentineCase galatianGospel
-- axioms: propext, Classical.choice, Quot.sound

lexical_defeats_trent_on_pauls_word

Paul's word defeats Trent read as a claim about it. Trent, so read, derives that δικαιόω denotes renewal; Paul's word entails that it does not, and so rebuts the step by which Trent derives it (RebutsStep). The attack succeeds because Trent's weakest link is not above the lexical case's.

theorem lexical_defeats_trent_on_pauls_word : Defeats lexicalCase
    tridentineOnPaulsWord
-- axioms: propext, Classical.choice, Quot.sound

trent_on_pauls_word_does_not_defeat_lexical

And the reply fails. Trent, read as a claim about Paul's word, attacks the lexical case's step in turn — but its weakest link is Trent's definition, rated disputed, and the lexical case's is wellSupported. A weaker argument's rebuttal does not defeat a stronger one.

theorem trent_on_pauls_word_does_not_defeat_lexical : ¬Defeats
    tridentineOnPaulsWord lexicalCase
-- axioms: propext, Classical.choice, Quot.sound

Why these are not counters

The absences above are computed, and a computation names no reason. The readings below do: each is a way of holding one position that leaves one premise or conclusion of another standing, and each result checks that the reading holds everything the first position holds as well.

apocalypticWithFaithReading

The apocalyptic world in which salvation is still received through faith — faith is not the condition, but it is the means. Grace and "not by works" hold. Justification is forensic only here, as in every world but Trent's, so it does not include sanctification.

def apocalypticWithFaithReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | Claim.rev22_11BeJustifiedStill => False
    | Claim.sir18_22BeJustifiedToDeath => False
    | Claim.jamesUsesDikaioAsPaul => False
    | Claim.pistisChristouObjective => False
    | Claim.justificationByFaithAlone => False
    | Claim.justificationIncludesSanctification => False
    | x => True

apocalyptic_grants_sola_fide_as_stated

The apocalyptic reading grants what the Reformed strands conclude. Grace, "not by works", and salvation received through faith all hold in its world; what it denies is that faith is the condition. So it rebuts neither Luke's case nor Acts'.

theorem apocalyptic_grants_sola_fide_as_stated : Grants apocalypticCase
    dominicalCase.conclusion
-- axioms: propext, Quot.sound

apocalyptic_grants_the_dominical_step

The apocalyptic reader grants the dominical step outright. Luke's step delivers that faith suffices — "your faith has saved you" — and the apocalyptic world holds that: faith is the means, though not the condition.

theorem apocalyptic_grants_the_dominical_step : Grants apocalypticCase
    dominicalToSufficiency
-- axioms: propext, Quot.sound

apocalyptic_grants_the_apostolic_step

And the apostolic step, for the same reason: Peter says faith suffices, and the apocalyptic reading does not deny it.

theorem apocalyptic_grants_the_apostolic_step : Grants apocalypticCase
    apostolicToSufficiency
-- axioms: propext, Quot.sound

lukeWithoutAloneReading

Luke's world without alone: every premise of the dominical case, faith sufficient, and justification not by faith alone — because nothing Luke says excludes another condition. Justification is forensic only here, as in every world but Trent's, so it does not include sanctification.

def lukeWithoutAloneReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | Claim.rev22_11BeJustifiedStill => False
    | Claim.sir18_22BeJustifiedToDeath => False
    | Claim.jamesUsesDikaioAsPaul => False
    | Claim.justificationByFaithAlone => False
    | Claim.justificationIncludesSanctification => False
    | x => True

luke_grants_the_apocalyptic_conclusion

Luke's case grants the apocalyptic conclusion. Everything the dominical case holds is compatible with justification not being by faith alone, so it does not rebut the apocalyptic reading. Only Paul's case, which argues for alone, does.

theorem luke_grants_the_apocalyptic_conclusion : Grants dominicalCase
    apocalypticCase.conclusion
-- axioms: propext, Quot.sound

peter_grants_the_apocalyptic_conclusion

And Peter's case.

theorem peter_grants_the_apocalyptic_conclusion : Grants apostolicCase
    apocalypticCase.conclusion
-- axioms: propext, Quot.sound

trentWithoutDeliveranceReading

Trent's world, with the objective genitive and the apocalyptic reading of δικαιοσύνη θεοῦ both denied. With Trent, it denies that faith is the only means of justification.

def trentWithoutDeliveranceReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | Claim.rev22_11BeJustifiedStill => False
    | Claim.sir18_22BeJustifiedToDeath => False
    | Claim.jamesUsesDikaioAsPaul => False
    | Claim.salvationNotByWorks => False
    | Claim.justificationIsForensicOnly => False
    | Claim.pistisChristouObjective => False
    | Claim.righteousnessOfGodIsDeliverance => False
    | Claim.justificationDistinctFromSanctification => False
    | Claim.faithIsSufficient => False
    | Claim.justificationByFaithAlone => False
    | x => True

trent_grants_the_subjective_genitive

Trent can grant the subjective genitive. Nothing Trent holds settles how πίστις Χριστοῦ is read, so the apocalyptic reading's denial of the objective genitive stands against Trent unanswered.

theorem trent_grants_the_subjective_genitive : Grants tridentineCase (notP
    Claim.pistisChristouObjective)
-- axioms: propext, Quot.sound

trentWithoutFaithAloneReading

Trent's world, in which justification is not by faith alone — the apocalyptic reading's conclusion, which Trent shares.

def trentWithoutFaithAloneReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | Claim.rev22_11BeJustifiedStill => False
    | Claim.sir18_22BeJustifiedToDeath => False
    | Claim.jamesUsesDikaioAsPaul => False
    | Claim.salvationNotByWorks => False
    | Claim.justificationIsForensicOnly => False
    | Claim.justificationByFaithAlone => False
    | Claim.justificationDistinctFromSanctification => False
    | Claim.faithIsSufficient => False
    | x => True

trent_grants_the_apocalyptic_conclusion

Trent grants the apocalyptic reading's conclusion: justification is not by faith alone. They agree on it for different reasons, so Trent does not rebut the apocalyptic reading.

theorem trent_grants_the_apocalyptic_conclusion : Grants tridentineCase
    apocalypticCase.conclusion
-- axioms: propext, Quot.sound

The dispute

partyNode

The package each party argues from.

def partyNode : Party → ArgumentPackage Claim :=
  fun x =>
    match x with
    | Party.pauline => paulineCase
    | Party.dominical => dominicalCase
    | Party.apostolic => apostolicCase
    | Party.trent => tridentineCase
    | Party.apocalyptic => apocalypticCase
    | Party.sanders => sandersCase
    | Party.critics => criticsCase
    | Party.jervell => jervellCase
    | Party.gospel => galatianGospel
    | Party.lexical => lexicalCase
    | Party.trentOnPaulsWord => tridentineOnPaulsWord
    | Party.romansOnTheWord => romansFourOnTheWord

solaFideDispute

The dispute over sola fide: every party's premises have a model, every party establishes its conclusion, and every party's inferences are rated.

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

reformed_strands_stand_with_the_critics

The Reformed strands and the critics stand together, where covenantal nomism fails and everything else holds.

theorem reformed_strands_stand_with_the_critics :
    solaFideDispute.StandTogether [Party.pauline, Party.dominical,
    Party.apostolic, Party.critics]
-- axioms: propext, Classical.choice, Quot.sound

paul_and_luke_stand_with_jervell

Paul and Luke stand with the critics and with Jervell.

theorem paul_and_luke_stand_with_jervell : solaFideDispute.StandTogether
    [Party.pauline, Party.dominical, Party.jervell, Party.critics]
-- axioms: propext, Classical.choice, Quot.sound

luke_and_acts_stand_with_sanders

Luke and Acts stand with Sanders: neither rests on ἔργα νόμου.

theorem luke_and_acts_stand_with_sanders : solaFideDispute.StandTogether
    [Party.dominical, Party.apostolic, Party.sanders]
-- axioms: propext, Classical.choice, Quot.sound

trent_stands_with_sanders_and_jervell

Trent stands with Sanders and Jervell.

theorem trent_stands_with_sanders_and_jervell : solaFideDispute.StandTogether
    [Party.trent, Party.sanders, Party.jervell]
-- axioms: propext, Classical.choice, Quot.sound

trent_stands_with_the_critics_and_jervell

Trent stands with the critics and Jervell.

theorem trent_stands_with_the_critics_and_jervell :
    solaFideDispute.StandTogether [Party.trent, Party.critics, Party.jervell]
-- axioms: propext, Classical.choice, Quot.sound

apocalyptic_stands_with_sanders_and_jervell

The apocalyptic reading stands with Sanders and Jervell.

theorem apocalyptic_stands_with_sanders_and_jervell :
    solaFideDispute.StandTogether [Party.apocalyptic, Party.sanders,
    Party.jervell]
-- axioms: propext, Classical.choice, Quot.sound

apocalyptic_stands_with_the_critics_and_jervell

The apocalyptic reading stands with the critics and Jervell.

theorem apocalyptic_stands_with_the_critics_and_jervell :
    solaFideDispute.StandTogether [Party.apocalyptic, Party.critics,
    Party.jervell]
-- axioms: propext, Classical.choice, Quot.sound

partyDefeats

The defeats of the dispute, as a table.

def partyDefeats : Party → Party → Prop

instDecidableRelPartyPartyDefeats

The table is finite, so membership in it is decidable.

def instDecidableRelPartyPartyDefeats : DecidableRel partyDefeats

partyStrength

Each party's weakest link: at the bottom for all but Paul's word.

def partyStrength : Party → ℕ :=
  fun x =>
    match x with
    | Party.lexical => 2
    | Party.romansOnTheWord => 2
    | x => 0

partyNode_strength

Each party's weakest link, as its package computes it.

theorem partyNode_strength : ∀ (i : Party), (partyNode i).strength =
    partyStrength i
-- axioms: propext

solaFideDispute_defeats

Who defeats whom, all 144 pairs. Trent and each Reformed strand defeat each other. The apocalyptic reading and Paul defeat each other; it and Luke's and Acts' cases do not conflict; it and Trent defeat each other. Sanders defeats Paul and the critics, and both defeat him back. Jervell and Acts defeat each other. Paul's gospel and Trent defeat each other, over Trent's definition. Trent read as a claim about Paul's word meets everyone Trent meets, both ways, and two parties more: Paul's word defeats it, lexically and from Romans 4, and it defeats neither back — its replies are weighed and fail. Nothing else.

Every cell is computed from the parties' premises by Horn.defeats? and checked by the kernel — the defeats, and the absences of defeat, alike. The table above is what the computation is checked against; none of it is assumed.

theorem solaFideDispute_defeats : ∀ (i j : Party), solaFideDispute.defeats i j
    ↔ partyDefeats i j
-- axioms: propext, Classical.choice, Quot.sound

solaFideFinite

The dispute in the form the verdict solver computes with: every party, and the table.

def solaFideFinite : Solver.Finite solaFideDispute.defeats :=
  {
    parties :=
      [Party.pauline, Party.dominical,
        Party.apostolic, Party.trent,
        Party.apocalyptic, Party.sanders,
        Party.critics, Party.jervell, Party.gospel,
        Party.lexical, Party.trentOnPaulsWord,
        Party.romansOnTheWord],
    complete := solaFideFinite._proof_1,
    defeats := fun i j => decide (partyDefeats i j),
    spec := solaFideFinite._proof_2 }

The dispute as a graph

solaFideDispute_supports

Nothing supports anything in the sola fide dispute, in all 144 pairs: no party's conclusion entails a claim another rests on. The critics' conclusion used to be one of Paul's premises; now the Pauline case rests on the critics' whole line instead (paulineCase), and the relation is the stronger one below. The Reformed strands, which share their conclusion, agree rather than support (see Testimony.Logic.Support). Every cell is computed by supports? and checked by the kernel.

theorem solaFideDispute_supports : ∀ (i j : Party), ¬solaFideDispute.supports
    i j
-- axioms: propext, Classical.choice, Quot.sound

partyPartOf

Whose case is part of whose, as a table: besides each party's own, two pairs.

def partyPartOf : Party → Party → Prop :=
  fun x x_1 =>
    match x, x_1 with
    | Party.critics, Party.pauline => True
    | Party.trent, Party.trentOnPaulsWord => True
    | i, j => i = j

instDecidableRelPartyPartyPartOf

The table is finite, so membership in it is decidable.

def instDecidableRelPartyPartyPartOf : DecidableRel partyPartOf

solaFideDispute_partOf

Whose case is part of whose, all 144 pairs: the critics' case is part of Paul's, since the Pauline case derives its ἔργα νόμου premise from the critics' line; Trent's case is part of Trent's read as a claim about Paul's word, which only adds to it; and every case is part of itself. Nothing else. Every cell is computed by partOf? and checked by the kernel.

theorem solaFideDispute_partOf : ∀ (i j : Party), solaFideDispute.partOf i j ↔
    partyPartOf i j
-- axioms: propext, Classical.choice, Quot.sound

solaFideMap

The dispute 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 solaFideDispute_defeats, the supports the cells of solaFideDispute_supports and the parts the cells of solaFideDispute_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.

What the dispute decides

onlyPaulsWordUnanswered

How the dispute is settled as far as it can be, in one stage: nothing defeats either route to Paul's word, so both come first; and nothing joins them, because every other party has an attacker that Paul's word does not rule out — each Reformed strand has Trent, Trent has Paul's case, the apocalyptic reading has Paul's case, Sanders has the critics and the critics Sanders, Jervell has Peter's case, Paul's gospel has Trent, and Trent read as a claim about Paul's word has Paul's word itself. Some of these are standoffs, not losses: Paul's gospel answers Trent as Trent answers it.

What the dispute forces is exactly Paul's word (δικαιόω, by the rule of least meaning), Romans 4:3–8, on Paul's word (by the rule of least meaning).

• Stage 1: Paul's word (δικαιόω, by the rule of least meaning), Romans 4:3–8, on Paul's word (by the rule of least meaning).
  • Paul's word (δικαιόω, by the rule of least meaning) is defeated by nothing.
  • Romans 4:3–8, on Paul's word (by the rule of least meaning) is defeated by nothing.
• Nothing else is forced:
  • Trent, against 'not by works' defeats Sola fide from Paul (Galatians 2:16), and nothing forced defeats Trent, against 'not by works'.
  • Trent, against 'not by works' defeats Luke 7:50: "your faith has saved you", and nothing forced defeats Trent, against 'not by works'.
  • Trent, against 'not by works' defeats Sola fide from Peter (Acts 15:9–11), and nothing forced defeats Trent, against 'not by works'.
  • Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works', and nothing forced defeats Sola fide from Paul (Galatians 2:16).
  • Sola fide from Paul (Galatians 2:16) defeats Apocalyptic reading, against faith as the condition, and nothing forced defeats Sola fide from Paul (Galatians 2:16).
  • Variegated nomism (Gathercole, Carson et al.) defeats Covenantal nomism (Sanders, Dunn), and nothing forced defeats Variegated nomism (Gathercole, Carson et al.).
  • Covenantal nomism (Sanders, Dunn) defeats Variegated nomism (Gathercole, Carson et al.), and nothing forced defeats Covenantal nomism (Sanders, Dunn).
  • Sola fide from Peter (Acts 15:9–11) defeats Law-observant Luke (Jervell), and nothing forced defeats Sola fide from Peter (Acts 15:9–11).
  • Trent, against 'not by works' defeats Paul's gospel (Galatians 1), against justification as renewal, and nothing forced defeats Trent, against 'not by works'.
  • Paul's word (δικαιόω, by the rule of least meaning) defeats Trent, against 'not by works', read as what Paul's word means, and nothing forced defeats Paul's word (δικαιόω, by the rule of least meaning).

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

• Sola fide from Paul (Galatians 2:16), weakest at disputed:
  • πίστις Χριστοῦ in Galatians 2:16 means faith in Christ, not Christ's faithfulness — dunn-once-more-pistis-christou-1991; matlock-detheologizing-2000; Gal 2:16; Rom 3:22; Phil 3:9
  • Second Temple Judaism: in by grace, staying in by works (encoded as a denial, so it ranks disputed) — sanders-paul-palestinian-judaism-1977
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Paul's word (δικαιόω, by the rule of least meaning), weakest at well supported:
  • In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004
• Luke 7:50: "your faith has saved you", weakest at disputed:
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Sola fide from Peter (Acts 15:9–11), weakest at disputed:
  • The yoke refused at Acts 15:10 is the whole law as a condition of salvation — bruce-acts-1988, ad loc. Acts 15:10; Acts 15:10; Gal 5:1; Jas 2:10; das-paul-law-covenant-2001
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Trent, against 'not by works', weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
• Apocalyptic reading, against faith as the condition, weakest at disputed:
  • πίστις Χριστοῦ is Christ's faithfulness, the means of God's deliverance (encoded as a denial, so it ranks disputed) — campbell-deliverance-god-2009; martyn-galatians-1997, ad loc. Gal 2:16; hays-faith-jesus-christ-2002
  • δικαιοσύνη θεοῦ names God's deliverance in Christ, not a status faith obtains — campbell-deliverance-god-2009; martyn-galatians-1997; Rom 3:21-26
• Covenantal nomism (Sanders, Dunn), weakest at disputed:
  • Second Temple Judaism: in by grace, staying in by works — sanders-paul-palestinian-judaism-1977
  • an inference step — dunn-new-perspective-2005; wright-what-paul-said-1997
• Variegated nomism (Gathercole, Carson et al.), weakest at disputed:
  • Second Temple Judaism also held final vindication according to works (encoded as a denial, so it ranks disputed) — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Law-observant Luke (Jervell), weakest at disputed:
  • an inference step — jervell-luke-people-god-1972
• Paul's gospel (Galatians 1), against justification as renewal, weakest at disputed:
  • an inference step — moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1
  • an inference step — westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965
• Trent, against 'not by works', read as what Paul's word means, weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 8; tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; npnf1-05-1887, §On the Spirit and the Letter, ch. 45 (26.45); mcgrath-iustitia-dei-2005
• Romans 4:3–8, on Paul's word (by the rule of least meaning), weakest at well supported:
  • Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

Why Paul's word (δικαιόω, by the rule of least meaning) defeats Trent, against 'not by works', read as what Paul's word means, at the level of the claims: whereTrentsWordReadingFalls.

only_pauls_word_prevails

Only Paul's word prevails outright. The grounded extension — what the dispute forces before any choice between rivals — is exactly Paul's word, by its two routes: Paul's δικαιόω does not denote the renewal of the inward man, by the lexical case and by the exegesis of Romans 4. Nothing defeats either: the one party that contradicts them, Trent read as a claim about Paul's word, rests on a definition rated disputed, and its replies fail against cases whose every link is rated wellSupported or better. Nothing else is forced: every other party is attacked by someone the dispute cannot rule out, whether it loses outright or stands off against a rival the dispute cannot choose between.

theorem only_pauls_word_prevails : Framework.grounded solaFideDispute.defeats
    = {Party.lexical, Party.romansOnTheWord}
-- axioms: propext, Classical.choice, Quot.sound

trentsWordReadingAnswered

Why Trent, read as a claim about Paul's word, cannot be defended: Paul's word defeats it, and nothing defeats Paul's word. (Romans 4, read for the word, does too; one unanswered defeater is enough.)

Trent, against 'not by works', read as what Paul's word means cannot be defended: no admissible position holds it.

• Paul's word (δικαιόω, by the rule of least meaning) defeats Trent, against 'not by works', read as what Paul's word means, and nothing defeats Paul's word (δικαιόω, by the rule of least meaning).

What this rests on. The reasons state 1 defeat and 12 absences of defeat, each a cell of the defeat table, solaFideDispute_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:

• Paul's word (δικαιόω, by the rule of least meaning), weakest at well supported:
  • In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004
• Trent, against 'not by works', read as what Paul's word means, weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 8; tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; npnf1-05-1887, §On the Spirit and the Letter, ch. 45 (26.45); mcgrath-iustitia-dei-2005
• Sola fide from Paul (Galatians 2:16), weakest at disputed:
  • πίστις Χριστοῦ in Galatians 2:16 means faith in Christ, not Christ's faithfulness — dunn-once-more-pistis-christou-1991; matlock-detheologizing-2000; Gal 2:16; Rom 3:22; Phil 3:9
  • Second Temple Judaism: in by grace, staying in by works (encoded as a denial, so it ranks disputed) — sanders-paul-palestinian-judaism-1977
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Luke 7:50: "your faith has saved you", weakest at disputed:
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Sola fide from Peter (Acts 15:9–11), weakest at disputed:
  • The yoke refused at Acts 15:10 is the whole law as a condition of salvation — bruce-acts-1988, ad loc. Acts 15:10; Acts 15:10; Gal 5:1; Jas 2:10; das-paul-law-covenant-2001
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Trent, against 'not by works', weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
• Apocalyptic reading, against faith as the condition, weakest at disputed:
  • πίστις Χριστοῦ is Christ's faithfulness, the means of God's deliverance (encoded as a denial, so it ranks disputed) — campbell-deliverance-god-2009; martyn-galatians-1997, ad loc. Gal 2:16; hays-faith-jesus-christ-2002
  • δικαιοσύνη θεοῦ names God's deliverance in Christ, not a status faith obtains — campbell-deliverance-god-2009; martyn-galatians-1997; Rom 3:21-26
• Covenantal nomism (Sanders, Dunn), weakest at disputed:
  • Second Temple Judaism: in by grace, staying in by works — sanders-paul-palestinian-judaism-1977
  • an inference step — dunn-new-perspective-2005; wright-what-paul-said-1997
• Variegated nomism (Gathercole, Carson et al.), weakest at disputed:
  • Second Temple Judaism also held final vindication according to works (encoded as a denial, so it ranks disputed) — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Law-observant Luke (Jervell), weakest at disputed:
  • an inference step — jervell-luke-people-god-1972
• Paul's gospel (Galatians 1), against justification as renewal, weakest at disputed:
  • an inference step — moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1
  • an inference step — westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965
• Romans 4:3–8, on Paul's word (by the rule of least meaning), weakest at well supported:
  • Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

Why Paul's word (δικαιόω, by the rule of least meaning) defeats Trent, against 'not by works', read as what Paul's word means, at the level of the claims: whereTrentsWordReadingFalls.

trent_on_pauls_word_indefensible

Trent, read as a claim about Paul's word, cannot be defended. No admissible set holds it: Paul's word defeats it, lexically and from Romans 4, and nothing answers either. This is the first horn of whatTrentsDefinitionClaims, weighed: if Trent's definition says what Paul's δικαιόω means, it cannot be held, for a stated and cited reason, at a step rated wellSupported.

theorem trent_on_pauls_word_indefensible : ∀ (S : Set Party),
    Framework.Admissible solaFideDispute.defeats S → Party.trentOnPaulsWord ∉
    S
-- axioms: propext, Classical.choice, Quot.sound

trentStandsWithSandersAndJervell

Why Trent can be defended: it stands with Sanders and Jervell, and answers every party that attacks it itself — each Reformed strand, Paul's gospel, and the apocalyptic reading, whose derived "not by works" it denies.

Trent, against 'not by works' is accepted on some resolution.

• A position holding Trent, against 'not by works', Covenantal nomism (Sanders, Dunn), Law-observant Luke (Jervell) can be held.
• None of Trent, against 'not by works', Covenantal nomism (Sanders, Dunn), Law-observant Luke (Jervell) defeats another, and each attack on them is answered from among them:
  • Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Sola fide from Paul (Galatians 2:16).
  • Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Luke 7:50: "your faith has saved you".
  • Sola fide from Peter (Acts 15:9–11) defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Sola fide from Peter (Acts 15:9–11).
  • Apocalyptic reading, against faith as the condition defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Apocalyptic reading, against faith as the condition.
  • Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Paul's gospel (Galatians 1), against justification as renewal.
  • Sola fide from Paul (Galatians 2:16) defeats Covenantal nomism (Sanders, Dunn), and Trent, against 'not by works' defeats Sola fide from Paul (Galatians 2:16).
  • Variegated nomism (Gathercole, Carson et al.) defeats Covenantal nomism (Sanders, Dunn), and Covenantal nomism (Sanders, Dunn) defeats Variegated nomism (Gathercole, Carson et al.).
  • Sola fide from Peter (Acts 15:9–11) defeats Law-observant Luke (Jervell), and Trent, against 'not by works' defeats Sola fide from Peter (Acts 15:9–11).

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

• Trent, against 'not by works', weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
• Covenantal nomism (Sanders, Dunn), weakest at disputed:
  • Second Temple Judaism: in by grace, staying in by works — sanders-paul-palestinian-judaism-1977
  • an inference step — dunn-new-perspective-2005; wright-what-paul-said-1997
• Law-observant Luke (Jervell), weakest at disputed:
  • an inference step — jervell-luke-people-god-1972
• Sola fide from Paul (Galatians 2:16), weakest at disputed:
  • πίστις Χριστοῦ in Galatians 2:16 means faith in Christ, not Christ's faithfulness — dunn-once-more-pistis-christou-1991; matlock-detheologizing-2000; Gal 2:16; Rom 3:22; Phil 3:9
  • Second Temple Judaism: in by grace, staying in by works (encoded as a denial, so it ranks disputed) — sanders-paul-palestinian-judaism-1977
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Luke 7:50: "your faith has saved you", weakest at disputed:
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Sola fide from Peter (Acts 15:9–11), weakest at disputed:
  • The yoke refused at Acts 15:10 is the whole law as a condition of salvation — bruce-acts-1988, ad loc. Acts 15:10; Acts 15:10; Gal 5:1; Jas 2:10; das-paul-law-covenant-2001
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Apocalyptic reading, against faith as the condition, weakest at disputed:
  • πίστις Χριστοῦ is Christ's faithfulness, the means of God's deliverance (encoded as a denial, so it ranks disputed) — campbell-deliverance-god-2009; martyn-galatians-1997, ad loc. Gal 2:16; hays-faith-jesus-christ-2002
  • δικαιοσύνη θεοῦ names God's deliverance in Christ, not a status faith obtains — campbell-deliverance-god-2009; martyn-galatians-1997; Rom 3:21-26
• Variegated nomism (Gathercole, Carson et al.), weakest at disputed:
  • Second Temple Judaism also held final vindication according to works (encoded as a denial, so it ranks disputed) — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Paul's gospel (Galatians 1), against justification as renewal, weakest at disputed:
  • an inference step — moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1
  • an inference step — westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965
• Paul's word (δικαιόω, by the rule of least meaning), weakest at well supported:
  • In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004
• Trent, against 'not by works', read as what Paul's word means, weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 8; tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; npnf1-05-1887, §On the Spirit and the Letter, ch. 45 (26.45); mcgrath-iustitia-dei-2005
• Romans 4:3–8, on Paul's word (by the rule of least meaning), weakest at well supported:
  • Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

Why Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', at the level of the claims: whyTheDominicalCaseStandsAgainstTrent.

Why Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works', at the level of the claims: whereTrentPartsFromPaul.

trent_defensible

Trent can be defended. Some maximal defensible position holds it, with Sanders and Jervell. Every party that defeats Trent — Paul, Luke, Peter, Paul's gospel, the apocalyptic reading — Trent defeats back, and the ratings, all at the bottom, break no tie. Paul's word does not attack it: Trent's definition, unread, says nothing about what δικαιόω means. In particular Trent answers the apocalyptic reading: that reading derives "not by works" on the way to its conclusion, and Trent denies it (trent_defeats_apocalyptic).

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

trentAnsweredByPaul

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

Trent, against 'not by works' is not accepted on every resolution.

• A position holding Sola fide from Paul (Galatians 2:16), Luke 7:50: "your faith has saved you", Sola fide from Peter (Acts 15:9–11), Variegated nomism (Gathercole, Carson et al.) can be held, and it holds Sola fide from Paul (Galatians 2:16); Sola fide from Paul (Galatians 2:16) conflicts with Trent, against 'not by works': Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Sola fide from Paul (Galatians 2:16).
• None of Sola fide from Paul (Galatians 2:16), Luke 7:50: "your faith has saved you", Sola fide from Peter (Acts 15:9–11), Variegated nomism (Gathercole, Carson et al.) defeats another, and each attack on them is answered from among them:
  • Trent, against 'not by works' defeats Sola fide from Paul (Galatians 2:16), and Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works'.
  • Apocalyptic reading, against faith as the condition defeats Sola fide from Paul (Galatians 2:16), and Sola fide from Paul (Galatians 2:16) defeats Apocalyptic reading, against faith as the condition.
  • Covenantal nomism (Sanders, Dunn) defeats Sola fide from Paul (Galatians 2:16), and Sola fide from Paul (Galatians 2:16) defeats Covenantal nomism (Sanders, Dunn).
  • Trent, against 'not by works', read as what Paul's word means defeats Sola fide from Paul (Galatians 2:16), and Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works', read as what Paul's word means.
  • Trent, against 'not by works' defeats Luke 7:50: "your faith has saved you", and Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works'.
  • Trent, against 'not by works', read as what Paul's word means defeats Luke 7:50: "your faith has saved you", and Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works', read as what Paul's word means.
  • Trent, against 'not by works' defeats Sola fide from Peter (Acts 15:9–11), and Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works'.
  • Law-observant Luke (Jervell) defeats Sola fide from Peter (Acts 15:9–11), and Sola fide from Peter (Acts 15:9–11) defeats Law-observant Luke (Jervell).
  • Trent, against 'not by works', read as what Paul's word means defeats Sola fide from Peter (Acts 15:9–11), and Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works', read as what Paul's word means.
  • Covenantal nomism (Sanders, Dunn) defeats Variegated nomism (Gathercole, Carson et al.), and Sola fide from Paul (Galatians 2:16) defeats Covenantal nomism (Sanders, Dunn).

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

• Sola fide from Paul (Galatians 2:16), weakest at disputed:
  • πίστις Χριστοῦ in Galatians 2:16 means faith in Christ, not Christ's faithfulness — dunn-once-more-pistis-christou-1991; matlock-detheologizing-2000; Gal 2:16; Rom 3:22; Phil 3:9
  • Second Temple Judaism: in by grace, staying in by works (encoded as a denial, so it ranks disputed) — sanders-paul-palestinian-judaism-1977
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Trent, against 'not by works', weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
• Luke 7:50: "your faith has saved you", weakest at disputed:
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Sola fide from Peter (Acts 15:9–11), weakest at disputed:
  • The yoke refused at Acts 15:10 is the whole law as a condition of salvation — bruce-acts-1988, ad loc. Acts 15:10; Acts 15:10; Gal 5:1; Jas 2:10; das-paul-law-covenant-2001
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Variegated nomism (Gathercole, Carson et al.), weakest at disputed:
  • Second Temple Judaism also held final vindication according to works (encoded as a denial, so it ranks disputed) — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Apocalyptic reading, against faith as the condition, weakest at disputed:
  • πίστις Χριστοῦ is Christ's faithfulness, the means of God's deliverance (encoded as a denial, so it ranks disputed) — campbell-deliverance-god-2009; martyn-galatians-1997, ad loc. Gal 2:16; hays-faith-jesus-christ-2002
  • δικαιοσύνη θεοῦ names God's deliverance in Christ, not a status faith obtains — campbell-deliverance-god-2009; martyn-galatians-1997; Rom 3:21-26
• Covenantal nomism (Sanders, Dunn), weakest at disputed:
  • Second Temple Judaism: in by grace, staying in by works — sanders-paul-palestinian-judaism-1977
  • an inference step — dunn-new-perspective-2005; wright-what-paul-said-1997
• Law-observant Luke (Jervell), weakest at disputed:
  • an inference step — jervell-luke-people-god-1972
• Paul's gospel (Galatians 1), against justification as renewal, weakest at disputed:
  • an inference step — moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1
  • an inference step — westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965
• Paul's word (δικαιόω, by the rule of least meaning), weakest at well supported:
  • In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004
• Trent, against 'not by works', read as what Paul's word means, weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 8; tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; npnf1-05-1887, §On the Spirit and the Letter, ch. 45 (26.45); mcgrath-iustitia-dei-2005
• Romans 4:3–8, on Paul's word (by the rule of least meaning), weakest at well supported:
  • Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

trent_not_forced

Nor is Trent forced. A maximal defensible position holds Paul's case with Luke's and Peter's, and none of them can be held with Trent.

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

apocalypticStandsWithLuke

Why the apocalyptic reading can be defended: it stands with Luke's case, with Peter's, and with the critics, and answers every party that defeats it — Paul, Trent, and Trent read as a claim about Paul's word — itself.

Apocalyptic reading, against faith as the condition is accepted on some resolution.

• A position holding Luke 7:50: "your faith has saved you", Sola fide from Peter (Acts 15:9–11), Apocalyptic reading, against faith as the condition, Variegated nomism (Gathercole, Carson et al.) can be held.
• None of Luke 7:50: "your faith has saved you", Sola fide from Peter (Acts 15:9–11), Apocalyptic reading, against faith as the condition, Variegated nomism (Gathercole, Carson et al.) defeats another, and each attack on them is answered from among them:
  • Trent, against 'not by works' defeats Luke 7:50: "your faith has saved you", and Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works'.
  • Trent, against 'not by works', read as what Paul's word means defeats Luke 7:50: "your faith has saved you", and Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', read as what Paul's word means.
  • Trent, against 'not by works' defeats Sola fide from Peter (Acts 15:9–11), and Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works'.
  • Law-observant Luke (Jervell) defeats Sola fide from Peter (Acts 15:9–11), and Sola fide from Peter (Acts 15:9–11) defeats Law-observant Luke (Jervell).
  • Trent, against 'not by works', read as what Paul's word means defeats Sola fide from Peter (Acts 15:9–11), and Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', read as what Paul's word means.
  • Sola fide from Paul (Galatians 2:16) defeats Apocalyptic reading, against faith as the condition, and Apocalyptic reading, against faith as the condition defeats Sola fide from Paul (Galatians 2:16).
  • Trent, against 'not by works' defeats Apocalyptic reading, against faith as the condition, and Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works'.
  • Trent, against 'not by works', read as what Paul's word means defeats Apocalyptic reading, against faith as the condition, and Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', read as what Paul's word means.
  • Covenantal nomism (Sanders, Dunn) defeats Variegated nomism (Gathercole, Carson et al.), and Variegated nomism (Gathercole, Carson et al.) defeats Covenantal nomism (Sanders, Dunn).

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

• Luke 7:50: "your faith has saved you", weakest at disputed:
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Sola fide from Peter (Acts 15:9–11), weakest at disputed:
  • The yoke refused at Acts 15:10 is the whole law as a condition of salvation — bruce-acts-1988, ad loc. Acts 15:10; Acts 15:10; Gal 5:1; Jas 2:10; das-paul-law-covenant-2001
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Apocalyptic reading, against faith as the condition, weakest at disputed:
  • πίστις Χριστοῦ is Christ's faithfulness, the means of God's deliverance (encoded as a denial, so it ranks disputed) — campbell-deliverance-god-2009; martyn-galatians-1997, ad loc. Gal 2:16; hays-faith-jesus-christ-2002
  • δικαιοσύνη θεοῦ names God's deliverance in Christ, not a status faith obtains — campbell-deliverance-god-2009; martyn-galatians-1997; Rom 3:21-26
• Variegated nomism (Gathercole, Carson et al.), weakest at disputed:
  • Second Temple Judaism also held final vindication according to works (encoded as a denial, so it ranks disputed) — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Sola fide from Paul (Galatians 2:16), weakest at disputed:
  • πίστις Χριστοῦ in Galatians 2:16 means faith in Christ, not Christ's faithfulness — dunn-once-more-pistis-christou-1991; matlock-detheologizing-2000; Gal 2:16; Rom 3:22; Phil 3:9
  • Second Temple Judaism: in by grace, staying in by works (encoded as a denial, so it ranks disputed) — sanders-paul-palestinian-judaism-1977
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Trent, against 'not by works', weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
• Covenantal nomism (Sanders, Dunn), weakest at disputed:
  • Second Temple Judaism: in by grace, staying in by works — sanders-paul-palestinian-judaism-1977
  • an inference step — dunn-new-perspective-2005; wright-what-paul-said-1997
• Law-observant Luke (Jervell), weakest at disputed:
  • an inference step — jervell-luke-people-god-1972
• Paul's gospel (Galatians 1), against justification as renewal, weakest at disputed:
  • an inference step — moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1
  • an inference step — westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965
• Paul's word (δικαιόω, by the rule of least meaning), weakest at well supported:
  • In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004
• Trent, against 'not by works', read as what Paul's word means, weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 8; tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; npnf1-05-1887, §On the Spirit and the Letter, ch. 45 (26.45); mcgrath-iustitia-dei-2005
• Romans 4:3–8, on Paul's word (by the rule of least meaning), weakest at well supported:
  • Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

Why Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', at the level of the claims: whyTheDominicalCaseStandsAgainstTrent.

apocalyptic_defensible

The apocalyptic reading can be defended. Some maximal defensible position holds it, and holds Luke's case and Peter's with it: they claim that faith saves, and the apocalyptic reading grants that, denying only that faith is the condition. Among the Reformed parties its one defeater is Paul, whom it defeats back, over the genitive; Trent, read either way, it defeats back over "not by works".

So the dispute between the Reformed reading and the apocalyptic one is where the literature has it: between Paul and Campbell, over πίστις Χριστοῦ — not between Campbell and Luke.

theorem apocalyptic_defensible : Framework.CredulouslyAccepted
    solaFideDispute.defeats Party.apocalyptic
-- axioms: propext, Classical.choice, Quot.sound

apocalypticAnsweredByPaul

Why the apocalyptic reading is not forced: a defensible position holds Paul, and Paul defeats it.

Apocalyptic reading, against faith as the condition is not accepted on every resolution.

• A position holding Sola fide from Paul (Galatians 2:16), Luke 7:50: "your faith has saved you", Sola fide from Peter (Acts 15:9–11), Variegated nomism (Gathercole, Carson et al.) can be held, and it holds Sola fide from Paul (Galatians 2:16); Sola fide from Paul (Galatians 2:16) conflicts with Apocalyptic reading, against faith as the condition: Sola fide from Paul (Galatians 2:16) defeats Apocalyptic reading, against faith as the condition, and Apocalyptic reading, against faith as the condition defeats Sola fide from Paul (Galatians 2:16).
• None of Sola fide from Paul (Galatians 2:16), Luke 7:50: "your faith has saved you", Sola fide from Peter (Acts 15:9–11), Variegated nomism (Gathercole, Carson et al.) defeats another, and each attack on them is answered from among them:
  • Trent, against 'not by works' defeats Sola fide from Paul (Galatians 2:16), and Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works'.
  • Apocalyptic reading, against faith as the condition defeats Sola fide from Paul (Galatians 2:16), and Sola fide from Paul (Galatians 2:16) defeats Apocalyptic reading, against faith as the condition.
  • Covenantal nomism (Sanders, Dunn) defeats Sola fide from Paul (Galatians 2:16), and Sola fide from Paul (Galatians 2:16) defeats Covenantal nomism (Sanders, Dunn).
  • Trent, against 'not by works', read as what Paul's word means defeats Sola fide from Paul (Galatians 2:16), and Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works', read as what Paul's word means.
  • Trent, against 'not by works' defeats Luke 7:50: "your faith has saved you", and Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works'.
  • Trent, against 'not by works', read as what Paul's word means defeats Luke 7:50: "your faith has saved you", and Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works', read as what Paul's word means.
  • Trent, against 'not by works' defeats Sola fide from Peter (Acts 15:9–11), and Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works'.
  • Law-observant Luke (Jervell) defeats Sola fide from Peter (Acts 15:9–11), and Sola fide from Peter (Acts 15:9–11) defeats Law-observant Luke (Jervell).
  • Trent, against 'not by works', read as what Paul's word means defeats Sola fide from Peter (Acts 15:9–11), and Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works', read as what Paul's word means.
  • Covenantal nomism (Sanders, Dunn) defeats Variegated nomism (Gathercole, Carson et al.), and Sola fide from Paul (Galatians 2:16) defeats Covenantal nomism (Sanders, Dunn).

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

• Sola fide from Paul (Galatians 2:16), weakest at disputed:
  • πίστις Χριστοῦ in Galatians 2:16 means faith in Christ, not Christ's faithfulness — dunn-once-more-pistis-christou-1991; matlock-detheologizing-2000; Gal 2:16; Rom 3:22; Phil 3:9
  • Second Temple Judaism: in by grace, staying in by works (encoded as a denial, so it ranks disputed) — sanders-paul-palestinian-judaism-1977
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Apocalyptic reading, against faith as the condition, weakest at disputed:
  • πίστις Χριστοῦ is Christ's faithfulness, the means of God's deliverance (encoded as a denial, so it ranks disputed) — campbell-deliverance-god-2009; martyn-galatians-1997, ad loc. Gal 2:16; hays-faith-jesus-christ-2002
  • δικαιοσύνη θεοῦ names God's deliverance in Christ, not a status faith obtains — campbell-deliverance-god-2009; martyn-galatians-1997; Rom 3:21-26
• Luke 7:50: "your faith has saved you", weakest at disputed:
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Sola fide from Peter (Acts 15:9–11), weakest at disputed:
  • The yoke refused at Acts 15:10 is the whole law as a condition of salvation — bruce-acts-1988, ad loc. Acts 15:10; Acts 15:10; Gal 5:1; Jas 2:10; das-paul-law-covenant-2001
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Variegated nomism (Gathercole, Carson et al.), weakest at disputed:
  • Second Temple Judaism also held final vindication according to works (encoded as a denial, so it ranks disputed) — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Trent, against 'not by works', weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
• Covenantal nomism (Sanders, Dunn), weakest at disputed:
  • Second Temple Judaism: in by grace, staying in by works — sanders-paul-palestinian-judaism-1977
  • an inference step — dunn-new-perspective-2005; wright-what-paul-said-1997
• Law-observant Luke (Jervell), weakest at disputed:
  • an inference step — jervell-luke-people-god-1972
• Paul's gospel (Galatians 1), against justification as renewal, weakest at disputed:
  • an inference step — moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1
  • an inference step — westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965
• Paul's word (δικαιόω, by the rule of least meaning), weakest at well supported:
  • In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004
• Trent, against 'not by works', read as what Paul's word means, weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 8; tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; npnf1-05-1887, §On the Spirit and the Letter, ch. 45 (26.45); mcgrath-iustitia-dei-2005
• Romans 4:3–8, on Paul's word (by the rule of least meaning), weakest at well supported:
  • Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

apocalyptic_not_forced

Nor is it forced. A maximal defensible position holds Paul's case — faith alone, from Galatians 2:16 read with the objective genitive — and cannot hold the apocalyptic reading with it. Between Paul and Campbell the dispute chooses neither: each is defensible, and neither is forced.

theorem apocalyptic_not_forced : ¬Framework.SkepticallyAccepted
    solaFideDispute.defeats Party.apocalyptic
-- axioms: propext, Classical.choice, Quot.sound

lukeStandsWithPeter

Why Luke's case can be defended: it stands with Peter's, the apocalyptic reading and the critics, and answers both its defeaters — Trent, and Trent read as a claim about Paul's word — itself.

Luke 7:50: "your faith has saved you" is accepted on some resolution.

• A position holding Luke 7:50: "your faith has saved you", Sola fide from Peter (Acts 15:9–11), Apocalyptic reading, against faith as the condition, Variegated nomism (Gathercole, Carson et al.) can be held.
• None of Luke 7:50: "your faith has saved you", Sola fide from Peter (Acts 15:9–11), Apocalyptic reading, against faith as the condition, Variegated nomism (Gathercole, Carson et al.) defeats another, and each attack on them is answered from among them:
  • Trent, against 'not by works' defeats Luke 7:50: "your faith has saved you", and Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works'.
  • Trent, against 'not by works', read as what Paul's word means defeats Luke 7:50: "your faith has saved you", and Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', read as what Paul's word means.
  • Trent, against 'not by works' defeats Sola fide from Peter (Acts 15:9–11), and Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works'.
  • Law-observant Luke (Jervell) defeats Sola fide from Peter (Acts 15:9–11), and Sola fide from Peter (Acts 15:9–11) defeats Law-observant Luke (Jervell).
  • Trent, against 'not by works', read as what Paul's word means defeats Sola fide from Peter (Acts 15:9–11), and Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', read as what Paul's word means.
  • Sola fide from Paul (Galatians 2:16) defeats Apocalyptic reading, against faith as the condition, and Apocalyptic reading, against faith as the condition defeats Sola fide from Paul (Galatians 2:16).
  • Trent, against 'not by works' defeats Apocalyptic reading, against faith as the condition, and Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works'.
  • Trent, against 'not by works', read as what Paul's word means defeats Apocalyptic reading, against faith as the condition, and Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', read as what Paul's word means.
  • Covenantal nomism (Sanders, Dunn) defeats Variegated nomism (Gathercole, Carson et al.), and Variegated nomism (Gathercole, Carson et al.) defeats Covenantal nomism (Sanders, Dunn).

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

• Luke 7:50: "your faith has saved you", weakest at disputed:
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Sola fide from Peter (Acts 15:9–11), weakest at disputed:
  • The yoke refused at Acts 15:10 is the whole law as a condition of salvation — bruce-acts-1988, ad loc. Acts 15:10; Acts 15:10; Gal 5:1; Jas 2:10; das-paul-law-covenant-2001
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Apocalyptic reading, against faith as the condition, weakest at disputed:
  • πίστις Χριστοῦ is Christ's faithfulness, the means of God's deliverance (encoded as a denial, so it ranks disputed) — campbell-deliverance-god-2009; martyn-galatians-1997, ad loc. Gal 2:16; hays-faith-jesus-christ-2002
  • δικαιοσύνη θεοῦ names God's deliverance in Christ, not a status faith obtains — campbell-deliverance-god-2009; martyn-galatians-1997; Rom 3:21-26
• Variegated nomism (Gathercole, Carson et al.), weakest at disputed:
  • Second Temple Judaism also held final vindication according to works (encoded as a denial, so it ranks disputed) — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Sola fide from Paul (Galatians 2:16), weakest at disputed:
  • πίστις Χριστοῦ in Galatians 2:16 means faith in Christ, not Christ's faithfulness — dunn-once-more-pistis-christou-1991; matlock-detheologizing-2000; Gal 2:16; Rom 3:22; Phil 3:9
  • Second Temple Judaism: in by grace, staying in by works (encoded as a denial, so it ranks disputed) — sanders-paul-palestinian-judaism-1977
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Trent, against 'not by works', weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
• Covenantal nomism (Sanders, Dunn), weakest at disputed:
  • Second Temple Judaism: in by grace, staying in by works — sanders-paul-palestinian-judaism-1977
  • an inference step — dunn-new-perspective-2005; wright-what-paul-said-1997
• Law-observant Luke (Jervell), weakest at disputed:
  • an inference step — jervell-luke-people-god-1972
• Paul's gospel (Galatians 1), against justification as renewal, weakest at disputed:
  • an inference step — moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1
  • an inference step — westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965
• Paul's word (δικαιόω, by the rule of least meaning), weakest at well supported:
  • In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004
• Trent, against 'not by works', read as what Paul's word means, weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 8; tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; npnf1-05-1887, §On the Spirit and the Letter, ch. 45 (26.45); mcgrath-iustitia-dei-2005
• Romans 4:3–8, on Paul's word (by the rule of least meaning), weakest at well supported:
  • Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

Why Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', at the level of the claims: whyTheDominicalCaseStandsAgainstTrent.

dominical_case_defensible

Luke's case can be defended. "Your faith has saved you", read as Luke says it, stands in six of the dispute's eight maximal defensible positions. Its only defeater is Trent, read or unread, over what justification is: Trent's definition denies that faith without charity suffices, and Luke's words say her faith saved her. It defeats Trent back, and conflicts with no other party.

theorem dominical_case_defensible : Framework.CredulouslyAccepted
    solaFideDispute.defeats Party.dominical
-- axioms: propext, Classical.choice, Quot.sound

lukeAnsweredByTrent

Why Luke's case is not forced: a defensible position holds Trent, and Trent defeats it.

Luke 7:50: "your faith has saved you" is not accepted on every resolution.

• A position holding Trent, against 'not by works', Covenantal nomism (Sanders, Dunn), Law-observant Luke (Jervell) can be held, and it holds Trent, against 'not by works'; Trent, against 'not by works' conflicts with Luke 7:50: "your faith has saved you": Trent, against 'not by works' defeats Luke 7:50: "your faith has saved you", and Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works'.
• None of Trent, against 'not by works', Covenantal nomism (Sanders, Dunn), Law-observant Luke (Jervell) defeats another, and each attack on them is answered from among them:
  • Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Sola fide from Paul (Galatians 2:16).
  • Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Luke 7:50: "your faith has saved you".
  • Sola fide from Peter (Acts 15:9–11) defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Sola fide from Peter (Acts 15:9–11).
  • Apocalyptic reading, against faith as the condition defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Apocalyptic reading, against faith as the condition.
  • Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Paul's gospel (Galatians 1), against justification as renewal.
  • Sola fide from Paul (Galatians 2:16) defeats Covenantal nomism (Sanders, Dunn), and Trent, against 'not by works' defeats Sola fide from Paul (Galatians 2:16).
  • Variegated nomism (Gathercole, Carson et al.) defeats Covenantal nomism (Sanders, Dunn), and Covenantal nomism (Sanders, Dunn) defeats Variegated nomism (Gathercole, Carson et al.).
  • Sola fide from Peter (Acts 15:9–11) defeats Law-observant Luke (Jervell), and Trent, against 'not by works' defeats Sola fide from Peter (Acts 15:9–11).

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

• Trent, against 'not by works', weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
• Luke 7:50: "your faith has saved you", weakest at disputed:
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Covenantal nomism (Sanders, Dunn), weakest at disputed:
  • Second Temple Judaism: in by grace, staying in by works — sanders-paul-palestinian-judaism-1977
  • an inference step — dunn-new-perspective-2005; wright-what-paul-said-1997
• Law-observant Luke (Jervell), weakest at disputed:
  • an inference step — jervell-luke-people-god-1972
• Sola fide from Paul (Galatians 2:16), weakest at disputed:
  • πίστις Χριστοῦ in Galatians 2:16 means faith in Christ, not Christ's faithfulness — dunn-once-more-pistis-christou-1991; matlock-detheologizing-2000; Gal 2:16; Rom 3:22; Phil 3:9
  • Second Temple Judaism: in by grace, staying in by works (encoded as a denial, so it ranks disputed) — sanders-paul-palestinian-judaism-1977
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Sola fide from Peter (Acts 15:9–11), weakest at disputed:
  • The yoke refused at Acts 15:10 is the whole law as a condition of salvation — bruce-acts-1988, ad loc. Acts 15:10; Acts 15:10; Gal 5:1; Jas 2:10; das-paul-law-covenant-2001
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Apocalyptic reading, against faith as the condition, weakest at disputed:
  • πίστις Χριστοῦ is Christ's faithfulness, the means of God's deliverance (encoded as a denial, so it ranks disputed) — campbell-deliverance-god-2009; martyn-galatians-1997, ad loc. Gal 2:16; hays-faith-jesus-christ-2002
  • δικαιοσύνη θεοῦ names God's deliverance in Christ, not a status faith obtains — campbell-deliverance-god-2009; martyn-galatians-1997; Rom 3:21-26
• Variegated nomism (Gathercole, Carson et al.), weakest at disputed:
  • Second Temple Judaism also held final vindication according to works (encoded as a denial, so it ranks disputed) — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Paul's gospel (Galatians 1), against justification as renewal, weakest at disputed:
  • an inference step — moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1
  • an inference step — westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965
• Paul's word (δικαιόω, by the rule of least meaning), weakest at well supported:
  • In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004
• Trent, against 'not by works', read as what Paul's word means, weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 8; tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; npnf1-05-1887, §On the Spirit and the Letter, ch. 45 (26.45); mcgrath-iustitia-dei-2005
• Romans 4:3–8, on Paul's word (by the rule of least meaning), weakest at well supported:
  • Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

Why Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', at the level of the claims: whyTheDominicalCaseStandsAgainstTrent.

Why Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works', at the level of the claims: whereTrentPartsFromPaul.

dominical_case_not_forced

Nor is it forced. A maximal defensible position holds Trent, and cannot hold Luke's case with it.

This is the dispute's verdict, stated plainly: between Trent and each Reformed party, the dispute chooses neither. Their weakest links are all disputed, so no rating breaks a tie, and every attack between Trent and the Reformed readings runs both ways. What decides between them is what justification is — and that is argued, not weighed: whyTheDominicalCaseStandsAgainstTrent locates Luke's disagreement with Trent at Trent's definition, and whereTrentPartsFromPaul (Gospel.lean) locates Paul's at one step, that a verdict on a finished work excludes the renewal wrought in us. The one thing the ratings do decide is that Trent cannot claim its definition as the meaning of Paul's word (trent_on_pauls_word_indefensible).

theorem dominical_case_not_forced : ¬Framework.SkepticallyAccepted
    solaFideDispute.defeats Party.dominical
-- axioms: propext, Classical.choice, Quot.sound

gospelStandsWithTheStrands

Why Paul's gospel can be defended: it stands with Paul's case, Luke's, Peter's, the critics and Paul's word, and answers both parties that defeat it — Trent, and Trent read as a claim about Paul's word — itself.

Paul's gospel (Galatians 1), against justification as renewal is accepted on some resolution.

• A position holding Paul's gospel (Galatians 1), against justification as renewal, Sola fide from Paul (Galatians 2:16), Luke 7:50: "your faith has saved you", Sola fide from Peter (Acts 15:9–11), Variegated nomism (Gathercole, Carson et al.), Paul's word (δικαιόω, by the rule of least meaning) can be held.
• None of Paul's gospel (Galatians 1), against justification as renewal, Sola fide from Paul (Galatians 2:16), Luke 7:50: "your faith has saved you", Sola fide from Peter (Acts 15:9–11), Variegated nomism (Gathercole, Carson et al.), Paul's word (δικαιόω, by the rule of least meaning) defeats another, and each attack on them is answered from among them:
  • Trent, against 'not by works' defeats Paul's gospel (Galatians 1), against justification as renewal, and Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works'.
  • Trent, against 'not by works', read as what Paul's word means defeats Paul's gospel (Galatians 1), against justification as renewal, and Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works', read as what Paul's word means.
  • Trent, against 'not by works' defeats Sola fide from Paul (Galatians 2:16), and Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works'.
  • Apocalyptic reading, against faith as the condition defeats Sola fide from Paul (Galatians 2:16), and Sola fide from Paul (Galatians 2:16) defeats Apocalyptic reading, against faith as the condition.
  • Covenantal nomism (Sanders, Dunn) defeats Sola fide from Paul (Galatians 2:16), and Sola fide from Paul (Galatians 2:16) defeats Covenantal nomism (Sanders, Dunn).
  • Trent, against 'not by works', read as what Paul's word means defeats Sola fide from Paul (Galatians 2:16), and Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works', read as what Paul's word means.
  • Trent, against 'not by works' defeats Luke 7:50: "your faith has saved you", and Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works'.
  • Trent, against 'not by works', read as what Paul's word means defeats Luke 7:50: "your faith has saved you", and Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works', read as what Paul's word means.
  • Trent, against 'not by works' defeats Sola fide from Peter (Acts 15:9–11), and Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works'.
  • Law-observant Luke (Jervell) defeats Sola fide from Peter (Acts 15:9–11), and Sola fide from Peter (Acts 15:9–11) defeats Law-observant Luke (Jervell).
  • Trent, against 'not by works', read as what Paul's word means defeats Sola fide from Peter (Acts 15:9–11), and Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works', read as what Paul's word means.
  • Covenantal nomism (Sanders, Dunn) defeats Variegated nomism (Gathercole, Carson et al.), and Sola fide from Paul (Galatians 2:16) defeats Covenantal nomism (Sanders, Dunn).

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

• Paul's gospel (Galatians 1), against justification as renewal, weakest at disputed:
  • an inference step — moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1
  • an inference step — westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965
• Sola fide from Paul (Galatians 2:16), weakest at disputed:
  • πίστις Χριστοῦ in Galatians 2:16 means faith in Christ, not Christ's faithfulness — dunn-once-more-pistis-christou-1991; matlock-detheologizing-2000; Gal 2:16; Rom 3:22; Phil 3:9
  • Second Temple Judaism: in by grace, staying in by works (encoded as a denial, so it ranks disputed) — sanders-paul-palestinian-judaism-1977
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Luke 7:50: "your faith has saved you", weakest at disputed:
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Sola fide from Peter (Acts 15:9–11), weakest at disputed:
  • The yoke refused at Acts 15:10 is the whole law as a condition of salvation — bruce-acts-1988, ad loc. Acts 15:10; Acts 15:10; Gal 5:1; Jas 2:10; das-paul-law-covenant-2001
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Variegated nomism (Gathercole, Carson et al.), weakest at disputed:
  • Second Temple Judaism also held final vindication according to works (encoded as a denial, so it ranks disputed) — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Paul's word (δικαιόω, by the rule of least meaning), weakest at well supported:
  • In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004
• Trent, against 'not by works', weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
• Apocalyptic reading, against faith as the condition, weakest at disputed:
  • πίστις Χριστοῦ is Christ's faithfulness, the means of God's deliverance (encoded as a denial, so it ranks disputed) — campbell-deliverance-god-2009; martyn-galatians-1997, ad loc. Gal 2:16; hays-faith-jesus-christ-2002
  • δικαιοσύνη θεοῦ names God's deliverance in Christ, not a status faith obtains — campbell-deliverance-god-2009; martyn-galatians-1997; Rom 3:21-26
• Covenantal nomism (Sanders, Dunn), weakest at disputed:
  • Second Temple Judaism: in by grace, staying in by works — sanders-paul-palestinian-judaism-1977
  • an inference step — dunn-new-perspective-2005; wright-what-paul-said-1997
• Law-observant Luke (Jervell), weakest at disputed:
  • an inference step — jervell-luke-people-god-1972
• Trent, against 'not by works', read as what Paul's word means, weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 8; tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; npnf1-05-1887, §On the Spirit and the Letter, ch. 45 (26.45); mcgrath-iustitia-dei-2005
• Romans 4:3–8, on Paul's word (by the rule of least meaning), weakest at well supported:
  • Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

Why Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works', at the level of the claims: whereTrentPartsFromPaul.

gospel_defensible

Paul's gospel can be defended, with every Reformed strand and with Paul's word: some maximal defensible position holds them all.

theorem gospel_defensible : Framework.CredulouslyAccepted
    solaFideDispute.defeats Party.gospel
-- axioms: propext, Classical.choice, Quot.sound

gospelAnsweredByTrent

Why Paul's gospel is not forced: a defensible position holds Trent, and Trent defeats it.

Paul's gospel (Galatians 1), against justification as renewal is not accepted on every resolution.

• A position holding Trent, against 'not by works', Covenantal nomism (Sanders, Dunn), Law-observant Luke (Jervell) can be held, and it holds Trent, against 'not by works'; Trent, against 'not by works' conflicts with Paul's gospel (Galatians 1), against justification as renewal: Trent, against 'not by works' defeats Paul's gospel (Galatians 1), against justification as renewal, and Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works'.
• None of Trent, against 'not by works', Covenantal nomism (Sanders, Dunn), Law-observant Luke (Jervell) defeats another, and each attack on them is answered from among them:
  • Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Sola fide from Paul (Galatians 2:16).
  • Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Luke 7:50: "your faith has saved you".
  • Sola fide from Peter (Acts 15:9–11) defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Sola fide from Peter (Acts 15:9–11).
  • Apocalyptic reading, against faith as the condition defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Apocalyptic reading, against faith as the condition.
  • Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works', and Trent, against 'not by works' defeats Paul's gospel (Galatians 1), against justification as renewal.
  • Sola fide from Paul (Galatians 2:16) defeats Covenantal nomism (Sanders, Dunn), and Trent, against 'not by works' defeats Sola fide from Paul (Galatians 2:16).
  • Variegated nomism (Gathercole, Carson et al.) defeats Covenantal nomism (Sanders, Dunn), and Covenantal nomism (Sanders, Dunn) defeats Variegated nomism (Gathercole, Carson et al.).
  • Sola fide from Peter (Acts 15:9–11) defeats Law-observant Luke (Jervell), and Trent, against 'not by works' defeats Sola fide from Peter (Acts 15:9–11).

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

• Trent, against 'not by works', weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
• Paul's gospel (Galatians 1), against justification as renewal, weakest at disputed:
  • an inference step — moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1
  • an inference step — westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965
• Covenantal nomism (Sanders, Dunn), weakest at disputed:
  • Second Temple Judaism: in by grace, staying in by works — sanders-paul-palestinian-judaism-1977
  • an inference step — dunn-new-perspective-2005; wright-what-paul-said-1997
• Law-observant Luke (Jervell), weakest at disputed:
  • an inference step — jervell-luke-people-god-1972
• Sola fide from Paul (Galatians 2:16), weakest at disputed:
  • πίστις Χριστοῦ in Galatians 2:16 means faith in Christ, not Christ's faithfulness — dunn-once-more-pistis-christou-1991; matlock-detheologizing-2000; Gal 2:16; Rom 3:22; Phil 3:9
  • Second Temple Judaism: in by grace, staying in by works (encoded as a denial, so it ranks disputed) — sanders-paul-palestinian-judaism-1977
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Luke 7:50: "your faith has saved you", weakest at disputed:
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Sola fide from Peter (Acts 15:9–11), weakest at disputed:
  • The yoke refused at Acts 15:10 is the whole law as a condition of salvation — bruce-acts-1988, ad loc. Acts 15:10; Acts 15:10; Gal 5:1; Jas 2:10; das-paul-law-covenant-2001
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Apocalyptic reading, against faith as the condition, weakest at disputed:
  • πίστις Χριστοῦ is Christ's faithfulness, the means of God's deliverance (encoded as a denial, so it ranks disputed) — campbell-deliverance-god-2009; martyn-galatians-1997, ad loc. Gal 2:16; hays-faith-jesus-christ-2002
  • δικαιοσύνη θεοῦ names God's deliverance in Christ, not a status faith obtains — campbell-deliverance-god-2009; martyn-galatians-1997; Rom 3:21-26
• Variegated nomism (Gathercole, Carson et al.), weakest at disputed:
  • Second Temple Judaism also held final vindication according to works (encoded as a denial, so it ranks disputed) — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Paul's word (δικαιόω, by the rule of least meaning), weakest at well supported:
  • In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004
• Trent, against 'not by works', read as what Paul's word means, weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 8; tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; npnf1-05-1887, §On the Spirit and the Letter, ch. 45 (26.45); mcgrath-iustitia-dei-2005
• Romans 4:3–8, on Paul's word (by the rule of least meaning), weakest at well supported:
  • Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004

Why Paul's gospel (Galatians 1), against justification as renewal defeats Trent, against 'not by works', at the level of the claims: whereTrentPartsFromPaul.

Why Luke 7:50: "your faith has saved you" defeats Trent, against 'not by works', at the level of the claims: whyTheDominicalCaseStandsAgainstTrent.

gospel_not_forced

Nor is it forced. Trent, as Trent states it — tied to neither reading of its definition — is still defensible, and Paul's gospel cannot be held with it. What decides between them is the step whereTrentPartsFromPaul names — that a verdict on a finished work excludes renewal — and it is rated disputed. The lexical case does not decide it: read as a claim about what God does, Trent's definition is not reached by anything Paul's word says (lexical_case_does_not_reach_what_god_does).

theorem gospel_not_forced : ¬Framework.SkepticallyAccepted
    solaFideDispute.defeats Party.gospel
-- axioms: propext, Classical.choice, Quot.sound

Why Luke's case stands against Trent

The verdicts above say that Luke's case and Trent defeat each other, and that the dispute chooses neither. This says why, at the level of the claims. The two part over what justification is: Trent defines it as the renewal of the inward man by infused charity, and from that definition it follows that faith without charity does not suffice. Luke's words say that her faith saved her.

whyTheDominicalCaseStandsAgainstTrent

Why Luke's case stands against Trent. The crux is Luke's own step: from "your faith has saved you", with σῴζω as salvation and her love as the evidence of forgiveness, to faith's sufficiency. Trent cannot hold it with Luke's words: its definition of justification as the renewal of the inward man (Session VI, ch. 7), with the step from that definition to denying that faith suffices (canon 9), contradicts it — and both are needed. Nothing else in Trent's case does: not its account of merit, not its reading of works.

So the disagreement is not about what Luke says. It is about what justification is. Grant Trent's definition, and "your faith has saved you" cannot mean that faith sufficed; grant that it did, and Trent's definition cannot stand.

Why Luke 7:50: "your faith has saved you" stands against Trent, against 'not by works'.

• The crux: \((P_{17} \land P_{18} \land P_{19}) \rightarrow P_{26}\), a premise of Luke 7:50: "your faith has saved you".
• What it does: its conclusion does not follow without it.
• Granted: \(P_{17}\), \(P_{18}\), \(P_{19}\), which the break also needs.
• Where the rival breaks: \(P_{33}\), \(P_{33} \rightarrow \lnot P_{26}\) cannot be held together with \((P_{17} \land P_{18} \land P_{19}) \rightarrow P_{26}\) and \(P_{17}\), \(P_{18}\), \(P_{19}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{17}\) Luke 7:50 — Jesus says ‘your faith has saved you’ after declaring sins forgiven — consensus: Luke 7:50; marshall-luke-1978, ad loc. Luke 7:50
  • \(P_{18}\) σῴζω in Luke 7:50 denotes salvation, not physical healing — well supported: kolb-wengert-book-of-concord-2000, §Apology IV, on love and the fulfilling of the law: Luke 7:47–50; padilla-narrative-criticism-2021, pp. 54–55; Luke 7:47-50; marshall-luke-1978, ad loc. Luke 7:50
  • \(P_{19}\) Luke 7:47 — her love is the evidence of her forgiveness, not its ground — plausible: padilla-narrative-criticism-2021, pp. 54–54; kolb-wengert-book-of-concord-2000, §Apology IV, on love and the fulfilling of the law: Luke 7:47–50; Luke 7:41-43; Luke 7:47; Luke 7:47-50
  • the step itself — disputed: tanner-decrees-1990, §Trent, Session VI (1547), canon 9

TestimonyArguments.SolaFide.Johannine — "this is the work of God, that you believe"

A fourth strand for sola fide, from John's Gospel, encoded on its own. Asked what they must do "to be doing the works of God", the crowd is told: "This is the work of God, that you believe in him whom he has sent" (John 6:28–29). The question of works is put to Jesus in terms, and he answers with believing. The Gospel says the same throughout: eternal life, and passing out of judgement, through believing in the Son (3:16–18, 3:36, 5:24), and it states its own purpose in those terms (20:31).

The hinge: what believing is

Both sides grant the verse. What divides them is what its believing is.

• Calvin reads it as trust. Christ calls faith a work only improperly: faith "brings nothing to God, but, on the contrary, places man before God as empty and poor, that he may be filled with Christ", and "bestows on man no other righteousness than that which he receives from Christ". It is "a passive work, to which no reward can be paid".
• Aquinas reads it as faith formed by charity. Paul distinguishes faith "only from external works"; to believe in him (in illum), as one's end, "is proper to faith living through the love of charity", and faith so living "is the principle of all our good works" (Super Ioannem 6, lect. 3, n. 901). That is Trent's account of justifying faith (Session VI, ch. 7): faith without hope and charity "neither unites man perfectly with Christ, nor makes him a living member of His body".

So the strand has the same shape as the others: shared texts, and a reading on which everything turns. Grant Aquinas his reading and the texts no longer deliver faith alone (johannine_strand_rests_on_believing_as_trust).

John has no word for justification

δικαιόω does not occur in John. The strand's step therefore runs from eternal life through believing to justification by faith alone, and that is an inference, not a reading of a word. It is cited to Calvin, whose comment on 6:29 speaks of the righteousness faith receives from Christ, and rated plausible: no cited source grants the strand's grounds and denies that step, but none argues the bridge from John's vocabulary to Paul's at length either.

Luther's answer, from Galatians 3

Aquinas's reading is not left standing unanswered. Luther meets it head-on in his lectures on Galatians. At 3:11: "The scholastics misconstrue this passage by saying: 'The just shall live by faith, if it is a working faith, or a faith formed and performed by charitable works.' … To speak of formed or unformed faith, a sort of double faith, is contrary to the Scriptures." At 3:12: "Does not the Law command charity? … If the law requires charity, charity is part of the Law and not of faith." So a faith that justifies because charity forms it justifies by the law after all — and "the law is not of faith" (Galatians 3:12).

The argument is encoded as a line of its own (lutherLine). Its grounds are both things Aquinas grants: the text of Galatians 3:11–12, and that love of God and neighbour is what the law commands (Deuteronomy 6:5). Its step is Luther's: from those, the believing that justifies is not faith formed by charity. Granted the step, Aquinas's reading of John 6:29 falls (luther_answers_aquinas_from_galatians). But the step is the whole of the answer: the texts alone do not exclude his reading (luther_answer_rests_on_his_step), and the step is rated disputed, because Aquinas grants both of its grounds and denies its conclusion. Nor does removing Aquinas's reading establish Calvin's: that the believing of 6:29 is not formed by charity is weaker than that it is trust.

Calvin makes the neighbouring argument in the Institutes (III.xi.19), which the library already cites for worksOfLawMeansWorksGenerally: against those who "pretend that the works excluded are ceremonial, not moral works", he cites Galatians 3:10 and 3:12 — the curse on everyone who does not continue in all that the law commands — and concludes that "the whole Law is spoken of when the power of justifying is denied to it". Aquinas's distinction is between external and inward works rather than ceremonial and moral ones, so it is Luther's argument on 3:11–12, not Calvin's, that meets him directly.

The Catholic reply rests on Galatians 5:6, "faith working through love", which Trent cites (Session VI, ch. 7). How Luther and Calvin read that verse is not yet encoded.

What is not yet done

The strand is encoded alone, as a package of its own. It is not yet part of reformed or of the sola fide dispute, and that is deliberate. Adding a fourth strand to reformed changes the joint results — no premise removed from the other three strands defeats sola fide while John's strand stands — and a Johannine party in Dispute.lean changes the defeat table. Both are the next step, tracked in issue #86, and every statement elsewhere that sola fide "runs on three strands" remains true of reformed until then.

Nor does it encode the obedience reading of 3:36, where the opposite of the one who believes is the one who "does not obey" (ἀπειθῶν): no source arguing that Johannine faith therefore includes obedience has been verified yet.

The lines

calvinOnJohnSix

Calvin's step from John to justification. John has no δικαιόω, so the bridge from eternal life through believing to justification by faith alone is an inference of its own. Rated plausible: no cited source grants the strand's grounds and denies the step, but the bridge rests on Calvin's comment rather than on an argument from John's vocabulary.

def calvinOnJohnSix : Source :=
  { primary := Reference.work calvinJohn (Bib.Locus.adLoc Scripture.john6_29),
    tradition := Tradition.reformedProtestant,
    confidence := Confidence.plausible }

aquinasOnFormedFaith

Aquinas's step: faith living through charity is not bare trust. Rated consensus: Calvin concedes it — his trust is precisely a faith that brings nothing — and the two divide over the premise, not the inference.

def aquinasOnFormedFaith : Source :=
  {
    primary :=
      Reference.work aquinasJohn
        (Bib.Locus.sectionRef "cap. 6, lect. 3, n. 901"),
    tradition := Tradition.romanCatholic, confidence := Confidence.consensus }

johannineToFaithAlone

The Johannine strand. From the work God requires (6:28–29), and eternal life through believing (3:16–18, 3:36, 5:24, 20:31), to justification by faith alone — by way of the reading of that believing as trust.

johannineLine — Johannine strand (John 6:29)

The Johannine line. Its texts are its own grounds, not shared prooftexts, because the strand is not yet part of reformed.

thomistLine — Faith formed by charity (Aquinas on John 6:29)

Aquinas's line. The believing of 6:29 is faith living through charity, and so not the bare trust the strand needs. The denial is derived, not assumed: it follows from Aquinas's own reading of the verse.

The packages

johannineCase — Sola fide from John (6:28–29)

Sola fide from John alone: the Johannine line, with the grounds and closing steps every Reformed strand shares.

Grounded in scripture alone: John 3:16–18, 3:36, 5:24, 20:31 — eternal life through believing in the Son.

thomistOnJohn — Aquinas on John 6:29 (faith formed by charity)

Aquinas on John: every text the Johannine strand reads, and every shared ground, with its believing read as faith formed by charity. The rival the strand is written against.

Grounded in scripture alone: John 3:16–18, 3:36, 5:24, 20:31 — eternal life through believing in the Son.

Results

johannine_strand_establishes

John alone delivers sola fide. Grant that the believing of 6:29 is trust, and the work God requires is no work at all: sola fide follows from John without Paul, Luke or Acts.

theorem johannine_strand_establishes : Establishes johannineCase
-- axioms: propext, Quot.sound

thomistReading

Aquinas's world: every text holds, and the believing of 6:29 is faith living through charity — so not bare trust, not faith alone, and faith without charity does not suffice. Grace and "not by works" still hold: Aquinas excludes external works, and grants that faith is God's gift.

def thomistReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.johannineBelievingIsTrust => False
    | Claim.justificationByFaithAlone => False
    | Claim.faithIsSufficient => False
    | Claim.salvationThroughFaith => False
    | x => True

johannine_strand_rests_on_believing_as_trust

The Johannine strand rests on believing as trust. Grant Aquinas every text the strand reads, and read their believing as he does — faith living through charity — and sola fide no longer follows. So John's Gospel, like Paul's Galatians and Luke's σῴζω, carries the conclusion only through a reading: here, of what it is to believe in him.

theorem johannine_strand_rests_on_believing_as_trust : ¬Establishes
    thomistOnJohn
-- axioms: propext, Quot.sound

johannineCase_is_satisfiable

The Johannine case has a model, so johannine_strand_establishes is not vacuous.

theorem johannineCase_is_satisfiable : Satisfiable johannineCase.premises
-- axioms: propext, Quot.sound

Luther's answer

lutherOnGalatiansThree

Luther's step, on Galatians 3:11–12: the law commands charity, and the law is not of faith, so faith formed by charity would justify by the law. Rated disputed: Aquinas grants both grounds — the text, and that the law commands love — and denies the conclusion, holding that justifying faith is formed by charity.

def lutherOnGalatiansThree : Source :=
  {
    primary :=
      Reference.work lutherGalatians
        (Bib.Locus.adLoc { book := Book.galatians, chapter := 3, verse := 12 }),
    supporting :=
      [Reference.work lutherGalatians
          (Bib.Locus.adLoc
            { book := Book.galatians, chapter := 3, verse := 11 })],
    tradition := Tradition.reformedProtestant,
    confidence := Confidence.disputed }

lutherLine — Luther on Galatians 3:11–12 (against faith formed by charity)

Luther's line. From Galatians 3:11–12 and the law's command of love to the denial of Aquinas's reading: the believing that justifies is not faith formed by charity, since charity is what the law commands and the law is not of faith.

lutherOnGalatians — Luther on Galatians 3:11–12 (against faith formed by charity)

Luther's answer to Aquinas as an argument: what Aquinas grants, with Luther's step, against the reading of 6:29 as faith formed by charity.

No premise here rests on scripture alone.

galatiansTextsAlone — Galatians 3:11–12 and the law's command of love, without Luther's step

The same grounds without Luther's step: Galatians 3:11–12, and that the law commands love.

No premise here rests on scripture alone.

luther_answers_aquinas_from_galatians

Luther answers Aquinas from Galatians 3. Grant what Aquinas grants — Galatians 3:11–12, and that the law commands love — and Luther's step, and the believing of John 6:29 is not faith formed by charity: a faith that justified because charity formed it would justify by the law, and the law is not of faith. What this removes is Aquinas's reading; it does not by itself establish Calvin's.

theorem luther_answers_aquinas_from_galatians : Establishes lutherOnGalatians
-- axioms: propext, Quot.sound

luther_answer_rests_on_his_step

Luther's answer rests on his step. The texts alone do not exclude Aquinas's reading: in Aquinas's world Galatians 3:11–12 holds, the law commands love, and the believing of 6:29 is faith formed by charity. What decides it is whether faith formed by charity counts as justification "by the law" — Luther's step, which Aquinas denies.

theorem luther_answer_rests_on_his_step : ¬Establishes galatiansTextsAlone
-- axioms: propext, Quot.sound

lutherReading

The Reformed world, in which the believing of John 6:29 is not faith formed by charity, and everything else holds.

def lutherReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.johannineBelievingIsFormedByCharity => False
    | x => True

lutherOnGalatians_is_satisfiable

Luther's package has a model, so luther_answers_aquinas_from_galatians is not vacuous.

theorem lutherOnGalatians_is_satisfiable : Satisfiable
    lutherOnGalatians.premises
-- axioms: propext, Quot.sound

whyLutherAnswersAquinas

Why Luther's answer stands against Aquinas. The crux is Luther's step: from Galatians 3:11–12 and the law's command of love, the believing that justifies is not faith formed by charity. With the two texts granted, Aquinas's reading of John 6:29 cannot keep its one distinctive ground — that the believing is formed by charity — and that ground alone breaks.

Unlike the Reformed distinction against Trent, this crux is part of Luther's case: without the step, the texts do not deliver his conclusion. So the answer is exactly as strong as the step, which is rated disputed — the step is Luther's, and the texts are granted by both sides.

Why Luther on Galatians 3:11–12 (against faith formed by charity) stands against Aquinas on John 6:29 (faith formed by charity).

• The crux: \((P_{40} \land P_{41}) \rightarrow \lnot P_{39}\), a premise of Luther on Galatians 3:11–12 (against faith formed by charity).
• What it does: its conclusion does not follow without it.
• Granted: \(P_{40}\), \(P_{41}\), which the break also needs.
• Where the rival breaks: \(P_{39}\) cannot be held together with \((P_{40} \land P_{41}) \rightarrow \lnot P_{39}\) and \(P_{40}\), \(P_{41}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{40}\) Galatians 3:11–12 — none is justified by the law; the law is not of faith — consensus: Gal 3:11-12; luther-commentary-galatians-1998, ad loc. Gal 3:11
  • \(P_{41}\) Love of God and neighbour is what the law commands — consensus: Deut 6:5; Matt 22:37-40; luther-commentary-galatians-1998, ad loc. Gal 3:12
  • the step itself — disputed: luther-commentary-galatians-1998, ad loc. Gal 3:12; luther-commentary-galatians-1998, ad loc. Gal 3:11

TestimonyArguments.SolaFide.Hearings — the same dispute, asked two narrower questions

A dispute answers the question it is asked, and the full sola fide dispute asks a crowded one: the Reformers, Trent, and three modern schools of Pauline scholarship at once. A reader usually wants something narrower. Two questions come up again and again, and each is answered here by hearing the same dispute with some of its parties set aside. Nothing is re-argued: a hearing keeps every defeat the full dispute proved, and only leaves some parties unheard.

What did the Reformation itself decide? The sixteenth-century dispute was Rome and the Reformers, before anyone had proposed a New Perspective on Paul or an apocalyptic reading of him. Heard that way (reformationAlone) — the sixteenth-century positions, argued with the modern evidence cited for each, so Joos, Silva and Barr among them — one thing is forced: Paul's word — δικαιόω does not denote the renewal of the inward man — by both routes, lexical and exegetical. So Trent cannot claim that its definition is what Paul's word means; that reading cannot be defended. What breaks is not Augustine's gloss — that he glossed the word so is not in question — but the step from a Latin gloss to what the Greek word denotes. But Trent's definition read as a claim about what God does is not touched by anything about the word, and there Trent and the Reformers tie: each defeats the other, and the ratings, all disputed, cannot choose between them. The Reformation dispute, heard on its own, comes down to what justification is — the question whatTrentsDefinitionClaims locates.

If Trent were not heard, would Scripture establish sola fide? It is a natural question for a Protestant reader, and the answer is more interesting than yes. Heard without Trent (withoutTrent), four things are forced: Paul's word, by both routes; Paul's gospel — justification is not the renewal of the inward man; and Luke's "your faith has saved you" — faith suffices. But sola fide itself, faith alone, is still not forced, from Paul or from Peter. What stops it is not Rome. It is three disputes inside modern Pauline scholarship:

• Campbell's apocalyptic reading takes πίστις Χριστοῦ as Christ's own faithfulness, and meets Paul over the genitive;
• Sanders and Dunn read ἔργα νόμου as Israel's boundary markers, and the critics who answer them are answered back;
• Jervell reads the yoke of Acts 15 as something other than the law as a condition of salvation, and meets Peter's case.

Each of those is a question about what a text says, and each is where the literature has it. Setting Rome aside does not make them go away.

Augustine stays where the full dispute has him. In the Reformation hearing he is the ground Trent's reading of Paul's word rests on; without Trent, his gloss goes with that reading, since nothing else rests on it. In both, he remains the cited reader who grants Romans 4:5–8 and reads it the other way, which is why Paul's step from Romans 4 is rated disputed. The library does not remove a reader because it judges him mistaken; it shows where his reading breaks, and where it does not.

The Reformation dispute, on its own

reformationAlone

The parties of the sixteenth-century dispute: the three Reformed strands, Paul's gospel, Paul's word by both routes, and Trent, read and unread. Not heard: the apocalyptic reading, Sanders and his critics, and Jervell.

def reformationAlone : Dispute Claim { i // i ∉ [Party.apocalyptic,
    Party.sanders, Party.critics, Party.jervell] } :=
  solaFideDispute.restrict fun x =>
    x ∉
      [Party.apocalyptic, Party.sanders,
        Party.critics, Party.jervell]

reformationAloneFinite

The Reformation dispute, in the form the verdict solver computes with.

def reformationAloneFinite : Solver.Finite fun i j => solaFideDispute.defeats
    ↑i ↑j :=
  solaFideFinite.restrict fun x =>
    x ∉
      [Party.apocalyptic, Party.sanders,
        Party.critics, Party.jervell]

reformationSettlesTheWord

How the Reformation dispute is settled as far as it can be: nothing defeats either route to Paul's word, so both come first, and nothing joins them. Each Reformed party is defeated by Trent, Trent by Paul's case (and by Luke's, Peter's and Paul's gospel), and Trent read as a claim about Paul's word by Paul's word itself.

What the dispute forces is exactly Paul's word (δικαιόω, by the rule of least meaning), Romans 4:3–8, on Paul's word (by the rule of least meaning).

• Stage 1: Paul's word (δικαιόω, by the rule of least meaning), Romans 4:3–8, on Paul's word (by the rule of least meaning).
  • Paul's word (δικαιόω, by the rule of least meaning) is defeated by nothing.
  • Romans 4:3–8, on Paul's word (by the rule of least meaning) is defeated by nothing.
• Nothing else is forced:
  • Trent, against 'not by works' defeats Sola fide from Paul (Galatians 2:16), and nothing forced defeats Trent, against 'not by works'.
  • Trent, against 'not by works' defeats Luke 7:50: "your faith has saved you", and nothing forced defeats Trent, against 'not by works'.
  • Trent, against 'not by works' defeats Sola fide from Peter (Acts 15:9–11), and nothing forced defeats Trent, against 'not by works'.
  • Sola fide from Paul (Galatians 2:16) defeats Trent, against 'not by works', and nothing forced defeats Sola fide from Paul (Galatians 2:16).
  • Trent, against 'not by works' defeats Paul's gospel (Galatians 1), against justification as renewal, and nothing forced defeats Trent, against 'not by works'.
  • Paul's word (δικαιόω, by the rule of least meaning) defeats Trent, against 'not by works', read as what Paul's word means, and nothing forced defeats Paul's word (δικαιόω, by the rule of least meaning).

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

• Sola fide from Paul (Galatians 2:16), weakest at disputed:
  • πίστις Χριστοῦ in Galatians 2:16 means faith in Christ, not Christ's faithfulness — dunn-once-more-pistis-christou-1991; matlock-detheologizing-2000; Gal 2:16; Rom 3:22; Phil 3:9
  • Second Temple Judaism: in by grace, staying in by works (encoded as a denial, so it ranks disputed) — sanders-paul-palestinian-judaism-1977
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
  • an inference step — gathercole-where-boasting-2002; carson-variegated-nomism-1-2001
• Paul's word (δικαιόω, by the rule of least meaning), weakest at well supported:
  • In Paul, δικαιόω is forensic: to declare righteous, not to make virtuous — bauer-danker-lexicon-2000, §s.v. δικαιόω; morris-apostolic-preaching-1965; moo-romans-1996, §p. 80; irons-righteousness-of-god-2015; wright-justification-2009; fitzmyer-romans-1993, ad loc. Rom 3:24
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004
• Luke 7:50: "your faith has saved you", weakest at disputed:
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Sola fide from Peter (Acts 15:9–11), weakest at disputed:
  • The yoke refused at Acts 15:10 is the whole law as a condition of salvation — bruce-acts-1988, ad loc. Acts 15:10; Acts 15:10; Gal 5:1; Jas 2:10; das-paul-law-covenant-2001
  • Good works are the fruit and evidence of saving faith, not its ground — westminster-confession-1647, §XI.2; XVI.2; XVI.5; calvin-institutes-1960, §III.xvi.1; Jas 2:18-22; Eph 2:10; Rom 6:22; Luke 17:10
  • Justification and sanctification are inseparable but distinct — westminster-confession-1647, §XIII.1; westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.6
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), canon 9
• Trent, against 'not by works', weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
• Paul's gospel (Galatians 1), against justification as renewal, weakest at disputed:
  • an inference step — moo-galatians-2013, ad loc. Gal 1:6; westminster-confession-1647, §XI.1
  • an inference step — westminster-confession-1647, §XI.1; calvin-institutes-1960, §III.xi.2; morris-apostolic-preaching-1965
• Trent, against 'not by works', read as what Paul's word means, weakest at disputed:
  • Justification is not remission of sins only, but renewal of the inward man — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; tanner-decrees-1990, §Trent, Session VI (1547), canon 11
  • an inference step — tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 8; tanner-decrees-1990, §Trent, Session VI (1547), Decree on Justification, ch. 7; npnf1-05-1887, §On the Spirit and the Letter, ch. 45 (26.45); mcgrath-iustitia-dei-2005
• Romans 4:3–8, on Paul's word (by the rule of least meaning), weakest at well supported:
  • Romans 4:4–5 contrasts wages owed with a gift reckoned to the one who believes — Rom 4:4-5; calvin-institutes-1960, §III.xi.18
  • λογίζομαι in Romans 4:3–11 is the language of reckoning: credited to one's account — bauer-danker-lexicon-2000, §s.v. λογίζομαι; moo-romans-1996, ad loc. Rom 4:3
  • A word contributes the least meaning its context requires; one occurrence does not carry the whole concept — silva-biblical-words-1994; joos-semantic-axiom-1972; barr-semantics-2004
  • an inference step — moo-romans-1996, ad loc. Rom 4:6; bauer-danker-lexicon-2000, §s.v. λογίζομαι
  • an inference step — silva-biblical-words-1994; moo-romans-1996, §p. 80; barr-semantics-2004