The shape of a rule

A legal rule, read carefully, is never a bare command. “You must file annual returns.” That looks simple. 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 of these exceptions can itself be excepted. The registrar’s revocation of the extension might itself be subject to appeal. The appeal process might be stayed by judicial review.

This is the natural consequence of a legal system that must be simultaneously general (applying to all companies) and fair (accommodating the infinite variety of actual situations). The tension between generality and fairness is resolved by defeasibility: a rule states the general case; exceptions carve out the specific ones. When practicing lawyers read a statute, they immediately look for the exceptions, the carve-outs, the schedules, the subordinate legislation that modifies the primary rule. The question is whether a machine can do the same.

What a defeasible rule is

Fix the object before the algorithms. A defeasible rule is three things: a base verdict, stating what holds in the general case; a finite set of exceptions, each pairing a guard – a predicate over the facts of a case – with the verdict that holds when the exception prevails; and a finite override relation between exceptions, recording which prevails when both fire. The rule is well-formed when the override relation is acyclic. The transitive closure of an acyclic override relation is a strict partial order on the exceptions – the exception order. Two exceptions are comparable when one overrides the other, directly or through a chain of overrides, and incomparable when neither does. An implementation assigns numeric priorities. An assignment that respects the order and gives no two exceptions the same number induces a linear extension of the order, every linear extension arises this way, and every such assignment is a faithful encoding. Respecting the order permits a tie only between incomparable exceptions, and a tie encodes no ordering between them, so the evaluator must supply one. A tied assignment is faithful for a pair the confluence check below clears, since no ordering of the two can then change the verdict; on a pair the check flags, it leaves the case to the evaluator’s tiebreak, taken up there. The numbers are an evaluation device. The rule is the order.

Well-formedness is a property to check, and checking it is the first of two static checks developed below. A structure whose overrides form a cycle is representable – it may faithfully record what overlapping enactments say – and it is not evaluable. The distinction between representing law and evaluating it runs through everything that follows.

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.” This fails for legal reasoning: a single constitutional provision overrides a thousand statutes. What decides that case is rank – lex superior derogat legi inferiori, the higher source prevails – and rank attaches to the sources, whatever the count.

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

Temporal ordering. The later rule wins – lex posterior derogat legi priori. The principle is real, and it answers a different question. A general statute enacted in 2025 does not thereby override a specific statute of 2020 that addresses precisely the situation at hand: recency and specificity are independent measurements. Temporal succession belongs on its own axis – which rules are in force, and when – handled by temporal stratification, the subject of a companion note, and independent of the ordering of exceptions within a rule.

Priority ordering. Exceptions stand in an explicit override relation, and among the exceptions that apply, the one the order places highest prevails. This models how legal systems resolve conflicts inside a rule, and the rest of this note develops it.

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 write precedence into their own text: “subject to subsection (4A),” “notwithstanding any other provision,” “regardless of status.” The example above is this case. Neither exception is more specific than the other – a non-profit with $5 million in revenue falls under A alone, a for-profit with $15 million under B alone, so neither guard entails the other and specificity is silent between them. What decides entity X is the enacted phrase “regardless of status”: the legislature ranked B over A when it wrote B. Rank enters the same way. Where conflicting provisions issue from sources at different levels – constitution, statute, subordinate regulation – lex superior supplies the override before any reading of the guards. In both forms the encoder’s priority transcribes an ordering stated by the law.

Specificity computes it. Lex specialis derogat legi generali: the more specific rule overrides the more general. The principle has exact content 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 one, and the entailment ranks the narrower exception above it, with no precedence clause required. For guards built from set memberships, threshold comparisons, and boolean conditions – the decidable classes described below – entailment between guards is itself decidable, so this source of priority is computable. It also explains why an exception outranks its base rule at all: the base rule applies to everyone, so every exception’s guard entails it. The argument for the principle is legislative effectiveness. If a specific exception did not prevail over the general rule it was enacted to qualify, enacting it would have changed nothing; a legislature that cannot make exceptions effective cannot refine its own law, and the system freezes at the level of its most general principles.

Someone owns it. When neither enacted text nor entailment decides – two incomparable exceptions, no precedence clause, guards that merely overlap – a priority is an act of interpretation. The system records it as one: assigned by a named author, attributed, open to challenge. A priority therefore carries its provenance – transcribed from the law, computed from entailment, or assigned by an author – and the record says which.

The defeat algorithm

Given a well-formed rule and a case, evaluation eliminates the defeasibility. A guard evaluates against the evidence supplied for the case, with three outcomes: true, false, or unknown – the facts present do not decide the guard, whose value turns on a fact that is missing or an event that has not yet occurred. Guards are decidable predicates (next section), so unknown records missing evidence and nothing else; a guard never fails to halt.

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.

