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

OverviewBoundariesCorpus formsPitfalls

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, item 1):

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

Output

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).
• 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: 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).

5. Common mistakes

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

6. References

• Neighbour pages: strict rules, priority, constraints.
• The pitfalls page lists the diagnostics (LDC-E1201, LDC-E1338) with wrong forms and fixes.