core/docs/decisions/ADR-0201-proposition-canonicalizer.md

ADR-0201 — Propositional Canonicalizer (the proof_chain keystone)

Status: Proposed (Phase 1 of proof_chain; standalone keystone shipped, not yet wired)

Date: 2026-06-02

Relates to: ADR-0131.1.B (math_symbolic_equivalence — the sibling pattern this mirrors), ADR-0132/0133/0134/0135 (binding-graph data model / adapter / admissibility / question-target — the future consumer), the wrong == 0 self-verification doctrine in generate/derivation/verify.py.

Context

CORE has confirmed three things about building proof_chain as a real reasoning primitive (not a declared label):

1. The ledger "operators" (proof_chain/causal/modal) are classification labels, not executors — proof_chain is green-field.
2. The wrong == 0 self-check is soundness, not correctness: it fires only when grounded+licensed derivations collapse to one unique canonical conclusion and rivals are checked for agreement. It needs a canonical, comparable conclusion. For arithmetic, exact numeric equality gave that for free.
3. The ADR-0132 binding graph is already the DAG substrate proof trees need (BoundEquation.dependencies + per-node admissibility + provenance), with a shipped, hand-rolled sibling — math_symbolic_equivalence — that already demonstrates the normalize → canonical-string → byte-equality → three-valued-verdict-with-REFUSED discipline for algebra.

Logic does not get a comparable canonical conclusion for free: two syntactically different formulas can be logically equivalent (P∧Q ≡ Q∧P, ¬¬P ≡ P, P→Q ≡ ¬P∨Q). Without a canonical form, the uniqueness/disagreement rule cannot fire and proof_chain degrades from sound to merely cautious. This ADR scopes the canonical form — the keystone everything else (rule checkers, the disagreement rule) depends on.

Decision

Canonicalize a propositional formula to a Reduced Ordered Binary Decision Diagram (ROBDD) under a fixed (sorted-atom) variable ordering, and use a canonical string serialization of the reduced diagram as the byte-equality discriminator (the logic analog of Polynomial.to_canonical_string()).

• ROBDD, not CNF/DNF. For a fixed ordering the ROBDD is canonical — two formulas are logically equivalent iff their reduced diagrams are isomorphic. CNF/DNF are merely normal (standardized shape), not canonical, and have no poly-time equivalence-preserving transform. Free bonuses for later: tautology = the 1-terminal, contradiction = the 0-terminal, f→g valid iff apply(f, ¬g, ∧) = the 0-terminal — so contradiction and proof "conclusion follows" reduce to ROBDD checks.
• Hand-rolled minimal, no external BDD library (operator-confirmed). Stays in CORE's idiom (the symbolic substrate is entirely hand-rolled), deterministic by construction, fully inspectable, zero opaque dependencies. ~370 LOC: tokenizer + recursive-descent parser + mk/apply/negate + unique table + canonical serialization.
• wrong == 0 discipline preserved. No approximate path. Out-of-grammar input raises LogicError; a diagram exceeding the node budget raises LogicBudgetError (a LogicError subclass, so callers refusing on LogicError refuse on budget too). Both surface as a REFUSED verdict — refuse rather than guess or churn.

Honesty boundary (stated, not hidden)

• Propositional logic (finite Boolean variables): canonical and decidable. ROBDD gives a unique form + constant-time equivalence. The full soundness gate transfers. This is the only regime this module claims.
• Cost caveat: ROBDD size can be exponential in the worst case and is ordering-sensitive. Canonicity is cheap to compare but not always cheap to build. For bounded proof-step propositions (a handful of atoms) this is a non-issue; the node budget refuses on adversarial blowup rather than hanging.
• Predicate / first-order logic: NOT canonical in general — undecidable. There is no ROBDD-style canonical form for full FOL. We do NOT claim wrong == 0 for quantified reasoning with this machinery. Quantifier-free fragments and specific decidable theories are later, separately-scoped steps, each with their own honest decidability claim.

What shipped in this phase (standalone)

• generate/logic_canonical.py — canonicalize(formula, *, max_nodes) -> CanonicalProposition{canonical_key, atoms, is_tautology, is_contradiction}; LogicError / LogicBudgetError.
• generate/logic_equivalence.py — check_equivalence(a, b) -> EquivalenceVerdict{EQUIVALENT|NOT_EQUIVALENT|REFUSED} (close mirror of math_symbolic_equivalence).
• tests/test_logic_canonical.py — 33 standalone tests: canonicity laws (commutativity, double-negation, De Morgan, implication rewrite, distributivity, absorption, irrelevant-variable elision), discrimination (non-equivalent → distinct keys), terminal collapse, byte-determinism, operator-spelling parity, and the refusal paths (malformed → LogicError; budget blowup → LogicBudgetError).

Tested in isolation, exactly as the sibling is standalone — proving the keystone holds alone before anything depends on it.

Proof obligation (per CLAUDE.md §Schema-Defined Proof Obligations)

The canonicity tests must be able to meaningfully fail. Verified by mutation: disabling the redundant-node reduction rule (low == high → low) flips P ∧ (Q ∨ ¬Q) ≡ P to false, failing test_irrelevant_variable_is_dropped_from_support. The equivalent-pairs and non-equivalent-pairs suites are mutually constraining: a collapse-everything canonicalizer fails discrimination; a no-reduction canonicalizer fails equivalence. The suite is non-vacuous by construction.

Explicitly deferred (NOT in this phase)

• Binding-graph wiring. proof_chain would be the binding graph's first consumer — there is no existing graph-builder→serving path to join. The integration is net-new wiring, scoped separately. The canonical key is designed to drop into BoundEquation.rhs_canonical (a string field) when that wiring is built.
• The acyclicity refusal. A cycle in a proof DAG is circular reasoning; the binding graph currently checks referential integrity but not cycles. The circular_dependency refusal is net-new and must land before the structure is load-bearing — not in this standalone phase.
• Inference rules. No operation_kind logic vocab and no _check_modus_ponens yet. One sound rule (modus_ponens) + the disagreement rule on the canonical key is the next phase, once this keystone is accepted.

Alternatives considered

• CNF/DNF canonical string — rejected: not canonical (clause/literal ordering is non-unique), and no poly-time equivalence-preserving transform exists.
• External BDD library (dd / CUDD) — rejected: the only opaque dependency in an otherwise hand-rolled substrate; determinism/trace_hash risk from hash-based node ids and reordering heuristics; CUDD is a C build/footprint cost; and the canonical-string serialization would still need to be hand-controlled for determinism, so the library does not save the load-bearing work.