RFD 0028 — Defeasibility redesign: honest heads, the defeat-directive plane, and strategy as a compilation scheme

• State: accepted — implementation planned
• Opened: 2026-06-11
• Decides: the complete replacement of the §7.8 strength-attribute surface (#[strict]/#[defeasible]/#[defeater]/#[priority], pub priority) with honest-head rules plus a defeat-directive plane — unmarked rules stay strict/classical, #[default] marks an overridable rule, #[defeats(target(args))] declares the attack, #[label(name)] gives a clause an identity — with head-level, clause-level, and trait-qualified targeting all in v1; the strategy-as-compilation architecture: the core language owns four strategy-neutral hooks (rule identity in the catalog, defeat edges on the wire, a transform slot between lowering and stratification, a provenance channel), and Governatori-with-explicit-superiority is strategy #1, specified as its compilation to the core stratified/WFS semantics; proof tags (+Δ/−Δ/+∂/−∂) finally surfaced through the provenance channel; and a loud migration — no silent aliasing. Settles the #244 design thread (including both correction comments: the grammar-clause rejection and the final lock) and stage 2 of #245. Hard prerequisite: the directive registry (audit dc-01). This RFD leads the arc per the workflow table — language surface: RFD + reference draft → Lean → code.

Prior state (verified at d26dc626): the attribute walker maps the strength triple onto RuleDeclBody.rule_strength (oxc-instantiate/src/lower.rs:145-147; wire field oxc-protocol/src/storage.rs:784; Lean mirror RuleStrength in Locality/DefeasibleExtraction.lean under @[language_interface]), and a fused strength-stratified evaluator computes final[H] = strict[H] ∪ (defeasible[H] \ defeater[H]), keyed by head name, blocking by exact head-tuple match (oxc-runtime/src/lib.rs:4810-4823). #[priority(N)] is silently dropped — the audit executed the repro (sf-02, probe p18: a program written to §7.8’s priority semantics computes different conclusions with zero diagnostics; #245) — and the pub priority { } superiority blocks §7.8 documents don’t parse at all: book-ahead prose presented as available. Unknown attributes are silently ignored across the board (audit dc-01: #[defeasable] passes ox check and silently strictens the rule). The whole §7.8 diagnostics block — OE0411–OE0414 — is phantom: zero presence in the catalog or the compiler (audit dc-03). The wire proof_tag field exists (storage.rs:1283, “Governatori-Rotolo 4-slot proof tag”) but lowering always writes None (lower.rs:6755) and its only live writer is fork promotion squatting it with promoted_from:{fork} (oxc-serve/src/lib.rs:2568).

Question

We lost a morning to three lines of the canonical example (examples/legal_norms_can_vote/norms.ar):

#[strict]     pub derive can_vote(p) :- SpecialClass(p);
#[defeasible] pub derive can_vote(p) :- Adult(p);
#[defeater]   pub derive can_vote(p) :- Felon(p);

The third rule spells the head it denies. §7.8 itself defines a defeater as A ⇝ ¬B — blocks B without asserting either — yet the surface writes can_vote(p) :- Felon(p). Everyone reads it as “felons can vote.” The attribute silently inverts the polarity of the head at a distance, which is unacceptable as a modeling surface — and the book even ships a phantom diagnostic (OE0413 DefeaterAssertsConclusion) acknowledging the confusion it documents.

Four defects, one design (#244):

1. The defeater writes the head it denies — the polarity flip lives in an attribute, invisible at the head.
2. No rule identity, no targeted defeat — attack resolution is head-name-only; the only priority knob is a global integer that is the wrong abstraction (magic numbers don’t compose across modules or packages) and is silently discarded today; the pub priority blocks are unimplemented prose.
3. No surface notion of a default rule — #[defeasible] is logician-speak; modelers think in defaults and exceptions.
4. Exceptions aren’t compositional — an exception must be written as the attacked predicate, in its terms; it can’t live in another module or impl under its own honest name. Post-#217 the rule catalog is qualified-path keyed, so the addressing substrate for cross-module targeting now exists.

Two questions, then. (1) What is the right surface — how does a modeler write defaults, exceptions, and attacks so that every rule reads true? (2) What does the core language own, versus what belongs to a particular flavor of defeasible reasoning — Governatori-style defeasible logic is one strategy among several (default logic, courteous LP, argumentation, ASP preferences), and the substrate must not privilege it.

D1 — Honest heads: a rule derives exactly what its head says

Unmarked = strict. A bare derive rule is classical, exactly as today — a Datalog program keeps meaning what it always meant, and strict conclusions cannot be overridden. #[default] marks an overridable rule (the Rust-specialization precedent — default fn — an established PL concept carrying exactly the right reading: this clause holds unless something more specific displaces it). An exception is an ordinary rule with its own honest head; the attack is carried by a directive (D2), never by the rule’s syntax. The canonical example becomes:

// strict = unmarked: special-class members vote, period
pub derive can_vote(p) :- SpecialClass(p);

// the overridable default
#[default]
#[label(adult)]
pub derive can_vote(p) :- Adult(p);

// the exception: an honest head, and the attack as a directive
#[defeats(can_vote(p))]
pub derive disenfranchised(p) :- Felon(p);

Every rule now reads true: special-class members can vote; adults can vote by default; felons are disenfranchised, and that disenfranchisement defeats the default. The pure ⇝ defeater — block without asserting anything anyone consumes — is recovered as the degenerate case: a #[defeats(…)] rule whose head no other rule or query reads. Heads never lie; the polarity flip is gone because there is no flip.

Numeric priority is subsumed, not replaced like-for-like: lex specialis becomes the specific rule defeating the general clause’s label — an explicit, resolution-checked, cross-package-stable edge instead of a pair of magic integers that only mean something relative to each other.

D2 — The attack is a directive, not grammar

Defeat edges are meta-level — statements about rules, not conditions in them. The #244 body sketched a trailing defeats … clause after the rule body; that sketch is rejected (first correction comment): trailing position reads as part of the body, conflating the object level (what the rule derives) with the meta level (which other rules it displaces). The right surface is the directive plane above the rule — Argon’s established home for argument-bearing compiler directives (the §13.5 MLT relational decorators already resolve type arguments and emit classification wire events; this is the same shape with rule-and-variable arguments instead of type arguments).

No new grammar keywords. A default modifier keyword was also rejected: default and defeats are strategy vocabulary (D6), and strategy vocabulary must not be privileged in the core grammar — the same neutrality reasoning as the no-ambient-vocabulary doctrine (#208), applied to reasoning strategies. The directives:

Hard prerequisite: the directive registry (audit dc-01) lands before or with these directives. Today an unknown attribute is silently ignored — #[defeasable] silently strictens a rule — and with #[defeats] carrying legal meaning, a typo must never silently change what a norm program concludes. Unknown or malformed directives refuse loudly; the registry is the gate.

D3 — Targeting: head-level, clause-level, trait-qualified — all in v1

All three targeting forms ship in v1; there is no interim subset (locked: no shortcuts).

• Head-level — #[defeats(can_vote(p))]: attacks every #[default] clause of that head.
• Clause-level — #[defeats(can_vote.adult(p))]: attacks exactly the clause labeled adult. head.label is the reference form; labels are per-head identities (D2).
• Trait-qualified — #[defeats(Vote::can_vote(p) @ A)]: attacks a trait member’s clause at a given impl target, using the post-#217 qualified catalog naming (Trait::member @ Type).

Targets are resolution-checked at elaboration (goto-def-able): an unresolvable target — no such head, no such label, no such qualified member — refuses loudly.

v1 scope (amended 2026-06-13, PR #354). Defeat-edge resolution is file-local in v1: a #[defeats] target resolves against the rule catalog of the module that declares the attack, and a target naming a head/label/member outside that file refuses as unresolvable (OE0716). This is consistent with D7’s structural guarantee — selection is per module, so a connected defeat graph is single-strategy because edges resolve within the module that declared them. It narrows the cross-package aspiration sketched above for the trait-qualified grain (“a regulation package can defeat a clause it does not own”): the addressing substrate (post-#217 qualified catalog naming) exists, but workspace-scoped resolution requires lifting the defeat pass out of per-file elaboration into a combined-artifact pass — a build-pipeline change deferred so it does not ride alongside the two correctness fixes this PR lands. Cross-module composition through honest heads (strategy-independent) is unaffected and works today. Tracked: #362. Rationale recorded per the locked-design amendment discipline (AGENTS.md “RFDs record settled designs”).

Directive arguments resolve against the decorated rule’s variables (head + body). The argument binding ties the attacker’s tuples to the target’s: #[defeats(can_vote(p))] on disenfranchised(p) :- Felon(p) blocks can_vote exactly for the p the attacker derives — per-tuple blocking, not head-wide suppression. An argument name that does not bind in the decorated rule is a loud error, never a fresh variable — the #242 lesson: a name silently treated as a fresh variable is how knows(x, carol) matched everything. The same single resolution discipline as RFD 0027 D1 applies inside directive argument position.

D4 — Attack discipline

• Strict conclusions are unattackable. A #[defeats] target that resolves to a head or clause not marked #[default] is a loud error. Adding rules to a classical program can only add conclusions; defeat exists only where overridability was declared.
• Defeat-graph cycles are refused loudly in v1. The graph is over resolved rule identities (clauses and heads), known at elaboration; acyclicity is decidable at build time (D10). Cyclic attack structures are exactly where the well-behaved compilation stories diverge; v1 refuses rather than picking one silently.
• Defeated defeaters are legal. A #[defeats] rule may itself be #[default] and be the target of another attack — the exception to the exception — subject to the cycle gate.
• Ambiguity blocking is retained (current behavior): a blocked tuple is simply absent from the head’s extent; it does not propagate a third truth value downstream. Ambiguity propagation is a different strategy (D7), not a switch on this one.
• Team defeat, recorded explicitly: survival is support-based, per tuple. A tuple is in the head’s extent iff some clause not attacked on that tuple derives it — clause-level targeting blocks only the labeled clause’s contribution; head-level targeting blocks all #[default] clauses. An unbeaten teammate keeps the conclusion. This is the reading clause-union forces, and it is recorded here as the chosen semantics rather than left implicit; stricter team-defeat variants belong to future strategy vocabularies.

D5 — Strategy = compilation scheme, not engine mode: the four hooks

The architectural decision (locked): a defeasibility strategy is a compilation scheme onto the core semantics, never an engine mode. The engine — classifier, stratifier, reasoner — stays strategy-blind. The core language owns exactly four strategy-neutral hooks:

1. Rule identity surviving lowering into the catalog. rule_id and qualified_path already survive (post-#217); #[label] extends identity to the clause grain. Identity is catalog-addressable — the same addressing that makes targets resolution-checked.
2. Defeat edges as resolved wire metadata in the .oxbin. Each edge: attacker identity, resolved target set, argument binding. Resolved at elaboration — the wire never carries bare text to be re-resolved downstream (the #213 discipline).
3. A transform slot in the pipeline, between lowering and stratification. The strategy compilation consumes the declared program + markers + edges and emits a core stratified/WFS program. Everything downstream of the slot sees ordinary rules.
4. A provenance channel on derived tuples (D8) — the strategy maps its proof statuses onto it; the channel itself is strategy-neutral.

A strategy is then a quadruple: (directive vocabulary, compilation scheme, tag mapping, correctness proof). The RuleStrength wire field and its Lean mirror retire with the surface triple — hook 1 supersedes the strength field: once the artifact’s defeasibility metadata carries default markers, labels, edges, and the strategy id (D6), a wire-level strength is no longer a hook but a strategy-internal derivative, reconstructed inside the transform where the compilation needs it (the retirement is carried as an explicit Lean obligation, D10.6).

Module extraction (§3.5) operates pre-transform, over labeled rules + defeat edges — which is exactly the granularity Locality/DefeasibleExtraction.lean already mechanizes (defeat_complete_preserves over rule identities and a superiority relation). The hooks were, in this sense, already proven before they were named.

D6 — Strategy #1: Governatori with explicit superiority, as its compilation

The first (and v1 only) strategy is Governatori-style defeasible logic with explicit superiority and ambiguity blocking, specified as its Maher-2021-style compilation onto the core stratified/WFS semantics. §7.8 already commits that “no separate reasoner is invoked; the existing stratified-fixpoint machinery is reused” — this RFD promotes that from implementation note to definition: the meaning of a #[default]/#[defeats] program is the meaning of its compiled core program. Superiority is the explicit edge set (D3); there is no implicit priority anywhere.

The strategy id is recorded in the .oxbin defeasibility metadata. v1 programs get it implicitly (the exact identifier is assigned at implementation); the field exists from day one so that artifacts are honest about which compilation gave them their meaning, and so that per-module strategy selection (D7) has a place to land.

The existing fused strength-stratified evaluator may survive only as a fast path under the oracle obligation (D10): it must agree with the compiled program on every input, checked by the RFD 0018 differential discipline. If it can’t be kept in agreement, it dies; the compiled program is the semantics either way.

D7 — Strategy evolution: per-module vocabularies, editions, and the tier ladder

• Future strategies arrive as use-imported macro-vocabulary packages once the macro atom matures (§13 V1): a package exports its directive vocabulary plus its compilation scheme. Selection is per module, which structurally guarantees that a connected defeat graph is single-strategy — edges resolve within the module that declared them, and cross-module composition happens only through honest heads, which are strategy-independent.
• Migration off the implicit default is edition-shaped: a deprecation window plus a mechanical migration tool (the rustfix precedent). No flag-day; no silent reinterpretation of existing programs.
• Cost containment: a strategy whose compilation needs more than stratified/WFS does not get a new engine — it lands on the §9 tier ladder: the #[brave]/stable-model tier or the ARS external-solver layer (§17). Strategy choice can change a program’s tier; it can never change the engine.

D8 — Provenance: the proof-tag channel, un-squatted

The Governatori proof tags — +Δ definitely provable, −Δ definitely refuted, +∂ defeasibly provable, −∂ defeasibly refuted — are finally surfaced on derived tuples through the provenance channel (hook 4). The tag mapping is strategy-owned: strategy #1 maps its compiled strata onto the four tags; a future strategy maps its own statuses. The §7.8 query surface for tags (match over +Δ/+∂/is unknown) stays as specified; this RFD supplies the channel it was always waiting for.

The wire proof_tag field is to be un-squatted: its only current writer is fork promotion stuffing promoted_from:{fork} into it (oxc-serve/src/lib.rs); fork lineage gets its own field, and proof_tag carries proof tags.

S3 status (amended 2026-06-13, PR #354). Proof tags are surfaced at query time today — Store::query_derive_explained computes each surviving tuple’s +Δ / +∂ tag from the compiled strata (the user-visible ox derive --explain surface, §7.8 tag queries). No proof tag is persisted to AxiomEvent.proof_tag (the comptime lifter writes None), so the fork-promotion squat does not collide with any proof-tag writer yet — but it is still a wrong use of the field. Moving fork lineage to its own field touches the @[language_interface] AxiomEvent wire shape (its Lean mirror, the oxbin codec, the Postgres column, and ~28 struct constructions), so the un-squat is deferred out of this correctness PR rather than landed beside the F1/F2 transform fixes. Tracked: #363.

D9 — Migration: loud deprecations, the §7.8 rewrite, diagnostic fates

• #[strict], #[defeasible], #[defeater], #[priority], and pub priority become loud deprecation errors pointing at the new forms. No silent aliasing — a norm program’s meaning never changes without the author seeing it. #245’s stage 1 (the interim loud refusal of #[priority]) is independent and lands first; this RFD is stage 2, removing the attribute for good.
• §7.8 is rewritten around the hooks/strategy split: the strength-attribute prose, the #[priority] section, and the pub priority blocks all die; the chapter specifies honest heads + the directive vocabulary as strategy #1 over the four hooks.
• examples/legal_norms_can_vote is migrated to the D1 form — the canonical example must read correctly, since misreading it is what started this.
• Diagnostic fates (all four are phantoms today — audit dc-03 — so nothing is removed from the catalog, only from the book): OE0413 (DefeaterAssertsConclusion) is moot — no rule can assert what a defeater denies, because no rule spells a head it denies. OE0412 (PriorityNotIntegral) dies with #[priority]. OE0414 (MixedStrengthAtHead) dissolves — strict and #[default] clauses sharing a head is the intended idiom (the special-class rule next to the adult default), not a hazard. OE0411’s concern (defeat cycle) survives as the new cycle-refusal code, under a fresh number (D11; no reuse).

D10 — Lean obligations

Surface settled (this RFD); per the workflow table the substrate semantics go Lean-first, leading each implementation slice:

1. Transform-correctness theorem. The compiled core program, evaluated under the existing stratified/WFS semantics, realizes the declared defeasible semantics: a per-tuple defeasibleWarranted-style specification over labeled rules + defeat edges (the DefeasibleExtraction.lean shape, lifted from rule grain to tuple grain with argument bindings) agrees with the compiled program’s model.
2. Fused-evaluator agreement. If the strength-stratified evaluator is retained as a fast path, it agrees with the compiled program as oracle on all inputs — the RFD 0018 differential-oracle discipline (semi-naive = oracle precedent).
3. Defeat-graph acyclicity is decidable — decidable checker plus non-vacuity witnesses on a concrete program (the #221 conformant_iff pattern).
4. Compatibility with defeat-aware module extraction (§3.5). defeat_complete_preserves already operates over rule identities + superiority edges, pre-transform; restate it over the new edge carrier and prove extraction-then-transform agrees with transform-then-extraction on the extraction signature.
5. Narrowing soundness re-keyed. The existing restriction — only narrowings established by strict rules are preserved under defeasible attack (TypeSystem/Soundness/Defeasibility.lean) — is restated over #[default]: the counterexample and the strict-only soundness theorem carry over unchanged in substance.
6. Wire mirrors under @[language_interface] for the defeasibility metadata (labels, edges, strategy id); the RuleStrength mirror retires with the surface triple.

D11 — Diagnostics inventory

All codes proposed; numbers assigned at implementation against the live catalog (the OE1322→OE1326 renumbering is the cautionary precedent; #150’s catalog-first discipline applies — no raw-string emissions). The 04xx range is proposed for the defeasibility plane: it is unallocated in appendix C’s range table, and the phantom OE0411–OE0414 die rather than being reused — no number reuse, per registry hygiene.

• Unknown directive — the registry gate itself (dc-01; attribute subsystem, 07xx range): an unrecognized or malformed #[…] refuses loudly.
• Unbound directive variable — a #[defeats] argument that binds in neither the head nor the body of the decorated rule; names the offender and the rule’s bound set; never a fresh variable.
• Unresolvable defeat target — no such head, no such label on that head, no such qualified trait member.
• Defeats a strict conclusion — the target resolves to a head/clause not marked #[default].
• Defeat-graph cycle — names the cycle, rule by rule.
• Duplicate label per head — two clauses of one head labeled identically.
• Deprecated strength attribute — #[strict]/#[defeasible]/#[defeater]/#[priority] or pub priority; the help text shows the new form for the specific case (migration, D9).

Alternatives considered

• Trailing defeats … grammar clause (the #244 body sketch): rejected — it reads as part of the rule body, conflating the object level with the meta level; defeat edges are statements about rules, and the surface must say so (first correction comment).
• default / defeats as grammar keywords: rejected — strategy vocabulary must not be privileged in the core grammar; the substrate stays neutral between defeasibility strategies exactly as it stays neutral between ontologies (#208’s reasoning, one level up). The directive plane carries the vocabulary; the grammar carries nothing.
• Numeric #[priority(N)] + pub priority superiority blocks: removed — global integers are non-compositional across modules and packages (whose 10 beats whose 7?), and both are dead in practice: the attribute is silently discarded (sf-02, #245) and the blocks never parsed. Explicit edges subsume the use cases: lex specialis is the specific rule defeating the general clause’s label; derived superiority (lex posterior over enactment dates) belongs to a future strategy vocabulary that derives edges, not to core.
• Engine-mode pluggable strategies (a strategy enum the reasoner switches on): rejected — the engine stays strategy-blind; compile-to-core keeps one trusted kernel and one mechanization target. The evidence the hooks suffice for the known strategy space: grounded argumentation semantics is the well-founded semantics of the argument meta-program (Dung 1995); courteous logic programs compile to LP with NAF (Grosof 1997); Governatori-style defeasible logic compiles to three strata of stratified Datalog (Maher 2021). Each is a quadruple over the same four hooks.
• Head-level-only targeting in v1: rejected — no interim subsets (locked: do the full thing). Clause-level and trait-qualified targeting are where cross-module exceptions live — defect 4 — and the addressing substrate (post-#217 qualified catalog naming) already exists; shipping head-level-only would re-create the compositionality gap this RFD exists to close.

Recorded non-decisions

• Trait-side strength pinning (the #240 shape): whether a trait can pin its members’ overridability, and whether one impl’s clause can be #[default] while another’s is strict — open, recorded in #244; nothing in this design forecloses it.
• Ambiguity propagation and stricter team-defeat variants — future strategy vocabularies, not switches on strategy #1 (D4, D7).
• Strategy-package format — the exact shape of a use-imported strategy vocabulary awaits the macro atom (§13 V1); only the hooks contract is fixed now.
• Temporal proof tags (the 4-slot Governatori-Rotolo schema) — stay deferred exactly as §7.8 already records.

Sequencing

Each slice is loud-complete on its own — no slice ships a parsed-but-inert surface — and the Lean obligations (D10) lead each slice’s semantics per the workflow table. One deliberate deviation from the “RFD + reference draft” pairing: the §7.8 rewrite waits for S4 rather than landing with this RFD — rewriting the chapter now would describe an unimplemented surface, repeating the exact book-ahead-of-code failure (pub priority, OE0411–OE0414) this RFD retires; until S4, §7.8 carries a superseded-pending marker pointing here.

The slices:

1. S1 — hooks. Rule identity and #[label] through lowering into the catalog; defeat edges as resolved wire metadata; the directive registry lands here as the prerequisite (dc-01) — unknown directives refuse loudly before any new directive exists to typo.
2. S2 — vocabulary + transform. #[default]/#[defeats] resolution and validation (D3/D4 gates); the strategy transform in the pipeline slot; the compiled program is the semantics, with the fused evaluator retained only under the oracle check (D6, D10.2).
3. S3 — provenance. Proof tags through the channel; proof_tag un-squatted (fork promotion gets its own field); the §7.8 tag-query surface lights up.
4. S4 — migration. Loud deprecation errors for the old surface; legal_norms_can_vote migrated; §7.8 rewritten around the hooks/strategy split; the phantom OE041x block dies with it.

Relationship to existing issues

• #244 — settled by this RFD, incorporating both correction comments (directive plane over grammar clause; the final lock).
• #245 — stage 1 (interim loud refusal of #[priority]) is independent and lands first; stage 2 is settled here: the attribute and the pub priority prose are removed for good.
• Audit dc-01 — the directive registry is the hard prerequisite (S1); dc-03 — the phantom OE0411–OE0414 citations die in the §7.8 rewrite; sf-02 — the executed priority-discard repro is resolved by removal, not implementation.
• #242 / #243 — the loud-unbound rule for directive arguments and resolution-checked qualified targets are those lessons, applied at the directive plane (D3).
• #240 — trait-side pinning stays open; recorded non-decision.
• RFD 0010 (negative facts) — orthogonal: defeat blocks, it does not assert negative catalog facts.
• RFD 0026 / #217 — qualified member naming is the targeting substrate for Trait::member @ Type defeat targets.
• RFD 0018 — the differential-oracle discipline governs the fused evaluator (D10.2).
• #134 — the WFS mechanization catch-up; the transform-correctness theorem (D10.1) lands against the same Reasoning/Datalog layer.