The shape of a rule

A legal rule includes the qualifications that govern its application. “You must file annual returns.” Its operative structure is: “You must file annual returns, unless you are a dormant company. Unless you are in administration. Unless you have been granted an extension by the registrar. Unless the registrar’s extension has been revoked because you failed to satisfy its conditions.” Each exception can itself have an exception. The registrar’s revocation might be subject to appeal, and judicial review might stay that appeal.

Defeasibility lets a legal system apply general rules while accommodating the variety of actual situations. The rule states the general case, and exceptions specify the cases that receive different treatment. Lawyers therefore read a statute alongside its exceptions, carve-outs, schedules, and subordinate legislation. A machine needs a representation of those qualifications.

What a defeasible rule is

A defeasible rule has a base verdict, a finite set of exceptions, and a finite override relation. The base verdict states what holds in the general case. Each exception pairs a guard, a predicate over the facts of a case, with the verdict that holds when the exception prevails. The override relation records which exception prevails when both fire. The rule is well-formed when that relation is acyclic. Its transitive closure is then a strict partial order on the exceptions: the exception order.

Two exceptions are comparable when one overrides the other, directly or through a chain, and incomparable when neither does. An implementation assigns numeric priorities. An assignment of distinct numeric priorities that respects the order induces a linear extension, and every linear extension arises this way. Every such assignment faithfully encodes the order.

An assignment that respects the order permits ties only between incomparable exceptions. A tie leaves their relative order to the evaluator. It is faithful for a pair cleared by the confluence check below, since ordering that pair cannot change the verdict. For a flagged pair, the evaluator’s tiebreak can decide the case. The numbers encode the exception order for evaluation.

The first static check below tests well-formedness. A cyclic override relation can faithfully represent overlapping enactments, but it cannot be evaluated. Representing the law and evaluating it are separate operations.

Why priority must be explicit

Consider two exceptions to a tax filing rule. Exception A: “Non-profit entities are exempt from filing.” Exception B: “Entities with revenue exceeding $10 million must file regardless of status.” Entity X is a non-profit with $15 million in revenue. Both exceptions apply. Which wins?

There are several candidate resolution strategies.

Majority vote. Count how many rules say “file” versus “don’t file.” A single constitutional provision overrides a thousand statutes, so counting does not resolve legal priority. Rank attaches to the sources: lex superior derogat legi inferiori, the higher source prevails.

Random selection. Pick one. This provides no legal justification.

Temporal ordering. The later rule wins: lex posterior derogat legi priori. Recency and specificity are independent. A general statute enacted in 2025 does not thereby override a specific statute of 2020 that addresses the situation. Temporal stratification determines which rules are in force and when, as the companion note explains. It is independent of the ordering of exceptions within a rule.

Priority ordering. Exceptions stand in an explicit override relation. Among the applicable exceptions, the one placed highest prevails. This models how legal systems resolve conflicts within a rule.

An override is legal content, so the question is where it comes from. There are three sources, in descending order of authority.

The law fixes it. Statutes state precedence through clauses such as “subject to subsection (4A),” “notwithstanding any other provision,” and “regardless of status.” In the example above, neither exception is more specific. A non-profit with $5 million in revenue falls under A alone, and a for-profit with $15 million falls under B alone. Neither guard entails the other, so specificity leaves them unordered. The phrase “regardless of status” ranks B over A and decides entity X’s case.

Where conflicting provisions come from different levels, such as constitution, statute, and subordinate regulation, lex superior supplies the override before the guards are considered. In both cases, the encoder transcribes the law’s ordering.

Specificity computes it. Lex specialis derogat legi generali: the more specific rule overrides the more general. This principle applies when one guard entails another. Take a base rule, “every company files”; an exception, “dormant companies are exempt”; and an exception to the exception, “dormant companies holding client assets must file.” Every dormant company holding client assets is a dormant company. The narrower guard entails the broader guard and therefore ranks above it, without a precedence clause.

For the decidable guard classes below, built from set memberships, threshold comparisons, and boolean conditions, entailment is itself decidable. This source of priority is therefore computable. It also explains why exceptions outrank the base rule: the base applies to everyone, so every exception’s guard entails it.

The principle lets legislatures qualify their general rules. If a specific exception did not prevail over the general rule it qualifies, enacting it would change nothing. A legislature unable to make exceptions effective could not refine its most general rules.

Someone owns it. When enacted text and entailment leave overlapping exceptions unordered, assigning priority is an act of interpretation. The system attributes that act to a named author and keeps it open to challenge. Each priority records its source: the law, computed entailment, or an author’s interpretation.

