Markdown for LLMs
Defeasible rules and unless
The source Markdown for this article. Copy it into your assistant or download it as a text file.
# 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 ;
```