Decidability

Tier ladder

Default module tier: structural.

Temporal sub-tier (orthogonal axis). Every program has a tier pair (main, temporal). The temporal sub-tier ladder:

The classifier accepts a program if both axes are tractable and the program respects additive composition between modal (box/diamond) and metric temporal operators — no nesting of one family inside the other. Cross-mixed nesting box(box_minus[a,b](C)) is refused at tier: recursive (OE0712 ModalTemporalCrossNestRefused) and routed to tier: fol. The grounding is Demri-Wałęga 2024 (Standpoint LTL): satisfiability is EXPSPACE-complete unrestricted, with a PSPACE fragment under interplay restriction that Argon’s rigidity-of-standpoints commitment satisfies.

Annotation:

#[dec(tier: recursive, temporal: stratified)]
mod my_module { … }

If only one axis is annotated, the other is inferred from the module’s content.

Mechanized at spec/lean/Argon/Decidability/Temporal.lean (TemporalSubTier lattice + additiveComposition predicate + admitsAt_admits soundness lemma).

Annotations

#[dec(tier:<name>)]
#[budget(heartbeats: Nat)]
#[scope(max: Nat)]
#[brave]                  // stable models (reserved)
#[coinductive]            // greatest fixpoint
#[constructive]           // required at tier 5+ for non-ground NAF
#[shape(<recognized-shape>)]
#[lattice(K3 | FDE | Boolean)]
#[consistency(strict | paraconsistent)]    // on standpoint
#[world(open | closed)]                     // on concept (World assumptions (CWA / OWA); live — marks the concept's world, default CWA)
#[default]                                  // on derive — overridable clause (Defeasibility, RFD 0028)
#[defeats(target(args))]                    // on derive — declares an attack (Defeasibility, RFD 0028)
#[label(name)]                              // on derive — clause identity, head.label (Defeasibility)
#[intrinsic]                                // on iof-body field
#[unproven] / #[assumed]                    // on test
#[language_interface]                       // on Lean-spec-bound items

Theory-specific annotations (e.g., #[order(N)] from the mlt package, #[potency(N)] from a potency package) are library macros in unprivileged theory packages, not language-level attributes — see Higher-order modeling and Stdlib (selected).

Reserved attribute names. The compiler-known attribute names listed above are reserved. A user pub macro <name> { … } or #[procmacro] pub fn <name>(…) declaration whose name collides with the reserved set is rejected at the declaration site with OE0708 ReservedAttributeName. The full reserved set:

brave, budget, coinductive, consistency, constructive, dec, default,
defeasible, defeater, defeats, derive, intrinsic, inverse, label,
language_interface, lattice, managed, no_implicit_prelude, priority,
procmacro, scope, shape, unproven, assumed, world

(defeasible, defeater, priority are removed surfaces — they stay reserved so a typo refuses with a migration hint, RFD 0028 D9 — and default, defeats, label are the replacements.)

This list is fixed; adding to it requires an edition bump (the edition = N field in ox.toml). Theory-specific attribute names (categorizes, partitions, subordinate_to, power_type_of, order, complete, potency, @n, …) live in their own unprivileged theory package (mlt, potency, …) as #[procmacro] / pub macro declarations, not as language-reserved attributes — see Higher-order modeling and Stdlib (selected).

unsafe logic

The only escape to full FOL:

unsafe logic {
    #[scope(max: 10)]
    forall p: Person where exists q: Person where ParentOf(p, q)
}

The body admits the rule-atom grammar of Rule-atom grammar; FOL binding quantifiers (forall x: T where … and exists x: T where …) are accepted without tier-cap rejection. No new connectives or syntax are introduced — only the elaborator’s tier classifier differs. The tier classifier statically routes the block to a backend (native / SMT / ASP / FOL prover) and emits a per-block verdict: TERMINATES, TERMINATES UNDER BOUND (requires #[scope] / #[budget]), or REJECTED.