Sola scriptura

This page is generated from arguments/TestimonyArguments/SolaScriptura. 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.SolaScriptura — scripture as the sole infallible rule of faith

The formal principle of the Reformation. Sola fide is a claim within scripture's teaching; sola scriptura is a claim about scripture's authority, and so must answer objections the material principle never faces.

What the dispute is not about

It is not about whether doctrine develops. Both Rome and the Protestant position encoded here hold that the deposit is closed while understanding of it deepens — doctrineDevelopsWithoutNewRevelation is shared ground, held by Newman and by Mathison alike. The disagreement is entirely over what authenticates a development: derivability from scripture, or the authority of the developing body. An encoding that opposed a static Protestantism to a developing Rome would describe a dispute neither party is having.

Four positions, not two

Mathison's taxonomy, after Oberman, separates what the seed encoding collapsed:

Orthodoxy is a fifth thing again, and not a variant of Rome: authority rests in the mind of the Church, expressed in the consensus of the Fathers and in conciliar decisions received by the whole Church. Florovsky rejects the two-sources model outright. The seed grounded a single "Catholic/Orthodox" line on magisteriumIsInfallible, which attributes to Orthodoxy a premise it does not hold.

tradition0_establishes is the result that most repays the split: the position Mathison calls "solo scriptura" and judges unbiblical and unworkable reaches the conclusion too, once stated by Geisler — who holds it — rather than by its critic.

Three objections, which do not reduce to one another

Self-refutation. If a doctrine binds only when scripture teaches it, and scripture does not teach sola scriptura, the position fails by its own standard.

The canon objection. If the canon is known through the Church's reception, an authority outside scripture is needed to identify scripture. Augustine supplies the classical form: ego vero Evangelio non crederem, nisi me catholicae Ecclesiae commoveret auctoritas.

The interpretive-authority regress. Cross and Judisch argue that the individual retains ultimate interpretive authority, exercised indirectly by choosing which body to submit to, so Tradition I is not principled distinct from Tradition 0 — "when I submit (so long as I agree), the one to whom I submit is me."

Encoding objections that tell against the position is not a concession; the project's ground rules require rival readings to be encoded with the same care as the ones argued for.

The hinge does two jobs, and they come apart

The seed asserted in prose that the dispute reduces to solaScripturaIsTaughtByScripture. Split into the two roles that premise actually plays, the claim is both weaker and sharper than that.

It is not load-bearing for reaching the conclusion: hinge_not_load_bearing_for_conclusion shows the eliminative line delivering the sole rule without it. It is load-bearing within the classical strand taken alone.

And against the self-refutation objection it is one of two answers, not the only one. The objection's step is a conjunction, so either conjunct may be denied: classical_answer_blocks_self_refutation denies that scripture fails to teach the principle, and scoping_blocks_self_refutation denies instead that the bindingness rule governs a claim about where binding doctrine comes from — the final-arbiter reading, on which scripture is not the only arbiter but the last one. The objection succeeds only against a position refusing both.

Redundancy does not defend a position here, which is where this argument parts company with SolaFide. There, a second strand defeated an attack on a premise. These objections are not premise attacks: each independently delivers the negation of the conclusion, so a further route to the conclusion does nothing against them. What answers an objection is denying one of its grounds.

The parity reply, and what it is worth

Kruger on the canon and Mathison on interpretive authority make the same move: concede the circularity, deny that it discriminates between the positions. What the move achieves is that the disputed proposition comes out independent of the reply's grounds: neither it nor its denial follows, because two readings satisfy those grounds and disagree about it. parity_leaves_the_canon_open and parity_leaves_the_distinction_open are those results.

Each used to be a pair — one result that the reply blocks the objection, another that it establishes nothing — and the pair is what hid a defect. Over Barrett's parity reply to Geisler the two halves asked about different propositions while being presented as complements; parity_leaves_the_defeat_open is the claim that was meant, and circle_parity_concedes_the_charge is the second question restated, since that reply does not merely fail to clear the charge of circularity but grants it as one of its own grounds.

The replies neutralise; they do not establish. compatibility_does_not_establish_criterion records the same lesson in BornOfAVirgin, for a different argument and a different reply — and not as an independence claim, because its two results range over different premise sets.

The circle inside Protestantism

circle_leaves_the_consensus_open encodes Geisler's charge against Tradition I: the creedal consensus is said to rest on scripture's clarity, while scripture's clear sense is said to be unobtainable without that consensus. Both legs in place, neither end is settled either way — a cycle of implications is satisfied outright by a valuation on which every node in it is false, and equally by one on which every node is true. circle_leaves_the_perspicuity_open says the same of the other end.

That charge is made from inside the Reformation, against the position this module encodes as the Protestant one. It is conditional like every result here: deny either leg and the circle is not there.

What Mark 7 settles

Jesus' rebuke of the elders' tradition (Mark 7:1–13; Matthew 15:1–9) is the text the Protestant case most often cites, and it used to sit among the shared grounds with no step reading it. It is a line of its own now, and it settles less than it is cited for. Its principle — God's word judges human tradition, and no commandment of men may be taught as God's word — is common ground: Rome holds it too. From the principle to sola scriptura needs one more premise, that no apostolic word survives outside Scripture, and Rome denies it.

whatTrentsTraditionIs is the dilemma a reader of Mark 7 needs. Read as commandments of men, Trent's tradition is what Mark 7 condemns; read as the apostolic word handed on unwritten, which is what Trent says it receives, Mark 7 does not reach it. Weighed as a dispute, Mark 7's principle — which both sides hold — prevails, Trent read as commandments of men cannot be defended, and between Mark 7's case for sola scriptura and Trent the dispute chooses neither (Mark7.lean, Dispute.lean, Hearings.lean).

Weighing it moved a rating. traditionIsCoordinateSourceOfRevelation was wellSupported, which made no difference while no dispute read it. In the Mark 7 dispute it would have decided who prevails, so it was audited: Geiselmann grants Trent's Session IV and denies that it canonised two coordinate sources, since the council replaced its draft's "partly … partly" with "and"; Congar judges that Trent left the question open. The claim is disputed now, and the Tridentine party is named "Trent (Tradition II)" rather than by the reading in dispute.

A limitation worth stating

The final-arbiter reading turns on a distinction between doctrine, which requires scriptural adjudication, and practice neither commanded nor forbidden, which does not. That is a scope distinction, and this fragment is propositional: it cannot quantify. The distinction is carried by atom design and by this docstring, not by the logic. What the encoding shows is what follows given the distinction, not that the distinction can be drawn.

Where things are

TestimonyArguments.SolaScriptura.Atoms — the atomic claims

Four positions, three objections and two parity replies, so the atom list is longer than most. It is grouped by what each atom belongs to rather than by kind, because the groups are what the lines are built from.

Two atoms are worth flagging. scriptureIsInfallible is granted by every party to the dispute and was absent from the seed encoding, which concluded that scripture is the sole infallible rule without ever saying that scripture is infallible; the eliminative line needs it stated. And thessalonians2_15TraditionBinding is a datum both sides must accommodate rather than a Roman premise — the seed filed it as the Catholic counter-text, which left the Protestant package with no answer to it.

TestimonyArguments.SolaScriptura.Sources — citation and classification for every atom

cite is total, so an uncited atom does not compile.

Where the positions disagree about an atom they are given the source that actually holds the claim: the Orthodox premise cites Florovsky and Ware rather than a Protestant account of Orthodoxy, and Tradition 0 cites Geisler rather than Mathison's description of it — Geisler's principal complaint being that the description is a caricature.

Ratings for inference steps

A step's rating is its own, cited to whoever grants its grounds and denies its conclusion — or, where no one was found who does, to whoever grants both.

The claims, numbered

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

mark7PrincipleInference

The rating of Mark 7's step, from the rebuke to the principle. No reader was found who grants the text and denies the principle; Rome grants it outright — the teaching office is "not above the word of God" (Dei Verbum 10) — and Calvin applies Matthew 15:9 to the laws of worship he opposed. Rated wellSupported rather than consensus, because the step generalises from one pericope.

def mark7PrincipleInference : Source :=
  {
    primary :=
      Reference.work tannerDecrees
        (Bib.Locus.sectionRef "Vatican II (1965), Dei Verbum 10"),
    supporting :=
      [Reference.work Bib.calvinInstitutes (Bib.Locus.sectionRef "IV.x.23")],
    tradition := Tradition.christianHistoricalGrammatical,
    confidence := Confidence.wellSupported }

principleToSoleRuleInference

The rating of the step from Mark 7's principle to the sole rule: disputed. Grant that God's word judges human tradition and that no apostolic teaching outside Scripture adds to it, and a reader may still deny that Scripture is the sole infallible rule. Geiselmann is that reader: he holds that Scripture contains all revealed content, grants the principle as every Catholic does, and as a Catholic after Vatican I still holds the Magisterium an infallible interpreter (Pastor Aeternus 4). Florovsky, for whom tradition adds nothing to Scripture, likewise keeps the mind of the Church as its authoritative interpreter.

def principleToSoleRuleInference : Source :=
  { primary := Reference.work geiselmannMeaningOfTradition,
    supporting :=
      [Reference.work tannerDecrees
          (Bib.Locus.sectionRef "Vatican I (1870), Pastor Aeternus, ch. 4"),
        Reference.work florovskyBibleChurchTradition],
    tradition := Tradition.romanCatholic, confidence := Confidence.disputed }

tridentineInference

The rating of Trent's step, from 2 Thessalonians 2:15 and tradition as a source of revelation to "Scripture is not the sole rule": wellSupported. Once the grounds are granted the conclusion all but follows, and no reader was found who grants both and denies it. Protestants deny the second ground instead, and that dissent is weighed in its own rating.

def tridentineInference : Source :=
  {
    primary :=
      Reference.work tannerDecrees
        (Bib.Locus.sectionRef
          "Trent, Session IV (1546), Decree on Sacred Books and Traditions"),
    tradition := Tradition.romanCatholic,
    confidence := Confidence.wellSupported }

cite

Citation and classification for every atom. Total, so nothing is uncited.

def cite : Claim → AtomMeta

TestimonyArguments.SolaScriptura.Lines — the inference steps and the lines of reason

Three routes reach the conclusion — the classical line, the eliminative line, and Mark 7's, which takes two lines — three positions deny it, and three objections attack it from different directions. The objections do not reduce to one another: self-refutation says the doctrine fails its own standard, the canon objection says an authority outside scripture is needed to identify scripture, and the interpretive-authority regress says the authority claimed is the claimant in disguise.

Redundancy does not defend the hinge here. In SolaFide, adding a second strand defeated an attack on a premise. These objections are not premise attacks: each independently delivers the negation of the conclusion, so a further route to the conclusion does nothing against them. What answers an objection is denying one of its grounds, which is why every reply below is written with Line.onGrounds — the objection's own line, with the ground the reply refuses put back as what the reply offers instead.

Steps reaching the conclusion

toSoleRule

Sufficiency and perspicuity, with the prooftexts and the claim that scripture teaches the principle, yield the sole infallible rule.

eliminativeToSoleRule

The eliminative route: scripture is infallible, nothing else is, so scripture is the sole infallible rule. It never asserts that scripture teaches the principle.

mark7ToPrinciple

Mark 7's step: from Jesus' rebuke of the elders' tradition to the principle it enacts — God's word judges human tradition. Rated wellSupported: no reader was found who grants the text and denies the principle, and Rome grants it in so many words (Dei Verbum 10). Not consensus, because the step generalises from one pericope.

principleExcludesMensCommandments

What the principle says of a commandment of men: it may not be bound on the Church as God's word. This is Isaiah 29:13 as Mark 7:7 quotes it.

principleToSoleRule

From Mark 7's principle to the sole rule. If God's word judges human tradition, and no apostolic word survives outside Scripture, Scripture is the sole infallible rule. Rated disputed: Geiselmann holds that Scripture contains all revealed content and, as a Catholic after Vatican I, keeps the Magisterium as its infallible interpreter; Florovsky holds that tradition adds nothing to Scripture and keeps the mind of the Church as its interpreter. Neither adds a word to Scripture; both deny it is the sole infallible rule.

tradition0ToSoleRule

Geisler's route: the historical-grammatical method suffices, so creeds may inform without binding, and no second infallible rule is needed.

Steps denying it

tridentineDeniesSoleRule

