Decidability Tiers

A rule that the reasoner cannot evaluate is a rule the reasoner cannot use. This is not a complaint — it is a design fact. Description Logic, Datalog, and full first-order logic occupy different points on the tractability/expressiveness curve, and a language that wants to run its rules has to make those points visible to the programmer.

Argon does that with a seven-tier decidability ladder. Every rule is automatically classified at elaboration time. Tiers from tier:structural through tier:recursive execute today. tier:fol admits semi-decidable rules through the unsafe logic { … } escape hatch. tier:modal and tier:mlt are reserved for std::kripke-driven modal reasoning and multi-level types respectively.

This chapter explains the ladder, shows one example per tier, and walks through the three related mechanisms that hang off it: #dec(<tier>) directives that scope ambient ceilings at module / block / declaration granularity, unsafe logic { … } blocks for the FOL escape hatch, and the recognizer table that lets carefully-shaped FOL bodies pass under stricter ceilings via shape-driven tier reduction.

The ladder

The ladder stands on its own — each tier corresponds to a real engine and a real cost model, grounded in the complexity classes those engines target. tier:structural is the polynomial concept-graph saturation regime described in Baader et al., Pushing the EL Envelope (IJCAI 2005); tier:recursive is stratified Datalog as formalized in Abiteboul, Hull & Vianu, Foundations of Databases (1995); tier:fol is unrestricted first-order logic; the four remaining tiers sit between, each with its own engine and acceptance criterion. The names describe what each tier admits and what it costs; they do not align to any other language’s expressivity slices.

Classification is automatic. There is no tier: annotation on a rule; the elaborator walks the body, assigns each atom and operator an intrinsic tier, and takes the maximum:

$$tier(body)=\underset{a\in atoms(body)}{\max }tier(a)$$

where the per-atom function $tier:Atom\to \{0,1,2,3,4,5,6\}$ is a structural recursion:

