Refuted on its own terms: test every position against its own commitments

[deanberris]

A library-wide audit. It is split into one sub-issue per argument so that different contributors can take them.

Why

Most rival readings in the library end up rated disputed. The rule is that a step is disputed when a cited source grants its grounds and denies its conclusion. That is honest, but it is the weakest verdict the library can give.

The logic supports a stronger verdict, refuted on its own terms: a position's own authors are committed, in their own texts, to premises that entail the negation of what the position needs. Such a result cannot be dismissed as the other side's opinion, because every premise in it is the position's own.

The worked example that prompted this is in SolaFide/Johannine.lean (PR #89):

• Aquinas reads the believing of John 6:29 as faith formed by charity.
• Luther answers from Galatians 3:11–12: the law commands charity, and the law is not of faith.
• luther_answer_rests_on_his_step shows the answer depends on Luther's step, which Aquinas denies. So the step is disputed.
• If Aquinas himself holds, elsewhere in his own texts, premises that entail Luther's step, then his reading of 6:29 contradicts his own commitments. That is a definitive result, not a disputed one. Whether he does is an open question.

The test, for each position

1. List what the position needs. Take each premise or step its conclusion depends on that a rival denies. The load-bearing results already name most of them.
2. Search the position's own sources. Look in the texts it is cited to, and other works by the same authors or councils, for commitments that entail the rival's step, or the negation of one of the position's own needed premises.
3. Verify before encoding. Quote the exact text, with a verifiable edition and locus (see .claude/skills/adding-a-citation). A commitment attributed to an author must be one they state. Do not infer it from their tradition, and do not paraphrase it into something stronger.
4. Encode what you find.
   • Add each commitment as an atom cited to the author's own work.
   • Prove that the position's premises plus those commitments either establish the negation of its conclusion or are unsatisfiable.
   • Name the result for what it shows, e.g. aquinas_formed_faith_contradicts_his_galatians.
   • Only an inference that is the position's own, or purely logical, may be used. If the bridge needs a step the position rejects, the result is still only disputed, and the issue should say so.
5. Record negative results. If the search finds nothing, say so on the sub-issue, with what was searched. "Their commitments are consistent here" is a finding.

Fairness is the point

Every position gets the same test, including the ones the library's arguments favour. The Reformed, Protestant and Christian readings are tested against Calvin, Luther, Westminster and their other cited sources exactly as rival readings are tested against theirs.

An audit that only looks for inconsistency on one side proves nothing, and would be the kind of overclaim this library exists to rule out. A tension found on the favoured side is recorded and encoded the same way.

Mechanics still to settle

The first contributor to finish a case should settle these and document them in docs/src/logic.md:

• How to state self-inconsistency. Either ¬ Satisfiable (pkg.premises ++ commitments), or Establishes of the negation of the position's conclusion from its own commitments. The first is cleaner, but may need a small lemma or tactic, since refute_with, satisfied_by and establish do not currently prove unsatisfiability directly.
• How such a result feeds the disputes in Dispute.lean. A position refuted on its own terms is arguably not consistent, and a Dispute refuses inconsistent nodes. Decide whether the self-refuted variant should enter as a party, or be reported alongside the dispute.

Sub-issues

One per argument. Each lists that argument's positions as a checklist, with the known disputed steps to start from.

Done when

Every position in every argument has been tested. Each has either an encoded, cited "refuted on its own terms" result, or a recorded negative result saying what was searched. The prose pages describe the outcomes accurately.