Design: derive the argument graph — supports, attacks and defeats computed and proved, not hand-written

[deanberris]

A design issue for the core logic. The sub-issues below are the steps, in order.

The problem

Every relation between positions in a dispute is currently proved by hand, one pair at a time. That costs more with each position added.

Source	Size in SolaFide/Dispute.lean	Why it hurts
Lists of definitions to unfold, passed to establish and satisfied_by	60 lists, 555 of 1,317 lines (42%), plus 173 lines (29%) of Results.lean	Every new definition must be added everywhere. A missing one fails with a misleading "not Horn" message.
Defeat proofs	about 12 lines each, 17 of them	The same shape every time: prove the rebuttal, then compare strengths.
Non-defeat proofs	about 45 lines each	A hand-counted case split over the target's premises (rcases … rfl | rfl …). A miscount has broken the build.
Verdict proofs	25–40 lines each	Hand-written reasoning about sets over the defeat table, redone whenever a party is added.

Integrating the Johannine strand (#86, #89) as a ninth party was estimated at 250–400 lines, most of it this repetition.

The idea

The edges are already determined by the premises. Every package is a list of formulas over shared atoms, and after the move to Horn-based establish, nearly every package is a set of Horn clauses:

• atoms;
• steps of the form "these atoms together imply that atom";
• denials of an atom.

For Horn clauses, entailment is decided by forward chaining in linear time. When a goal is not derived, the set of atoms reached is itself a countermodel. So one engine, proved correct once, can compute every relation in both directions, each with a proof:

• Attacks (undermining or rebutting): forward-chain the attacker's premises and see whether the negation of a target premise or conclusion is reached. "Yes" is proved by the derivation.
• No attack: the forward-chaining result is the countermodel. This replaces the hand-written non-defeat proofs.
• Supports: a supports b if a's conclusion is, or entails, a premise of b.
• Stand together: the combined premises of several parties have a model.
• Defeats: attack filtered by strength, which is already decidable.

The positions and the proved edges between them form a graph, a checked version of an ontology of the debate. It can be queried programmatically:

• verdicts;
• what a verdict rests on;
• cruxes (Graph step 4: "P holds because Q" — checkable explanations of why a position prevails #96);
• indirect attacks (if a supports b and b attacks c, a indirectly attacks c).

The rule this must not break

Edges are computed and proved, never asserted. Dispute.lean opens with "Who defeats whom is not stipulated". A hand-entered Supports or Attacks edge would bring back exactly the stipulation the library exists to rule out. Every edge in the graph carries a proof, or a countermodel for its absence.

Prior art

• ASPIC+ (Modgil and Prakken). Attacks are derived from the internal structure of arguments, not declared. The library's Dispute already follows its weakest-link preference.
• Bipolar argumentation (Cayrol and Lagasquie-Schiex). A support relation alongside attack, with derived supported and secondary attacks.

The design extends the library's existing model rather than replacing it.

Steps (sub-issues)

1. Named unfold sets. One registered set of definitions per argument, tagged where each definition is written. This is prototyped and works; see the first sub-issue.
2. A certified Horn engine, and the defeat table derived from it, benchmarked on the current eight-party sola fide dispute.
3. A registry of positions and a generated graph, with a verified verdict solver, graph queries and rendered argument maps.
4. "P holds because Q" as graph queries. This is Graph step 4: "P holds because Q" — checkable explanations of why a position prevails #96, rebuilt on the graph.

Risks to settle early

• Kernel speed. native_decide is banned, so every computation must be checked by the kernel itself. Generating one small theorem per pair keeps each check cheap and lets them run in parallel. Benchmark in step 2 before committing.
• Equality on the claim type must compute in the kernel. CLAUDE.md records that List.filter over a derived DecidableEq (Formula α) does not reduce there. The engine should work on the atom type, and step 2 should test that its equality reduces.
• Non-Horn packages. The engine reports them as unknown, and they are proved by hand as now. Step 1 keeps those proofs short.

Relation to other issues

• Graph step 4: "P holds because Q" — checkable explanations of why a position prevails #96 ("P holds because Q") becomes step 4.
• Refuted on its own terms: test every position against its own commitments #91 (the own-terms audit) gets its unsatisfiability proofs from the step 2 engine.
• Sola fide: a Johannine strand — "this is the work of God, that you believe" #86 (integrating the Johannine strand) is cheap after step 2: adding a party becomes adding a node.

Done when

• A new argument's dispute is declared by tagging its positions, and its defeat table and verdicts are derived and checked.
• Dispute.lean for sola fide is rebuilt on the derived table, with every existing verdict re-proved, not assumed.
• The argument pages render the derived graph.