Norm against norm: defeat and priority
The four-states tutorial ended in debt: FALSE_ONLY for access could not
be obtained. A strict rule can do one thing: derive its own head. The
negative head from the negation tutorial can
refuse, but it too answers only for itself: next to a general norm that
permits, the refusal yields BOTH. Real law is arranged differently:
a general norm may have an exception, the exception its own exception,
and the winner is not what was written later but what is stronger on
a recognised ground.
This is layer L1: the layer view of the page will say L1 and
explain exactly what for. The core offers two different tools here, and
confusing them is costly.
language "law.core" version "0.2";package tutorial.archive version "0.3.0";namespace "urn:law:tutorial:archive";
entity Person;
relation in_researcher_registry(p: Person) kind institutional;relation accredited(p: Person) kind institutional;relation reader_suspended(p: Person) kind institutional;relation has_outstanding_debt(p: Person) kind institutional;relation may_enter_rare_room(p: Person) kind institutional;relation may_enter_reading_room(p: Person) kind institutional;First tool: defeat
Section titled “First tool: defeat”The general access norm is now defeasible: “as a general rule”, not
“always”.
rule RareRoomAccess defeasible { for p: Person; when in_researcher_registry(p) and accredited(p); then may_enter_rare_room(p);}A suspended reader ticket removes access. This is written as a rule with
a defeat clause: it derives nothing of its own but takes away the
support of someone else’s conclusion.
rule SuspensionQuarantine defeater { for p: Person; when reader_suspended(p); defeat may_enter_rare_room(p);}Let us see what comes out.
| Facts | may_enter_rare_room |
|---|---|
| listed, accredited | TRUE_ONLY |
| same + ticket suspended | NEITHER |
NEITHER, not FALSE_ONLY, and that is the point of defeat.
A suspended ticket does not mean the reader is barred from the room: it
means the ground for access has lapsed. The difference is not
pedantry: in the first case the archive must refuse, in the second it
must look into it. A defeater removes the support and stays silent about
the opposite.
A strict norm cannot be defeated
Section titled “A strict norm cannot be defeated”Access to the general reading room is a strict norm that knows no exceptions.
rule GeneralReadingRoom strict { for p: Person; when in_researcher_registry(p); then may_enter_reading_room(p);}The temptation to write a defeater against it is understandable, and it runs into a compiler refusal. Here is the block that is not on this page and cannot be:
rule SuspensionBlanket defeater { for p: Person; when reader_suspended(p); defeat may_enter_reading_room(p);}error LDC-E4112: DEFEATER_WITHOUT_CANDIDATE: defeater "SuspensionBlanket"атакует positive-голову "may_enter_reading_room", но у неё нетdefeasible-продюсера (§107.3; DECISION-0111 §2.1)The diagnostic reads: “…attacks the positive head … but it has no defeasible producer”.
The reason lies in what a defeater does at all. It asserts nothing of
its own but removes the support of a defeasible conclusion.
may_enter_reading_room has no defeasible support: the only producer of
the head is strict, and a strict conclusion and an empirical assertion
do not become defeat candidates. The defeater has nothing
to defeat, and the rule is not “powerless” but meaningless.
Such a block used to compile and silently do nothing. That turned out to be the worst option: the norm looked written, the author counted the exception as handled, while the runtime answer was the same as without it. Now a defeater must have an ordinary defeasible producer of its head and polarity, otherwise the source is rejected statically.
This lesson is load-bearing: redirect the working
defeater of the previous section at the strict head, and
the compiler must answer exactly LDC-E4112. Should the compiler stop
refusing, the page that tells about the refusal will fall.
The strict norm itself knows no defeat: with a suspended ticket,
may_enter_reading_room stays TRUE_ONLY.
| Facts | may_enter_reading_room |
|---|---|
| listed, ticket suspended | TRUE_ONLY |
The practical conclusion: strict is a declaration that “there are no
exceptions and will be none”. It is placed deliberately, not by default,
and now the price of a mistake shows at check, not at runtime.
Second tool: priority
Section titled “Second tool: priority”Defeat removes support. But an exception norm often has content of its own: it does not merely cancel access, it refuses. Such a norm is written as an ordinary rule with a negative head.
rule DebtorRefusal defeasible { for p: Person; when has_outstanding_debt(p); then not may_enter_rare_room(p);}Now a reader in debt gets two conclusions at once: the general norm
grants access, the special one refuses. The core keeps such
a conflict rather than resolving it by itself: the answer is BOTH,
exactly as in the four-states tutorial.
For a winner to emerge, the ground of victory is declared explicitly.
priority DebtOverAccess { prefer DebtorRefusal over RareRoomAccess; reason lex_specialis;}| What is in the package | may_enter_rare_room when in debt |
|---|---|
| without the priority declaration | BOTH |
with DebtOverAccess | FALSE_ONLY |
Here is the promised FALSE_ONLY. Both rows of the table hold:
as is, and with the priority block cut out.
The reason field matters here. lex_specialis is not a comment: it is
the named legal ground on which the special norm defeats the general
one. Priority without a ground is arbitrariness written into code; with
a ground it is verifiable and contestable.
How to choose the tool
Section titled “How to choose the tool”defeater | norm with a negative head + priority | |
|---|---|---|
| What it does | removes support | asserts the opposite |
| Answer | NEITHER | FALSE_ONLY |
| When | the ground of application has lapsed | the norm directly forbids |
The question that decides the choice sounds like this: must the authority refuse, or must it look into it? A suspended ticket requires looking into it; an unsettled debt requires refusal.
All NEITHERs in these tutorials came from incomplete input. But there
is incompleteness that law closes by itself: a registry declared
complete turns a missing entry into a full negative fact. That is the
closed world, the next tutorial.
The exercise for this page is /tutorials/exercise-defeaters/.
Documentation for Arxo. Writings — blog.arxo.io.
Anonymous visit counts on stats.arxo.io, no cookies.