Skip to content
docs
Arxo ↗

Norm against norm: defeat and priority

For LLMs5 sections

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.

Arxo Law
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;

The general access norm is now defeasible: “as a general rule”, not “always”.

Arxo Law
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.

Arxo Law
rule SuspensionQuarantine defeater {
for p: Person;
when reader_suspended(p);
defeat may_enter_rare_room(p);
}

Let us see what comes out.

Factsmay_enter_rare_room
listed, accreditedTRUE_ONLY
same + ticket suspendedNEITHER

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.

Access to the general reading room is a strict norm that knows no exceptions.

Arxo Law
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:

Arxo Law
rule SuspensionBlanket defeater {
for p: Person;
when reader_suspended(p);
defeat may_enter_reading_room(p);
}
Output
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.

Factsmay_enter_reading_room
listed, ticket suspendedTRUE_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.

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.

Arxo Law
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.

Arxo Law
priority DebtOverAccess {
prefer DebtorRefusal over RareRoomAccess;
reason lex_specialis;
}
What is in the packagemay_enter_rare_room when in debt
without the priority declarationBOTH
with DebtOverAccessFALSE_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.

defeaternorm with a negative head + priority
What it doesremoves supportasserts the opposite
AnswerNEITHERFALSE_ONLY
Whenthe ground of application has lapsedthe 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.