Reasoning

A derive program is a set of rules (derive); its meaning is the set of tuples those rules derive. This chapter fixes that meaning: the least-fixpoint model of the positive program, the stratification that orders negation, the well-founded semantics that handles recursion through negation, and the defeasibility layer that compiles overrides onto all of it. The surface — what a derive rule looks like and what each clause is allowed to say — is in derive; this chapter is what the engine computes from it.

Least-fixpoint model

A positive derive program (no negation, no aggregation) denotes a single model: the least fixpoint of its immediate-consequence operator. Start from the ground facts, apply every rule once to derive new tuples, repeat until nothing new appears. Over a finite domain this terminates, and the result is unique — independent of the order rules fire. Multiple derive clauses with matching head name and arity union into one relation node, so a seed tuple and a recursive clause over the same head share a fixpoint (seeds ∪ derived-closure).

Aggregation extends the operator without breaking uniqueness, provided each aggregate reads a strictly lower stratum than its head writes (the stratification below). The aggregate fold then sees a converged input relation before it runs, so the fixpoint over the layered program is still unique.

Stratified negation

Negation breaks the monotonicity the least fixpoint relies on: a tuple that adds to a positive relation can remove a tuple that a not atom guarded. Stratification restores order. The rules are partitioned along their axis dependency graph — which axes a rule’s body reads against which axis its head writes — and each layer is evaluated to fixpoint before the layer above it reads its negation. A rule’s body negation must read a relation already converged in a lower stratum.

The graph must be acyclic for this layering to exist. The Lean substrate proves (Theorem 2) that a cycle in the axis dependency graph admits a Cat1/Cat2 rule pair whose stratified fixpoint is order-dependent — there is no canonical layer assignment, so the program has no single stratified model. Cross-stratum, acyclic negation is ordinary stratified negation and is evaluated by this layering.

A negation cycle that no stratification can layer — p :- not q, q :- not p — is not rejected. It is dispatched to the well-founded semantics below. (The diagnostic that once rejected such a cycle, OE1309, no longer fires from stratification; it survives only as the dispatch seam.)

Well-founded semantics

Negation reads against the well-founded model, computed by the Van Gelder–Ross–Schlipf 1991 alternating fixpoint. WFS is the default because the well-founded model always exists and is unique — every program has exactly one, with no choice for the engine to make. The headline consequence: recursion through negation is accepted. A negation cycle that strict stratification cannot layer is evaluated by the alternating fixpoint rather than refused.

The alternating fixpoint is three-valued: every atom is true, false, or undefined. The engine materializes the definitely-true extent as the head’s rows, and an atom the alternating fixpoint cannot pin to true or false — a genuine standoff — is carried alongside as the head’s undefined extent. The query surface is four-valued: a definitely-true tuple is an Is row, and an undefined tuple surfaces as a Can row, by default — never silently omitted, because an omitted standoff is byte-indistinguishable from a definite Not (the epistemic failure the Truth4 discipline exists to prevent). A rule body still joins only against definite rows — an undefined atom does not fire downstream rules; propagating undefined-ness through body joins is the engine-level three-valued lift, tracked separately.

For conditional obligations this keeps the sound projection while restoring the honesty: an obligation whose trigger is genuinely undecided neither fires nor is denied — and the read says so (Can) instead of omitting it.

The envelope contract: the four-valued agent view carries Can rows inline and counts them in hidden.can; the human fail-closed K3 projection (opt-in) drops Can rows from the row list but still reports them in hidden.can — drop-but-count, never a silent collapse. ox derive prints the undefined extent after the definite tuples (silent when empty). The defeat-plane evaluator is two-valued wherever the defeat graph is acyclic — where no defeat target depends back on its own attacker, every head is definitely true or definitely false and contributes no undefined extent. A genuine mutual-defeat cycle — a target whose attacker’s derivation depends in turn on that same target (a rule-dependency cycle through the attacker’s derivation, not a defeat-graph identity cycle, which OE0718 refuses at build time) — has no stable two-valued answer: those heads are undefined under the well-founded model, surfaced as Can like any other undefined extent, and are never resolved by evaluation order. The legacy strength-stratified evaluator remains two-valued by contract.

