Defeasibility

Real rules have exceptions. Adults may vote, unless they are felons, except for certain special classes. A node is presumed flagged, unless something clears it. Classical Datalog has no room for this; Argon makes it first-class without letting any rule lie about what it derives. The reference fixes the design under defeasible reasoning on three commitments: a rule derives exactly what its head says, the attack between rules is a directive rather than a clause, and the meaning of a defeasible program is its compilation onto the core fixpoint. RFD 0028 — Defeasibility redesign: honest heads, the defeat-directive plane, and strategy as a compilation scheme records the design decision.

A rule comes in one of three strengths. An unmarked derive rule is strict — classical Datalog, unattackable; adding more rules can only add its conclusions. #[default] marks a clause defeasible — it holds unless an applicable attacker blocks it, the reading of Rust’s default fn. A defeater is an ordinary rule whose body, when it fires, blocks a target conclusion; it carries #[defeats(target(args))], and in the degenerate case where no one reads its own head it does nothing but block. #[label(name)] gives a clause an identity so an attack can name it.

The franchise model reads true at every line. Special-class members vote by a strict clause; adults vote by a defeasible one; felons are an exception with its own honest head:

pub derive can_vote(p) :- SpecialClass(p);          // strict, unattackable

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

#[defeats(can_vote(p))]
pub derive disenfranchised(p) :- Felon(p);          // the attack is a directive

No rule spells out the head it denies. The exception lives under its own name, disenfranchised, and the attack rides the directive above it. Because the #[defeats] argument resolves against the attacker’s own variables, the block is per-tuple: disenfranchised(p) blocks can_vote for exactly the p it derives, not the whole head. A #[defeats] argument bound in neither head nor body is a loud error, never a fresh variable. The strict clause is out of reach — a special-class felon still votes, because the attack resolves only against the defeasible adult clause. Targets are resolution-checked at elaboration, so an unresolvable or strict target refuses rather than misfiring, and a cycle in the attack graph is refused outright rather than resolved by a silent choice.

A tuple survives when some clause not attacked on it derives it — team defeat: an unbeaten teammate keeps the conclusion. A blocked tuple is simply absent from the extent; it does not propagate a third truth value downstream. Every later rule reads that post-defeat extent, even through strict intermediate rules. Marking a later reader #[default] makes that reader overridable; it does not restore blocked input rows. With no attacker on the reader, it returns the same rows as an otherwise identical strict reader. Defeaters can themselves be defeated. A pardon that defeats a disenfranchisement restores the vote: the #[defeats] rule is itself #[default] and attacked in turn, and as long as the chain bottoms out the pardoned felon’s can_vote returns. The block is computed from each attacker’s surviving extent, so a defeated defeater stops blocking exactly where it was beaten.

The strategy that runs is Governatori-style defeasible logic with explicit superiority and ambiguity blocking, compiled in three strata — support, then blocking from surviving attackers, then a team-defeat fold — onto the same stratified and well-founded engine of Reasoning. No separate reasoner runs; the engine stays strategy-blind, and the strategy’s identity is recorded in the built artifact so it is honest about which compilation gave it its meaning. The Lean proves the defeat algebra over each clause’s converged contribution: the team-defeat fold equals the declarative warranted set (compiled_extent_eq_warranted), strict clauses are unattackable, ambiguity blocking holds, and a defeated defeater no longer blocks (defeated_defeater_does_not_block). What the Lean does not yet re-prove is the correspondence for a recursive clause’s fixpoint under defeat; that rests on the differential-oracle corpus, where a transitive closure under a live defeat plane returns its full extent and a pardoned felon regains the vote.

Proof tags

Every derived fact carries a proof tag, surfaced through the provenance channel by ox derive --explain. +Δ marks a conclusion definitely provable — supported by a strict, unattackable clause. +∂ marks one defeasibly provable — supported by a surviving default clause after defeat resolution. Their negatives, −Δ and −∂, mark definite and defeasible refutation. The tag is the difference between a fact that holds come what may and one that holds only because nothing beat it:

$ ox derive examples/legal_norms_can_vote can_vote --explain
  +Δ (dave)     // strict special-class clause
  +∂ (alice)    // surviving adult default

A defeasible model reports not only what survived but on what strength, so an answer that looks wrong is something to investigate rather than accept.