Definitions: boundaries

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.

What the construct does NOT do in 0.2: limits, closed lists, neighbouring constructs, and the selection rule.

OverviewBoundariesCorpus formsPitfalls

Does not do

• Does not apply contraposition. The reverse direction becomes an inference only when the author writes a separate rule with a literal head. An explicit negative classification is a separate rule … then not ….
• Has no hidden strength. Exceptions and presumptive character are classification … defeasible or separate defeasible rules; a definition has no strength at all.
• Is indistinguishable by outcome from a strict rule. The observed status of the sufficient half matches a strict rule: the difference is in the proof graph (the was_derived_from edge) and in the explanation (“by definition”). Whoever looks for the difference in engine answers mistakes the level: the difference is in tracing, as with source anchors.
• Does not change the theory. The provenance edge is inside contentHash and artifactHash but outside theoryHash: an implementation dropping the edge or recording other attributes yields different node bytes and fails conformance checks, but the theory is the same.
• Does not infer by the necessary half. necessary is only a constraint “concept requires condition”: on its own it establishes no concept.

Reserved and closed

• Definition modes are necessary and exact; the sufficient rule half is generated by exact.
• A definition body is only when, scope, effective, source anchor, label, meta: no for binders — parameters go in the header; no unless — no exceptions.
• The definition identifier must resolve to a relation of the same signature, but declaring it as a separate relation is forbidden — the compiler synthesizes it itself, a repeat is LDC-E1201.
• Classification strength is strict or defeasible.

Neighbours and selection rule

• definition … exact vs rule … strict: name and explanation against a one-off inference; outcome matches, the difference is in the graph. See the strict-rules page.
• definition vs classification … strict: term-definition intent (often with scope) against sorting into classes; new material defaults to a definition.
• definition vs classification … defeasible: without exceptions against with exceptions; a presumptive qualification is only the second form.
• A necessary half (“concept requires condition”) vs constraint: restricting a concept against a general inference restriction. See the constraints page.
• Definition scope vs rule scope: a term’s domain against an inference’s applicability condition. See the time page.