The Argon Substrate

Argon’s compiler ships with zero foundational ontology content. It does not know what a kind is, what rigidity means, or what a relator does. The keywords kind, subkind, role, phase, relator, category, mixin — all the vocabulary the introduction promised was not built in — are exactly that. Identifiers, declared by user packages, brought into scope by use.

What the compiler does ship is the substrate that lets a vocabulary package declare them. This chapter is that substrate: the four declaration forms — pub metaxis, pub metatype, pub metarel, pub decorator — that turn a Markdown-flat universe of names into a typed metaontology where the compiler can check Person : Kind, route a transitive decorator to a recognized fast-path, or refuse pub kind X : Role because rigid cannot specialize anti-rigid.

The rest of Part 2 uses UFO’s metatypes (kind, role, …) as if they were primitives, because UFO is the most established vocabulary and the chapters need something to model with. This chapter is what makes that legitimate. UFO is one user package built on the substrate. BFO is another. So is whatever your team needs that doesn’t yet exist.

Why a substrate

Foundational ontologies do not agree.

UFO carves the world along rigidity (does the type apply necessarily, or contingently?) and sortality (does it carry an identity criterion?). BFO carves along temporal status (continuant vs. occurrent) and dependence (does the entity require a specific bearer?). DOLCE has its own axes, GFO its own. They overlap in places, contradict in others. None is wrong; each is a different commitment about what categories are foundational.

A language that bakes one of these in cannot host the others. Make rigidity a built-in keyword and BFO no longer fits — BFO does not commit to rigidity at the upper level. Make temporal_status built-in and you have privileged BFO over UFO.

Argon’s solution is to ship the machinery — axes, metatypes, metarels, decorators — and let the foundational ontology supply the content. UFO declares rigidity; BFO declares temporal_status; both packages run on the same compiler. A project picks one (or several, if their axes do not collide) by writing use.

The four declaration forms

pub metaxis, pub metatype, pub metarel, pub decorator. They are language primitives — the compiler parses each as a top-level declaration form, like fn in Rust or data in Haskell. Everything else in an ontology package — the kinds, the roles, the transitive decorator — is built from these four.

pub metaxis — declare an axis

A metaxis (short for meta-axis) is a dimension along which metatypes vary. Rigidity is one. Sortality is another. Temporal-status is another. A metaxis declaration names the axis, scopes it to the kind of declaration it qualifies (type, rel, or dec), and supplies its value space.

The simplest form is a finite enumeration:

pub metaxis rigidity for type {
    rigid,
    anti_rigid,
    semi_rigid
}

rigidity qualifies type declarations. Its value set is {rigid, anti_rigid, semi_rigid}. The values are atoms — bare identifiers carving the axis into points.

A metaxis can also be a typed domain. Instead of an enumeration, it admits values from a primitive type, optionally narrowed by a refinement predicate:

use std::math::Nat;

pub metaxis cardinality_floor : Nat for rel where { _ > 0 }

The values are natural numbers; the refinement requires positivity. A metarel that binds cardinality_floor = 0 triggers a refinement violation at elaboration time. Typed-domain axes admit Nat, Int, Real, Bool, and String, with promotion Nat → Int → Real.

A package may declare any number of axes. The constraint is one of acyclicity: the meta-property calculus that runs at elaboration time builds a dependency DAG over axes (axis B reads axis A), and a cycle is rejected at vocabulary-load time. Within that constraint, axes are free.

pub metatype — declare a metatype

A metatype is a bundle of axis values. Where a metaxis says “here is an axis,” a metatype says “here is a point in axis space.” kind lives at { rigid, sortal, provides_identity }. role lives at { anti_rigid, sortal, relational }. The declaration form is a record literal over in-scope axes:

pub metatype kind = {
    rigidity = rigid,
    sortality = sortal,
    identity_provision = provides
}

(In practice, packages often elide the axis names when the values themselves are unambiguous: pub metatype kind = { rigid, sortal, provides }. Either form is accepted; the compiler resolves each value against in-scope axes.)

A metatype’s name is the surface keyword. After

pub metatype kind = { rigid, sortal, provides }

writing

pub kind Person { ... }

is a concept declaration whose metatype is kind. The grammar position where a metatype name appears — between pub and the concept’s identifier — accepts any in-scope pub metatype. There is nothing privileged about kind in the parser.