$$\begin{array}{rcl}tier(\mathsf{MetaPropertyLookup}(c,a,v))& =& 0\\ tier(cspecializes{c}^{\prime })& =& 1\\ tier(count(\dots )\bowtie n)& =& 2\\ tier(e_1\bowtie e_2)& =& 3\text{where }\bowtie \in \{<,\le ,=,\ne ,\ge ,>\}\\ tier(e_{1}op{e}_2)& =& 4\text{where }op\in Allen\\ tier(\exists x:T.\varphi )& =& \{\begin{array}{ll}5& \text{if scope-bounded by }@[scope]\\ 6& \text{otherwise}\end{array}\\ tier(\forall x:T.\varphi )& =& 6\\ tier(op(e_1,\dots ,e_k))& =& \max (tier(op),tier(e_1),\dots ,tier(e_k))\end{array}$$

The recursion is implemented in argon/oxc/src/meta/classify.rs and surfaces through OI0804 at elaboration time. Aggregates compose by max; the binding-form forall is the single construct that can force a rule to tier:fol unilaterally — unless the recognizer (see below) matches the body against a known shape and reduces the effective tier.

The classification surfaces through OI0804 — an info-level diagnostic emitted at elaboration time so you can see what tier each derive rule landed at:

$ ox check
OI0804

  > [OI0804] derive rule `ActiveLease` classified at tier:recursive
    ,-[11:1]
 11 | ,-> pub derive ActiveLease(l: Lease) :-
 12 | |       l: Lease,
 13 | |       l.start_date <= today(),
 14 | |       l.end_date > today()
 15 | |->
    : `---- tier:recursive
    `----
  help: for more information, try `ox explain OI0804`

ox explain OI0804 prints the long-form explanation: which sub-expressions contributed which intrinsic tiers, and how they composed.

One example per tier

The seven tiers, illustrated against the running lease ontology and standard-shape predicates over it.

Tier 0 — MetaPropertyOnly

Pure meta-property lookups. No traversal of the structural graph; no value comparisons; no arithmetic.

pub derive RigidConcept(c: ⊤) :-
    A.rigidity(c) == rigid

The reasoner answers this from the meta-property calculus’s IS-state (Stratum 0). Polynomial in the number of axes × the number of concepts. The classifier rejects nothing here.

Tier 1 — HierarchyTraversal

Subtype reasoning, transitive closure, simple sibling-axiom checks.

pub derive AnyResidentialSibling(l: Lease) :-
    l: Lease,
    l specializes ResidentialLease

The nous saturator handles tier-1 rules by traversing the type hierarchy.

Tier 2 — CountingAndPaths

Bounded-length path queries through the structural graph.

pub derive HasGuarantorWithin2Hops(l: Lease) :-
    l: Lease,
    l connected_by mediates within 2 to Guarantor

within N caps the traversal depth; the connected_by operator becomes a bounded path expression.

Tier 3 — ValuePredicates

Comparisons over value-typed fields plus integer arithmetic. The QF-LIA fragment.

pub derive ActiveLease(l: Lease) :-
    l: Lease,
    l.start_date <= today(),
    l.end_date > today()

Tier 3 is the highest of the executable tiers — the running edge of what the saturator + value-predicate engine produces results for today. Most real domain rules sit at tier 3. OI0804 for any rule in the lease tutorial reports tier 3 because of the date comparisons.

Tier 4 — Temporal

Allen-interval operators (before, after, meets, overlaps, during, contains, …) — DatalogMTL territory.

pub derive OverlapsActive(a: Lease, b: Lease) :-
    a: Lease, b: Lease,
    a overlaps b,
    a end_date > today()

The Allen operator forces tier 4. Today the elaborator parses, type-checks, and emits the rule into the IR; the saturator does not produce derivations from tier-4 rules until the DatalogMTL execution path ships. ox check reports OI0804: Tier 4 (temporal) and the rule’s body becomes design intent rather than a live derivation.

Tier 5 — BoundedFOL

First-order rules with bounded-cardinality scope annotations. Classical Kodkod territory.

@[scope(leases: 100)]
pub derive AtLeastOneLeaseHasNoTenant() :-
    exists l: Lease where not exists t: Tenant where l.tenant == t

The exists introduces a true binding-form quantifier; the @[scope] annotation tells the classifier it is bounded. Tier 5 is syntax-only today; without @[scope] the same rule is tier 6.

Tier 6 — FullFOL

Unbounded forall / exists, full first-order logic. Semi-decidable.

unsafe logic {
    pub derive transitivity_of_specialization(x: ⊤, y: ⊤, z: ⊤) :-
        forall x, y, z: ⊤ where x specializes y, y specializes z
        => x specializes z
}

The forall binding-form forces tier 6. A tier-6 rule outside an unsafe logic { … } block is a hard error — OE0809: Tier 6 rule outside unsafe logic block. Inside the block, the rule parses, elaborates, and lands in the IR with OI0808 (“unsafe logic rule gated”) — the rule is a property of the source, not of any saturation result.

The decision to gate tier 6 behind unsafe logic is deliberate: full FOL is an escape hatch for rare cases (theorem-shaped invariants you intend to mechanically verify but not execute). It is not a programming idiom.

#dec(<tier>) — capping an effective fragment by scope

A mature ontology project usually wants to be conservative: “we only commit to tier:recursive-or-below reasoning in this module; flag anything that creeps higher.” The #dec(<tier>) directive declares an ambient ceiling at module, block, or declaration scope:

#dec(tier:recursive)

mod core_rules {
    pub derive ActiveLease(l: Lease) :-
        l: Lease,
        l.start_date <= today(),
        l.end_date > today()

    #dec(tier:closure)
    pub derive Ancestor(p: Person, c: Person) :-
        p parent_of c
        => p ancestor_of c
}

unsafe logic {
    pub derive transitivity_of_specialization(x: ⊤, y: ⊤, z: ⊤) :-
        forall x, y, z: ⊤ where x specializes y, y specializes z
        => x specializes z
}

The directive scopes:

• Module head. #dec(<tier>) at the top of a .ar file binds the ambient ceiling for every item in the file.
• Per-block. #dec(<tier>) { … } binds an ambient inside a block — handy for a research subsection that uses one stricter-or-looser tier than its surroundings.
• Per-declaration. #dec(<tier>) immediately preceding a pub derive (or any other tier-classified declaration) overrides the enclosing ambient for that declaration only.
• unsafe logic { … }. Injects a whole-block tier:fol ambient, the FOL escape hatch. Every item nested inside — derive rules, nested concept declarations, anything else admitted in block scope — inherits FOL regardless of any outer ceiling.

Stricter wins: the effective ceiling at any point is min over the entire ambient stack. A #dec(tier:closure) declaration nested inside a #dec(tier:recursive) module compares its rules against the stricter closure ceiling, not the looser ambient.

A rule whose effective syntactic tier exceeds the stack’s ceiling fires OE0604 TierViolation. The check runs at elaboration, before any reasoning, so the build fails with a precise pointer at the offending rule.

There is no [reasoning] max_tier manifest field. Per-scope tier concerns live in source directives; package-wide concerns (no-std, edition, dependencies) live in the manifest. The two never mix.

Recognized-shape tier reduction

A rule’s effective tier is min(syntactic_tier, recognized_tier). Carefully-shaped FOL bodies pass under stricter ceilings:

pub decorator transitive(r: rel) on rel = {
    semantics: forall x y z. r(x, y) and r(y, z) -> r(x, z)
}

#dec(tier:closure)
@[transitive]
pub rel parent_of(p: Person, c: Person)

The decorator’s body is syntactically tier:fol (forall is a binding-form quantifier). But the recognizer matches the body against RecognizedShapeKind::Transitive { rel } — the canonical FOL shape for transitivity — and the effective tier collapses to tier:closure. The parent_of rule passes the #dec(tier:closure) ceiling. The reasoner takes the transitive-closure fast-path.

The recognizer admits ten canonical shapes (Transitive, Symmetric, Asymmetric, Reflexive, Irreflexive, Functional, InverseFunctional, QualifiedCardinality, DisjointClasses, CoveringClasses). Six normalization passes (alpha-rename, flatten-associative, push-negations-inward, implications-to-disjunctions, canonicalize-equality, sort-conjuncts) ensure that semantically-equivalent bodies with different syntactic surfaces match the same canonical form. Bodies that don’t match any shape — the common case for hand-written forall — fall through to generic FOL handling and require unsafe logic { … } to lift the FOL ceiling.

@[theorem] — mechanical verification at compile time

Some derive rules are theorems — claims that hold over the entire model rather than a particular saturation. For those, mark the rule with @[theorem]:

@[theorem]
pub derive specialization_is_transitive(x: ⊤, y: ⊤, z: ⊤) :-
    x specializes y,
    y specializes z
    => x specializes z

@[theorem] triggers the compiler to attempt mechanical verification at ox check / ox build time, using the saturator + the meta-property calculus. If the proof succeeds, the rule is a verified invariant. If the verifier cannot decide it, you get a warning and the rule continues to act as a regular derivation.

Two restrictions, both enforced as warnings:

• OW0821 — @[theorem] is only valid on derive items. Placing it on compute, mutation, query, etc. is rejected.
• OW0822 — @[theorem] declared twice on the same derive is also rejected.

@[theorem] is the right way to raise confidence above the executable cutoff: a tier-5 or tier-6 derive that is mechanically verified is more trustworthy than the same rule running, even if execution were available.

#[unproven] and #[assumed] — test markers

Two related decorators, both applied to test blocks:

• #[unproven] — the test asserts a theorem-shaped claim without mechanical verification. The test runs as usual; the marker is a future-reader signal that the claim deserves verification.
• #[assumed] — the test injects the body’s claim as a postulate within the test’s scope. Useful when a real-world axiom (for example, “every SSN is unique”) is needed downstream but cannot be derived from the model.

#[unproven]
test "subtyping is transitive across the entire lattice" {
    /* claim — not yet mechanically verified */
}

#[assumed]
test "every SSN is unique" {
    assert forall p1, p2: Person where p1.ssn == p2.ssn => p1 == p2
}

Both attributes are restricted to test blocks. Placing #[unproven] or #[assumed] on a non-test item produces OW0823 TestAttributeNonTest.

unsafe logic — escape hatch for tier 6

unsafe logic { … } is the only place tier-6 rules are admitted. Inside the block:

unsafe logic {
    pub derive transitivity_of_specialization(x: ⊤, y: ⊤, z: ⊤) :-
        forall x, y, z: ⊤ where x specializes y, y specializes z
        => x specializes z
}

Three diagnostics shape this surface:

• OI0808 — informational; “unsafe logic rule gated” — emitted for every rule in the block, confirming the rule is parsed and lands in the IR but does not execute.
• OE0809 — error; “Tier-6 rule outside unsafe logic block” — emitted if you forget the block.
• OW0806 — warning; “Tier-6 rule without heartbeat budget” — emitted when a tier-6 rule lacks a @[budget] annotation. Once tier-6 execution lands, budgets become mandatory.

The block is for design intent: you have a property the model needs, you can express it in FOL, and you want it in the source so future readers see the trajectory. You do not get a result at evaluation time today, and that is the contract.

Configuring the tier classification

Three annotations let you tune what the classifier does with a particular rule:

• @[complexity(<class>)] — pin the rule’s tier explicitly. Useful for the OE0805 check: if your asserted complexity contradicts what the classifier computes, the build fails. Treat this as a regression-guard for refactors that would silently raise a rule’s tier.
• @[budget(N)] — heartbeat budget for a tier-6 rule (and, when tier-5/6 execution lands, a runtime fairness limit).
• @[scope(domain: N)] — bounded-cardinality annotation that lets a tier-5 rule stay at tier 5 instead of escalating to tier 6.

Invalid keys in @[budget] are OE0810; in @[scope], OE0811. Unknown complexity classes in @[complexity] are OE0812.

A worked example showing all three at once. The catalog’s _catalog/decorator-{complexity,monotone,scope,budget}/ directories ship runnable variants for each.

// @[complexity(ptime)] pins a rule to Tier ≤ 2. A body that
// classifies higher triggers OE0805 at ox check time.
@[complexity(ptime)]
pub derive simple_subsumption(p: Person) :-
    p: Person                                // tier:closure — passes

@[complexity(ptime)]
pub derive AgeFloor(p: Person) :-            // OE0805: ptime asserted,
    p: Person, p.age > 0                     // tier:recursive classified

// @[monotone] asserts the rule body uses no negation / no
// is-ambiguous / is-unknown / is-timeout atoms. The elaborator's
// find_non_monotone_atom walker checks; OE0807 fires on violation.
@[monotone]
pub derive HasAdult(p: Person) :- p: Person, p.age >= 18

// @[scope] bounds a tier-5 quantifier. Without it the same rule
// would classify at tier:fol; the bound keeps it in BoundedFOL.
@[scope(max: 16)]
pub derive AtLeastOneActiveLease() :-
    exists l: Lease where ActiveLease(l)

The @[complexity] annotation in particular is the canonical regression-guard pattern: assert your intended ceiling, and let OE0805 flag the refactor that quietly raises a rule’s effective tier.

What every tier-classifier diagnostic means

Quick reference; see Appendix C for the canonical registry.

Why a tier ladder rather than profiles

Description Logic profiles (EL, QL, RL, plus EL++ and DL-Lite variants) come from a tradition of “pick the maximal sublanguage you can decide in time T.” They are ontology-engineering choices, and they apply to a whole language at once.

Argon’s ladder is a programmer’s surface. Each tier corresponds to a real engine that the toolchain ships (or will ship), with a real cost model. The classifier tells you which engine your rule lands on. #dec(<tier>) lets you pin scopes — module, block, declaration — to a tractability target. The recognizer collapses recognized-shape FOL bodies under stricter ceilings without forcing every rule into the unsafe logic escape hatch. @[theorem] raises confidence above the executable cutoff for the rare cases that need it.

The seven-tier ladder is the lever; the per-rule classification is what makes it useful. Decidability moves from a property of the language to a property of the rule, made visible at compile time.

What’s next

Chapter 5.1 explains the meta-property calculus that powers tier 0. Chapter 5.2 covers @[default] / @[override] / @[defeat], which interact with tier classification (defeasibility is itself stratified). Chapter 5.4 covers the bitemporal axes — orthogonal to tiers but reasoning-relevant.