Tradition II. Binding unwritten tradition as a coordinate source denies that scripture is the sole rule.

magisterialDeniesSoleRule

Tradition III. An infallible magisterium is a second infallible rule, whatever is said about sources.

orthodoxDeniesSoleRule

Orthodoxy. The mind of the Church interpreting infallibly is likewise a second infallible rule — and it is not the magisterial premise.

The three objections

selfRefutationStep

If a doctrine binds only when scripture teaches it, and scripture does not teach sola scriptura, then sola scriptura does not bind.

canonObjectionStep

If the canon is known only through the Church's reception, and identifying the canon requires an infallible authority, then an infallible authority outside scripture is needed to identify scripture.

interpretiveRegressStep

Cross and Judisch: if the individual retains ultimate interpretive authority, exercised indirectly by choosing the body to submit to, then Tradition I's ministerial authority is not a principled difference from Tradition 0.

Geisler's circle

Two legs, each supplying the other's ground. The consensus of the Church is said to rest on the clarity of scripture, while the clear sense of scripture is said to require the consensus of the Church.

consensusRestsOnPerspicuity

Leg one: the creedal consensus rests on scripture's clarity.

perspicuityRestsOnConsensus

Leg two: scripture's clear sense is not obtainable without that consensus.

The lines

classicalLine — Classical (scripture teaches the principle)

The classical Protestant line, running through the claim that scripture teaches the principle.

eliminativeLine — Eliminative (nothing else is infallible)

The eliminative line, which reaches the conclusion without the hinge.

