64f3da18a7
Phase 2.3: the first inference rule + the wrong=0 mechanism for proofs. - generate/proof_chain/rules.py: evaluate_modus_ponens / evaluate_proof_conclusion. Proof-layer dispatch (Option B) over proposition FORMULAS via the canonicalizer; never touches check_admissibility/_resolve_dep_units (proofs have no units). Disagreement rule = the select_self_verified twin: pool ALL admissible single-step MP derivations, require a unique canonical key == declared conclusion. Pooling (not filter-to-declared-first) is the soundness mechanism. - generate/logic_canonical.py: parse_top_implication (+ _unparse) — recovers an implication's syntactic antecedent/consequent (the ROBDD form doesn't preserve it). - Closed typed-reason set; the corpus's finer labels consolidate (6 disagreement refuse-labels -> conclusion_disagreement; 4 antecedent-flavor labels -> unestablished_antecedent — same redundancy, same mechanism-makes-one-distinction principle). - Honesty boundary (exact scope): guarantees a unique conclusion among SINGLE-STEP MP over the premises, NOT "uniquely entailed" by all strategies. Cross-check: all 24 GPT-5.5 adversarial corpus cases agree on OUTCOME against the real rule (no rule bug / no corpus outcome-misread); reasons consolidate as above. Mutation: filter-to-declared-first makes DISAGREE-007/010 wrongly admit -> pooling tests fail (pooling load-bearing). Drive-by fix (cleanup-as-you-find): merged ADR-0204 ProofNode.__post_init__ was dedented to module level -> all ProofNode validation was silently DEAD (smoke skips the dedicated test file; the smoke != full-suite hazard). Re-indented; validation restored. Additive (math lane untouched). Full binding-graph surface green; smoke 67.
116 lines
6.4 KiB
Markdown
116 lines
6.4 KiB
Markdown
# 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.
|