If the resolver cannot find a pub metatype matching that name, the compiler emits OE0605 UnknownMetatype with a four-variant hint: the name might be unimported, ambiguous across packages, declared as something other than a metatype, or genuinely undeclared.

pub metarel — declare a relation metatype

Concept declarations describe individuals. Relations describe how individuals connect: mediates, componentOf, inheresIn. Just as concepts have metatypes that classify them (a Person is a kind), relations have metarels that classify them (a mediates is a material_relator_relation). A metarel declaration ties a relation kind to its endpoint constraints, default cardinalities, and any decorators it implies:

pub metarel mediates = {
    source: relator,
    target: kind,
    cardinality_default: { source: [0..1], target: [1..*] },
    properties: { irreflexive, asymmetric }
}

mediates is a relation whose source must be a relator and whose target must be a kind; by default a relator mediates one or more kinds. The properties set lists structural-property names that apply to every relation tagged with this metarel. The body is record-shaped (= { ... }) — the same shape pub metatype and pub decorator use.

When user code writes pub rel teaches(t: Course, s: Student) :: mediates, the compiler validates the endpoints (Course must be a relator-typed concept, Student a kind-typed concept) and applies the cardinality defaults if the rel does not specify its own. Endpoint mismatches emit OE0226 MetarelEndpointMismatch; an unknown metarel name is OE0225 UnknownMetarel.

pub decorator — declare a decorator

Decorators are reusable annotations that lower to compiler behavior. @[transitive] on a relation tells the reasoner to compute the relation’s transitive closure. @[theorem] on a derive rule marks the rule as a theorem claim — at the current cut, the marker is preserved through emission and surfaces in the kernel’s runtime so a future verification pipeline can target it; the compile-time pass does not yet attempt mechanical verification. The decorators themselves are user-declared:

pub decorator transitive() on rel = {
    semantics: r(x),
    lowers_to: transitive_closure
}

A decorator declaration carries:

• a parameter list (transitive is zero-arg; inverse(of: rel) takes one);
• a target (on rel, on type, on dec, on field, on individual, or on frame);
• a semantics body — a Datalog atom that anchors the decorator’s compile-time intent. The body’s logical content rides on the lowers_to: recognized shape, not on the surface atom itself; conventionally semantics: is a stub atom and the recognizer table picks up the shape;
• an optional lowers_to: <shape> hint that pre-tags the decorator with a recognized canonical shape (more on this below).

When user code writes @[transitive] on a relation, the compiler binds transitive against in-scope decorator declarations, validates arity / target / argument types, and lowers the application. A mismatch emits one of OE0229 UnknownDecorator, OE0230 ArityMismatch, OE0231 TargetMismatch, OE0234 ArgumentTypeMismatch.

The lowers_to hint is the substrate’s bridge to the recognizer table — a set of canonical FOL shapes (transitive, symmetric, functional, disjoint-classes, qualified-cardinality, …) that the compiler can route to a fast-path implementation in the reasoner. A user decorator whose body matches a recognized shape gets the fast-path treatment for free; one that does not falls through to generic Datalog. Chapter 5’s Metatype Calculus covers the recognizer in detail.

How user packages compose this

UFO declares its core axes and metatypes using these four forms — nothing else. Here is the start of UFO’s prelude.ar, which ships with the package:

pub metaxis rigidity for type {
    rigid,
    anti_rigid,
    semi_rigid,
    order: anti_rigid < semi_rigid < rigid
}

pub metaxis sortality for type {
    sortal,
    non_sortal
}

pub metaxis identity_provision for type {
    provides,
    inherits,
    condition: rigidity == rigid and sortality == sortal
}

pub metatype kind     = { rigid, sortal, provides }
pub metatype subkind  = { rigid, sortal, inherits }
pub metatype role     = { anti_rigid, sortal, relational }
pub metatype phase    = { anti_rigid, sortal, intrinsic }
pub metatype relator  = { rigid, sortal, provides }
pub metatype category = { rigid, non_sortal }

That is the entire mechanism. UFO publishes this file (and a much larger one for relations, decorators, and structural-check rules); user code writes use ufo::prelude::*; from that point kind, role, phase are in scope as identifiers the parser can dispatch.

BFO is a peer package that publishes a different prelude:

pub metaxis temporal_status for type {
    temporal,
    atemporal
}