The order of the scan carries the logic. A true guard above an unknown one settles the case – the higher exception fires whichever way the missing fact resolves. An unknown guard above a true one leaves the answer open – which exception fires turns on evidence the system does not hold. The answer is the verdict together with the exception that fired and the evidence that fired it, and on that object the scan is exact: under a given extension it returns an answer exactly when every way of supplying the missing facts yields that answer, and unknown exactly when which exception fires turns on a fact still missing. On the bare verdict the scan is exact where every guard is decided, sound where some are not – a verdict it returns holds, in that extension, however the missing facts are supplied – and conservative: a case reported unknown may already have its verdict fixed. Within one extension this happens whenever the open exceptions above the first true guard all carry that guard’s verdict, or, when no guard below is true, all carry the base verdict, and otherwise only where two open guards share a missing fact; across extensions, when the rule passes the confluence check below, another extension may place a true guard above the open one and return the verdict outright. The scan looks for neither. It stops at the highest open guard and requests that fact, because what it certifies is the verdict with its justification, and the justification is what the missing fact decides.

This is the defeat eliminator: it takes a rule with exceptions and eliminates the defeasibility, returning the base verdict, a firing exception, or an admission of ignorance. Unknown is an outcome in its own right, the system’s report of its own epistemic state, and the report names the guard and the missing fact – which is precisely a request for the evidence that would settle the case. The companion paper Lex, a typed language for jurisdictional rules, keeps guards total – Boolean predicates over a typed evidence record – and its verdict vocabulary carries the unsettled case as an explicit element, Pending, of its five-verdict chain. The three-valued guard and the pending verdict are one discipline at two layers: missing evidence becomes an explicit outcome.

Guards must be decidable

For the algorithm to work, the guards on exceptions – the conditions that determine whether an exception applies – 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” is not, nor is “reasonable person,” nor “best interests of the company”: these are judgment-dependent, and a system that pretended to decide them mechanically would be dangerous. Decidability also pins down the third outcome above: with non-termination excluded, unknown has a single source, absent evidence.

But many legal questions are decidable. 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? These are the guards a machine can evaluate, and they cover many of the compliance questions institutions face daily. They also analyze well: for guards built from these forms, entailment and joint satisfiability are decidable, and the static checks of the next section rest on exactly that.

The evidence from guard evaluation is the formal justification for the answer. When the system selects an exception because the entity’s revenue exceeded $10 million, the evidence – the specific revenue figure, the threshold, the comparison – is part of the answer. An auditor can trace from the conclusion to the specific fact that produced it. This is auditability by construction.

Two static checks

The exception order earns its keep before any case arrives. Two checks run at analysis time, on the rule alone.

Acyclicity. The first check is well-formedness itself: the override relation must contain no cycle. Nothing prevents a cycle from arising in the law. Exception A is enacted to override B, B to override C, C to override A – each pairwise override deliberate, introduced by an amendment or asserted by an authority that never saw the composition. A machine handed such a structure has nothing to evaluate, because every scan order contradicts some override. The structure is still worth holding: it is a faithful description of what the enactments say, and the check marks it as data awaiting resolution. Resolution is a legal act – a judge, a regulator, or an amendment breaks the cycle – and the record tracks who resolved it, under what authority, with what reasoning. The resolution becomes part of the rule’s history.

Confluence. The second check makes numeric priorities honest. A linear extension orders every incomparable pair, different extensions order some pairs differently, and the check asks whether the verdict can depend on that choice. For every incomparable pair of exceptions, require one of two things: the guards are jointly unsatisfiable – no case fires both – or the two verdicts agree. Both conditions are decidable for the guard classes above. A rule that passes is confluent, in this exact sense: on a case whose guards are all decided, every linear extension returns the same verdict, and where evidence is missing, two extensions can differ only in precision – one may report unknown where another already sees the answer – never in the verdict. The decided-case half has a short argument: returning the base verdict requires every guard false, which no extension can contradict; and if two extensions fire different exceptions on the same case, each scan found its exception true with everything above it false, so each exception sits below the other in the opposite extension – the pair is incomparable with both guards true, and the check forces their verdicts to agree. A pair that fails the check is a genuine conflict, surfaced before any case arrives: some possible case fires both exceptions toward different verdicts, and the rule under-determines it. The repair is an override from one of the three sources above – enacted, computed, or owned. The check is conservative, flagging a pair even when a higher exception happens to fire on every case the pair shares; for a legal instrument, conservative is the correct direction.

A deterministic evaluator must still return something when a flagged pair is left unrepaired. Lex’s mechanized evaluator breaks ties between equal numeric priorities by source position: the exception written earlier wins. Source position is an encoding accident with no legal meaning, and that is the argument for the check: until an override with an owner is added, a flagged pair’s shared cases are decided by an accident of transcription, and the check is what makes the accident visible.