#[brave] / stable-model semantics — multiple two-valued models, with credulous and skeptical readings — is out of scope (Out of scope). WFS is the single evaluation discipline.

Defeasible reasoning

Real ontologies have exceptions and overrides; classical Datalog does not. Argon’s defeasibility (RFD 0028) makes them first-class without letting any rule lie about what it derives. The design has three commitments:

1. Honest heads. A rule derives exactly what its head says. An unmarked derive rule is strict — classical Datalog, exactly as derive; its conclusions cannot be overridden.
2. The attack is a directive, not grammar. Whether one rule displaces another is a statement about rules, carried in the directive plane above the rule, never a clause inside its body.
3. Strategy is a compilation scheme. The meaning of a defeasible program is the meaning of its compilation onto the core stratified/WFS semantics. No separate reasoner runs; the engine stays strategy-blind.

The directive vocabulary

The canonical example — adults can vote by default, felons are disenfranchised, special-class members vote regardless — reads true at every line:

// strict = unmarked: special-class members vote, period (unattackable)
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);

No rule spells the head it denies. The exception lives under its own name (disenfranchised); the attack rides the directive plane. The pure “block without asserting” defeater (Governatori’s ⇝) is the degenerate case — a #[defeats(…)] rule whose head no one reads.

Targeting

A #[defeats] target is resolution-checked at elaboration (goto-def-able); an unresolvable target refuses loudly. A target resolves over the attacking module’s import-scoped catalog — its own rules plus the pub rules reachable through its use imports (RFD 0082), so an exception can live in another file and name what it overrides under its own honest name. Scope follows ordinary name resolution exactly: importing the rule (a use leaf, glob, or alias) puts its bare short name in scope; importing only its module binds the module name, so its members are addressable by the qualified-path spelling, not by bare name. Three targeting forms ship, plus qualified-path disambiguation:

• 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. This is lex specialis — the specific rule defeating the general clause’s label, an explicit module-stable edge rather than a pair of magic priority integers.
• Trait-qualified — #[defeats(Vote::can_vote(p) @ A)]: attacks a trait member’s clause at a given impl target, using the qualified catalog naming (Rule-atom grammar).
• Qualified-path disambiguation — #[defeats(other_module::can_vote(p))]: when a bare short name is visible from more than one imported module it is ambiguous and refuses (OE0736); the qualified path resolves the head against exactly the named module. An own-module declaration shadows imported ones, like every other resolution position.

Cross-module targeting has three bounds. Defeat visibility equals ordinary name visibility (OE0737): a rule the attacking module cannot name is not a legal target — a non-pub rule is attackable only from its own module and that module’s descendants (the ordinary descendant-private rule), never from a distance. #[default] is the consent token: a rule can be overridden from another file only if its own author marked it #[default] (OE0717, unchanged). The edge stays inside one package (OE0738): a package is a trust and versioning boundary, and a dependency update must not silently change a program’s conclusions — cross-package composition goes through ordinary use of public predicates (honest heads), never through a defeat edge.

Arguments resolve against the decorated rule’s variables. #[defeats(can_vote(p))] on disenfranchised(p) blocks can_vote exactly for the p the attacker derives — per-tuple blocking, not head-wide suppression. A #[defeats] argument that binds in neither the head nor the body of the rule is a loud error (OE0721), never a fresh variable.

Discipline

