Markdown for LLMs

Definitions, classifications, constraints, and fictions

The source Markdown for this article. Copy it into your assistant or download it as a text file.

# 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.

```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".

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

```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.

```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.

```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.

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

```text
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:

```text
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:

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

The diagnostic reads: 'constraint "LoanNeedsDueDate": `require` uses unbound variables [p]'.

Mandatory parts and admissible strengths:

```text
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:

```text
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/](/tutorials/exercise-definitions/).