mark7Line — Mark 7 (God's word judges human tradition)

Mark 7, as a line of its own: Jesus' rebuke of the elders' tradition, and the principle it enacts. It delivers the principle, and no more.

mark7SoleRuleLine — From Mark 7's principle to the sole rule

From Mark 7 to the sole rule: the principle, with the premise that no apostolic word survives outside Scripture. The principle is carried in by mark7Line; this line's own ground is the one Rome denies.

tradition0Line — Tradition 0 (creeds informative, not normative)

Tradition 0, as Geisler states it rather than as Mathison describes it.

tridentineLine — Trent (Tradition II)

Tradition II, the Tridentine two-source position. Its step is rated wellSupported: once unwritten tradition is granted as a source of revelation alongside Scripture, no reader was found who denies that Scripture is then not the sole rule. Protestants deny the ground instead, and that dissent is weighed in the ground's own rating.

vaticanLine — Tradition III (the magisterium as the one real source)

Tradition III, resting on Vatican I rather than on Trent.

orthodoxLine — Orthodox (the mind of the Church)

The Orthodox line, grounded on the mind of the Church.

selfRefutationLine — Self-refutation objection

The self-refutation objection.

canonObjectionLine — Canon objection

The canon objection.

interpretiveRegressLine — Interpretive-authority regress

The interpretive-authority regress.

The replies, as substituted grounds

Each reply is the objection's own line with the ground it refuses replaced by what the reply offers instead. Adding a premise could never block a valid argument; taking away the ground it needed is what a reply actually does.

selfRefutationUnderClassicalAnswer — Self-refutation objection

The classical answer to self-refutation: scripture does teach the principle.

selfRefutationUnderFinalArbiter — Self-refutation objection

The final-arbiter answer: the bindingness rule governs first-order doctrine, not a claim about where binding doctrine comes from.

canonUnderParity — Canon objection

Kruger's parity reply: the canon's reception is conceded, and what the objection needed — that identifying it requires an infallible authority — is replaced by the observation that the rival's authority is self-authenticating too.

regressUnderParity — Interpretive-authority regress

Mathison's parity reply: choosing Rome is itself an act of private judgement, so private judgement does not separate the positions.

Geisler's charge as an argument, and the replies to it

The cycle results above are a formal fact: a cycle of implications grounds neither end. The line below is the dialectical fact — Geisler charging circularity, and what answers the charge. They are different claims, and both are worth having.

Every reply denies the second leg, that scripture's clear sense is unobtainable without the consensus. Barrett's is the exception: it concedes the circle and denies that circularity is a defect peculiar to Tradition I, which is why circleDefeatsLine carries the universality claim as a ground of its own.

circleStep

Both legs together make the reasoning circular.

circularityDefeats

Circularity defeats the position if it is not a feature of every appeal to an ultimate authority. Geisler's charge needs the second conjunct, and it is what Barrett denies.

geislerCircleLine — Geisler's circularity charge against Tradition I

Geisler's circularity charge.

circleDefeatsLine — The circularity defeats Tradition I

The charge pressed home: the circularity defeats the position.

circleUnderAccountability — Geisler's circularity charge against Tradition I

Allen and Swain's reply. The consensus is established by and accountable to scripture, so it is a product of reading scripture rather than a precondition of it.

circleUnderScripturalBounding — Geisler's circularity charge against Tradition I

The proposed reply. Scripture itself bounds the interpretive office — elders commended to the word (Acts 20:32), required to hold to it (Titus 1:9), forbidden to domineer (1 Peter 5:2–3) — so the consensus's own warrant is read off scripture, and perspicuity is in any case claimed only for what is necessary for salvation.

defeatUnderParity — The circularity defeats Tradition I

Barrett's parity reply. The circle is conceded; what is denied is that it is peculiar to this position.

Shared grounds and closing steps

sharedGrounds

What the Protestant packages rest on beyond any single line: the prooftext that belongs to no strand, the shared datum of 2 Thessalonians 2:15, and the commitments of the final-arbiter reading. Mark 7 used to sit here too, a premise no step read; it is a line of its own now (mark7Line).

TestimonyArguments.SolaScriptura.Packages — the positions, and the variants results refute

Four positions on tradition, three objections, two parity replies, and the variants each result needs. The rivals were written before anything was proved about the position argued for.

Several packages are built to be refuted. A reply is shown to block an objection by writing the objection's line on the reply's grounds and exhibiting a countermodel.

The parity replies have no packages at all. What they do is that the disputed proposition comes out independent of the reply's grounds — neither entailed nor refuted by them — and Independent takes a premise list and a formula, so the reply's Line is all it needs.

The positions

protestant — Protestant (sola scriptura as final arbiter)

The Protestant position: three routes to the conclusion, on the final-arbiter reading — the classical, the eliminative, and Mark 7's. Scripture is not the only authority but the only infallible one; tradition is ministerial, and practices neither commanded nor forbidden need no scriptural warrant.

Grounded in scripture alone: 2 Thessalonians 2:15 — hold to the traditions taught by word or letter.

tradition0 — Tradition 0 (creeds informative, not normative)

Tradition 0, as Geisler states it: creeds inform without binding, and the historical-grammatical method does the work an authoritative interpreter was supposed to do.

No premise here rests on scripture alone.

tridentine — Trent (Tradition II)

Tradition II, the Tridentine two-source position. Its line delivers the denial, so the package is not the line as it stands: the question asked of these premises is whether sola scriptura follows, and the answer is that they entail its negation.

Grounded in scripture alone: 2 Thessalonians 2:15 — hold to the traditions taught by word or letter.

vaticanI — Tradition III (the magisterium as the one real source)

Tradition III, resting on Vatican I. Kept separate from tridentine because Mathison argues it escapes several objections to the two-source view while incurring its own.

No premise here rests on scripture alone.

orthodox — Orthodox (the mind of the Church)

The Orthodox position, on the mind of the Church rather than on a magisterium.

No premise here rests on scripture alone.

The objections

selfRefutation — Self-refutation objection

The self-refutation objection, as a package concluding the negation.

No premise here rests on scripture alone.

canonObjection — Canon objection

The canon objection, likewise.

No premise here rests on scripture alone.

interpretiveRegress — Interpretive-authority regress

The interpretive-authority regress, concluding that Tradition I is not principled distinct from Tradition 0.

No premise here rests on scripture alone.

The two answers to self-refutation

selfRefutationAnswered — Self-refutation objection, answered from scripture's own teaching

The objection with the classical answer in place of the ground it needed.

No premise here rests on scripture alone.

selfRefutationUnderScope — Self-refutation objection, answered by scoping the bindingness rule

The objection with the final-arbiter answer in place of the ground it needed.

No premise here rests on scripture alone.

The parity replies

No package here. What a parity reply does is stated as Independent over the reply's own line — see Results — and independence is a claim about a premise set and a proposition, not about a package's conclusion. Four packages used to stand here, two per reply, because Establishes is package-shaped and the reply had to be asked its question twice: once for the block and once for the conclusion. One statement replaces each pair, and the scaffolding goes with them.

The hinge, in its two roles

protestantWithoutHinge — Protestant, minus the claim that scripture teaches the principle

The Protestant position with the classical line stripped of the hinge. The eliminative and Mark 7 routes are untouched.

Grounded in scripture alone: 2 Thessalonians 2:15 — hold to the traditions taught by word or letter.

classicalStrandWithoutHinge — Classical (scripture teaches the principle)

The classical line alone, stripped of the hinge.

No premise here rests on scripture alone.

Geisler's charge, and the three replies

geislerCircle — Geisler's circularity charge against Tradition I

Geisler's charge, stated as its holder states it.

No premise here rests on scripture alone.

circleDefeats — The circularity defeats Tradition I

The charge pressed home to a defeat.

No premise here rests on scripture alone.

geislerCircleUnderAccountability — Geisler's charge, with the accountability reply in play

The charge with Allen and Swain's accountability reply in play.

No premise here rests on scripture alone.

geislerCircleUnderScripturalBounding — Geisler's charge, with the scriptural-bounding reply in play

The charge with the proposed scriptural-bounding reply in play.

No premise here rests on scripture alone.

circleParityConcedingTheCharge — Barrett's parity reply, asked about the charge itself

Barrett's parity grounds, asked about the charge itself.

Not "asked to clear the charge", which is what this package used to ask. The reply concedes the circle — traditionIReasoningIsCircular is one of its grounds — so the interesting question is not whether it fails to deliver the denial but that it delivers the charge. Asked the weaker question the answer is "no"; asked this one it is "yes, by its own premises".

No premise here rests on scripture alone.

Geisler's circle

traditionICircle — Tradition I's hermeneutical circle

Both legs of the circle Geisler alleges in Tradition I, asked for the consensus.

No premise here rests on scripture alone.

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

The results this module exists for are the two on the hinge. The seed asserted in prose that the dispute reduces to solaScripturaIsTaughtByScripture; here that claim is split into the two roles the premise actually plays, because they come apart.

The positions

protestant_establishes

Given the Protestant premises, on any of its three routes, the conclusion follows.

theorem protestant_establishes : Establishes protestant
-- axioms: propext, Quot.sound

tradition0_establishes

Tradition 0 establishes it too. Geisler rejects Mathison's claim that tradition is hermeneutically necessary; he does not reject sola scriptura. The position Mathison calls "solo scriptura" and judges unbiblical and unworkable reaches the same conclusion by a different route, once it is stated by someone who holds it rather than by its critic.

theorem tradition0_establishes : Establishes tradition0
-- axioms: propext, Quot.sound

tridentineReading

The Tridentine reading, written down: tradition is a coordinate source, so scripture is not the sole rule.

def tridentineReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.scriptureIsSoleInfallibleRule => False
    | x => True

tridentine_not_establishes

The two-source premises do not establish sola scriptura — they entail its negation.

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

magisterialReading

The post-Vatican I reading: the magisterium is the living interpreter, so scripture is not the sole infallible rule.

def magisterialReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.scriptureIsSoleInfallibleRule => False
    | x => True

vaticanI_not_establishes

Tradition III likewise entails the negation — by a different premise from Tradition II's, which is why the two are separate packages.

theorem vaticanI_not_establishes : ¬Establishes vaticanI
-- axioms: propext, Quot.sound

orthodoxReading

The Orthodox reading: the mind of the Church interprets infallibly, with no magisterium and no second source of revelation.

def orthodoxReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.scriptureIsSoleInfallibleRule => False
    | x => True

orthodox_not_establishes

Orthodoxy also entails the negation, and on its own premise. The seed encoding grounded a single "Catholic/Orthodox" line on magisterial infallibility, which attributes to Orthodoxy a premise it does not hold.

theorem orthodox_not_establishes : ¬Establishes orthodox
-- axioms: propext, Quot.sound

The three objections, each valid on its own grounds

selfRefutation_is_valid

The self-refutation objection is valid: granted that only scriptural doctrine binds and that scripture does not teach sola scriptura, the position fails by its own standard.

theorem selfRefutation_is_valid : Establishes selfRefutation
-- axioms: propext, Quot.sound

canonObjection_is_valid

The canon objection is valid on its own grounds: if the canon is known through the Church's reception and identifying it requires an infallible authority, then an authority outside scripture is needed to identify scripture.

theorem canonObjection_is_valid : Establishes canonObjection
-- axioms: propext, Quot.sound

interpretiveRegress_is_valid

The interpretive-authority regress is valid on its own grounds. It attacks something the other two do not: not whether the doctrine is scriptural or whether the canon can be identified, but whether the authority Tradition I submits to is anything other than the one submitting.

theorem interpretiveRegress_is_valid : Establishes interpretiveRegress
-- axioms: propext, Quot.sound

The hinge, in its two roles

solaScripturaIsTaughtByScripture does two jobs, and they come apart. It is not load-bearing for reaching the conclusion, because the eliminative line reaches it without the hinge. It is load-bearing within the classical strand, and — the result that matters — it is one of only two things that answer the self-refutation objection.

hinge_not_load_bearing_for_conclusion

The hinge is not load-bearing for the conclusion. Strip it and the eliminative line still delivers the sole rule, and so does Mark 7's — each on a premise of its own that the classical line does not need.

theorem hinge_not_load_bearing_for_conclusion : Establishes
    protestantWithoutHinge
-- axioms: propext, Quot.sound

hingeDeniedReading

The reading on which scripture does not teach the principle, and the sole rule does not follow.

def hingeDeniedReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.solaScripturaIsTaughtByScripture => False
    | Claim.scriptureIsSoleInfallibleRule => False
    | x => True

hinge_is_load_bearing_within_classical_strand

Within the classical strand taken alone the hinge is still load-bearing: remove it and that strand yields nothing.

theorem hinge_is_load_bearing_within_classical_strand : ¬Establishes
    classicalStrandWithoutHinge
-- axioms: propext, Quot.sound

The two answers to self-refutation

The objection's step is a conjunction, so there are two ways to deny it. The seed encoded only the first. Neither answer is redundant with the other: each removes a different ground, and the objection succeeds only if both are refused.

scriptureTeachesItReading

The reading on which scripture does teach the principle.

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

classical_answer_blocks_self_refutation

The classical answer blocks the objection. Assert that scripture teaches the principle and the objection no longer delivers its denial.

theorem classical_answer_blocks_self_refutation : ¬Establishes
    selfRefutationAnswered
-- axioms: propext, Quot.sound

finalArbiterReading

The final-arbiter reading: scripture adjudicates doctrine rather than sourcing every binding claim, so the bindingness rule does not apply reflexively to a claim about where doctrine comes from.

def finalArbiterReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.onlyScripturalDoctrineIsBinding => False
    | Claim.solaScripturaIsTaughtByScripture => False
    | x => True

scoping_blocks_self_refutation

And the final-arbiter answer blocks it too, without the hinge. This is the answer the seed did not encode. It concedes that scripture does not teach the principle in the sense the objection requires, and denies instead that the bindingness rule governs a claim of this kind.

So the objection is defeated on either route, and succeeds only against a position that refuses both — which is what "the dispute reduces to the hinge" was gesturing at, and is narrower than that phrase suggests.

theorem scoping_blocks_self_refutation : ¬Establishes selfRefutationUnderScope
-- axioms: propext, Quot.sound

The parity replies, and what they are worth

Kruger on the canon and Mathison on interpretive authority make the same move: concede the circularity, deny that it discriminates between the positions.

Each used to get two results — one that it blocks the objection, one that it establishes nothing — and that is one result too many. A premise set that entails neither a proposition nor its negation leaves that proposition independent of it, and blocking and establishing-nothing are the two halves of that single fact. Foundation names the notion for provability; Testimony.Logic.Independent is its semantic counterpart, and leaves_open proves it from the two readings the premises admit.

The gain is not brevity. Stated as a pair, nothing checks that the two halves are about the same proposition — and in the Geisler case below they were not.

parityEstablishesNothingReading

The reading on which the parity point is granted and the sole rule still does not follow: the canon came through the Church, the rival's authority is self-authenticating too, and scripture is not the sole infallible rule.

def parityEstablishesNothingReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.scriptureIsSoleInfallibleRule => False
    | x => True

krugerParityReading

Kruger's reading: the canon's reception is conceded, and the demand for an infallible identifying authority is refused, because the rival's own authority is self-authenticating too.

def krugerParityReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.identifyingCanonRequiresInfallibleAuthority => False
    | x => True

parity_leaves_the_canon_open

The parity reply leaves the canon question open. Granted Kruger's grounds, the sole infallible rule neither follows nor fails: his own reading has it, and the reading on which the parity point is conceded and the sole rule still denied has it not. Both satisfy every premise.

That is the whole of what the reply achieves, in one claim. It blocks the canon objection — the objection's denial is no longer entailed — and it establishes nothing, because the conclusion is not entailed either. The parity move is purely defensive, and this is the form that says so without saying it twice.

theorem parity_leaves_the_canon_open : Independent canonUnderParity.premises
    (p Claim.scriptureIsSoleInfallibleRule)
-- axioms: propext, Quot.sound

distinctionUnestablishedReading

The reading on which the parity point is granted and the distinction still does not follow: tradition is ministerial, choosing an authority is private judgement, and sola scriptura does not differ in principle from solo scriptura.

def distinctionUnestablishedReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.traditionIDiffersInPrincipleFromTradition0 => False
    | x => True

mathisonParityReading

Mathison's reading: ministerial authority is retained, and the claim that the individual keeps ultimate interpretive authority is refused, because choosing Rome is itself an act of private judgement.

def mathisonParityReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.individualRetainsUltimateInterpretiveAuthority =>
      False
    | x => True

parity_leaves_the_distinction_open

And the same for interpretive authority. That choosing an authority is itself private judgement defeats the charge that Tradition I collapses into Tradition 0; it does not show that Tradition I differs from it in principle. Both readings satisfy Mathison's grounds, so his grounds settle the question neither way.

The same shape, twice, against two different objections — which is the point. It is a property of the move, not of the objection it answers.

theorem parity_leaves_the_distinction_open : Independent
    regressUnderParity.premises (p
    Claim.traditionIDiffersInPrincipleFromTradition0)
-- axioms: propext, Quot.sound

Geisler's circle

neitherEndReading

The reading on which neither the consensus nor the clarity it is said to rest on obtains.

def neitherEndReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.creedalConsensusIsHermeneuticallyNecessary => False
    | Claim.scriptureIsPerspicuous => False
    | x => True

bothEndsHoldReading

The reading on which both ends of the circle obtain: the consensus is hermeneutically necessary and scripture is clear. A cycle of implications is satisfied by this as readily as by the reading on which every node is false, which is what it means for the cycle to settle nothing.

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

circle_leaves_the_consensus_open

Geisler's circularity charge against Tradition I, shown rather than alleged. The creedal consensus is said to rest on scripture's clarity, and scripture's clear sense is said to be unobtainable without that consensus. Put both legs in place and the consensus is left independent of them: it does not follow, and neither does its denial.

A cycle of implications is satisfied outright by a valuation on which every node in it is false, and equally by one on which every node is true. Nothing enters such a loop from outside, so nothing comes out of it — in either direction. That second direction is what this result gained when it stopped being a bare ¬ Establishes: a circle is not merely silent about whether its nodes hold, it is silent about whether they fail.

Like every result here this is conditional: deny either leg and the circle is not there. What it settles is that the charge is structural rather than rhetorical — and it is made from inside Protestantism, against the position this module encodes as the Protestant one.

theorem circle_leaves_the_consensus_open : Independent
    traditionICircle.premises (p
    Claim.creedalConsensusIsHermeneuticallyNecessary)
-- axioms: propext, Quot.sound

circle_leaves_the_perspicuity_open

And the other end is no better off. The same two legs, asked about perspicuity instead of the consensus, leave it open in the same way and on the same two readings.

Both results are needed, and they are not two halves of one claim: a circle has two ends, and each is a separate proposition the premises fail to settle. What is one claim is each result's own two directions, which is why each is an Independent rather than a pair.

theorem circle_leaves_the_perspicuity_open : Independent
    traditionICircle.premises (p Claim.scriptureIsPerspicuous)
-- axioms: propext, Quot.sound

Geisler's charge, and the three replies

The cycle results above are a formal fact about a cycle of implications. These are about the charge as an argument: whether it goes through, and what answers it. Two replies deny its second leg; Barrett's concedes the circle and denies that circularity is peculiar to this position.

geislerCircle_is_valid

Geisler's charge is valid on its own grounds: grant that the consensus rests on scripture's clarity and that scripture's clear sense requires the consensus, and the reasoning is circular.

theorem geislerCircle_is_valid : Establishes geislerCircle
-- axioms: propext, Quot.sound

accountabilityReading

The reading on which the consensus is a product of scripture rather than a precondition of reading it.

def accountabilityReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.perspicuityRequiresCreedalConsensus => False
    | Claim.traditionIReasoningIsCircular => False
    | x => True

accountability_blocks_the_circle

Allen and Swain's reply blocks the charge. If the creedal consensus is established by and accountable to scripture, it is what reading scripture produces rather than what reading scripture presupposes, and the second leg fails.

What this costs is worth stating: Geisler quotes Mathison saying that it is "to the Church that we must turn for the true interpretation of the Scripture" and that without the early rule of faith "hermeneutical chaos and anarchy" reigns. If that is Tradition I, the reply defends a weaker position than the one charged.

theorem accountability_blocks_the_circle : ¬Establishes
    geislerCircleUnderAccountability
-- axioms: propext, Quot.sound

scripturallyBoundedOfficeReading

The reading on which scripture bounds the interpretive office, and perspicuity is claimed only for salvation essentials.

def scripturallyBoundedOfficeReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.perspicuityRequiresCreedalConsensus => False
    | Claim.traditionIReasoningIsCircular => False
    | x => True

scripturalBounding_blocks_the_circle ⚗

The scriptural-bounding reply blocks the charge too, and on scriptural rather than confessional grounds.

What is novel here. No source was found advancing these texts as an answer to the circularity charge; the passages are cited and the use is assembled in this library. Acts 20:32 commends the Ephesian elders to "the word of his grace" rather than to their own office; Titus 1:9 constitutes the office by holding to "the trustworthy word as taught"; 1 Peter 5:2–3 forbids domineering. If scripture bounds the interpretive office, the consensus's own warrant is read off scripture, so it cannot be a precondition of reading scripture — and Westminster I.7 restricts the perspicuity claim to what is necessary for salvation, which is not the set of boundaries the creeds fix.

What would settle whether it is really new. Mark Thompson's A Clear and Present Word treats the church-as-interpreter objection at length and was not available here; Vanhoozer's Biblical Authority after Babel covers the same ground. Either may already make this argument, in which case this result should be recited to them and the tag dropped.

What it deliberately does not claim. That scripture confers the office. Conferral invites the recognition/conferral distinction Mathison presses against Rome over the canon, and boundedness is all the reply needs. It also does not escape the regress: a critic may say the texts are read this way because of a tradition. It moves the dispute to far less contested ground; it does not leave it.

theorem scripturalBounding_blocks_the_circle : ¬Establishes
    geislerCircleUnderScripturalBounding
-- axioms: propext, Quot.sound

universalCircularityReading

Barrett's own reading: the circle is granted, it is granted to be universal, and so it does not defeat this position in particular.

def universalCircularityReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.circularityDefeatsTraditionI => False
    | x => True

universalityDoesNotAcquitReading

The sceptic's reading of the same grounds: the circle is granted and its universality is granted, and the defeat lands anyway. That every ultimate authority reasons in a circle is read as a charge against all of them rather than an acquittal of any — including Tradition I.

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

parity_leaves_the_defeat_open

Barrett's parity reply leaves the defeat open. Concede the circle; deny that it is a defect peculiar to this position, since any appeal to an ultimate authority is circular. On his grounds the defeat does not follow — and neither does its failure, because the same grounds are satisfied by the reading on which universal circularity convicts everyone rather than excusing anyone.

The sixth instance of one move. Kruger on the canon, Mathison on interpretive authority, Athanasius on ὁμοούσιος, Whitaker on unwritten tradition, Geisler himself on who may interpret the Old Testament, and now Barrett on perspicuity — against Geisler, who deploys it himself elsewhere.

This result is not what it was. It stood as half of a pair whose other half asked a different question of the same premises — whether the reply clears the charge of circularity, not whether it blocks the defeat — and the pair was presented as though the two were complements. Naming the shape exposed that: an independence claim has to say which proposition is left open, and only one of the two could be named.

theorem parity_leaves_the_defeat_open : Independent defeatUnderParity.premises
    (p Claim.circularityDefeatsTraditionI)
-- axioms: propext, Quot.sound

circle_parity_concedes_the_charge

The reply does not merely fail to clear the charge — it grants it. This is the second question, kept because it is worth asking and restated because the answer is stronger than "establishes nothing". Barrett's grounds include traditionIReasoningIsCircular outright: what the parity move denies is that the circularity is damaging, not that it is there. A position defended only by this reply is circular and keeping company, and that now follows from the reply's own premises rather than from the failure of a rival reading.

theorem circle_parity_concedes_the_charge : Establishes
    circleParityConcedingTheCharge
-- axioms: propext

Refusing a ground, and denying it

Every reply above is written the same way, as the objection's own line with a ground replaced. That shape covers two different moves. A reply can deny the ground — entail its negation — or merely refuse it, declining to grant it without asserting the opposite. A denial is an attack, and in a dispute an attack can defeat (Testimony.Logic.Dispute). A refusal attacks nothing: it takes the ground away, which is what Line.onGrounds encodes, and the question it leaves is an entailment question the results above already answer.

Five of the seven replies here refuse. Each refusal is shown by a reading that grants the reply's grounds and keeps the refused ground true. The other two deny, and each denial is an entailment.

kruger_refuses_rather_than_denies

Kruger refuses the canon objection's ground; he does not deny it. On the reading that grants his grounds and still denies the sole rule, identifying the canon does require an infallible authority.

theorem kruger_refuses_rather_than_denies : ¬Entails canonUnderParity.premises
    (∼p Claim.identifyingCanonRequiresInfallibleAuthority)
-- axioms: propext, Quot.sound

mathison_refuses_rather_than_denies

Mathison refuses the regress's ground. Granted his grounds, the individual may still retain ultimate interpretive authority.

theorem mathison_refuses_rather_than_denies : ¬Entails
    regressUnderParity.premises (∼p
    Claim.individualRetainsUltimateInterpretiveAuthority)
-- axioms: propext, Quot.sound

final_arbiter_refuses_rather_than_denies

The final-arbiter answer refuses the self-refutation objection's ground. Scoping the bindingness rule to first-order doctrine does not deny that only scriptural doctrine binds.

theorem final_arbiter_refuses_rather_than_denies : ¬Entails
    selfRefutationUnderFinalArbiter.premises (∼p
    Claim.onlyScripturalDoctrineIsBinding)
-- axioms: propext, Quot.sound

accountability_refuses_rather_than_denies

Allen and Swain refuse the circle's second leg. A consensus accountable to scripture does not, by itself, deny that perspicuity requires the consensus.

theorem accountability_refuses_rather_than_denies : ¬Entails
    circleUnderAccountability.premises (∼p
    Claim.perspicuityRequiresCreedalConsensus)
-- axioms: propext, Quot.sound

scriptural_bounding_refuses_rather_than_denies

The scriptural-bounding reply refuses the same leg.

theorem scriptural_bounding_refuses_rather_than_denies : ¬Entails
    circleUnderScripturalBounding.premises (∼p
    Claim.perspicuityRequiresCreedalConsensus)
-- axioms: propext, Quot.sound

classical_answer_denies_the_ground

The classical answer denies the self-refutation objection's ground. It asserts that scripture teaches the principle, which is the negation of what the objection assumes.

theorem classical_answer_denies_the_ground : Entails
    selfRefutationUnderClassicalAnswer.premises (∼notP
    Claim.solaScripturaIsTaughtByScripture)
-- axioms: propext, Quot.sound

barrett_denies_the_ground

Barrett denies the ground Geisler's charge needs. He asserts that every appeal to an ultimate authority is circular, the negation of what the charge assumes.

theorem barrett_denies_the_ground : Entails defeatUnderParity.premises (∼notP
    Claim.everyUltimateAuthorityIsCircular)
-- axioms: propext, Quot.sound

Satisfiability

Entails quantifies over the valuations satisfying the premises, so a premise set with no model entails everything — including the negation of what its own author intended. A package built from contradictory premises would Establishes its conclusion, the proof would close, and every gate would pass.

Only packages carrying a positive Establishes result need checking here. A package with a ¬ Establishes result is satisfiable already: its countermodel is a valuation on which every premise holds.

These are not tagged @[headline]. They are claims about the health of the encoding, not about the dispute.

everythingHoldsReading

The reading on which every claim in this argument holds at once. Not a position anyone occupies — it is the witness that the packages built only from positive grounds are coherent.

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

protestant_is_satisfiable

The Protestant package has a model, so protestant_establishes is not vacuous.

theorem protestant_is_satisfiable : Satisfiable protestant.premises
-- axioms: propext, Quot.sound

tradition0_is_satisfiable

Tradition 0's package has a model.

theorem tradition0_is_satisfiable : Satisfiable tradition0.premises
-- axioms: propext, Quot.sound

protestantWithoutHinge_is_satisfiable

The Protestant package minus the hinge has a model, so hinge_not_load_bearing_for_conclusion is not vacuous either — which matters, since a load-bearing result that held only because its premises were contradictory would be precisely backwards.

theorem protestantWithoutHinge_is_satisfiable : Satisfiable
    protestantWithoutHinge.premises
-- axioms: propext, Quot.sound

geislerCircle_is_satisfiable

Geisler's charge has a model.

theorem geislerCircle_is_satisfiable : Satisfiable geislerCircle.premises
-- axioms: propext, Quot.sound

circleParityConcedingTheCharge_is_satisfiable

Barrett's parity grounds have a model — the sceptic's reading, which grants the circle, grants its universality, and lets the defeat land.

theorem circleParityConcedingTheCharge_is_satisfiable : Satisfiable
    circleParityConcedingTheCharge.premises
-- axioms: propext, Quot.sound

selfRefutationOwnReading

The world the self-refutation objection describes: scripture does not teach the principle, so the sole rule does not bind.

def selfRefutationOwnReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.solaScripturaIsTaughtByScripture => False
    | Claim.scriptureIsSoleInfallibleRule => False
    | x => True

selfRefutation_is_satisfiable

The self-refutation objection has a model.

theorem selfRefutation_is_satisfiable : Satisfiable selfRefutation.premises
-- axioms: propext, Quot.sound

canonObjectionOwnReading

The world the canon objection describes: the canon comes through the Church, so scripture is not the sole infallible rule.

def canonObjectionOwnReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.scriptureIsSoleInfallibleRule => False
    | x => True

canonObjection_is_satisfiable

The canon objection has a model.

theorem canonObjection_is_satisfiable : Satisfiable canonObjection.premises
-- axioms: propext, Quot.sound

interpretiveRegressOwnReading

The world the regress describes: sola scriptura does not differ in principle from solo scriptura.

def interpretiveRegressOwnReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.traditionIDiffersInPrincipleFromTradition0 => False
    | x => True

interpretiveRegress_is_satisfiable

The interpretive-authority regress has a model.

theorem interpretiveRegress_is_satisfiable : Satisfiable
    interpretiveRegress.premises
-- axioms: propext, Quot.sound

TestimonyArguments.SolaScriptura.Mark7 — what Jesus' rebuke of tradition settles

The Pharisees and scribes ask why Jesus' disciples eat with unwashed hands, against "the tradition of the elders". Jesus answers with Isaiah 29:13 — "in vain do they worship me, teaching as doctrines the commandments of men" — and with Corban: a gift vowed to God releases a son from supporting his father and mother, "thus making void the word of God by your tradition" (Mark 7:1–13; Matthew 15:1–9). The Protestant case has always cited it. Until now it only sat among the shared grounds, and no step read it.

What Mark 7 settles

The principle is common ground. God's word judges human tradition: no commandment of men may be taught as God's word, and a tradition that voids God's command is void. Rome says the same — its teaching office is "not above the word of God" (Dei Verbum 10) — and so the principle is not a Protestant win. Trent, as it states its position, can hold every word of it (trent_grants_marks_principle).

It does not reach sola scriptura on its own. From the principle to "Scripture is the sole infallible rule" needs one more premise: that no apostolic teaching handed on outside Scripture survives as God's word. Without it, Mark 7 leaves the sole rule open — neither it nor its denial follows (mark7_without_the_hinge_leaves_the_sole_rule_open). With it, the conclusion follows (mark7Case_establishes), and the premise is rated disputed: Rome denies it from 2 Thessalonians 2:15 ("by word or by letter"). The step itself is disputed too. A reader can grant the principle, and grant that nothing apostolic survives outside Scripture, and still deny that Scripture is the sole infallible rule: Florovsky, for whom tradition adds nothing to Scripture and the mind of the Church interprets it; or a Catholic who holds Scripture materially sufficient and the Magisterium infallible.

What Rome's "tradition" means

The question the passage raises for a reader is whether the tradition Jesus condemns is the thing Rome means by Tradition. whatTrentsTraditionIs answers both readings.

• Read as commandments of men — Calvin's reading of the laws of worship he opposed, applying Matthew 15:9 to them (Institutes IV.x.23) — Trent's claim is exactly what Mark 7 condemns. The reading cannot be held with Mark 7's principle, at a step rated wellSupported.
• Read as the apostolic word handed on unwritten — what Trent says it receives, traditions "received by the Apostles from the mouth of Christ himself, or from the Apostles themselves, the Holy Ghost dictating" (Session IV, in Waterworth's translation) — Mark 7 does not reach it. Nothing in the principle is denied. The reading meets the Mark 7 case only at the premise the step to sola scriptura needs, that no apostolic word survives outside Scripture, and that premise is disputed.

So Mark 7 does not decide between Rome and the Reformers. It moves the question to what the sola scriptura argument already turned on: whether any unwritten apostolic word survives and can be identified — and, even granting that none does, whether the principle then makes Scripture the sole infallible rule.

The quotation

mark7QuotesIsaiah

Mark 7:6–7 quotes Isaiah 29:13. Typed .quotation, not .allusion: Jesus introduces the words with "as it is written", and Mark gives them close to the Septuagint's wording.

def mark7QuotesIsaiah : IntertextEdge :=
  { fromPassage := Scripture.mark7_7, toPassage := Scripture.isaiah29_13,
    relation := RelationType.quotation,
    source := Scripture.na28Apparatus Scripture.mark7_7 }

matthew15QuotesIsaiah

Matthew 15:8–9 quotes the same verse, in the parallel account.

def matthew15QuotesIsaiah : IntertextEdge :=
  { fromPassage := Scripture.matthew15_9, toPassage := Scripture.isaiah29_13,
    relation := RelationType.quotation,
    source := Scripture.na28Apparatus Scripture.matthew15_9 }

The positions

mark7Principle — Mark 7: God's word judges human tradition

Mark 7's principle: Jesus' rebuke of the elders' tradition, and what it enacts — God's word judges human tradition, and no commandment of men is to be taught as God's word. It concludes the principle, and claims nothing about Scripture's place among the rules of faith.

No premise here rests on scripture alone.

mark7Case — Sola scriptura from Mark 7

Mark 7's case for sola scriptura: the principle, and the premise that no apostolic word survives outside Scripture.

No premise here rests on scripture alone.

mark7CaseWithoutTheHinge — Sola scriptura from Mark 7, without the premise about unwritten apostolic word

Mark 7's case without the premise that no apostolic word survives outside Scripture: the text, the principle, and the step to the sole rule.

No premise here rests on scripture alone.

tridentineCase — Trent (Tradition II)

Trent (Tradition II), as Mathison reads it: 2 Thessalonians 2:15 and tradition as a source of revelation alongside Scripture, so Scripture is not the sole rule. Unread: it says what Trent receives, not whether it is apostolic word or a commandment of men. The package tridentine asks these premises whether sola scriptura follows; this one states what they conclude, which is what a dispute weighs.

Grounded in scripture alone: 2 Thessalonians 2:15 — hold to the traditions taught by word or letter.

Two readings of Trent's "tradition"

trentReadAsMensCommandments

Reading Trent's traditions as commandments of men: God "is worshipped with laws of human invention", Calvin says of the laws of worship he opposed, and he applies Matthew 15:9 to them — "in vain do they worship me, teaching for doctrines the commandments of men" (Institutes IV.x.23). Rated disputed: Trent, Dei Verbum 9–10 and the Catechism deny that what Trent receives is of human origin — the Catechism (§83) distinguishes the apostolic Tradition from the "theological, disciplinary, liturgical or devotional traditions" which "can be retained, modified or even abandoned". No one reads Trent as claiming human origin: this is a reading of what those traditions are, not of what Trent says.

def trentReadAsMensCommandments : Source :=
  {
    primary :=
      Reference.work Bib.calvinInstitutes (Bib.Locus.sectionRef "IV.x.23"),
    tradition := Tradition.reformedProtestant,
    confidence := Confidence.disputed }

trentReadAsApostolicWord

Reading Trent's traditions as the apostolic word handed on unwritten: what Trent says it receives, the traditions "received by the Apostles from the mouth of Christ himself, or from the Apostles themselves, the Holy Ghost dictating" (Session IV, Waterworth 18). Dei Verbum 9 says the same: tradition "takes the word of God entrusted by Christ the Lord and the Holy Spirit to the Apostles, and hands it on". Rated consensus as an account of what Trent claims: Calvin and Chemnitz do not deny that Trent claims apostolic origin; they deny that the claim is true.

def trentReadAsApostolicWord : Source :=
  { primary := Reference.work waterworthTrent (Bib.Locus.page 18),
    supporting :=
      [Reference.work tannerDecrees
          (Bib.Locus.sectionRef
            "Trent, Session IV (1546), Decree on Sacred Books and Traditions"),
        Reference.work tannerDecrees
          (Bib.Locus.sectionRef "Vatican II (1965), Dei Verbum 9"),
        Reference.work catechismCatholicChurch (Bib.Locus.sectionRef "83")],
    tradition := Tradition.romanCatholic, confidence := Confidence.consensus }

asMensCommandments

Trent's tradition, read as commandments of men: what it receives alongside Scripture is a commandment of men, bound on the Church as God's word.

def asMensCommandments : Reading Claim :=
  { name := "as commandments of men",
    commits := p Claim.mensCommandmentBindsAsGodsWord,
    source := trentReadAsMensCommandments }

asApostolicWord

Trent's tradition, read as the apostolic word handed on unwritten: some apostolic teaching outside Scripture survives as God's word.

def asApostolicWord : Reading Claim :=
  { name := "as the apostolic word handed on unwritten",
    commits := notP Claim.noApostolicWordOutsideScripture,
    source := trentReadAsApostolicWord }

tridentineAsMensCommandments — Trent (Tradition II), read as commandments of men

Trent, with its tradition read as commandments of men.

Grounded in scripture alone: 2 Thessalonians 2:15 — hold to the traditions taught by word or letter.

tridentineAsApostolicWord — Trent (Tradition II), read as the apostolic word handed on unwritten

Trent, with its tradition read as the apostolic word handed on unwritten.

Grounded in scripture alone: 2 Thessalonians 2:15 — hold to the traditions taught by word or letter.

Readings, written down

marksPrincipleReading

The Reformed world: Mark 7's text and principle, no commandment of men bound as God's word, no apostolic word outside Scripture, and sola scriptura.

def marksPrincipleReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.mensCommandmentBindsAsGodsWord => False
    | x => True

romeGrantsMarksPrincipleReading

Rome's world, granting Mark 7: God's word judges human tradition and no commandment of men may be bound as God's word; but apostolic teaching survives outside Scripture, so Scripture is not the sole infallible rule. Nor is the Church's consensus a mere product of reading Scripture: for Rome, Scripture and Tradition flow from one source (Dei Verbum 9). A world must choose here, because the meanings exclude the consensus being that product and its being needed for Scripture's clear sense (TestimonyArguments.Meanings.SolaScriptura.joins).

def romeGrantsMarksPrincipleReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.creedalConsensusIsDerivedFromScripture => False
    | Claim.mensCommandmentBindsAsGodsWord => False
    | Claim.noApostolicWordOutsideScripture => False
    | Claim.scriptureIsSoleInfallibleRule => False
    | x => True

mensCommandmentsReading

A world in which Trent, its tradition read Calvin's way, holds together: its tradition is a commandment of men bound as God's word, and Scripture is not the sole rule. It must give up Mark 7's principle, so no one holds this world; it shows only that the reading is coherent on its own.

def mensCommandmentsReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.godsWordJudgesTradition => False
    | Claim.scriptureIsSoleInfallibleRule => False
    | x => True

Mark 7's principle, and what it reaches

mark7Principle_establishes

Mark 7 delivers its principle: God's word judges human tradition.

theorem mark7Principle_establishes : Establishes mark7Principle
-- axioms: propext, Quot.sound

mark7Principle_is_satisfiable

Mark 7's principle can be held without contradiction.

theorem mark7Principle_is_satisfiable : Satisfiable mark7Principle.premises
-- axioms: propext, Quot.sound

trent_grants_marks_principle

Trent grants Mark 7's principle. Trent's position, as it states it, can be held with the principle and everything Mark 7 says: the reading on which apostolic teaching survives outside Scripture, and no commandment of men is bound as God's word.

theorem trent_grants_marks_principle : Grants tridentineCase (p
    Claim.godsWordJudgesTradition)
-- axioms: propext, Quot.sound

mark7Case_establishes

Mark 7's case for sola scriptura holds, given its premise that no apostolic word survives outside Scripture.

theorem mark7Case_establishes : Establishes mark7Case
-- axioms: propext, Quot.sound

mark7Case_is_satisfiable

Mark 7's case can be held without contradiction.

theorem mark7Case_is_satisfiable : Satisfiable mark7Case.premises
-- axioms: propext, Quot.sound

mark7_without_the_hinge_leaves_the_sole_rule_open

Without that premise, Mark 7 leaves the sole rule open. Grant the text, the principle, and the step from them to the sole rule: sola scriptura neither follows nor fails. Rome's reading grants all of it and denies the sole rule; the Reformed reading grants all of it and holds the sole rule. One fact, not two: Mark 7 alone blocks no argument against sola scriptura and establishes none for it.

theorem mark7_without_the_hinge_leaves_the_sole_rule_open : Independent
    mark7CaseWithoutTheHinge.premises (p Claim.scriptureIsSoleInfallibleRule)
-- axioms: propext, Quot.sound

tridentineCase_establishes

Trent, as it states its position, holds together.

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

tridentineCase_is_satisfiable

Trent's case can be held without contradiction: Rome's world.

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

tridentineAsMensCommandments_establishes

Trent read as commandments of men still concludes what Trent concludes.

theorem tridentineAsMensCommandments_establishes : Establishes
    tridentineAsMensCommandments
-- axioms: propext, Quot.sound

tridentineAsApostolicWord_establishes

Trent read as the apostolic word still concludes what Trent concludes.

theorem tridentineAsApostolicWord_establishes : Establishes
    tridentineAsApostolicWord
-- axioms: propext, Quot.sound

tridentineAsMensCommandments_is_satisfiable

The first reading is fair: Trent, read as receiving commandments of men, can be held without contradiction — so long as Mark 7's principle is not held with it.

theorem tridentineAsMensCommandments_is_satisfiable : Satisfiable
    tridentineAsMensCommandments.premises
-- axioms: propext, Quot.sound

tridentineAsApostolicWord_is_satisfiable

The second reading is fair: Trent, read as receiving the apostolic word, can be held without contradiction.

theorem tridentineAsApostolicWord_is_satisfiable : Satisfiable
    tridentineAsApostolicWord.premises
-- axioms: propext, Quot.sound

mark7_does_not_reach_the_apostolic_word

Mark 7 does not reach the second reading. Trent, read as receiving the apostolic word, can be held with every premise of Mark 7's principle: it binds no commandment of men as God's word.

theorem mark7_does_not_reach_the_apostolic_word : Satisfiable
    (mark7Principle.premises ++ tridentineAsApostolicWord.premises)
-- axioms: propext, Quot.sound

Where each reading breaks

whereTheMensCommandmentsReadingFalls

Why Mark 7 stands against Trent, read as commandments of men. The crux is what the principle says of a commandment of men: it may not be bound as God's word. What it breaks is Trent's claim with the reading — tradition received alongside Scripture, and that tradition a commandment of men. Nothing else in Trent is touched. The crux is Mark 7's answer to the reading, not part of its case for the principle, which follows without it.

Why Mark 7: God's word judges human tradition stands against Trent (Tradition II), read as commandments of men.

• The crux: \(P_{37} \rightarrow \lnot P_{38}\), a premise of Mark 7: God's word judges human tradition.
• What it does: its conclusion follows without it — the crux is its answer to Trent (Tradition II), read as commandments of men.
• Granted: \(P_{3}\), \(P_{3} \rightarrow P_{37}\), which the break also needs.
• Where the rival breaks: \(P_{13}\), \(P_{13} \rightarrow P_{38}\) cannot be held together with \(P_{37} \rightarrow \lnot P_{38}\) and \(P_{3}\), \(P_{3} \rightarrow P_{37}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{3}\) Mark 7:1–13 (Matthew 15:1–9) — Jesus rebukes the elders' tradition, Corban above all, for voiding God's command — consensus: Mark 7:1-13; Matt 15:1-9; calvin-institutes-1960, §IV.x.10
  • \(P_{37}\) God's word judges human tradition: no commandment of men may be taught as God's word, and a tradition that voids God's command is void — consensus: tanner-decrees-1990, §Vatican II (1965), Dei Verbum 10; calvin-institutes-1960, §IV.x.23; florovsky-bible-church-tradition-1972
  • the step itself — well supported: tanner-decrees-1990, §Vatican II (1965), Dei Verbum 10; calvin-institutes-1960, §IV.x.23

whereTheApostolicWordReadingFalls

Why Mark 7's case stands against Trent, read as the apostolic word. Not at the principle, which this reading grants, but at the premise the step to sola scriptura needs: that no apostolic teaching survives outside Scripture. The reading denies exactly that, and the premise is rated disputed. The step from it to the sole rule is disputed too, so granting the premise would not alone settle the question.

Why Sola scriptura from Mark 7 stands against Trent (Tradition II), read as the apostolic word handed on unwritten.

• The crux: \(P_{39}\), a premise of Sola scriptura from Mark 7.
• What it does: its conclusion does not follow without it.
• Where the rival breaks: \(P_{13}\), \(P_{13} \rightarrow \lnot P_{39}\) cannot be held together with \(P_{39}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{39}\) No apostolic teaching handed on outside Scripture survives, identifiable as the word of God — disputed: whitaker-disputation-1849, p. 506; westminster-confession-1647, §I.6

The dilemma

whatTrentsTraditionIs

What Trent's tradition is, read both ways. The claim is Trent's: tradition is received as a source of revelation alongside Scripture.

Read as commandments of men, it cannot be held with Mark 7's principle, at a step rated wellSupported: Isaiah 29:13, as Jesus quotes it, says a commandment of men may not be bound as God's word.

Read as the apostolic word handed on unwritten — what Trent says it receives — Mark 7's principle does not reach it. It cannot be held with Mark 7's case for sola scriptura, but only at that case's own premise that no apostolic word survives outside Scripture, which is disputed. That is the question the sola scriptura argument already turns on; Mark 7 does not settle it.

Each reading is fair: Trent read either way can be held without contradiction. Which reading fits Trent is not something the dilemma decides; what it shows is what each costs.

Every reading of \(P_{13}\), answered. Trent (Tradition II) holds \(P_{13}\). It is read 2 ways here, and each reading is checked; none can be left out.

1. Read as commandments of men. The claim commits Trent (Tradition II) to \(P_{38}\) — so read by calvin-institutes-1960, §IV.x.23 (disputed).

Against Mark 7: God's word judges human tradition, it cannot be held. Where it breaks:

Why Mark 7: God's word judges human tradition stands against Trent (Tradition II), read as commandments of men.

• The crux: \(P_{37} \rightarrow \lnot P_{38}\), a premise of Mark 7: God's word judges human tradition.
• What it does: its conclusion follows without it — the crux is its answer to Trent (Tradition II), read as commandments of men.
• Granted: \(P_{3}\), \(P_{3} \rightarrow P_{37}\), which the break also needs.
• Where the rival breaks: \(P_{13}\), \(P_{13} \rightarrow P_{38}\) cannot be held together with \(P_{37} \rightarrow \lnot P_{38}\) and \(P_{3}\), \(P_{3} \rightarrow P_{37}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{3}\) Mark 7:1–13 (Matthew 15:1–9) — Jesus rebukes the elders' tradition, Corban above all, for voiding God's command — consensus: Mark 7:1-13; Matt 15:1-9; calvin-institutes-1960, §IV.x.10
  • \(P_{37}\) God's word judges human tradition: no commandment of men may be taught as God's word, and a tradition that voids God's command is void — consensus: tanner-decrees-1990, §Vatican II (1965), Dei Verbum 10; calvin-institutes-1960, §IV.x.23; florovsky-bible-church-tradition-1972
  • the step itself — well supported: tanner-decrees-1990, §Vatican II (1965), Dei Verbum 10; calvin-institutes-1960, §IV.x.23

2. Read as the apostolic word handed on unwritten. The claim commits Trent (Tradition II) to \(\lnot P_{39}\) — so read by waterworth-trent-1848, p. 18; tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; tanner-decrees-1990, §Vatican II (1965), Dei Verbum 9; catholic-church-catechism-2000, §83 (consensus).

Against Mark 7: God's word judges human tradition, it is not reached: Mark 7: God's word judges human tradition holds, and can be held together with it.

Against Sola scriptura from Mark 7, it cannot be held. Where it breaks:

Why Sola scriptura from Mark 7 stands against Trent (Tradition II), read as the apostolic word handed on unwritten.

• The crux: \(P_{39}\), a premise of Sola scriptura from Mark 7.
• What it does: its conclusion does not follow without it.
• Where the rival breaks: \(P_{13}\), \(P_{13} \rightarrow \lnot P_{39}\) cannot be held together with \(P_{39}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(P_{39}\) No apostolic teaching handed on outside Scripture survives, identifiable as the word of God — disputed: whitaker-disputation-1849, p. 506; westminster-confession-1647, §I.6

TestimonyArguments.SolaScriptura.Dispute — what Mark 7 decides between Rome and the Reformers

Mark7.lean asks what each position entails. This module asks what happens when they meet. Five parties: Mark 7's principle; Mark 7's case for sola scriptura; Trent, as it states its position; and Trent with its tradition read each of the two ways the dilemma whatTrentsTraditionIs names. Who defeats whom is not stipulated — each defeat, and each absence of one, is computed from the parties' premises and checked by the kernel (see Testimony.Logic.Dispute).

How to read the verdicts

• 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. A defeat that runs both ways is 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.
• Forced. Accepted however every standoff is resolved: nothing attacks it that it cannot rule out.
• Can be defended. 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: the dispute, as argued, cannot make a reader accept it.
• Cannot be defended. No consistent position can hold it and answer its attackers.
• A defensible position that cannot be enlarged (a maximal one) is a consistent position answering every attack on its members, to which no other party can be added without losing that. "Some maximal defensible position holds it" means a reader can hold it and lose nothing by it.

The ratings decide one thing here

Every party but one rests on something rated disputed. Mark 7's case rests on the premise that no apostolic word survives outside Scripture. Trent rests on tradition as a source of revelation alongside Scripture — a claim this module's audit moved from wellSupported to disputed, because Geiselmann grants Session IV and denies that it canonised two coordinate sources. The reading of Trent as commandments of men rests on Calvin's reading, which Rome denies.

The exception is Mark 7's principle. Its text is consensus, and its step from the text is wellSupported: no one was found who grants Mark 7 and denies that God's word judges human tradition. So an attack on it from a party at the bottom fails, and its attack on such a party succeeds.

Who defeats whom

• Mark 7's principle defeats Trent read as commandments of men, and not the reverse. Read that way, Trent binds a commandment of men as God's word; the principle denies that any may be. The reading's reply, from a claim rated disputed, fails against the principle.
• Mark 7's case and Trent defeat each other, whichever way Trent is read. One concludes that Scripture is the sole infallible rule, the other that it is not; and Trent read as the apostolic word also denies the premise Mark 7's case needs. Each side's weakest link is disputed, so no rating breaks the tie.
• Mark 7's principle and Trent do not conflict, read as Trent states it or as the apostolic word (trent_grants_marks_principle).

What follows

Mark 7's principle is forced (marks_principle_prevails), and it is common ground: Rome grants it. Trent, read as commandments of men, cannot be defended (trent_as_mens_commandments_indefensible). Between Mark 7's case for sola scriptura and Trent, the dispute chooses neither: each can be defended, and neither is forced (mark7_case_defensible, mark7_case_not_forced, trent_defensible_against_mark7, trent_not_forced_against_mark7). Mark 7 does not decide the Reformation's question. What would decide it is argued, not weighed: whether any apostolic word survives outside Scripture, and, even granting that none does, whether the principle then makes Scripture the sole infallible rule. Both are rated disputed.

Strength

mark7Principle_strength

Mark 7's principle does not rest on anything disputed. The text is consensus, and the step from it wellSupported, so its weakest link is well supported: 2 on the scale from 0, disputed, to 3, consensus.

theorem mark7Principle_strength : mark7Principle.strength = 2
-- axioms: propext

mark7Case_strength

Mark 7's case rests on the premise that no apostolic word survives outside Scripture, rated disputed.

theorem mark7Case_strength : mark7Case.strength = 0
-- axioms: propext

tridentineCase_strength

Trent rests on tradition as a coordinate source of revelation, rated disputed.

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

tridentineAsMensCommandments_strength

Trent read as commandments of men rests on everything Trent does, and on Calvin's reading, rated disputed.

theorem tridentineAsMensCommandments_strength :
    tridentineAsMensCommandments.strength = 0
-- axioms: propext

tridentineAsApostolicWord_strength

Trent read as the apostolic word rests on everything Trent does.

theorem tridentineAsApostolicWord_strength :
    tridentineAsApostolicWord.strength = 0
-- axioms: propext

The dispute

mark7PartyNode

The package each party argues from.

def mark7PartyNode : Mark7Party → ArgumentPackage Claim :=
  fun x =>
    match x with
    | Mark7Party.principle => mark7Principle
    | Mark7Party.mark7 => mark7Case
    | Mark7Party.trent => tridentineCase
    | Mark7Party.trentAsMensCommandments =>
      tridentineAsMensCommandments
    | Mark7Party.trentAsApostolicWord =>
      tridentineAsApostolicWord

mark7Dispute

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

def mark7Dispute : Dispute Claim Mark7Party :=
  { node := mark7PartyNode,
    consistent := mark7Dispute._proof_1,
    sound := mark7Dispute._proof_2,
    rated := mark7Dispute._proof_8 }

marks_principle_stands_with_trent

Mark 7's principle stands with Trent, as Trent states it and read as the apostolic word: Rome's world, in which the principle holds and apostolic teaching survives outside Scripture.

theorem marks_principle_stands_with_trent : mark7Dispute.StandTogether
    [Mark7Party.principle, Mark7Party.trent, Mark7Party.trentAsApostolicWord]
-- axioms: propext, Classical.choice, Quot.sound

mark7PartyDefeats

The defeats of the dispute, as a table.

def mark7PartyDefeats : Mark7Party → Mark7Party → Prop :=
  fun x x_1 =>
    match x, x_1 with
    | Mark7Party.principle,
      Mark7Party.trentAsMensCommandments => True
    | Mark7Party.mark7, Mark7Party.trent => True
    | Mark7Party.mark7,
      Mark7Party.trentAsMensCommandments => True
    | Mark7Party.mark7,
      Mark7Party.trentAsApostolicWord => True
    | Mark7Party.trent, Mark7Party.mark7 => True
    | Mark7Party.trentAsMensCommandments,
      Mark7Party.mark7 => True
    | Mark7Party.trentAsApostolicWord,
      Mark7Party.mark7 => True
    | x, x_2 => False

instDecidableRelMark7PartyMark7PartyDefeats

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

def instDecidableRelMark7PartyMark7PartyDefeats : DecidableRel
    mark7PartyDefeats

mark7PartyStrength

Each party's weakest link: at the bottom for all but Mark 7's principle.

def mark7PartyStrength : Mark7Party → ℕ :=
  fun x =>
    match x with
    | Mark7Party.principle => 2
    | x => 0

mark7PartyNode_strength

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

theorem mark7PartyNode_strength : ∀ (i : Mark7Party), (mark7PartyNode
    i).strength = mark7PartyStrength i
-- axioms: propext

mark7Dispute_defeats

Who defeats whom, all 25 pairs. Mark 7's principle defeats Trent read as commandments of men, and that reading's reply fails against it. Mark 7's case and Trent defeat each other, as Trent states it and read either way. 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.

theorem mark7Dispute_defeats : ∀ (i j : Mark7Party), mark7Dispute.defeats i j
    ↔ mark7PartyDefeats i j
-- axioms: propext, Classical.choice, Quot.sound

mark7Finite

The dispute in the form the verdict solver computes with.

def mark7Finite : Solver.Finite mark7Dispute.defeats :=
  {
    parties :=
      [Mark7Party.principle, Mark7Party.mark7,
        Mark7Party.trent,
        Mark7Party.trentAsMensCommandments,
        Mark7Party.trentAsApostolicWord],
    complete := mark7Finite._proof_1,
    defeats := fun i j => decide (mark7PartyDefeats i j),
    spec := mark7Finite._proof_2 }

The dispute as a graph

mark7Dispute_supports

Nothing supports anything in the dispute over Mark 7, in all 25 pairs: no party's conclusion entails a claim another rests on. Mark 7's principle is derived inside Mark 7's case, not assumed there, so the relation between them is not support. Every cell is computed by supports? and checked by the kernel.

theorem mark7Dispute_supports : ∀ (i j : Mark7Party), ¬mark7Dispute.supports i
    j
-- axioms: propext, Classical.choice, Quot.sound

mark7PartyPartOf

Whose case is part of whose, as a table: besides each party's own, Trent's is part of each reading of it.

def mark7PartyPartOf : Mark7Party → Mark7Party → Prop :=
  fun x x_1 =>
    match x, x_1 with
    | Mark7Party.trent,
      Mark7Party.trentAsMensCommandments => True
    | Mark7Party.trent,
      Mark7Party.trentAsApostolicWord => True
    | i, j => i = j

instDecidableRelMark7PartyMark7PartyPartOf

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

def instDecidableRelMark7PartyMark7PartyPartOf : DecidableRel mark7PartyPartOf

mark7Dispute_partOf

Whose case is part of whose, all 25 pairs: Trent's case is part of each reading of it, which only adds to it; and every case is part of itself. Every cell is computed by partOf? and checked by the kernel.

theorem mark7Dispute_partOf : ∀ (i j : Mark7Party), mark7Dispute.partOf i j ↔
    mark7PartyPartOf i j
-- axioms: propext, Classical.choice, Quot.sound

mark7Map

The dispute over Mark 7 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 mark7Dispute_defeats, the supports the cells of mark7Dispute_supports and the parts the cells of mark7Dispute_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

marksPrincipleUnanswered

How the dispute is settled as far as it can be, in one stage: nothing defeats Mark 7's principle, so it comes first; and nothing joins it. Mark 7's case has Trent, and Trent has Mark 7's case — a standoff; Trent read as the apostolic word has Mark 7's case; and Trent read as commandments of men has the principle itself.

What the dispute forces is exactly Mark 7: God's word judges human tradition.

• Stage 1: Mark 7: God's word judges human tradition.
  • Mark 7: God's word judges human tradition is defeated by nothing.
• Nothing else is forced:
  • Trent (Tradition II) defeats Sola scriptura from Mark 7, and nothing forced defeats Trent (Tradition II).
  • Sola scriptura from Mark 7 defeats Trent (Tradition II), and nothing forced defeats Sola scriptura from Mark 7.
  • Mark 7: God's word judges human tradition defeats Trent (Tradition II), read as commandments of men, and nothing forced defeats Mark 7: God's word judges human tradition.
  • Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten, and nothing forced defeats Sola scriptura from Mark 7.

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

• Mark 7: God's word judges human tradition, weakest at well supported:
  • an inference step — tanner-decrees-1990, §Vatican II (1965), Dei Verbum 10; calvin-institutes-1960, §IV.x.23
• Sola scriptura from Mark 7, weakest at disputed:
  • No apostolic teaching handed on outside Scripture survives, identifiable as the word of God — whitaker-disputation-1849, p. 506; westminster-confession-1647, §I.6
  • an inference step — geiselmann-meaning-of-tradition-1966; tanner-decrees-1990, §Vatican I (1870), Pastor Aeternus, ch. 4; florovsky-bible-church-tradition-1972
• Trent (Tradition II), weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
• Trent (Tradition II), read as commandments of men, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
  • an inference step — calvin-institutes-1960, §IV.x.23
• Trent (Tradition II), read as the apostolic word handed on unwritten, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966

Why Mark 7: God's word judges human tradition defeats Trent (Tradition II), read as commandments of men, at the level of the claims: whereTheMensCommandmentsReadingFalls.

Why Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten, at the level of the claims: whereTheApostolicWordReadingFalls.

marks_principle_prevails

Mark 7's principle prevails outright, and it is common ground. The grounded extension — what the dispute forces before any choice between rivals — is exactly the principle: God's word judges human tradition, and no commandment of men may be taught as God's word. Nothing defeats it: the one party that contradicts it, Trent read as commandments of men, rests on a reading rated disputed, and its reply fails against a principle whose every link is rated wellSupported or better. And Trent, as it states its position, does not contradict it at all (trent_grants_marks_principle).

What this does not claim: that sola scriptura is forced. Mark 7's case for it is not (mark7_case_not_forced).

theorem marks_principle_prevails : Framework.grounded mark7Dispute.defeats =
    {Mark7Party.principle}
-- axioms: propext, Classical.choice, Quot.sound

mensCommandmentsReadingAnswered

Why Trent, read as commandments of men, cannot be defended: Mark 7's principle defeats it, and nothing defeats the principle.

Trent (Tradition II), read as commandments of men cannot be defended: no admissible position holds it.

• Mark 7: God's word judges human tradition defeats Trent (Tradition II), read as commandments of men, and nothing defeats Mark 7: God's word judges human tradition.

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

• Mark 7: God's word judges human tradition, weakest at well supported:
  • an inference step — tanner-decrees-1990, §Vatican II (1965), Dei Verbum 10; calvin-institutes-1960, §IV.x.23
• Trent (Tradition II), read as commandments of men, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
  • an inference step — calvin-institutes-1960, §IV.x.23
• Sola scriptura from Mark 7, weakest at disputed:
  • No apostolic teaching handed on outside Scripture survives, identifiable as the word of God — whitaker-disputation-1849, p. 506; westminster-confession-1647, §I.6
  • an inference step — geiselmann-meaning-of-tradition-1966; tanner-decrees-1990, §Vatican I (1870), Pastor Aeternus, ch. 4; florovsky-bible-church-tradition-1972
• Trent (Tradition II), weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
• Trent (Tradition II), read as the apostolic word handed on unwritten, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966

Why Mark 7: God's word judges human tradition defeats Trent (Tradition II), read as commandments of men, at the level of the claims: whereTheMensCommandmentsReadingFalls.

trent_as_mens_commandments_indefensible

Trent, read as commandments of men, cannot be defended. No consistent position that answers its attackers can hold it: Mark 7's principle defeats it, and nothing answers the principle. This is the first horn of whatTrentsTraditionIs, weighed: if what Trent receives alongside Scripture were a commandment of men, Jesus' words in Mark 7 would condemn it, at a step rated wellSupported.

What this does not claim: that Trent's tradition is a commandment of men. Trent says the opposite, and Calvin's reading of it is rated disputed.

theorem trent_as_mens_commandments_indefensible : ∀ (S : Set Mark7Party),
    Framework.Admissible mark7Dispute.defeats S →
    Mark7Party.trentAsMensCommandments ∉ S
-- axioms: propext, Classical.choice, Quot.sound

mark7StandsWithItsPrinciple

Why Mark 7's case can be defended: it stands with Mark 7's principle, and answers every party that defeats it — Trent, read or unread — itself.

Sola scriptura from Mark 7 is accepted on some resolution.

• A position holding Mark 7: God's word judges human tradition, Sola scriptura from Mark 7 can be held.
• None of Mark 7: God's word judges human tradition, Sola scriptura from Mark 7 defeats another, and each attack on them is answered from among them:
  • Trent (Tradition II) defeats Sola scriptura from Mark 7, and Sola scriptura from Mark 7 defeats Trent (Tradition II).
  • Trent (Tradition II), read as commandments of men defeats Sola scriptura from Mark 7, and Mark 7: God's word judges human tradition defeats Trent (Tradition II), read as commandments of men.
  • Trent (Tradition II), read as the apostolic word handed on unwritten defeats Sola scriptura from Mark 7, and Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten.

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

• Mark 7: God's word judges human tradition, weakest at well supported:
  • an inference step — tanner-decrees-1990, §Vatican II (1965), Dei Verbum 10; calvin-institutes-1960, §IV.x.23
• Sola scriptura from Mark 7, weakest at disputed:
  • No apostolic teaching handed on outside Scripture survives, identifiable as the word of God — whitaker-disputation-1849, p. 506; westminster-confession-1647, §I.6
  • an inference step — geiselmann-meaning-of-tradition-1966; tanner-decrees-1990, §Vatican I (1870), Pastor Aeternus, ch. 4; florovsky-bible-church-tradition-1972
• Trent (Tradition II), weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
• Trent (Tradition II), read as commandments of men, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
  • an inference step — calvin-institutes-1960, §IV.x.23
• Trent (Tradition II), read as the apostolic word handed on unwritten, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966

Why Mark 7: God's word judges human tradition defeats Trent (Tradition II), read as commandments of men, at the level of the claims: whereTheMensCommandmentsReadingFalls.

Why Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten, at the level of the claims: whereTheApostolicWordReadingFalls.

mark7_case_defensible

Sola scriptura from Mark 7 can be defended. Some maximal defensible position holds it, with Mark 7's principle. Every party that defeats it — Trent, as it states its position and read either way — it defeats back.

theorem mark7_case_defensible : Framework.CredulouslyAccepted
    mark7Dispute.defeats Mark7Party.mark7
-- axioms: propext, Classical.choice, Quot.sound

mark7AnsweredByTrent

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

Sola scriptura from Mark 7 is not accepted on every resolution.

• A position holding Mark 7: God's word judges human tradition, Trent (Tradition II), Trent (Tradition II), read as the apostolic word handed on unwritten can be held, and it holds Trent (Tradition II); Trent (Tradition II) conflicts with Sola scriptura from Mark 7: Trent (Tradition II) defeats Sola scriptura from Mark 7, and Sola scriptura from Mark 7 defeats Trent (Tradition II).
• None of Mark 7: God's word judges human tradition, Trent (Tradition II), Trent (Tradition II), read as the apostolic word handed on unwritten defeats another, and each attack on them is answered from among them:
  • Sola scriptura from Mark 7 defeats Trent (Tradition II), and Trent (Tradition II) defeats Sola scriptura from Mark 7.
  • Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten, and Trent (Tradition II) defeats Sola scriptura from Mark 7.

What this rests on. The reasons state 3 defeats and 13 absences of defeat, each a cell of the defeat table, mark7Dispute_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 (Tradition II), weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
• Sola scriptura from Mark 7, weakest at disputed:
  • No apostolic teaching handed on outside Scripture survives, identifiable as the word of God — whitaker-disputation-1849, p. 506; westminster-confession-1647, §I.6
  • an inference step — geiselmann-meaning-of-tradition-1966; tanner-decrees-1990, §Vatican I (1870), Pastor Aeternus, ch. 4; florovsky-bible-church-tradition-1972
• Mark 7: God's word judges human tradition, weakest at well supported:
  • an inference step — tanner-decrees-1990, §Vatican II (1965), Dei Verbum 10; calvin-institutes-1960, §IV.x.23
• Trent (Tradition II), read as the apostolic word handed on unwritten, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
• Trent (Tradition II), read as commandments of men, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
  • an inference step — calvin-institutes-1960, §IV.x.23

Why Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten, at the level of the claims: whereTheApostolicWordReadingFalls.

mark7_case_not_forced

Nor is it forced. A maximal defensible position holds Trent, with Mark 7's principle and with Trent read as the apostolic word, and cannot hold Mark 7's case with it. Their weakest links are all disputed, so no rating breaks the tie. What would decide it is argued, not weighed: whether any apostolic word survives outside Scripture (whereTheApostolicWordReadingFalls), and, even granting that none does, whether the principle then makes Scripture the sole infallible rule — a step Geiselmann and Florovsky deny.

theorem mark7_case_not_forced : ¬Framework.SkepticallyAccepted
    mark7Dispute.defeats Mark7Party.mark7
-- axioms: propext, Classical.choice, Quot.sound

trentStandsWithMarksPrinciple

Why Trent can be defended against Mark 7: it stands with Mark 7's principle and with its own reading as the apostolic word, and answers Mark 7's case itself.

Trent (Tradition II) is accepted on some resolution.

• A position holding Mark 7: God's word judges human tradition, Trent (Tradition II), Trent (Tradition II), read as the apostolic word handed on unwritten can be held.
• None of Mark 7: God's word judges human tradition, Trent (Tradition II), Trent (Tradition II), read as the apostolic word handed on unwritten defeats another, and each attack on them is answered from among them:
  • Sola scriptura from Mark 7 defeats Trent (Tradition II), and Trent (Tradition II) defeats Sola scriptura from Mark 7.
  • Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten, and Trent (Tradition II) defeats Sola scriptura from Mark 7.

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

• Mark 7: God's word judges human tradition, weakest at well supported:
  • an inference step — tanner-decrees-1990, §Vatican II (1965), Dei Verbum 10; calvin-institutes-1960, §IV.x.23
• Trent (Tradition II), weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
• Trent (Tradition II), read as the apostolic word handed on unwritten, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
• Sola scriptura from Mark 7, weakest at disputed:
  • No apostolic teaching handed on outside Scripture survives, identifiable as the word of God — whitaker-disputation-1849, p. 506; westminster-confession-1647, §I.6
  • an inference step — geiselmann-meaning-of-tradition-1966; tanner-decrees-1990, §Vatican I (1870), Pastor Aeternus, ch. 4; florovsky-bible-church-tradition-1972
• Trent (Tradition II), read as commandments of men, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
  • an inference step — calvin-institutes-1960, §IV.x.23

Why Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten, at the level of the claims: whereTheApostolicWordReadingFalls.

trent_defensible_against_mark7

Trent, as it states its position, can be defended against Mark 7 — and with Mark 7's principle. Some maximal defensible position holds Trent, the principle, and Trent read as the apostolic word. Granting everything Mark 7's principle says costs Trent nothing, so long as what it receives is the apostolic word and not a commandment of men.

theorem trent_defensible_against_mark7 : Framework.CredulouslyAccepted
    mark7Dispute.defeats Mark7Party.trent
-- axioms: propext, Classical.choice, Quot.sound

trentAnsweredByMark7

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

Trent (Tradition II) is not accepted on every resolution.

• A position holding Mark 7: God's word judges human tradition, Sola scriptura from Mark 7 can be held, and it holds Sola scriptura from Mark 7; Sola scriptura from Mark 7 conflicts with Trent (Tradition II): Sola scriptura from Mark 7 defeats Trent (Tradition II), and Trent (Tradition II) defeats Sola scriptura from Mark 7.
• None of Mark 7: God's word judges human tradition, Sola scriptura from Mark 7 defeats another, and each attack on them is answered from among them:
  • Trent (Tradition II) defeats Sola scriptura from Mark 7, and Sola scriptura from Mark 7 defeats Trent (Tradition II).
  • Trent (Tradition II), read as commandments of men defeats Sola scriptura from Mark 7, and Mark 7: God's word judges human tradition defeats Trent (Tradition II), read as commandments of men.
  • Trent (Tradition II), read as the apostolic word handed on unwritten defeats Sola scriptura from Mark 7, and Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten.

What this rests on. The reasons state 6 defeats and 7 absences of defeat, each a cell of the defeat table, mark7Dispute_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 scriptura from Mark 7, weakest at disputed:
  • No apostolic teaching handed on outside Scripture survives, identifiable as the word of God — whitaker-disputation-1849, p. 506; westminster-confession-1647, §I.6
  • an inference step — geiselmann-meaning-of-tradition-1966; tanner-decrees-1990, §Vatican I (1870), Pastor Aeternus, ch. 4; florovsky-bible-church-tradition-1972
• Trent (Tradition II), weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
• Mark 7: God's word judges human tradition, weakest at well supported:
  • an inference step — tanner-decrees-1990, §Vatican II (1965), Dei Verbum 10; calvin-institutes-1960, §IV.x.23
• Trent (Tradition II), read as commandments of men, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
  • an inference step — calvin-institutes-1960, §IV.x.23
• Trent (Tradition II), read as the apostolic word handed on unwritten, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966

Why Mark 7: God's word judges human tradition defeats Trent (Tradition II), read as commandments of men, at the level of the claims: whereTheMensCommandmentsReadingFalls.

Why Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten, at the level of the claims: whereTheApostolicWordReadingFalls.

trent_not_forced_against_mark7

Nor is Trent forced. A maximal defensible position holds Mark 7's case for sola scriptura, and cannot hold Trent with it. Between them the dispute chooses neither.

theorem trent_not_forced_against_mark7 : ¬Framework.SkepticallyAccepted
    mark7Dispute.defeats Mark7Party.trent
-- axioms: propext, Classical.choice, Quot.sound

TestimonyArguments.SolaScriptura.Hearings — Mark 7, heard against each reading of Trent

The dispute over Mark 7 hears Trent three ways at once: as Trent states its position, and with its tradition read each of the two ways the dilemma whatTrentsTraditionIs names. A reader usually has one reading in mind, and asks what Mark 7 settles if that is what Trent means. Each question is answered by hearing the same dispute with the other readings set aside. Nothing is re-argued: a hearing keeps every defeat the full dispute proved.

If Rome's tradition were the commandments of men, would Mark 7 settle sola scriptura? Heard against that reading alone (mensCommandmentsHearing), Mark 7's case is forced — but only because nothing left in the hearing contests it. The reading is the only party that attacks it, and the principle defeats the reading. Mark 7's case still rests on two things rated disputed: that no apostolic word survives outside Scripture, and the step from the principle to the sole rule. The reading of Trent as commandments of men contests neither, and the parties that would are set aside. This is the Protestant polemic at full strength — and it holds only on a reading of Trent that Trent itself denies.

If Rome's tradition is the apostolic word handed on unwritten, what does Mark 7 settle? Heard against that reading (apostolicWordHearing), only the principle — which the reading grants. Mark 7's case and the reading defeat each other at one premise, that no apostolic word survives outside Scripture, and each side's weakest link is disputed. So the dispute chooses neither.

The difference between the two hearings is the whole of what Mark 7 contributes: against Rome's tradition read as human, it leaves Mark 7's case unopposed; against it read as apostolic, it leaves the question where it was. Which it is, Mark 7 does not say.

Heard against the reading as commandments of men

mensCommandmentsHearing

Mark 7's principle and case, heard against Trent read as commandments of men. Not heard: Trent as it states its position, and Trent read as the apostolic word.

def mensCommandmentsHearing : Dispute Claim { i // i ∈ [Mark7Party.principle,
    Mark7Party.mark7, Mark7Party.trentAsMensCommandments] } :=
  mark7Dispute.restrict fun x =>
    x ∈
      [Mark7Party.principle, Mark7Party.mark7,
        Mark7Party.trentAsMensCommandments]

mensCommandmentsHearingFinite

The hearing, in the form the verdict solver computes with.

def mensCommandmentsHearingFinite : Solver.Finite fun i j =>
    mark7Dispute.defeats ↑i ↑j :=
  mark7Finite.restrict fun x =>
    x ∈
      [Mark7Party.principle, Mark7Party.mark7,
        Mark7Party.trentAsMensCommandments]

mensCommandmentsHearingSettles

How the hearing is settled, in two stages: nothing defeats Mark 7's principle, so it comes first; the principle defeats the reading, and with the reading answered Mark 7's case has no attacker left, so it comes second.

What the dispute forces is exactly Mark 7: God's word judges human tradition, Sola scriptura from Mark 7.

• Stage 1: Mark 7: God's word judges human tradition.
  • Mark 7: God's word judges human tradition is defeated by nothing.
• Stage 2: Sola scriptura from Mark 7.
  • Trent (Tradition II), read as commandments of men defeats Sola scriptura from Mark 7, and Mark 7: God's word judges human tradition defeats Trent (Tradition II), read as commandments of men.
• Nothing else is forced:
  • Mark 7: God's word judges human tradition defeats Trent (Tradition II), read as commandments of men, and nothing forced defeats Mark 7: God's word judges human tradition.

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

• Mark 7: God's word judges human tradition, weakest at well supported:
  • an inference step — tanner-decrees-1990, §Vatican II (1965), Dei Verbum 10; calvin-institutes-1960, §IV.x.23
• Sola scriptura from Mark 7, weakest at disputed:
  • No apostolic teaching handed on outside Scripture survives, identifiable as the word of God — whitaker-disputation-1849, p. 506; westminster-confession-1647, §I.6
  • an inference step — geiselmann-meaning-of-tradition-1966; tanner-decrees-1990, §Vatican I (1870), Pastor Aeternus, ch. 4; florovsky-bible-church-tradition-1972
• Trent (Tradition II), read as commandments of men, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
  • an inference step — calvin-institutes-1960, §IV.x.23

Why Mark 7: God's word judges human tradition defeats Trent (Tradition II), read as commandments of men, at the level of the claims: whereTheMensCommandmentsReadingFalls.

mark7_forced_against_mens_commandments

Against Rome's tradition read as commandments of men, Mark 7's case is unopposed. Heard against that reading alone, Mark 7's principle and Mark 7's case for sola scriptura are both forced: the reading is the only party in the hearing that attacks the case, and the principle defeats it.

What this does not claim: that Rome's tradition is the commandments of men — Trent says what it receives came from Christ and the apostles, and the reading that says otherwise is rated disputed. Nor that Mark 7's case is sound. It still rests on the premise that no apostolic word survives outside Scripture, and on a step Geiselmann and Florovsky deny, both disputed; no party heard here contests either. Trent as it states its position, and Trent read as the apostolic word, are set aside.

theorem mark7_forced_against_mens_commandments : Framework.grounded
    mensCommandmentsHearing.defeats = Solver.toSet (Witness.listSub
    (Membership.mem [Mark7Party.principle, Mark7Party.mark7,
    Mark7Party.trentAsMensCommandments]) [Mark7Party.principle,
    Mark7Party.mark7])
-- axioms: propext, Classical.choice, Quot.sound

Heard against the reading as the apostolic word

apostolicWordHearing

Mark 7's principle and case, heard against Trent read as the apostolic word handed on unwritten. Not heard: Trent as it states its position, and Trent read as commandments of men.

def apostolicWordHearing : Dispute Claim { i // i ∈ [Mark7Party.principle,
    Mark7Party.mark7, Mark7Party.trentAsApostolicWord] } :=
  mark7Dispute.restrict fun x =>
    x ∈
      [Mark7Party.principle, Mark7Party.mark7,
        Mark7Party.trentAsApostolicWord]

apostolicWordHearingFinite

The hearing, in the form the verdict solver computes with.

def apostolicWordHearingFinite : Solver.Finite fun i j => mark7Dispute.defeats
    ↑i ↑j :=
  mark7Finite.restrict fun x =>
    x ∈
      [Mark7Party.principle, Mark7Party.mark7,
        Mark7Party.trentAsApostolicWord]

apostolicWordHearingSettles

How the hearing is settled: nothing defeats Mark 7's principle, so it comes first; and nothing joins it, because Mark 7's case and the reading defeat each other.

What the dispute forces is exactly Mark 7: God's word judges human tradition.

• Stage 1: Mark 7: God's word judges human tradition.
  • Mark 7: God's word judges human tradition is defeated by nothing.
• Nothing else is forced:
  • Trent (Tradition II), read as the apostolic word handed on unwritten defeats Sola scriptura from Mark 7, and nothing forced defeats Trent (Tradition II), read as the apostolic word handed on unwritten.
  • Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten, and nothing forced defeats Sola scriptura from Mark 7.

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

• Mark 7: God's word judges human tradition, weakest at well supported:
  • an inference step — tanner-decrees-1990, §Vatican II (1965), Dei Verbum 10; calvin-institutes-1960, §IV.x.23
• Sola scriptura from Mark 7, weakest at disputed:
  • No apostolic teaching handed on outside Scripture survives, identifiable as the word of God — whitaker-disputation-1849, p. 506; westminster-confession-1647, §I.6
  • an inference step — geiselmann-meaning-of-tradition-1966; tanner-decrees-1990, §Vatican I (1870), Pastor Aeternus, ch. 4; florovsky-bible-church-tradition-1972
• Trent (Tradition II), read as the apostolic word handed on unwritten, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966

Why Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten, at the level of the claims: whereTheApostolicWordReadingFalls.

against_the_apostolic_word_only_the_principle_is_forced

If Rome's tradition is the apostolic word, Mark 7 forces only its principle — which that reading grants. Mark 7's case and the reading stand off at the premise that no apostolic word survives outside Scripture.

theorem against_the_apostolic_word_only_the_principle_is_forced :
    Framework.grounded apostolicWordHearing.defeats = Solver.toSet
    (Witness.listSub (Membership.mem [Mark7Party.principle, Mark7Party.mark7,
    Mark7Party.trentAsApostolicWord]) [Mark7Party.principle])
-- axioms: propext, Classical.choice, Quot.sound

mark7AnsweredByTheApostolicWord

Why Mark 7's case is not forced in this hearing: a defensible position holds the reading, with the principle, and the reading defeats Mark 7's case.

Sola scriptura from Mark 7 is not accepted on every resolution.

• A position holding Mark 7: God's word judges human tradition, Trent (Tradition II), read as the apostolic word handed on unwritten can be held, and it holds Trent (Tradition II), read as the apostolic word handed on unwritten; Trent (Tradition II), read as the apostolic word handed on unwritten conflicts with Sola scriptura from Mark 7: Trent (Tradition II), read as the apostolic word handed on unwritten defeats Sola scriptura from Mark 7, and Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten.
• None of Mark 7: God's word judges human tradition, Trent (Tradition II), read as the apostolic word handed on unwritten defeats another, and each attack on them is answered from among them:
  • Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten, and Trent (Tradition II), read as the apostolic word handed on unwritten defeats Sola scriptura from Mark 7.

What this rests on. The reasons state 2 defeats and 5 absences of defeat, each a cell of the defeat table, mark7Dispute_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 (Tradition II), read as the apostolic word handed on unwritten, weakest at disputed:
  • Tradition is a coordinate source of revelation alongside scripture — tanner-decrees-1990, §Trent, Session IV (1546), Decree on Sacred Books and Traditions; mathison-shape-sola-scriptura-2001; geiselmann-meaning-of-tradition-1966; congar-tradition-and-traditions-1966
• Sola scriptura from Mark 7, weakest at disputed:
  • No apostolic teaching handed on outside Scripture survives, identifiable as the word of God — whitaker-disputation-1849, p. 506; westminster-confession-1647, §I.6
  • an inference step — geiselmann-meaning-of-tradition-1966; tanner-decrees-1990, §Vatican I (1870), Pastor Aeternus, ch. 4; florovsky-bible-church-tradition-1972
• Mark 7: God's word judges human tradition, weakest at well supported:
  • an inference step — tanner-decrees-1990, §Vatican II (1965), Dei Verbum 10; calvin-institutes-1960, §IV.x.23

Why Sola scriptura from Mark 7 defeats Trent (Tradition II), read as the apostolic word handed on unwritten, at the level of the claims: whereTheApostolicWordReadingFalls.

mark7_not_forced_against_the_apostolic_word

So, against the apostolic word, sola scriptura from Mark 7 is not forced. A defensible position that cannot be enlarged holds Mark 7's principle together with Trent read as the apostolic word, and cannot hold Mark 7's case with them. What would decide is argued, not weighed: whether any apostolic word survives outside Scripture, and whether the principle would then make Scripture the sole rule. Both are rated disputed, and neither is something Mark 7 speaks to.

theorem mark7_not_forced_against_the_apostolic_word :
    ¬Framework.SkepticallyAccepted apostolicWordHearing.defeats
    ⟨Mark7Party.mark7, ⋯⟩
-- axioms: propext, Classical.choice, Quot.sound