Derive defeat between packages and settle disputes with Dung semantics

[deanberris]

Closes #62.

The issue's three questions

Does a Lean 4 argumentation library exist? No. I checked Reservoir, the GitHub argumentation topic and the literature. The only mechanised prior art is Isabelle/HOL (Steen & Fuenmayor, arXiv:2110.09174). So Testimony.Logic.Framework implements Dung's semantics itself, taking Knaster–Tarski (OrderHom.lfp) and Zorn (zorn_subset_nonempty) from Mathlib instead of proving them again.

Should the attack relation be recorded or computed? Computed. Recording it would have mislabelled half the existing replies. The existing replies built with Line.onGrounds turn out to make two different moves:

• a refusal declines a ground without asserting its negation. This is not an attack. Kruger, Mathison, the final-arbiter answer, and both replies to Geisler's circle are refusals.
• a denial entails the negation of a ground. This is an attack. Berry, Postell, the classical answer to self-refutation, and Barrett are denials.

Each of these nine classifications is now a theorem: five *_refuses_rather_than_denies by countermodel, four *_denies_the_ground by establish.

Would a framework change existing results? No existing entailment result changes. What it adds is a result entailment cannot state: who prevails.

Two findings that shaped the design

Premise attacks between classical arguments always come in pairs. Under symmetric attack, Dung's semantics reduce to a consistency check (Cayrol, IJCAI 1995), and no argument ever wins. So attack is filtered into defeat by cited confidence, on ASPIC+'s weakest-link rule. This makes the ratings load-bearing, and the docs say so.

The weakest link has to include inference steps. Otherwise the placement of a contested move decides the result: in an atom it is rated, in a step it is not. So a Dispute refuses any node whose inferences are unrated. The rule for rating a step is that it is disputed when a cited source grants its grounds and denies its conclusion.

What's added

• Testimony/Logic/Framework.lean: conflict-free, admissible, complete, preferred and grounded extensions, and skeptical and credulous acceptance. Also grounded_eq_of_iterate, grounded_eq_empty_of_attacked and preferred_of_blocked.
• Testimony/Logic/Dispute.lean:
  • UnderminesOn, Rebuts, Attacks, strength, Defeats.
  • Dispute, whose nodes must be satisfiable, must establish their conclusions, and must have rated inferences.
  • Compact tools:
    • Dispute.StandTogether: one named world settles every pair in a group.
    • not_defeats_of_outweighed.
    • Dispute.restrict, for hearings.
    • The defeat_table and grounded_by tactics.
• Line.inference and ArgumentPackage.inferences: citations rating the steps.
• Testimony/Arguments/BornOfAVirgin/Dispute.lean: six parties (the scriptural reading, the critic, Berry, Postell on Isaiah 9 and 11, Postell on Micah 5, and Motyer). All 36 pairs are proved, and there are eight headlines:
  • christian_defeats_critical, and nothing_prevails_unanswered: the two tie.
  • scriptural_reading_prevails_once_replies_are_heard: grounded = {scriptural, Berry, Postell, Motyer, Micah}.
  • critical_denial_indefensible: nothing defeats Postell, and he defeats the critic.
  • scriptural_reading_prevails_without_postell: the Micah counterexample suffices on its own.
  • nothing_prevails_without_the_counterexamples: the verdict rests on Postell's inference, rated plausible, in its two instances.
  • nothing_prevails_on_motyer_alone and motyer_rests_on_his_inference.
• SolaScriptura/Results.lean: the refusal/denial theorems.
• Docs: a "sixth idea" section in reading-the-logic.md, a "Disputes" section in logic.md, a roadmap finding, a limits paragraph, and CLAUDE.md entries.
• statusgen: now sorts headlines by import order.

Added in review

• Sources, each read in full:
  • the church fathers: Justin, Irenaeus, Origen, Jerome;
  • Motyer, TynBul 21.1 (1970);
  • Compton, DBSJ 12 (2007);
  • Young, WTJ 15.2 (1953), part one only;
  • Rhodea, JETS 56.1 (2013);
  • Johnson, JETS 53.2 (2010);
  • Brown, TS 33.1 (1972) and Fitzmyer, TS 34.4 (1973), on the historical premise, which stays disputed.
• Ratings corrected to the library's definition.
  • Both critical premises are now disputed.
  • The inference steps are rated:
    • Berry's: disputed;
    • Motyer's: disputed;
    • both of Postell's: plausible;
    • the critic's: consensus.
• Motyer's reply and Postell's Micah counterexample as parties, each with its rival written first.
• Luke as a disputed allusion, with the birth-announcement form as the rival reading.
• The Isaiah dispute rewritten compactly.
• The patristic "sign" argument is tracked in Encode the patristic "sign" argument against an ordinary pregnancy at Isaiah 7:14 #73.

Checks

• lake build passes. The only warnings are the two in Entail.lean that are already on main.
• lake lint passes.
• lake exe axiom-audit passes, with only propext, Classical.choice and Quot.sound.
• testimony_lint.py passes, and so do its 84 tests.
• The --check runs for bibgen, statusgen, argdoc and argtex all pass.
• Not run locally: mdbook and tectonic. CI runs mdbook.

🤖 Generated with Claude Code

https://claude.ai/code/session_01VGgpRWs6WLZF6e3Qb3fWRP