The defeat algorithm

Given a well-formed rule and a case, evaluation resolves the exceptions. A guard evaluates the supplied evidence as true, false, or unknown. Unknown means that a missing fact or an event that has not yet occurred prevents a decision. Guards are decidable predicates, as the next section specifies, so they always halt. Unknown records missing evidence.

The scan runs down the exceptions in priority order – any linear extension of the exception order – and stops at the first guard that is not false.

1. If that guard is true, the exception fires: its verdict is the answer, and the evidence that satisfied the guard is attached to the answer.
2. If that guard is unknown, the answer is unknown: the missing fact decides whether this exception fires, and the scan reads no further.
3. If every guard is false, the base verdict applies.

A true guard above an unknown guard settles the case: the higher exception fires however the missing fact resolves. An unknown guard above a true guard leaves the answer open because the missing evidence determines which exception fires. An answer contains the verdict, the exception that fired, and the evidence that satisfied its guard. For this object, the scan is exact under a given extension. It returns an answer exactly when every completion of the missing facts yields that answer. It returns unknown exactly when a missing fact determines which exception fires.

For the bare verdict, the scan is exact when every guard is decided. When evidence is missing, it is sound: any returned verdict holds under that extension however the missing facts resolve. It is also conservative, because an unknown answer may have a fixed verdict. Within one extension, this occurs whenever every open exception above the first true guard has that guard’s verdict. If no lower guard is true, it occurs whenever all open exceptions have the base verdict. Otherwise, within one extension, it occurs only where two open guards share a missing fact.

Across extensions, a confluent rule may place a true guard above an open guard in one extension and return the verdict there. The scan does not search for these alternatives. It stops at the highest open guard and requests the missing fact. That fact determines the justification, which the answer must certify along with the verdict.

The defeat eliminator returns the base verdict, a firing exception, or unknown. An unknown answer names the guard and the missing fact, requesting the evidence needed to settle the case. The companion paper Lex, a typed language for jurisdictional rules, uses total Boolean guards over a typed evidence record. Its five-verdict chain includes Pending for unsettled cases. Both the three-valued guard and the pending verdict represent missing evidence explicitly.

Guards must be decidable

Exception guards must be decidable: given the facts a guard names, a machine computes true or false in bounded time. “If the entity’s revenue exceeds $10 million” is decidable. “If the entity is acting in good faith”, “reasonable person,” and “best interests of the company” require judgment. Treating those judgments as mechanically decidable would be dangerous. With non-termination excluded, unknown has one source: absent evidence.

Many daily compliance questions use decidable guards. Membership in a finite set: is this entity on the sanctions list? Threshold comparisons: does this transaction exceed the reporting threshold? Boolean conditions: does this entity hold a valid license? For guards built from these forms, entailment and joint satisfiability are also decidable. The static checks below use those properties.

Guard evaluation supplies the formal justification for the answer. If revenue exceeding $10 million selects an exception, the answer includes the revenue figure, threshold, and comparison. An auditor can trace the conclusion to the fact that produced it.

Two static checks

Two static checks examine the exception order before any case is evaluated.

Acyclicity. The override relation must contain no cycle. The law can contain one: A overrides B, B overrides C, and C overrides A. Each pairwise override may be deliberate, introduced by an amendment or asserted by an authority unaware of the others. Every scan order then contradicts some override. The system retains the structure as a faithful record of the enactments and marks it as awaiting resolution.

A judge, regulator, or amendment must resolve the cycle. The rule’s history records who resolved it, under what authority, and with what reasoning.

Confluence. A linear extension orders every incomparable pair, and different extensions may order those pairs differently. The check asks whether that choice can affect the verdict. For every incomparable pair, require either jointly unsatisfiable guards, so no case fires both, or equal verdicts. Both conditions are decidable for the guard classes above. A rule that passes is confluent: with all guards decided, every linear extension returns the same verdict. With missing evidence, extensions can differ in precision, with one reporting unknown, but cannot return conflicting verdicts.

For decided cases, the proof has two cases. Returning the base verdict requires every guard to be false, which holds in every extension. If two extensions fire different exceptions, each selected guard is true and every guard above it is false. Each selected exception therefore sits below the other in the opposite extension. The pair is incomparable and both guards are true, so the check requires equal verdicts.

