The decidability ladder

Expressiveness and cost trade against each other, and Argon makes the trade visible. Every module sits on one of seven tiers, ordered by what its rules are allowed to say:

Each rung admits everything the rung below admits and one form more — closure adds transitive closure, recursive adds recursion through negation, fol adds unrestricted quantification — and pays for the added power in worst-case cost. The bottom two tiers run in polynomial time. expressive is still decidable but can cost exponential time in the worst case. fol is only semi-decidable: a query may run forever, which is why it is reachable only through the explicit unsafe logic escape and never by default.

The default tier is structural. A program that only declares concepts, subtypes them, and asks membership questions stays at the bottom of the ladder and runs in polynomial time, no annotation required.

The classifier reads the program, not the author

A module’s tier is computed, not asserted. The classifier walks every rule, assigns each atom the lowest tier that admits it, and takes the maximum across the program — a module lands on the lowest tier sufficient to admit everything it contains. A single recursive-through-negation rule pulls the whole module to recursive; without it the module stays lower. The mechanization proves the assignment sound: if the classifier reports tier t, every atom in the program is admitted at t, so the cost bound for t holds for the whole program. An author may annotate a module’s intended tier with #[dec(tier: …)], but the annotation is checked against the computed tier, not trusted in its place — a module that claims structural while containing a recursive rule is refused, not quietly promoted.

A second axis runs alongside the main ladder for temporal operators, classified the same way, and a package may cap the tier it will admit with a [lattice] ceiling in its manifest. Reaching past the ceiling is a build error, which is how a package that means to stay tractable keeps a contributor from silently raising its cost. The reference fixes the full ladder, the temporal sub-tiers, and the annotation surface under Decidability.

The polynomial floor is proven

The base tier’s cost claim is not an estimate. The Lean mechanization proves that for a fixed predicate at the structural tier, evaluation cost is bounded by a polynomial in the size of the data (d1_polynomial_bound over the D1Pred fragment). The predicate’s own size and quantifier depth are constants for a given program, so the bound is polynomial in the number of individuals — the data complexity that matters when the schema is fixed and the store grows. This is the formal content behind “structural runs in polynomial time”: a theorem about the fragment, carried in the substrate rather than asserted in prose.

Shapes the executor cannot run are refused, never dropped

The classifier’s verdict has teeth. A program at a tier the executor cannot yet evaluate, or a rule shape outside the supported fragment, is refused at ox check and ox build with a coded diagnostic — never accepted and silently skipped. A query touching an unsafe logic first-order rule is refused pending the first-order executor and its time budget; a federated bridge body is refused because the federation fixpoint does not yet fire it. The discipline is uniform: a built artifact is one whose every rule the runtime can evaluate, so a program never compiles green and then dies, or worse, returns a wrong answer, on a form the executor quietly declined to run. What the executor cannot do, it says so, at build, with the fix in the diagnostic.