One further consequence of an explicit structure: it can be content-addressed. The rule – base verdict, exceptions, override relation, authorities – has a canonical encoding, and the hash of that encoding names the rule. Two rules with the same canonical structure receive the same identifier, wherever and by whomever they were encoded, which makes de-duplication and cross-reference exact: a corpus recognizes that two packs carry the identical rule, and a citation pins the exact rule it relies on. The identity is identity of canonical form – guards that mean the same thing in different syntax hash apart – and for audit and reference, sameness of form is precisely the checkable thing. A companion note on content-addressed identity develops the scheme.

When independent rules conflict

Everything above concerns exceptions within a single rule. What happens when two different rules contradict each other?

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 exactly as far as the override relation extends, and here the relation is silent: no enacted text ranks the two rules, the sources stand at the same rank, neither guard entails the other, and no common authority has assigned a priority. Priorities between conflicting rules can themselves be derived by argument – Prakken and Sartor (1997) formalize the derivation, with the interaction of specificity and recency as the central case – but a derived priority is an interpretation, and an interpretation needs an owner. The position taken here is to keep the override relation explicit and to treat every extension of it as new legal content, entering through the same three sources as any other priority.

Where the relation is silent, the machine stops and balancing begins. Balancing means identifying the principles at stake (financial transparency against medical privacy), citing precedents where similar conflicts were resolved, and producing a reasoned verdict. It is the formal counterpart of judicial reasoning. The system structures the record – the principles stated, the precedents cited, the rationale recorded, the deciding authority named – and carries the outcome forward like any other authority’s act. Lex draws the boundary in its type system: where a rule requires a determination no mechanical predicate fixes, it carries a typed discretion hole naming the decision required and the authority entitled to make it; evaluation proceeds to the hole and stops, and the decision enters as a signed, revocable attestation binding the signer, the exact value, and the rule version.

The division of labor is exact. Given the override relation, resolution is mechanical: the scan of the defeat algorithm. Extending the relation is judgment: an act with an owner, an authority, and a rationale. A system that conflates the two fails in one of two ways: it demands balancing where priority already decides, and clear cases stall; or it applies mechanical priority where judgment is required, and hard cases are decided by nobody.

Why this matters for computation

A computer system that executes law must implement defeasibility, because law is defeasible. A system that treats legal rules as flat conditionals – if X then Y – produces wrong answers whenever an exception applies.

Compliance software that hardcodes rules as boolean checks meets this structure with the manual override flag: the rule says one thing, reality requires another, and a human bridges the gap by clicking a button. The flag is a confession that the system’s model of law is thinner than the law. Consider what it records: that a departure happened, who clicked, and when. The legal basis of the departure lives outside the system – which exception justified it, on what evidence, under whose authority. When a regulator asks why a transaction was processed despite an apparent violation, a name and a timestamp is the whole of the answer.

A system that implements defeasibility – explicit priorities with provenance, decidable guards, evidence-bearing verdicts, tracked authorities – has no gap for a button to bridge. The exception is part of the rule. The resolution is part of the proof. The authority is part of the record. The trace of the defeat scan – the verdict, the exception that fired, the evidence that fired it, the source of the priority that ranked it – is the audit record.

Prior art

The ingredients are established. Defeasible logic has carried rules ranked by a superiority relation since Nute’s formulations in the 1980s, and Governatori, Prakken, and Sartor built three decades of legal-reasoning theory on that base; Prakken and Sartor (1997) in particular derive priorities by argument along the two axes this note keeps separate. Catala (Merigoux, Chataing, and Protzenko, ICFP 2021) made base-case-plus-exceptions the core of a language for executable statutes, with code interleaved into the legal text it formalizes; its default calculus signals a conflict when two exceptions, neither above the other, fire on the same case. Lex, the companion paper, carries the structure as a typed language form – Boolean guards, explicit numeric priorities, a mechanized priority evaluator – inside a full logic of authority, legal time, and discretion. What this note isolates is the working discipline the structure supports: verdicts that carry their evidence and their authority, and the two checks – acyclicity and confluence – run over the exception order before any case is decided, moving conflict detection from evaluation time to analysis time.

A defeasible rule is a small formal object: a base verdict, finitely many guarded exceptions, an acyclic override relation. Its priorities carry provenance – enacted, computed from entailment, or owned by an author. Its evaluation is a three-valued scan returning the base verdict, a firing exception with its evidence, or unknown with the fact that would settle the case. Its defects are caught before cases arrive: cycles, and incomparable exceptions that can fire together toward different verdicts. Everything past its edge – the cycle to break, the conflict between independent rules to balance, the priority only judgment supplies – is assigned to a named authority and recorded. The machine resolves what the law has ordered, reports what the evidence leaves open, and keeps the record of every judgment it could not make.