A failing pair identifies guards that can fire together toward different verdicts, leaving their priority underdetermined. An override from the law, computed entailment, or an author resolves the conflict. The check is conservative: it flags such a pair even if a higher exception fires on every case they share. For a legal instrument, conservative conflict reporting is appropriate.

A deterministic evaluator must still return an answer when a flagged pair remains unrepaired. Lex’s mechanized evaluator breaks ties between equal numeric priorities by source position: the earlier exception wins. Source position has no legal meaning. Until an attributed override resolves the pair, transcription order decides its shared cases. The check exposes that dependence.

The explicit rule structure also permits content addressing. A canonical encoding contains the base verdict, exceptions, override relation, and authorities. Its hash names the rule. Identical canonical structures receive the same identifier regardless of where or by whom they were encoded. This permits exact de-duplication across packs and citations to exact rules.

Identity here means identity of canonical form. Semantically equivalent guards written in different syntax receive different hashes. Canonical form supplies the checkable equality needed for audit and reference. The companion note on content-addressed identity develops this scheme.

When independent rules conflict

The override relation so far orders exceptions within one rule. Independent rules can also conflict.

Rule A: “Financial institutions must report all transactions exceeding $10,000.” Rule B: “Medical payments are confidential and shall not be disclosed to financial regulators.” A hospital makes a $50,000 payment to a medical equipment supplier through a financial institution. Both rules apply. Neither is an exception to the other. They are independent rules from independent authorities that happen to conflict in this case.

The defeat eliminator resolves conflicts only where the override relation supplies a priority. Here, no enacted text ranks the rules, their sources have equal rank, neither guard entails the other, and no common authority has assigned priority. Prakken and Sartor (1997) formalize how argument can derive priorities between rules, especially through the interaction of specificity and recency. A derived priority remains an interpretation and needs an owner. Every extension of the explicit override relation therefore enters as new legal content through the same three sources.

Where the relation supplies no priority, evaluation stops for balancing. Balancing identifies the principles at stake, here financial transparency and medical privacy, cites precedents, and gives a reasoned verdict. It is the formal counterpart of judicial reasoning. The system records the principles, precedents, rationale, and deciding authority, then carries the outcome forward as an act of that authority.

Lex represents a required non-mechanical determination as a typed discretion hole. The hole names the decision and the authority entitled to make it. Evaluation stops there until a signed, revocable attestation supplies the decision. The attestation binds the signer, exact value, and rule version.

Given an override relation, the defeat scan resolves priority mechanically. Extending that relation requires judgment with an owner, authority, and rationale. Confusing these roles can stall clear cases by requiring balancing where priority already decides. It can also let mechanical priority decide hard cases without an accountable judgment.

Why this matters for computation

A system that executes law must represent defeasibility. Flat conditionals, if X then Y, give wrong answers whenever an omitted exception applies.

Compliance software that hardcodes boolean checks handles exceptions through manual overrides. Such a flag records a departure, who clicked, and when. The legal basis remains outside the system: which exception applied, on what evidence, and under whose authority. A regulator asking why an apparent violation was permitted receives only a name and timestamp.

Explicit priorities with provenance, decidable guards, evidence-bearing verdicts, and tracked authorities put the exception and its justification in the rule system. The defeat trace supplies the audit record: the verdict, firing exception, evidence, and source of its priority.

Prior art

Nute’s formulations in the 1980s gave defeasible logic rules ranked by a superiority relation. Governatori, Prakken, and Sartor developed three decades of legal-reasoning theory from that basis. Prakken and Sartor (1997) derive priorities by argument along the two axes this note separates. Catala (Merigoux, Chataing, and Protzenko, ICFP 2021) made base cases and exceptions central to executable statutes, interleaving code with legal text. Its default calculus reports a conflict when two unordered exceptions fire on the same case.

Lex represents the structure as a typed form with Boolean guards, numeric priorities, and a mechanized priority evaluator. It places that form within a logic of authority, legal time, and discretion. This note develops the associated evaluation and analysis: verdicts carry evidence and authority, while acyclicity and confluence checks detect conflicts before case evaluation.

A defeasible rule contains a base verdict, finitely many guarded exceptions, and an acyclic override relation. Its priorities record whether they came from enactment, entailment, or an author’s judgment. A three-valued scan returns the base verdict, a firing exception with evidence, or unknown with the missing fact. Static checks detect cycles and incomparable exceptions that can fire toward different verdicts. A named authority must resolve cycles, balance conflicts between independent rules, and supply priorities that require judgment. The system records those decisions alongside its mechanical results and requests for evidence.