pub metaxis dependence for type {
    independent,
    specifically_dependent,
    generically_dependent
}

pub metatype continuant                       = { temporal }
pub metatype occurrent                        = { atemporal }
pub metatype independent_continuant           = { temporal, independent }
pub metatype specifically_dependent_continuant = { temporal, specifically_dependent }

BFO declares temporal_status and dependence; UFO declares rigidity, sortality, identity_provision. Zero shared source. A project that imports use bfo::prelude::* writes pub independent_continuant Object {} instead of pub kind Person {} — the same compiler, the same substrate, a different vocabulary on top.

A project can also import both, provided the axes do not collide. The meta-property calculus treats two non-overlapping vocabulary packages as independent — one’s rules do not see the other’s facts. A shared axis (both packages declare rigidity) requires a confluence check, which the calculus runs at vocabulary-load time.

Two runnable example packages exercise the substrate from opposite ends. argon/examples/bfo-smoke/ is the minimal BFO smoke test — declares two BFO axes (temporal_status, dependence), four BFO metatypes (continuant, occurrent, independent_continuant, specifically_dependent_continuant), six BFO concepts, and two BFO disjointness rules. Zero shared source with the UFO package; both compile against the same oxc. argon/examples/dolce-lite/ does the same for DOLCE-Lite.

For the four substrate declaration forms tested in isolation, the catalog ships:

// _catalog/metarel-keyword/composition/ — exercises pub metarel
// with concept-reference endpoints (RFD-0031). Three rels use the
// same metarel; the compiler validates each endpoint against the
// concept-typed source/target via the four-arm endpoint resolver.

pub metaxis dependence_axis for type { independent, dependent }
pub metatype kind = { independent }
pub metatype mode = { dependent }

pub concept Aspect <: ConcreteIndividual

pub metarel characterization = {
    source: Aspect,           // concept reference (RFD-0031 Arm 3)
    target: ConcreteIndividual,
}

pub rel inheres_in(s: IntrinsicMode, t: Quality) :: characterization

Variants: _catalog/metarel-keyword/{minimal,composition}/ and the dedicated decorator workspaces under _catalog/decorator-{theorem,monotone,cache,chain,defeat,scope,complexity,unproven}/.

What you can do with this

The practical takeaway: you are not limited to the metatypes UFO ships.

A regulated-systems project that wants to distinguish Regulation from Norm from Procedure — three concepts UFO does not separate — declares its own axis and metatypes:

pub metaxis enforceability for type {
    enforceable,
    advisory,
    informational
}

pub metatype regulation = { rigid, sortal, enforceable }
pub metatype norm       = { rigid, sortal, advisory }
pub metatype procedure  = { rigid, non_sortal, informational }

These metatypes can layer on top of UFO’s (the rigid and sortal values come from UFO’s axes) or stand alone (declare your own foundational axes; ship them in your own package). User code in the regulated-systems project then writes:

use std::math::{String, Date};

pub regulation TaxRegulation12 {
    statute_id: String,
    effective_date: Date,
    text: String
}

The compiler treats regulation exactly the way it treats kind: it resolves the metatype, propagates its axis profile to TaxRegulation12, runs the meta-property calculus, fires whatever structural rules the package declared, classifies the concept against the inferred profile, and admits the declaration if everything is consistent. There is no compiler change. There is no special case. The substrate is the mechanism; the package is the content.

The same pattern applies at the relation and decorator level. A medical project might declare a treats(source: treatment, target: disease) metarel; a legal project might declare a @[binding] decorator that lowers to a custom Datalog rule. The substrate handles both because both are built from the same four forms.

Where we go next

This chapter taught the surface of the substrate — what the four declaration forms look like, how they compose, what OE0605 and OE0226 and OE0229 are checking for. The rest of Part 2 uses metatypes from UFO to teach concepts (2.2), relations (2.3), rules (2.4), computations (2.5), and the type system over them (2.6). When those chapters write pub kind, pub role, pub relator, you now know where the keywords come from.

The deeper machinery — the IS / CAN / NOT three-valued semantics, the stratified fixpoint with its termination and uniqueness results, cross-package metatype composition, the recognizer table’s shape-dispatch rules, and the structural-check error class — lives in Chapter 5.1: The Metatype Calculus. That chapter is the place to go when you start declaring your own axes and want to understand exactly what the engine does with them.