• Strict conclusions are unattackable (OE0717). A #[defeats] target resolving to a head or clause not marked #[default] refuses: adding rules to a classical program can only add conclusions.
• Defeat-graph cycles are refused (OE0718). The graph over resolved rule identities is acyclic by build-time check; cyclic attack structures are where the well-behaved compilation stories diverge, and Argon refuses rather than picking one silently.
• Defeated defeaters are legal — a #[defeats] rule may itself be #[default] and be attacked in turn (the exception to the exception), as long as the chain bottoms out.
• Team defeat, ambiguity blocking. A tuple is in the head’s extent iff some clause not attacked on that tuple derives it — an unbeaten teammate keeps the conclusion. A blocked tuple is simply absent from the extent; it does not propagate a third truth value downstream. This clean present/absent verdict holds wherever the defeat is acyclic. It does not hold on a genuine mutual-defeat cycle — a target whose attacker’s derivation depends back on that same target (a rule-dependency cycle, distinct from the defeat-graph identity cycle OE0718 refuses) — where the tuple is neither definitely present nor definitely absent but undefined under the well-founded model (surfaced as Can, above); there is no order-of-evaluation answer.
• Downstream rules read warranted extents. Once a tuple is blocked, every later positive body atom reads the post-defeat extent, including through any number of strict intermediate heads. Marking a downstream reader #[default] makes that reader overridable; it does not switch its inputs back to the pre-defeat support catalog. If no rule attacks that reader, it derives the same tuples as an otherwise identical strict reader.
• Duplicate labels per head refuse (OE0719); labels are per-head identities.

Worked: acyclic defeat vs a mutual-defeat cycle

When the attacker’s own derivation never reads back through its target, every head settles — two-valued, no third truth value anywhere. A defaulted discount, attacked by a fraud hold whose body reads only base facts:

#[default]
pub derive discount(o) :- Large(o);

#[defeats(discount(o))]
pub derive fraud_hold(o) :- Flagged(o);

A flagged large order’s discount is definitely false — absent from the extent, not undefined. The hold fires, the default is blocked, and nothing downstream ever sees a Can.

Now let each attacker’s body read the other default’s head:

#[default]
pub derive keys_a(p) :- Employee(p);

// a's disqualifier holds exactly when b's access does
#[defeats(keys_a(p))]
pub derive conflict_a(p) :- keys_b(p);

#[default]
pub derive keys_b(p) :- Employee(p);

// ... and b's disqualifier reads a's access back
#[defeats(keys_b(p))]
pub derive conflict_b(p) :- keys_a(p);

The defeat graph itself is still acyclic — conflict_a attacks keys_a, conflict_b attacks keys_b, no attacker is anyone’s target — so the program is admitted, not refused. But the rule-dependency graph now cycles through negation: keys_a holds unless conflict_a blocks it, conflict_a holds exactly when keys_b does, and symmetrically back. Neither head can settle: granting keys_a blocks keys_b, which withdraws the very conflict that would have blocked keys_a — and the mirror-image assignment is equally supported. There is no stable two-valued answer, and no evaluation order is allowed to invent one. Both keys_a and keys_b surface undefined (Can) for every employee, per the envelope contract above.

Because undefined is a defined outcome here — not an error — the elaborator does not refuse this program; it warns. OW0740 (mutual-defeat-cycle-undefined) fires at elaboration whenever the resolved defeat plane forms such a rule-dependency cycle through defeat, naming the mutually-defeating public heads (here keys_a and keys_b) so an author who expected a definite verdict learns those heads read Can. The lint is representation-independent — it inspects the resolved defeat edges and the lowered rule bodies, not whether the plane is compiled to strict rules or evaluated by the runtime resolver — and fires only for this shape: never for the OE0718 identity cycle (refused earlier), never for a defeat-free recursion-through-negation cycle (the ordinary well-founded treatment above), and never for the acyclic stratified-defeat fragment (provably two-valued). To recover a definite classification, break the cycle: remove or redirect one attack so no attacker’s derivation reads back through its own target. A strict base clause is a partial remedy only — it settles the tuples it covers (those become definite, and definite verdicts cascade around the cycle for them), but the heads stay cyclic for every other tuple and the warning stands.

Strategy #1: Governatori with explicit superiority

