Defeasible rules and unless

For LLMs7 sections

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; resolving collisions between opposite inferences lives on the priority page.

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.

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:

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).
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 — with the “no priority” counterfactuals there.

5. Common mistakes

unless on a strict rule — rejection LDC-E4110; defeater against a strict head — rejection LDC-E4112 (pitfalls, item 1).
The proviso does not bind all head variables — LDC-E4101 on the name <Rule>/unless/N (pitfalls, item 2).
Expected Refuted, got Not established, not refuted — a bare unless was taken instead of the contrary one (pitfalls, item 3).
A defeater cancelled a valued literal and carried away another’s inference — warning LDC-E2144 (pitfalls, item 4).
Priority between same-polarity heads — warning LDC-E2142: the edge expresses nothing (pitfalls, item 5).
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).
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 (strict strength), priority (priority, conditional priority over a defeater), negation (negation).
The defeater-vs-priority tutorial lives in the tutorials catalogue.
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

Show syntax reference

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):

(* 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 ;

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.