Definitions: pitfalls

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.

Wrong forms, silent outcomes, LDC-E diagnostics, typical mistakes of formalizers and AI agents, and how to detect them. Items marked “confirmed by runs” were reproduced during this research on the installed engine.

OverviewBoundariesCorpus formsPitfalls

1. A separate relation for the definition name (finding, confirmed by runs)

Arxo Law

relation minor(p: Person) kind institutional {
    label ru-KZ official "является несовершеннолетним";
}
definition minor(p: Person) exact {
    when under_eighteen(p);
}
// error LDC-E1201: имя "minor" уже объявлено + LDC-E1338 о двойном StableId

A definition and a relation share one namespace: the compiler synthesizes the relation itself, writing it by hand is a static rejection. The correct form is a lone definition: definition Sheaf(f: Presheaf) exact stands alone, without any companion relation. The AI agent, used to “vocabulary first, then rules”, writes relation automatically — here that is a mistake. Detection: LDC-E1201 on a definition line means almost always exactly this, not a random name clash.

2. One-way definitions

For a named qualification with both a deriving rule and a necessary constraint, use definition … exact. For a one-way inference, write a strict rule explicitly.

3. Expecting contraposition from exact (silent outcome)

A definition does not apply contraposition: from “of full age” nothing about age follows until the author writes a separate rule with a literal head. An explicit negative classification is likewise set by a separate rule … then not …. Detection: a question about the concept’s negation answers Not established, not refuted on any case — and that is not “facts missing” but the absence of the reverse direction. A test on the concept’s negation must exist separately from the test on the concept.

4. A definition with exceptions

A definition has no hidden strength: if the qualification has ordinary exceptions or a presumptive character, take classification … defeasible or separate defeasible rules. A definition “that is almost always true” is a wrong form choice: the first exception will demand a rewrite, and until then the definition will give a strict inference where the law gives a contestable one.

5. Redeclaring the definition name

Arxo Law

relation minor(p: Person) kind institutional;
definition minor(p: Person) exact { ... }

The definition synthesizes its own relation. Declaring the same relation separately creates a duplicate name and is rejected; use the definition alone.

6. A definition without scope on a polysemous term

One term can have different definitions in different packages and contexts, and a legal definition must have scope. Without scope, a term living in two contexts (e.g. “place of residence” in substantive and in procedural law) gives two unconditional strict inferences under one name — a hidden definition conflict surfacing as Contradiction at a consumer importing both packages. Detection: a term with two scopeless definitions is a candidate for scope refinement; scope is written as a scope clause in the definition body.