The strategy is Governatori-style defeasible logic with explicit superiority and ambiguity blocking, specified as its Maher-2021 three-stratum compilation onto the core stratified/WFS semantics:

1. Support — run every clause (strict + default, plus the attacker rules’ own honest heads) to fixpoint over the materialized base, and attribute each clause’s contribution over that converged catalog — a recursive clause sees its own prior tuples, so transitive closure does not under-derive.
2. Blocking, from surviving attackers — project each attacker’s surviving extent (resolved in defeat-graph topological order, which exists because the graph is acyclic) through its edge argument binding to the blocked target tuples (per-tuple). A defeated defeater contributes nothing — it no longer blocks on the tuples where it was itself defeated.
3. Team-defeat fold — strict clauses contribute unconditionally; a default clause contributes the tuples no surviving edge blocks.

Clause attribution composes these strata rather than exposing raw support as a downstream read model. When attributing one defeasible head, the evaluator keeps that head’s own converged support available for recursive clauses, replaces other defeasible heads with their warranted extents, and recomputes strict intermediate heads over those warranted extents. This preserves recursive closure without allowing a downstream default clause to recover a tuple defeated upstream.

The strategy id is recorded in the .oxbin so an artifact is honest about which compilation gave it its meaning. Future strategies (default logic, courteous LP, argumentation, ASP preferences) arrive as use-imported macro-vocabulary packages selected per module; the engine never changes.

Proof tags

Every derived fact carries one of four tags (Rule-atom grammar), surfaced through the provenance channel (ox derive --explain):

• +Δ definitely provable — supported by a strict (unattackable) clause.
• −Δ definitely refuted.
• +∂ defeasibly provable — a surviving #[default] clause supports it after defeat resolution.
• −∂ defeasibly refuted — every supporting clause was attacked.

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

For an artifact whose defeat plane was compiled at elaboration (the strict-WFS lowering recorded in the artifact’s defeat-provenance section), --explain additionally prints the compilation header. The header is artifact-scoped — the carrier records the whole module’s compiled plane, whatever rule is queried — and lists the strategy that gave the compiled rules their meaning and, per source clause, its #[default]/strict kind, #[label], emitted internal support relation, and the #[defeats] edges that clause declared (a clause-level target keeps its .label grain):

artifact: defeat plane COMPILED at elaboration (strategy: Governatori with explicit
superiority); 2 source clause(s) lowered to strict WFS rules
  #[default] m::can_vote #[label(adult)] → support $defeat::support::m::can_vote::adult
  strict m::disenfranchised → support $defeat::support::m::disenfranchised::#0
      defeats m::can_vote.adult

The Lean substrate proves the defeat algebra over each clause’s converged contribution: the team-defeat fold realizes the declarative per-tuple warranted set (Argon.Reasoning.Defeasibility.Transform.compiled_extent_eq_warranted), strict conclusions are unattackable (strict_clause_unattackable), ambiguity blocking holds (all_supporting_clauses_attacked_absent), and — modelling the blocking sets as derived from the attackers’ surviving extents rather than as opaque inputs — a defeated defeater no longer blocks (defeated_defeater_does_not_block, block_mono_in_survivors, pardoned_target_survives). The safe interaction with occurrence typing carries over — only narrowings established by strict (non-#[default]) rules are preserved under defeasible attack (Argon.TypeSystem.Soundness.Defeasibility).

Migration from the strength triple

The pre-RFD-0028 surface — #[strict] / #[defeasible] / #[defeater], #[priority(N)], and pub priority blocks — is removed, and refuses loudly (OE0722) with no silent aliasing. The map:

• #[defeasible] → #[default].
• #[defeater] (which spelled the head it denied) → an ordinary rule under its own honest head carrying #[defeats(target(args))]; the targeted clause must be #[default].
• #[strict] → delete it; unmarked rules are already strict.
• #[priority(N)] / pub priority → an explicit #[defeats] edge. 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.