Beyond — Advanced

This part covers the parts of Argon a working programmer can use without studying the calculus underneath, but that ontology engineers, language designers, and verification-minded readers will want the formal grounding for.

The four chapters in this part:

• 5.1 The Metatype Calculus — the substrate’s calculus in detail: the IS / CAN / NOT three-valued state, the axis dependency DAG, the three-stratum fixpoint, cross-package composition, recognizer dispatch over canonical FOL shapes, and sibling-axiom propagation through user-declared structural rules. The chapter states the principal termination, uniqueness, and composition results.
• 5.2 Defeasibility and Multi-Stratum Reasoning — the @[default] / @[override] / @[defeat] decorators, Governatori three-stratum compilation, NaF stratification, rule-conflict resolution. Builds on the foundational defeasibility-logic work of Reiter, García & Simari, and Governatori et al.
• 5.3 Decidability Tiers — the seven-tier ladder in detail (tier:structural through tier:mlt), tier-cap enforcement at the module level, classification as a structural recursion, @[theorem] for compile-time mechanical verification, unsafe logic { ... } blocks, #[unproven] / #[assumed] test markers.
• 5.4 Standpoints and Bitemporal Reasoning — standpoint declarations and the standpoint lattice, standpoint-discriminated queries, bitemporal axes (valid-time × tx-time) deep-dive, time-travel queries (--as-of-valid, --as-of-tx), forks and structural sharing.

Mathematical preliminaries

A few notational conventions this part uses, drawn from the foundational-ontology and formal-methods literature.

Three-valued state ($K3$). Every (concept, axis, value) triple in the meta-property calculus carries one of three values: $\mathsf{IS}$ (positively held), $\mathsf{NOT}$ (positively excluded), $\mathsf{CAN}$ (genuinely indeterminate). The information ordering is $\mathsf{CAN}⊑\mathsf{IS}$ and $\mathsf{CAN}⊑\mathsf{NOT}$, with $\mathsf{IS}$ and $\mathsf{NOT}$ incomparable. This is canonical $K3$ — Kleene’s strong three-valued logic (Kleene, Introduction to Metamathematics, 1952), realized as the consistent fragment of the four-valued $\mathsf{FDE}$ bilattice (Belnap 1977 / Dunn 1976) under the Pietz-Rivieccio “Exactly True” designation. The $\mathsf{CAN}$ / $\mathsf{IS}$ / $\mathsf{NOT}$ naming follows the engine’s internal vocabulary.

Stratified evaluation. A stratum is an evaluation phase that reads only from earlier strata’s completed states. Stratified semantics for negation goes back to Apt, Blair & Walker (Towards a Theory of Declarative Knowledge, 1988); Argon uses stratification both for negation-as-failure inside rule bodies and for the three-stratum meta-property calculus.

Decidability tiers. Each rule lands at a tier $t\in \{0,1,2,3,4,5,6\}$ classified by the compiler. Tiers 0–3 are executable (the saturator produces results); tiers 4–6 are syntax-only (parsed and type-checked but not evaluated by today’s runtime). The classification is a structural recursion over the rule body, taking the maximum of intrinsic-tier per atom.

Bitemporal axes. Every fact is timestamped with a valid-time $t_v$ (when the fact is true in the world) and a transaction-time $t_x$ (when the system learned it). A query against the log filters by both. Retraction is a new event with later $t_x$; the original fact is preserved. The model follows Snodgrass & Ahn (Temporal Databases, 1986) and Jensen, Soo & Snodgrass (Unifying temporal data models via a conceptual model, 1994).

Standpoints. A standpoint is a named position in a partial-order lattice; facts and rules are tagged with their standpoint and queries can be discriminated to a particular vantage. Standpoints discriminate, they do not partition — a fact in default is also visible in any descendant unless explicitly retracted.

Principal results

Each chapter in this part states the math the implementation rides on. Three results carry the substrate:

• Meta-property fixpoint — termination and uniqueness of the stratified fixpoint over an acyclic axis-dependency graph; package composition (disjoint non-interference, shared-axis confluence); $\mathsf{CAN}$ at completion is genuine indeterminacy. Covered in Chapter 5.1.
• Flow-typing soundness — occurrence-typing narrowing persists across body atoms and survives monotone rule composition; CWA→OWA narrowing preservation. Covered in Chapter 5.1’s stratification discussion and applied throughout Chapter 2.
• Refinement-fragment decidability — the refinement type-checking fragment is decidable in PTIME, with staging correctness for the multi-package case. Covered in Chapter 2.6 and Chapter 5.3.

Reading order

If you have read Parts 1–4, the chapters below can be read in any order. A natural sequence:

1. Ch5.1 Metatypes — explains the calculus that powers Tier 0 reasoning across the language.
2. Ch5.3 Decidability Tiers — shows the ladder the compiler classifies every rule against.
3. Ch5.2 Defeasibility — the layer that runs on top of the tier ladder, organising rule conflicts.
4. Ch5.4 Standpoints + Bitemporal — the runtime story, orthogonal to (and composing with) all of the above.

Or skip directly to the chapter that answers a specific question. Each is self-contained.