# Defeasible rules and unless

**In one sentence:** `defeasible` records a general norm that has lawful
exceptions; `unless` builds an exception into the rule body, while a
`defeater` moves it into a separate rule that removes another’s support
without asserting anything in return. The author uses them when the source
says “as a rule … except in cases …”.

The language specification treats a defeasible rule as a general norm with
lawful exceptions: an `unless` clause builds the exception into the rule
body, while a separate `defeater` rule removes the general norm’s support
without asserting anything in return. Strict strength without exceptions
lives on the [strict-rules page](/constructs/rule-strict/); resolving
collisions between opposite inferences lives on the
[priority page](/constructs/priority/).

## 1. When to use and when not to

| Instead | Selection rule |
|---|---|
| `strict` vs `defeasible` | No exceptions now or ever — `strict` (nobody defeats it; two strict rules with opposite heads give a preserved Contradiction). At least one conceivable exception — `defeasible`: `unless` on a strict rule is rejected with `LDC-E4110` |
| `unless` vs a separate `defeater` | The exception belongs to the same article and the same variables — `unless` in the body (generated node `<Rule>/unless/N`). The exception lives in another act, is reused by several norms, or needs its own `when` with priority — a separate `defeater` with `defeat` |
| Bare `unless F;` vs contrary `unless F then not p(x);` | “Permission is not issued, but not refused either” — bare: after defeat the answer is Not established, not refuted. “Selling is prohibited” — contrary: it generates a defeasible rule with head `not p(x)` and direct priority over the general one, answer Refuted. Expected Refuted, got Not established, not refuted — the bare form was taken instead of the contrary one |
| `unless`/`defeater` vs `priority` | A proviso removes support; priority resolves a collision of two opposite inferences. Different mechanisms: priority with no opposite heads is opposed to nothing (warning `LDC-E2142`) |
| `defeater` vs a `not` head | A head with explicit negation and priority is written as a `defeasible` rule with `then not p(x)`, not as a defeater: a defeater does not support complements |

## 2. Minimal example

Package `research.constructs.defeasible_unless`: a small registered enterprise is
exempt from planned inspections if there were no violations last year.

```law
rule SmallEnterpriseExempt defeasible {
    for e: Enterprise;
    when small_enterprise(e) and registered(e);
    then exempt_from_planned_inspection(e);
    unless violation_found_last_year(e);
}
```

Case facts: `small_enterprise(alpha)`, `registered(alpha)`.
Query: `evaluate truth(exempt_from_planned_inspection(alpha))`.

Actual engine answer:

```text
law test research.constructs.defeasible_unless: мир research.constructs.defeasible_unless
  ok   [research.constructs.defeasible_unless#authored] tests/01-norm-fires.lawtest / general norm fires without exception
  ok   [research.constructs.defeasible_unless#authored] tests/02-norm-defeated.lawtest / exception fact defeats the norm without proving complement
  ok   [research.constructs.defeasible_unless#authored] tests/02-norm-defeated.lawtest / missing premise keeps the rule silent
итого: 3 проверено, 3 прошли, 0 не прошли, 0 не исполнены; код 0
```

`law engine check` — `check OK`, no warnings. Sensitivity:
adding the fact `violation_found_last_year(alpha)` changes the answer from
Established to Not established, not refuted (the generated defeater
`SmallEnterpriseExempt/unless/0` removed the support, the complement is not
derived); removing `small_enterprise` gives Not established, not refuted — the rule
stays silent, it does not refuse. The example is not vacuous: both
facts are load-bearing.

Nearest wrong outcome: cutting the `unless` clause out of the package — the
violation case answers Established instead of Not established, not refuted (the counterfactual
is held by the second package `research.constructs.standalone_defeater`, where the
same pair is written as a separate defeater and gives the same two answers).

## 3. Example by domain

- **Law:** the carve-out from the scope of ILO Convention No. 138 —
  package `intl.labour.c138` (ILO Convention No. 138, minimum age)
  (`unless hazardous_work(w) then not excludable_work(w)`): the contrary
  form gives a refusal Refuted, not silence (see the
  [corpus forms](/constructs/rule-defeasible-unless/corpus-forms/)).
- **Law:** presumption of innocence with a conviction proviso —
  package `fr.declaration.rights_1789` (Declaration of the Rights of Man and of the Citizen, France, 1789)
  (`unless declared_guilty(who) then not innocent(who)`): the same contrary
  form in the 1789 declaration.
- **Custom:** presumption of honesty with a caught-red-handed proviso —
  package `ru.dal.poslovitsy` (Russian folk sayings)
  (`unless poyman_s_polichnym(ch) then not chist_ot_tatby(ch)`): a folk
  proverb by the same mechanics (exception clauses work outside written law).
- **Law:** exemption of a person from the 1916 requisition —
  package `ru.empire.requisition_1916` (1916 requisition decree, Russian Empire): the package comment records that
  `strict` “would have silently swallowed” the exemptions, so the form
  `unless … then not …` was taken.
- **Teaching case:** package `research.constructs.standalone_defeater` — the same norm, but
  the exception moved into a separate `ViolationRemovesExemption
  defeater` rule with `defeat exempt_from_planned_inspection(e)`; answers
  are the same (Established / Not established, not refuted), the difference is the extension
  point: a new exceptional fact is added as a new defeater, not by editing
  the rule.

## 4. How the engine answers

Table — actual runs of this section’s teaching packages:

| Facts | Question | Answer | Why |
|---|---|---|---|
| `small_enterprise`, `registered` | `exempt_from_planned_inspection` | Established | defeasible rule fired, defeater silent |
| same + `violation_found_last_year` | same | Not established, not refuted | defeater removed support; complement not derived |
| only `registered` | same | Not established, not refuted | premise not established — rule silent |
| separate defeater + both norm facts | same | Established | defeater silent, candidate alive |
| same + violation | same | Not established, not refuted | `ViolationRemovesExemption` removed support |
| `registered_trader`, `stall_requested` | `may_use_stall` | Established | general rule, bare proviso silent |
| same + `stall_reserved` | `may_use_stall` | Not established, not refuted | bare proviso — a generated defeater |
| `registered_trader` | `may_trade_in_winter` | Established | general rule |
| same + `perishable_goods` | `may_trade_in_winter` | Refuted | contrary proviso: a defeasible `not` with direct priority |

Sensitivity of the second package mirrors the first: removing the
`ViolationRemovesExemption` rule from the standalone-defeater package
changes the violation case’s answer from Not established, not refuted to Established — the
outcome is decided by the defeater itself, not by a missing premise (the
package’s first test holds the premise complete in both scenarios).

- A bare body literal reads as established: a fact with Contradiction
  support does not activate an ordinary rule.
- In `proof` — the support of the rule application; after defeat the
  application is marked defeated, the head without support.
- In `why_not` the unestablished conjunct is named explicitly; a rule
  outside its effect window is named a not-applicable candidate, not “false”.
- Not derived is not refuted: Not established, not refuted, not Refuted;
  negative support comes only from an explicit `not`, a negative fact, or
  closure.
- Clashes with a defeater under conditional priority live on the
  [priority page](/constructs/priority/) — with the “no priority” counterfactuals there.

## 5. Common mistakes

1. `unless` on a strict rule — rejection `LDC-E4110`; defeater against
   a strict head — rejection `LDC-E4112` (pitfalls, item 1).
2. The proviso does not bind all head variables — `LDC-E4101` on the name
   `<Rule>/unless/N` (pitfalls, item 2).
3. Expected Refuted, got Not established, not refuted — a bare `unless` was taken instead
   of the contrary one (pitfalls, item 3).
4. A defeater cancelled a valued literal and carried away another’s inference —
   warning `LDC-E2144` (pitfalls, item 4).
5. Priority between same-polarity heads — warning
   `LDC-E2142`: the edge expresses nothing (pitfalls, item 5).
6. Answer Contradiction although “it is clear which norm is special”: speciality is
   not counted by number of conditions — declare `priority` with a
   `reason` (pitfalls, item 6).
7. A `then { a; b; }` block is not lowered: warning `LDC-E1302`, zero
   rules in the compiled output; write separate `then` clauses (pitfalls,
   item 7).

## 6. References

- Neighbour pages: [strict rules](/constructs/rule-strict/) (strict strength),
  [priority](/constructs/priority/) (priority, conditional priority over a defeater),
  [negation](/constructs/negation-and-status/) (negation).
- The defeater-vs-priority tutorial lives in the [tutorials catalogue](/tutorials/defeaters/).
- The pitfalls page lists the diagnostics (`LDC-E4110`, `LDC-E4112`,
  `LDC-E4101`, `LDC-E2144`, `LDC-E2142`, `LDC-E1302`) with wrong forms and fixes.

## 7. Grammar excerpt

Productions of the `rule_decl` family (defeasible strength is the
`defeasible` alternative of `rule_strength`; the `unless` expansion is the
`unless_clause`/`defeat_clause` productions below; strict strength lives on the
[strict-rules page](/constructs/rule-strict/)):

```ebnf
(* DECISION-0183: header parameters and body binders are mutually exclusive. *)
rule_decl               = "rule", identifier, [ rule_parameters ], rule_strength, "{",
                            { rule_item },
                          "}" ;
rule_parameters         = "(", [ rule_parameter, { ",", rule_parameter }, [ "," ] ], ")" ;
rule_parameter          = identifier, { ",", identifier }, ":", type_ref ;
rule_strength           = "strict" | "defeasible" | "defeater" ;

(* Errata E-0114: кардинальности rule_item. `when` — любое число, тело
   правила есть их конъюнкция в порядке записи (§94); `then` — любое число,
   каждая клауза даёт своё правило `<rule>/head/N` (§99); `scope`,
   `effective`, `defeat` — не более одной, повтор — LDC-E1329. *)
rule_item               = binder
                        | rule_local
                        | scope_clause
                        | effective_clause
                        | governs_clause
                        | when_clause
                        | then_clause
                        | defeat_clause
                        | unless_clause
                        | source_anchor_item
                        | "interpretation", reference_list, ";"
                        | label_item
                        | metadata_item ;

(* Errata E-0070: хвост `in expression` у биндера снят — сужение домена
   пишется конъюнктом в `when`; парсер хвост не разбирал никогда. *)
binder                  = "for", identifier, { ",", identifier },
                          ":", type_ref, ";" ;
rule_local              = "let", identifier, ":", type_ref, "=", expression, ";" ;
scope_clause            = "scope", formula, ";" ;
effective_clause        = "effective", interval_literal, ";" ;
governs_clause          = "governs", identifier, interval_literal, ";" ;
when_clause             = "when", formula, ";" ;
(* Errata E-0082: завершающая `;` у одиночного вывода необязательна —
   `us.declaration`, `eng.leviathan_1651` пишут `then duty D { … } }`, и
   `check` чист. *)
then_clause             = "then", ( conclusion, [ ";" ]
                                   | "{", { conclusion, ";" }, "}" ) ;
defeat_clause           = "defeat", proposition, ";" ;
unless_clause           = "unless", [ identifier, "when" ], formula, [ "then", proposition ], ";" ;

conclusion              = proposition
                        | norm_conclusion ;
```