Axiom-ADT variant catalog
The canonical axiom_events table (The single-event-log architecture) carries one of 26 axiom-kind variants. Each variant has a stable string tag (the axiom_kind column value) and a canonical-CBOR body shape (the body BYTEA payload).
The catalog is ontology-neutral. UFO contributes zero variants; UFO-specific meta-properties (rigidity, sortality, identity-provision) are meta_property events whose body declares (axis, target, value). Other vocabulary packages (BFO, DOLCE, MLT) contribute zero variants on the same principle.
The variants mirror Argon’s CoreIR 1:1. The canonical source is the Lean inductive Argon/Storage/AxiomKind.lean (variant set and order) and Argon/Storage/AxiomBody.lean (per-variant body shapes); the Rust mirror is oxc-protocol::storage::AxiomKind, pinned against drift by oxc-protocol/tests/drift.rs. When CoreIR shakes during compiler development, the Lean drives and this catalog follows. For the exact CBOR field shape of any variant, read AxiomBody.lean — it is authoritative; the body shapes are not reproduced here.
The 26 variants
Tag (axiom_kind) | Group | Notes |
|---|---|---|
concept_decl | Declarations (11) | Ontology-neutral; UFO axes via meta_property |
relation_decl | is_iof / is_subsumption flags identify privileged relations | |
struct_decl | ADT-product type | |
enum_decl | ADT-sum type | |
metaxis_decl | A meta-axis exists; vocab packages ship their axes here | |
metatype_decl | Bundles axis-value commitments for a concept-introducer | |
metarel_decl | Structural mirror of metatype_decl, for relations | |
standpoint_decl | Multi-parent DAG; rigidity per node | |
module_decl | Carries the composition signature (Composition signature) | |
trait_decl | Trait surface | |
impl_decl | Conditional impls supported | |
iof_assertion | Assertions (7) | “individual is an instance of concept”; bitemporal-aware |
iof_refutation | Strong (classical) negation of an iof_assertion (RFD 0010); maps to Truth4::Not at federation; same body as iof_assertion | |
relation_tuple | n-ary relation tuple; literal codomains allowed | |
relation_tuple_refutation | Strong-negation counterpart of relation_tuple (RFD 0010); same body as relation_tuple | |
property_assertion | Literal-valued specialization of relation_tuple; declared-symbol carrier | |
individual_property_assertion | Per-instance mut-field set (RFD 0006); per-instance IndividualId carrier | |
meta_property | Vocab-specific axis values land here, not in catalog columns | |
subsumption_axiom | Axioms (2) | sub <: super edge; multi-parent via multiple events |
partition_axiom | Vocab-neutral cover; MLT’s partitions(T) lowers onto this | |
rule_decl | Rule-modes (4) | Unifies fn / derive / query / mutate / check via a rule_mode field |
query_decl | Distinct from rule_decl to index queries; query-specific attrs (group_by, order_by, limit, offset) | |
mutation_decl | Named pub mutate; operations include forget (capability-gated, Capability surface) | |
compute_decl | Inline-compute (tier: recursive by definition) | |
bridge_decl | Federation (1) | Bridge rules bridge rule — directional inference between standpoints; added in δ.2 |
test_decl | Tests (1) | testing / The test atom — ox test in-language unit test (RFD 0048); body is a mutate-body Vec<Operation> plus Operation::Assert, run by ox test. Inert at query/serve time — carries no rule-mode semantics |
Total: 26. The body encoding is canonical CBOR (deterministic per RFC 8949 §4.2.1); content_id = SHA-256(body), so identical bodies deduplicate. UUIDs encode as bytes(16). The per-variant body maps are specified in Argon/Storage/AxiomBody.lean.
The set is MVP-final but not closure-locked. Additive variant additions bump core_ir_version minor; breaking changes bump major.
A .oxbin reader that encounters an unknown axiom_kind in the events section MUST report OE1220 UnknownAxiomKind(kind) and refuse the load — unless the artifact is lenient-validated (The OxbinRuntime trait surface), in which case the unknown events are dropped from the in-memory representation but kept on disk. Strict runtimes always fail.