Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

RFD-0004 — Decidability ladder is Argon’s own, never framed in OWL terms

Committed Opened 2026-05-03 · Committed 2026-05-03

Question

Argon offers a graduated decidability ladder. Should its tiers be named or described using OWL profile terminology (EL++, OWL 2 EL/QL/RL/DL, SROIQ, ALC), or in Argon’s own vocabulary?

Decision

Argon’s decidability ladder uses Argon’s own tier names exclusively: tier:structural → tier:closure → tier:expressive → tier:recursive → tier:fol → tier:modal → tier:mlt. OWL profile names and adjacent description-logic vocabulary (fragment, profile) are forbidden when describing the ladder, the reasoner, or any expressivity-bounded sublanguage of Argon.

Recognized shapes inhabit the recognized tier — when an expression matches a canonical shape with a known fast-path implementation, its tier classification is the shape’s tier, not the syntactic tier of the source expression.

Rationale

The ladder is independent of OWL. Argon’s tiers are designed around the algorithmic complexity profile of evaluating expressions in each tier, not around any specific description-logic profile. Coincidental expressivity overlap with an OWL profile is an artifact of mathematics, not a design choice. Surfacing the equivalence in user-facing text imports OWL framing, OWL constraints, and OWL idioms that are not load-bearing for the language.

Tier-as-OWL-profile leaks foundational opinions. OWL profiles are designed around specific RDF-graph evaluation patterns. Argon’s reasoner (nous) is not an OWL reasoner; describing it as “the EL++ reasoner” misrepresents its architecture and binds it to a specification it does not implement. Describe the reasoner by what it does (classification, subsumption, role-closure, saturation), never by OWL vocabulary.

Recognized-shape tier classification. A transitive decorator on a relation lowers to a recognized-shape Datalog rule with a known polynomial-time algorithm. Even though the syntactic representation might appear at a higher tier, the recognized shape’s known evaluation cost is the operative classification. This keeps the ladder honest: tier reflects evaluation cost, not syntactic surface area.

Consequences

  • Any document, comment, or diagnostic that names a tier as EL++ is incorrect and gets fixed when noticed.
  • The reasoner is described as “the structural reasoner” or “nous” — never “the EL++ reasoner.”
  • tier:fol is the FOL escape hatch tier; unsafe logic { … } blocks live there. There is no tier:OWL_2_DL.
  • Recognizer table dispatch (transitive, symmetric, asymmetric, reflexive, irreflexive, functional, inverse-functional, qualified-cardinality, disjoint-classes, covering-classes) classifies recognized expressions into the recognized tier.