Definitions, classifications, constraints, and fictions

A rule says “hence follows”. But an act has other ways of speaking: “a researcher is one who…”, “a debtor is deemed…”, “an issued document must have a return term”, “a letter counts as received”. The first and second are a definition and a classification; they derive. The third is a constraint; it derives nothing but checks. The fourth is a fiction: an institutional fact by the act’s say-so, not by observation. The corpus holds 70 definitions, 244 constraints, and 18 fictions (measured 05.09.2026), and the costliest mistake on this page is confusing a necessary condition with a deriving rule.

Arxo Law

language "law.core" version "0.2";
package tutorial.archive version "0.9.0";
namespace "urn:law:tutorial:archive";

entity Person;

relation in_researcher_registry(p: Person) kind institutional;
relation accredited(p: Person) kind institutional;
relation overdue_item(p: Person) kind empirical;
relation debt_settled(p: Person) kind empirical;
relation document_lent(p: Person) kind empirical;
relation due_date_set(p: Person) kind empirical;
relation notice_sent_to_registered_address(p: Person, on: Date) kind empirical { key(p); }
relation notified(p: Person, on: Date) kind institutional;

A definition in both directions

“A researcher is a reader listed in the registry and holding a valid accreditation.” The exact mode gives both halves: the sufficient one — a strict rule “registry and accreditation, hence researcher” — and the necessary one — a constraint “researcher, hence registry and accreditation”.

Arxo Law

definition Researcher(p: Person) exact {
    when in_researcher_registry(p) and accredited(p);
}

The definition name is the predicate: no separate relation Researcher needs declaring; the compiler synthesises it from the signature. The body has no for binder: the definition’s parameters are its only variables, and there is nowhere to introduce an auxiliary name.

Facts	Researcher	Document
registry, accreditation	TRUE_ONLY	—
registry	NEITHER	—
status fed as a fact, registry, accreditation refuted	TRUE_ONLY	issue CONSTRAINT_VIOLATED
status fed as a fact, registry	TRUE_ONLY	—

The first row is the test from this page, byte for byte:

Arxo Law

test "определение: реестр и аккредитация — исследователь" {
    given {
        context {
            decision_time @2026-03-01T09:00:00+05:00;
            knowledge_time @2026-03-01T09:00:00+05:00;
            legal_time @2026-03-01;
            timezone "Asia/Almaty";
        }
        assert in_researcher_registry(entity_ref("urn:tutorial:ivanova")) {
            id "assert-reg";
            origin case_input;
        }
        assert accredited(entity_ref("urn:tutorial:ivanova")) {
            id "assert-acc";
            origin case_input;
        }
    }
    evaluate truth(Researcher(entity_ref("urn:tutorial:ivanova")));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;
}

The test name reads: “Definition: registry and accreditation — researcher.”

The third row is the point of the necessary half. Someone wrote into the case “Ivanova is a researcher”, while the committee revoked the accreditation. The definition does not apply contraposition: the status did not become FALSE_ONLY; it stayed an established case fact. Instead the constraint fired, and the document carries a CONSTRAINT_VIOLATED finding. A necessary condition checks consistency rather than deriving a denial; if a negative qualification is needed, it is written as a separate rule with a not head. The fourth row: nothing is known about accreditation — the requirement is NEITHER, the constraint verdict UNDETERMINED, no issue.

The necessary mode gives the necessary constraint alone. Use exact when both the strict deriving rule and the necessary constraint are wanted. For a one-way rule, write an ordinary strict rule explicitly.

Classification with exceptions

A definition knows no exceptions: exact is strict in both directions. When qualification is “as a general rule”, a classification with strength is needed.

Arxo Law

classification DebtorReader(p: Person) defeasible {
    when overdue_item(p);
}

rule SettledDebtIsNotDebt defeater {
    for p: Person;
    when debt_settled(p);
    defeat DebtorReader(p);
}

Facts	DebtorReader
overdue	TRUE_ONLY
overdue, debt settled	NEITHER

A classification lowers into an ordinary rule of the declared strength, and the defeater from the defeat tutorial works against it as against any defeasible conclusion. A classification cannot carry the defeater strength: it either supports the class or is a separate targeted exception. And the compiler rejects a defeater against an exact definition: a strict conclusion has no defeasible support.

A constraint that derives nothing

“An issued document must have a return term.” The temptation to record this as a rule “issued, hence a term exists” is strong, and it is wrong: a rule would establish a term nobody assigned. A constraint checks rather than derives.

