docs← Back to article

Markdown for LLMs

Definitions: boundaries

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

Download this articlePlain text ↗
# 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.

## 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](/constructs/rule-strict/).
- `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](/constructs/constraint/).
- Definition `scope` vs rule `scope`: a term’s domain
  against an inference’s applicability condition. See the
  [time page](/constructs/time/).