diff --git a/docs/decisions/ADR-0205-modus-ponens-disagreement-rule.md b/docs/decisions/ADR-0205-modus-ponens-disagreement-rule.md new file mode 100644 index 00000000..03621d9b --- /dev/null +++ b/docs/decisions/ADR-0205-modus-ponens-disagreement-rule.md @@ -0,0 +1,116 @@ +# ADR-0205 — modus_ponens + the Disagreement Rule (proof_chain's first inference rule) + +**Status:** Accepted (proof_chain phase 2.3 — the first inference rule + the wrong=0 mechanism) +**Date:** 2026-06-02 +**Relates to:** ADR-0204 (proof-graph builder — the proof-step shape this rule consumes), +ADR-0201/0201.1/0202 (canonicalizer + contract), ADR-0203 (acyclicity guard), +`generate.derivation.verify.select_self_verified` (the arithmetic twin of the disagreement rule). +**Deferred to:** ADR-0206 (atom→carrier grounding). + +--- + +## Context + +proof_chain has a DAG substrate (ADR-0204) and a canonical form (ADR-0201). Phase +2.3 adds the first **inference rule** (`modus_ponens`) and the **wrong=0 mechanism +for proofs** (the disagreement/uniqueness rule). GPT-5.5 authored an independent +adversarial corpus (`modus_ponens_cases.json`, 24 cases: 6 valid / 8 invalid / 10 +disagreement) against the ADR-0202 grammar, with the proof-step shape left +`[PENDING ADR-0204 SHAPE]` and the disagreement cases `[CONFIRM WITH OPUS]` — the +contract-first handshake. + +## Decision + +### 1. The MP-rule contract (committed before the rule) + +- **Proof-step shape** = the already-landed ADR-0204 `Proof`/`ProofNode` + (`proof_from_premises` desugars premises→premise-nodes, conclusion→mp-node). The + `[PENDING ADR-0204 SHAPE]` placeholders resolve to this; the rule also accepts a + bare `(premises, conclusion)` for corpus cross-check. +- **Closed typed-reason set** (`generate/proof_chain/rules.py::MP_REASONS`): + `unique_canonical_conclusion` (admit); `missing_implication`, + `unestablished_antecedent`, `conclusion_mismatch`, `conclusion_disagreement` (refuse). + +### 2. `evaluate_modus_ponens` — ROBDD-exact, bypassing unit-resolution + +In `generate/proof_chain/rules.py` (the proof-layer dispatch, ADR-0205 Option B): +operates on proposition **formulas** via the canonicalizer; **never** calls +`check_admissibility` / `_resolve_dep_units` (proofs have no units — the named 2.2 +constraint, satisfied by construction). An implication `A→B` fires iff `key(A)` is +an established premise key; the consequent `B` is recovered syntactically +(`logic_canonical.parse_top_implication`) because the ROBDD form does not preserve +which side is antecedent (`P→Q` and `¬P∨Q` share one diagram). + +### 3. The disagreement / uniqueness rule (the wrong=0 mechanism) + +The literal twin of `select_self_verified`: **pool ALL admissible single-step MP +derivations the premise set supports**, collect their canonical conclusion keys, and +admit iff they collapse to exactly one key equal to the declared conclusion; +≥2 distinct keys → refuse (`conclusion_disagreement`); one key ≠ declared → +`conclusion_mismatch`; no admissible derivation → `missing_implication` / +`unestablished_antecedent`. + +**Pooling over the premise set — NOT filtering to the declared conclusion first — +is the soundness mechanism.** Filter-first would admit-by-assertion when the same +premises admit a different key (the `20/5 == 4` class one level up): e.g. a premise +set that MP-derives both an unrelated tautology and the declared atom, or both the +declared atom and a strictly stronger one. Collapse-vs-conflict is judged by **exact +canonical key**, never surface — equivalent paths (`P∧Q`/`Q∧P`, `Q→R`/`¬Q∨R`, +`Q`/`Q∧(R∨¬R)`) collapse and admit; subtly-different ones (`P∧Q`/`P∨Q`, `P→Q`/`Q→P`, +`Q`/`Q∧R`) refuse. + +### 4. Reason-set consolidation (the reconciliation finding) + +The mechanism makes one distinction per axis; the corpus's finer labels collapse onto +the closed set — *the same redundancy confirmed for the disagreement labels applies to +the invalid labels*: + +- 6 disagreement refuse-labels (conflicting / contradictory / tautology_vs_substantive + / distinct_atom / near_miss / stronger) → **`conclusion_disagreement`** (the rule + knows only: keys agree or they don't). +- 4 antecedent-flavor labels (missing_antecedent / antecedent_mismatch / + affirming_consequent / implication_direction_mismatch) → **`unestablished_antecedent`** + (the rule knows only: the available implication's antecedent is or isn't an + established premise; `affirming_consequent` and `implication_direction_mismatch` are + the identical pattern `A→B, conclusion≡A, premise≡B` — no mechanical distinction). + +This consolidation is conveyed back to GPT-5.5 for the corpus's committed reasons. + +## Honesty boundary (load-bearing — exact scope stated) + +Through phase 2.3, proof_chain is **sound over its declared atoms**, not grounded in +recognized input (grounding is 2.4). And the disagreement rule's guarantee has a +**precise scope**: it guarantees a unique conclusion among **single-step modus ponens +derivations over the given premises** — **NOT** "uniquely entailed" by all proof +strategies (a stronger, currently-false claim). This must never be read as +"uniquely entailed." Same discipline as propositional-not-FOL. + +## Evidence (cross-checked, not asserted) + +- **All 24 corpus cases agree on OUTCOME against the real rule** (6 admit / 8 refuse + / 4 admit / 6 refuse) — no rule bug, no corpus outcome-misread. Reasons: 3 exact, + 21 consolidate onto the closed set as above. +- `tests/test_proof_chain_rules.py` — the 24 cases (transcribed, reproducible) + the + pooling guards. **Mutation:** a filter-to-declared-conclusion-first variant makes + MP-DISAGREE-007/010 wrongly admit → `test_pooling_*` fail. Pooling is load-bearing. +- **Drive-by fix (cleanup-as-you-find):** the merged ADR-0204 `ProofNode.__post_init__` + was dedented to module level, so **all `ProofNode` validation was silently dead** + (smoke skips the dedicated test file, so the merge missed it — the "smoke ≠ full + suite" hazard). Re-indented; validation restored; + `test_self_dependency_refused_at_proof_model` passes. +- Full binding-graph + admissibility surface green; smoke 67. Additive (no math path + touched). + +## Three deferrals — settled + +1. **modus_ponens bypasses unit-resolution** — by construction (proof-layer dispatch). +2. **Conclusion typing** — the rule needs the declared conclusion's key + premise + formulas, both reachable; `conclusion_symbol_id` suffices, **no `BoundUnknown`**. +3. **`semantic_role`** — proofs still not wired into serving; **stays `"unknown"`.** + +## Deferred + +- **2.4** — atom→ADR-0144 `EpistemicNode` grounding (ADR-0206). Until then, "sound + over declared atoms," never "reasons over input." +- Multi-step proof composition and a proof *search* (the disagreement rule here is + over a given premise set, single-step) — later, separately scoped. diff --git a/generate/logic_canonical.py b/generate/logic_canonical.py index bf13cd2d..0e8bb091 100644 --- a/generate/logic_canonical.py +++ b/generate/logic_canonical.py @@ -266,6 +266,41 @@ def _collect_atoms(ast: _Ast) -> set[str]: return _collect_atoms(ast[1]) | _collect_atoms(ast[2]) +_BINARY_OPS: Final[dict[str, str]] = {"and": "&", "or": "|", "implies": "->", "iff": "<->"} + + +def _unparse(ast: _Ast) -> str: + """Render an AST back to a fully-parenthesized formula string. Used to hand a + sub-formula (e.g. an implication's antecedent/consequent) back to + :func:`canonicalize`. Parenthesized everywhere so re-parsing is unambiguous.""" + kind = ast[0] + if kind == "atom": + return ast[1] + if kind == "const": + return "true" if ast[1] else "false" + if kind == "not": + return f"(~{_unparse(ast[1])})" + return f"({_unparse(ast[1])} {_BINARY_OPS[kind]} {_unparse(ast[2])})" + + +def parse_top_implication(formula: str) -> tuple[str, str] | None: + """If ``formula``'s top-level connective is ``->``, return + ``(antecedent, consequent)`` as formula strings; else ``None``. + + Modus ponens needs the syntactic antecedent/consequent of an implication + premise — the ROBDD form does not preserve which side is which (``P->Q`` and + ``~P|Q`` share one diagram), so this works at the parse layer. Raises + :class:`LogicError` / :class:`LogicRegimeError` on malformed / out-of-regime + input, consistent with :func:`canonicalize`.""" + _reject_out_of_regime_text(formula) + tokens = _tokenize(formula) + _reject_out_of_regime_tokens(tokens) + ast = _Parser(tokens).parse() + if ast[0] == "implies": + return _unparse(ast[1]), _unparse(ast[2]) + return None + + # --------------------------------------------------------------------------- # ROBDD manager (hand-rolled, minimal: mk + apply + negate + unique table) # --------------------------------------------------------------------------- diff --git a/generate/proof_chain/__init__.py b/generate/proof_chain/__init__.py index 9c75b18e..3a15a037 100644 --- a/generate/proof_chain/__init__.py +++ b/generate/proof_chain/__init__.py @@ -1,12 +1,14 @@ -"""ADR-0204 — proof_chain: propositional proof graphs over the binding-graph DAG. +"""ADR-0204/0205 — proof_chain: propositional proof graphs over the binding-graph DAG. -Phase 2.2 (this module set): the proof-graph *builder* — proof → binding graph, -structure only. The canonicalizer (`generate.logic_canonical`) and equivalence -check (`generate.logic_equivalence`) it rides on are top-level modules; the -inference rule (`modus_ponens` + the disagreement rule) is phase 2.3 / ADR-0205. +- Phase 2.2 (ADR-0204): the proof-graph *builder* — proof → binding graph, structure + only (`build_proof_graph`). +- Phase 2.3 (ADR-0205): the first inference rule + the wrong=0 mechanism — + `evaluate_modus_ponens` / `evaluate_proof_conclusion` (modus_ponens + the + disagreement/uniqueness rule), in `rules.py`. -Honesty boundary (load-bearing through 2.3): sound over declared atoms, not -grounded in recognized input. +Honesty boundary (load-bearing through 2.3): sound over declared atoms, not grounded +in recognized input; the disagreement rule guarantees a unique conclusion among +SINGLE-STEP modus ponens over the premises, not "uniquely entailed" by all strategies. """ from __future__ import annotations @@ -19,8 +21,26 @@ from .builder import ( build_proof_graph, ) from .model import Proof, ProofError, ProofNode, proof_from_premises +from .rules import ( + CONCLUSION_DISAGREEMENT, + CONCLUSION_MISMATCH, + MISSING_IMPLICATION, + MP_REASONS, + UNESTABLISHED_ANTECEDENT, + UNIQUE_CANONICAL_CONCLUSION, + MPOutcome, + MPVerdict, + evaluate_modus_ponens, + evaluate_proof_conclusion, +) __all__ = ( + "CONCLUSION_DISAGREEMENT", + "CONCLUSION_MISMATCH", + "MISSING_IMPLICATION", + "MP_REASONS", + "MPOutcome", + "MPVerdict", "PROOF_INTRODUCED_BY", "PROOF_NO_UNIT", "PROOF_SOURCE_ID", @@ -28,6 +48,10 @@ __all__ = ( "ProofError", "ProofGraph", "ProofNode", + "UNESTABLISHED_ANTECEDENT", + "UNIQUE_CANONICAL_CONCLUSION", "build_proof_graph", + "evaluate_modus_ponens", + "evaluate_proof_conclusion", "proof_from_premises", ) diff --git a/generate/proof_chain/model.py b/generate/proof_chain/model.py index 64c7bdc6..04595a00 100644 --- a/generate/proof_chain/model.py +++ b/generate/proof_chain/model.py @@ -37,26 +37,26 @@ class ProofNode: depends_on: tuple[str, ...] rule: str -def __post_init__(self) -> None: - object.__setattr__(self, "depends_on", tuple(self.depends_on)) + def __post_init__(self) -> None: + object.__setattr__(self, "depends_on", tuple(self.depends_on)) - if not isinstance(self.node_id, str) or not self.node_id.isidentifier(): - raise ProofError( - "ProofNode.node_id must be a Python identifier str; " - f"got {self.node_id!r}" - ) - if not isinstance(self.formula, str) or not self.formula.strip(): - raise ProofError("ProofNode.formula must be a non-empty str") - if not isinstance(self.rule, str) or not self.rule.strip(): - raise ProofError("ProofNode.rule must be a non-empty str") - if self.rule != self.rule.strip(): - raise ProofError("ProofNode.rule must not have leading/trailing whitespace") - if self.rule == "premise" and self.depends_on: - raise ProofError('ProofNode.rule == "premise" requires empty depends_on') - if self.node_id in self.depends_on: - # A self-dependency is a length-1 cycle; the binding-graph acyclicity - # guard (ADR-0203) would also catch it, but refuse early and clearly. - raise ProofError(f"ProofNode {self.node_id!r} depends on itself") + if not isinstance(self.node_id, str) or not self.node_id.isidentifier(): + raise ProofError( + "ProofNode.node_id must be a Python identifier str; " + f"got {self.node_id!r}" + ) + if not isinstance(self.formula, str) or not self.formula.strip(): + raise ProofError("ProofNode.formula must be a non-empty str") + if not isinstance(self.rule, str) or not self.rule.strip(): + raise ProofError("ProofNode.rule must be a non-empty str") + if self.rule != self.rule.strip(): + raise ProofError("ProofNode.rule must not have leading/trailing whitespace") + if self.rule == "premise" and self.depends_on: + raise ProofError('ProofNode.rule == "premise" requires empty depends_on') + if self.node_id in self.depends_on: + # A self-dependency is a length-1 cycle; the binding-graph acyclicity + # guard (ADR-0203) would also catch it, but refuse early and clearly. + raise ProofError(f"ProofNode {self.node_id!r} depends on itself") @dataclass(frozen=True, slots=True) diff --git a/generate/proof_chain/rules.py b/generate/proof_chain/rules.py new file mode 100644 index 00000000..2ca0d991 --- /dev/null +++ b/generate/proof_chain/rules.py @@ -0,0 +1,127 @@ +"""ADR-0205 — modus_ponens + the disagreement/uniqueness rule (proof_chain 2.3). + +The first inference rule, and the wrong=0 mechanism for proofs. Operates on +proposition FORMULAS via the canonicalizer (`generate.logic_canonical`) — the +proof-layer dispatch (Option B): it never touches the math `check_admissibility` / +`_resolve_dep_units` (proofs have no units; the named 2.2 constraint, satisfied by +construction). + +The disagreement rule is the literal twin of +`generate.derivation.verify.select_self_verified`: **pool ALL admissible single-step +MP derivations the premise set supports**, collect their canonical conclusion keys, +and admit iff they collapse to exactly one key equal to the declared conclusion. +Pooling over the premise set — NOT filtering to the declared conclusion first — is +the soundness mechanism: filter-first would admit-by-assertion when the same +premises admit a different key (the ``20/5 == 4`` class one level up). + +**Honesty-boundary scope (load-bearing):** this guarantees a unique conclusion among +**single-step modus ponens** derivations over the given premises — NOT "uniquely +entailed" by all proof strategies. Same discipline as propositional-not-FOL. + +Closed typed-reason set (the mechanism makes exactly these distinctions; the corpus's +finer labels collapse onto them — ADR-0205 §reason-set): + * 6 disagreement refuse-labels → ``conclusion_disagreement``; + * 4 antecedent-flavor labels (missing_antecedent / antecedent_mismatch / + affirming_consequent / implication_direction_mismatch) → ``unestablished_antecedent``. +""" + +from __future__ import annotations + +from dataclasses import dataclass +from enum import Enum +from typing import Final + +from generate.logic_canonical import canonicalize, parse_top_implication +from generate.proof_chain.model import Proof, ProofError + + +class MPOutcome(str, Enum): + ADMIT = "admit" + REFUSE = "refuse" + + +# Closed reason vocabulary. +UNIQUE_CANONICAL_CONCLUSION: Final[str] = "unique_canonical_conclusion" # admit +MISSING_IMPLICATION: Final[str] = "missing_implication" +UNESTABLISHED_ANTECEDENT: Final[str] = "unestablished_antecedent" +CONCLUSION_MISMATCH: Final[str] = "conclusion_mismatch" +CONCLUSION_DISAGREEMENT: Final[str] = "conclusion_disagreement" + +MP_REASONS: Final[frozenset[str]] = frozenset({ + UNIQUE_CANONICAL_CONCLUSION, + MISSING_IMPLICATION, + UNESTABLISHED_ANTECEDENT, + CONCLUSION_MISMATCH, + CONCLUSION_DISAGREEMENT, +}) + + +@dataclass(frozen=True, slots=True) +class MPVerdict: + outcome: MPOutcome + reason: str + conclusion_key: str | None # the unique admitted key (admit only) + derived_keys: tuple[str, ...] # distinct admissible-derivation keys (sorted) + + +def evaluate_modus_ponens(premises: tuple[str, ...], conclusion: str) -> MPVerdict: + """Single-step modus ponens + the disagreement rule over ``premises``. + + Admit iff the admissible single-step MP derivations the premises support + collapse to exactly one canonical key equal to ``conclusion``'s key. Refuses + (typed) otherwise. Propagates the canonicalizer's ``LogicError`` family on a + malformed / out-of-regime premise or conclusion.""" + conclusion_key = canonicalize(conclusion).canonical_key + + # Each premise establishes its own canonical key; implications also expose a + # syntactic (antecedent, consequent). + established: set[str] = set() + implications: list[tuple[str, str]] = [] + for premise in premises: + established.add(canonicalize(premise).canonical_key) + parts = parse_top_implication(premise) + if parts is not None: + implications.append(parts) + + if not implications: + return MPVerdict(MPOutcome.REFUSE, MISSING_IMPLICATION, None, ()) + + # Enumerate admissible derivations: an implication A->B fires iff key(A) is an + # established premise; it yields B. Pool over the WHOLE premise set. + derived: dict[str, None] = {} # insertion-ordered distinct yielded keys + for antecedent, consequent in implications: + if canonicalize(antecedent).canonical_key in established: + derived[canonicalize(consequent).canonical_key] = None + + if not derived: + # Implication(s) present, but none has an established antecedent. + return MPVerdict(MPOutcome.REFUSE, UNESTABLISHED_ANTECEDENT, None, ()) + + distinct = tuple(sorted(derived)) + if len(distinct) >= 2: + # The premises admit deriving distinct conclusions → disagreement. + return MPVerdict(MPOutcome.REFUSE, CONCLUSION_DISAGREEMENT, None, distinct) + + only = distinct[0] + if only != conclusion_key: + # A single admissible derivation, but it concludes something else. + return MPVerdict(MPOutcome.REFUSE, CONCLUSION_MISMATCH, None, distinct) + + return MPVerdict(MPOutcome.ADMIT, UNIQUE_CANONICAL_CONCLUSION, only, distinct) + + +def evaluate_proof_conclusion(proof: Proof) -> MPVerdict: + """Evaluate ``proof``'s conclusion node as a modus_ponens step. + + Wires the rule to the ADR-0204 ``Proof``: gathers the conclusion node's + dependency-node formulas as the premise set and evaluates. Requires the + conclusion node's ``rule == "modus_ponens"``.""" + by_id = {n.node_id: n for n in proof.nodes} + concl = by_id[proof.conclusion_id] + if concl.rule != "modus_ponens": + raise ProofError( + f"evaluate_proof_conclusion expects a modus_ponens conclusion; " + f"got rule={concl.rule!r}" + ) + premises = tuple(by_id[dep].formula for dep in concl.depends_on) + return evaluate_modus_ponens(premises, concl.formula) diff --git a/tests/test_proof_chain_rules.py b/tests/test_proof_chain_rules.py new file mode 100644 index 00000000..f3db5c4f --- /dev/null +++ b/tests/test_proof_chain_rules.py @@ -0,0 +1,125 @@ +"""ADR-0205 — modus_ponens + disagreement rule (phase 2.3). + +The 24 adversarial corpus cases (GPT-5.5's independent oracle) transcribed for a +committed, reproducible cross-check against the real rule: 6 valid / 8 invalid / +10 disagreement. The disagreement cases are the wrong=0 guard — 007/010 in +particular pin the pooling semantics: pool ALL admissible MP derivations and +require a unique key. A filter-to-declared-conclusion-first rule would admit them +(admit-by-assertion); pool-first refuses. That test failing under filter-first is +the proof the soundness mechanism is load-bearing. +""" + +from __future__ import annotations + +import pytest + +from generate.proof_chain import ( + CONCLUSION_DISAGREEMENT, + CONCLUSION_MISMATCH, + MISSING_IMPLICATION, + MP_REASONS, + Proof, + ProofNode, + UNESTABLISHED_ANTECEDENT, + UNIQUE_CANONICAL_CONCLUSION, + MPOutcome, + evaluate_modus_ponens, + evaluate_proof_conclusion, +) + +# (id, premises, conclusion, expected_outcome, expected_reason) — reasons are the +# CLOSED set; the corpus's finer labels collapse onto them (ADR-0205 §reason-set). +CASES = [ + # --- valid (admit) --- + ("VALID-001", ("P", "P -> Q"), "Q", "admit", UNIQUE_CANONICAL_CONCLUSION), + ("VALID-002", ("P_rains", "P_rains -> Q_ground_wet"), "Q_ground_wet", "admit", UNIQUE_CANONICAL_CONCLUSION), + ("VALID-003", ("P and R", "(P and R) -> Q"), "Q", "admit", UNIQUE_CANONICAL_CONCLUSION), + ("VALID-004", ("P_switch_on", "P_switch_on -> (Q_lamp_lit or R_alarm_on)"), "Q_lamp_lit or R_alarm_on", "admit", UNIQUE_CANONICAL_CONCLUSION), + ("VALID-005", ("P", "P -> (Q -> R)"), "Q -> R", "admit", UNIQUE_CANONICAL_CONCLUSION), + ("VALID-006", ("(P or Q) and not R", "((P or Q) and not R) -> S"), "S", "admit", UNIQUE_CANONICAL_CONCLUSION), + # --- invalid (refuse, typed) --- + ("INVALID-001", ("P", "P -> Q"), "R", "refuse", CONCLUSION_MISMATCH), + ("INVALID-002", ("P",), "Q", "refuse", MISSING_IMPLICATION), + ("INVALID-003", ("Q", "P -> Q"), "P", "refuse", UNESTABLISHED_ANTECEDENT), # corpus: affirming_consequent + ("INVALID-004", ("R", "P -> Q"), "Q", "refuse", UNESTABLISHED_ANTECEDENT), # corpus: antecedent_mismatch + ("INVALID-005", ("P", "Q -> P"), "Q", "refuse", UNESTABLISHED_ANTECEDENT), # corpus: implication_direction_mismatch + ("INVALID-006", ("P", "(P or R) -> Q"), "Q", "refuse", UNESTABLISHED_ANTECEDENT), # corpus: antecedent_mismatch + ("INVALID-007", ("P", "P -> (Q or R)"), "Q", "refuse", CONCLUSION_MISMATCH), + ("INVALID-008", ("P -> Q",), "Q", "refuse", UNESTABLISHED_ANTECEDENT), # corpus: missing_antecedent + # --- disagreement (admit: collapse to one key; refuse: distinct keys) --- + ("DISAGREE-001", ("A", "A -> C", "B", "B -> C"), "C", "admit", UNIQUE_CANONICAL_CONCLUSION), + ("DISAGREE-002", ("A", "A -> (P and Q)", "B", "B -> (Q and P)"), "P and Q", "admit", UNIQUE_CANONICAL_CONCLUSION), + ("DISAGREE-003", ("A", "A -> (Q -> R)", "B", "B -> (not Q or R)"), "Q -> R", "admit", UNIQUE_CANONICAL_CONCLUSION), + ("DISAGREE-004", ("A", "A -> Q", "B", "B -> (Q and (R or not R))"), "Q", "admit", UNIQUE_CANONICAL_CONCLUSION), + ("DISAGREE-005", ("A", "A -> (P and Q)", "B", "B -> (P or Q)"), "P and Q", "refuse", CONCLUSION_DISAGREEMENT), + ("DISAGREE-006", ("A", "A -> Q_ground_wet", "B", "B -> Q_ground_damp"), "Q_ground_wet", "refuse", CONCLUSION_DISAGREEMENT), + ("DISAGREE-007", ("A", "A -> (R or not R)", "B", "B -> Q"), "Q", "refuse", CONCLUSION_DISAGREEMENT), + ("DISAGREE-008", ("A", "A -> Q", "B", "B -> not Q"), "Q", "refuse", CONCLUSION_DISAGREEMENT), + ("DISAGREE-009", ("A", "A -> (P -> Q)", "B", "B -> (Q -> P)"), "P -> Q", "refuse", CONCLUSION_DISAGREEMENT), + ("DISAGREE-010", ("A", "A -> Q", "B", "B -> (Q and R)"), "Q", "refuse", CONCLUSION_DISAGREEMENT), +] + + +@pytest.mark.parametrize("cid,premises,conclusion,outcome,reason", CASES, ids=[c[0] for c in CASES]) +def test_corpus_case(cid, premises, conclusion, outcome, reason) -> None: + v = evaluate_modus_ponens(premises, conclusion) + assert v.outcome.value == outcome, cid + assert v.reason == reason, cid + assert v.reason in MP_REASONS + + +def test_admit_yields_the_canonical_conclusion_key() -> None: + from generate.logic_canonical import canonicalize + v = evaluate_modus_ponens(("P", "P -> Q"), "Q") + assert v.outcome is MPOutcome.ADMIT + assert v.conclusion_key == canonicalize("Q").canonical_key + + +# --------------------------------------------------------------------------- +# The pooling semantics — the wrong=0 mechanism. 007/010 MUST refuse: the premises +# admit deriving a second distinct key, so pool-first refuses. A filter-first rule +# (keep only derivations whose key == declared conclusion, then check uniqueness) +# would admit both — admit-by-assertion. These assertions fail under that mutation. +# --------------------------------------------------------------------------- + + +def test_pooling_refuses_unrelated_tautology_path() -> None: + # 007: one path yields T (R or not R), the substantive path yields Q. + v = evaluate_modus_ponens(("A", "A -> (R or not R)", "B", "B -> Q"), "Q") + assert v.outcome is MPOutcome.REFUSE + assert v.reason == CONCLUSION_DISAGREEMENT + assert len(v.derived_keys) == 2 # T and key(Q) — distinct, pooled + + +def test_pooling_refuses_stronger_conclusion_path() -> None: + # 010: paths yield Q and (Q and R) — distinct keys. + v = evaluate_modus_ponens(("A", "A -> Q", "B", "B -> (Q and R)"), "Q") + assert v.outcome is MPOutcome.REFUSE + assert v.reason == CONCLUSION_DISAGREEMENT + assert len(v.derived_keys) == 2 + + +def test_equivalent_paths_collapse_not_disagree() -> None: + # 003: Q->R and (not Q or R) are equivalent → one key → admit. + v = evaluate_modus_ponens(("A", "A -> (Q -> R)", "B", "B -> (not Q or R)"), "Q -> R") + assert v.outcome is MPOutcome.ADMIT + assert len(v.derived_keys) == 1 + + +# --------------------------------------------------------------------------- +# Wiring to the ADR-0204 Proof. +# --------------------------------------------------------------------------- + + +def test_evaluate_proof_conclusion_via_builder_shape() -> None: + proof = Proof( + nodes=( + ProofNode("premise_0", "P", (), "premise"), + ProofNode("premise_1", "P -> Q", (), "premise"), + ProofNode("conclusion", "Q", ("premise_0", "premise_1"), "modus_ponens"), + ), + conclusion_id="conclusion", + ) + v = evaluate_proof_conclusion(proof) + assert v.outcome is MPOutcome.ADMIT + assert v.reason == UNIQUE_CANONICAL_CONCLUSION