Arxo Law

constraint LoanNeedsDueDate {
    for p: Person;
    when document_lent(p);
    require due_date_set(p);
    severity error;
    message "У выданного документа обязан быть срок возврата.";
}

The message reads: “An issued document must have a return term.”

Facts	Verdict	Document
issued, term assigned	SATISFIED	—
issued, term refuted	VIOLATED	issue CONSTRAINT_VIOLATED
issued	UNDETERMINED	—
not issued	did not fire	—

A constraint is computed at every query after all rule strata, and its result is a separate document item of the CONSTRAINT kind, not a support of anything. It takes no part in defeat and priorities, and by itself creates no violation or sanction: if the act ties non-observance to a consequence, the consequence is written as an ordinary rule from established facts — like the fine in the duty tutorial. UNDETERMINED yields no issue: “the term is not stated in the case” and “there is no term” are different things, and the constraint does not pass the first off as the second. The test guards the verdict by observing issue(CONSTRAINT_VIOLATED).

You saw the constraint from a real article — the choice of one of two benefits — in the article-text tutorial; here the same construction on a teaching act, with three outcomes instead of one.

Fiction

“A letter sent to the registry address counts as received.” Nobody observed the receipt; the act recognises it. This is a fiction, and its head is institutional by construction.

Arxo Law

fiction DeemedNotified strict {
    for p: Person;
    for on: Date;
    when notice_sent_to_registered_address(p, on);
    deem notified(p, on);
}

Facts	notified
letter sent on 10 February	TRUE_ONLY on 10 February

A fiction’s strength is mandatory, and the core does not supply it: strict is “counts always”, defeasible is “counts unless proven otherwise”, and the second is defeated by a defeater like any defeasible rule. Declare the head empirical and the compiler warns: the observed is established by case fact, not by recognition:

Output

warning LDC-E1309: fiction "DeemedNotified": голова над `empirical`-отношением
"notified" (§147) — наблюдаемое устанавливают фактом дела, а не признанием

The warning reads: ‘fiction “DeemedNotified”: a head over the empirical relation “notified” — the observed is established by case fact, not by recognition’.

It is a warning, and check stays green; the broken variant still compiles and the code must sound in the warnings — read them.

How to choose the construction

The act says	Construction	Derives?
“X is one who…” and back	definition … exact	yes, and checks the converse
“X is one who…” with exceptions	classification … defeasible	yes, defeasibly
“X only if…”	definition … necessary or constraint	no, checks
“with X there must be Y”	constraint	no, checks
“X counts as Y”	fiction	yes, an institutional fact

The question that decides the choice: may the system establish this by itself? If the act merely requires it to be so — a constraint. If the act makes it so by its word — a fiction or a rule.

Compiler refusals

A definition body has no binder, and a free name is an error, not an implied variable:

Output

error LDC-E1322: имя "q" в теле `definition` §151 не является ни её
параметром, ни объявленным символом пакета — это свободная переменная

The diagnostic reads: ‘name “q” in a definition body is neither its parameter nor a declared package symbol — it is a free variable’.

A constraint is range-restricted too: require without a binding when is rejected:

Output

error LDC-E4101: constraint "LoanNeedsDueDate": require использует
несвязанные переменные [p] (§190)

The diagnostic reads: ‘constraint “LoanNeedsDueDate”: require uses unbound variables [p]’.

Mandatory parts and admissible strengths:

Output

error LDC-E0201: constraint LoanNeedsDueDate без require (§139)
error LDC-E0201: сила фикции обязательна: strict | defeasible (§147)
error LDC-E0201: `defeater` не может быть силой классификации (§148)

The diagnostics read: “‘constraint LoanNeedsDueDate’ without require”; “‘a fiction’s strength is mandatory: strict | defeasible’”; “‘defeater cannot be a classification’s strength’”.

And a defeater against a definition:

Output

error LDC-E4112: DEFEATER_WITHOUT_CANDIDATE: defeater "SettledDebtIsNotDebt"
атакует positive-голову "Researcher", но у неё нет defeasible-продюсера

The diagnostic reads: ‘…attacks the positive head “Researcher” but it has no defeasible producer’.

All six refusals belong to the language.

Next

Definitions and classifications qualify; the next page is about presumptions: when the act orders something to count as established until proven otherwise, and how a rebuttal returns the conclusion.

The exercise for this page is /tutorials/exercise-definitions/.