# Definitions

> Updated 3 October 2026: `concept`, `except_when`, `claim`, `definition … sufficient`, and `default` strength have been removed, together with their special deprecation diagnostic. References below to the former behavior and corpus sources are historical. New source uses `relation`, `unless`, `duty`, a strict rule, and `defeasible`.

**In one sentence:** `definition` names a qualification — “who (what) counts
as …”: the sufficient half infers the concept from conditions as a strict
rule, the necessary half restricts the concept by a condition as a
constraint, `exact` does both at once. The author uses a definition when a
norm needs a name for repeated application, and the explanation must say “by
definition”, not “by rule”.

The language specification treats a definition as a named qualification:
the sufficient half infers the concept from conditions like a strict rule,
the necessary half restricts the concept like a constraint, and `exact`
does both at once. Definitions are chosen when a norm needs a reusable name
whose explanation reads “by definition”, not “by rule”.

## 1. When to use and when not to

| Instead | Selection rule |
|---|---|
| `definition … exact` vs `rule … strict` | A qualification with a name, referenced by other norms and explanations, is a definition: generated nodes carry the `was_derived_from` edge, and verbalization may say “by definition”. A one-off inference without a name is a strict rule. The sufficient direction derives the same predicate; `exact` additionally checks the necessary condition through a constraint and records its origin in the proof graph |
| `exact` vs `necessary` | A full two-way link (“if and only if”) — `exact`: a sufficient strict rule plus a necessary constraint. Only a restriction (“the concept requires the condition”, with no right to infer the concept from the condition) — `necessary`: such a half infers nothing on its own |
| `definition` vs `classification … strict` | Both can infer a class from conditions; `definition … exact` also applies the necessary constraint, while strict classification is one-way. Choose by whether you need an equivalence or a classification rule |
| `definition` vs a `defeasible` norm | If the qualification has ordinary exceptions or a presumptive character, a definition will not do: it has no hidden strength. Then `classification … defeasible` or separate defeasible rules |

## 2. Minimal example

Package `research.definition.exact_minor`: a minor is a person under eighteen. An
important formality: a separate `relation minor…` next to the definition is
forbidden — the compiler synthesizes the relation itself, and redeclaration
gives `LDC-E1201` (see the [definition pitfalls](/constructs/definition/pitfalls/), item 1):

```law
entity Person {
    label ru-KZ official "Человек";
}
relation under_eighteen(p: Person) kind institutional {
    label ru-KZ official "младше восемнадцати лет";
}
definition minor(p: Person) exact {
    label ru-KZ official "Несовершеннолетний: лицо младше восемнадцати лет";
    when under_eighteen(p);
}
```

Case facts: `under_eighteen(urn:case:research:definition:anna)` with
`origin case_input`. Query: `evaluate truth(minor(...))`.

Actual engine answer:

```text
law test research.definition.exact_minor: мир research.definition.exact_minor
  ok   [research.definition.exact_minor#authored] tests/01-minor-holds.lawtest / urn:query:research-definition-01
  ok   [research.definition.exact_minor#authored] tests/02-minor-absent.lawtest / urn:query:research-definition-02
итого: 2 проверено, 2 прошли, 0 не прошли, 0 не исполнены; код 0
```

`law engine check` — `check OK`, no warnings. Sensitivity:
without the `under_eighteen` fact the answer is Not established, not refuted
(the minor-absent test) — the example is not vacuous.

Second package `research.definition.strict_classification`: the neighbouring form
`classification driver … strict` with condition `holds_licence(p)`.
Actual answer: condition present — Established
(the driver-holds test), condition absent — Not established, not refuted
(the driver-absent test), `law test` — 2/2. Observed behaviour
matches the definition — and that is the finding: the choice between forms
is decided by intent and node provenance, not by outcome.

Nearest wrong outcome: expecting contraposition from `exact` — “since of
full age, therefore not under eighteen” as a separate inference. A
`definition` does not apply contraposition: the reverse direction
becomes an inference only when the author writes a separate rule with a
literal head; the needed refusal is set by a separate `rule … then not …`.

## 3. Example by domain

- **Science:** package `nasem.reproducibility` (NASEM reproducibility definitions, US science) —
  `pub definition … exact` with three conjuncts and a source anchor:
  reproducibility as the same data, the same code, the same analysis
  conditions (see the [corpus forms](/constructs/definition/corpus-forms/)).
- **Standard:** package `w3c.prov` (W3C PROV, provenance standard) —
  `pub definition Communication … exact` over a same-named relation:
  the definition names, the relation records the fact.
- **Law:** the Civil Code of Kazakhstan articles on persons define
  qualifications as strict rules, not as
  `definition` — see the breakdown in the [corpus forms](/constructs/definition/corpus-forms/): the corpus
  leans to rules where the qualification is woven into the article.
- **Teaching case:** package `research.definition.strict_classification` — classification as a
  neighbour: same observed behaviour, different declared intent.

## 4. How the engine answers

Table — actual runs of this section’s teaching packages:

| Facts | Question | Answer | Why |
|---|---|---|---|
| `under_eighteen(anna)` | `minor(anna)` | Established | sufficient half of `exact` fired as a strict rule |
| no facts | `minor(boris)` | Not established, not refuted | condition not established |
| `holds_licence(vera)` | `driver(vera)` | Established | strict classification infers the concept |
| no facts | `driver(gena)` | Not established, not refuted | condition not established |

- Generated nodes carry the provenance edge `was_derived_from` to the
  concept symbol with attributes `declaration: "definition"`, `mode`,
  `part` (and `alternative` on a split sufficient half).
  The edge is inside `contentHash` and `artifactHash` but
  outside `theoryHash`: same theory as a handwritten rule, with a
  “by definition” explanation.
- The necessary half infers nothing on its own: `necessary` without a
  sufficient part is only a constraint (necessary is “concept requires
  condition”, not a rule). Which status a question about the concept
  answers with the condition established but no sufficient half was not
  checked on this section’s teaching packages (both examples are `exact` and strict
  classification); the Not established, not refuted claim here is inferred from the language description, not a
  run fact.
- For one-way inference, write a strict `rule`. Use `definition … exact`
  when you also need the necessary constraint and definition provenance.
- On `why_not` of an unfired definition nothing was checked on these
  teaching packages: by expansion design (the sufficient half is a
  strict rule) naming the unestablished condition is expected, as for an
  ordinary rule, but no run confirmed it.

Note on body form: unlike a rule, a definition has no `for` binders — the
parameters go in the header (`minor(p: Person)`), and the body takes only
`when`, `scope`, `effective`, anchor, label, and `meta`. Conditions
with exceptions do not fit here grammatically: there is no `unless` in a
definition body, and that is not an omission but a consequence —
definitions have no exceptions by definition. Whoever tries to
express “counts as …, except …” in one definition writes a non-definition:
the split is a strict sufficient part plus a separate defeasible
exception-norm with priority (see the [priority page](/constructs/priority/)).

## 5. Common mistakes

1. A separate `relation` for the definition name — `LDC-E1201` +
   `LDC-E1338` (pitfalls, item 1).
3. Expecting contraposition from `exact` (pitfalls, item 3).
4. A definition with exceptions instead of `classification … defeasible`
   (pitfalls, item 4).
6. A definition without `scope` where the term lives in several contexts
   (pitfalls, item 6).

## 6. References

- Neighbour pages: [strict rules](/constructs/rule-strict/),
  [priority](/constructs/priority/), [constraints](/constructs/constraint/).
- The pitfalls page lists the diagnostics (`LDC-E1201`, `LDC-E1338`) with
  wrong forms and fixes.