RFD-0044 — Cross-level instantiation (MLT)

Question

How does Argon express concept-to-concept instantiation — the powertype pattern at the heart of multi-level theory — while preserving foundational-ontology neutrality? This RFD specifies the substrate change RFD-0040 D12 commits to.

Context

Argon’s Core IR has one atom for the instance-of relation:

#![allow(unused)]
fn main() {
// argon/oxc/src/core_ir.rs:771
Instantiates { individual: String, concept_id: u64 }
}

The first parameter is locked to String (an individual identifier). The atom expresses order-0 → order-1 instantiation: alice : Person. It cannot express Person : AnimalSpecies — concept-to-concept, the case multi-level theory (MLT, Carvalho & Almeida 2017) and Tonto (the OntoUML DSL) handle natively.

The :: operator (Person :: Kind) does not fill the gap. It lowers to CoreRuleAtom::Meta { subject, expected: Some("kind") } — meta-property assignment, asserting that Person has the meta-property kind. That is classification by metatype, not instantiation of another concept.

A team contributor’s diagnosis after auditing the IR:

Argon cannot represent concept-to-concept instantiation anywhere in Core IR. Not just on declarations — anywhere. The relevant Core IR atom is locked to order-0 → order-1 instantiation (an individual is an instance of a concept). There is no Core IR variant for order-1 → order-2 (a concept is an instance of a higher-order concept). So Tonto’s kind Dog (instanceOf AnimalSpecies), encoded in OntoUML as an «instantiation» Relation between two Class nodes, has no current Core IR analog in Argon.

The audit also surfaced the half-built infrastructure that already exists:

• crates/nous/src/multilevel.rs:14–81 enforces UFO axiom A-108 (categorization order constraints) when concepts declare order and categorizes axes. The order-arithmetic works; it has no IR or surface to drive it.
• argon/examples/lease-story/packages/ufo/src/mlt.ar documents the Carvalho & Almeida axioms (a105–a108) as relational facts but is orphaned — no story module uses it.

This RFD closes the gap with one IR generalization plus a new elaboration phase that derives order. The substrate stays vocabulary-neutral; UFO, BFO, or any other vocabulary can ride on top via decorators.

Decision

D1 — Generalize the IR atom

Replace Instantiates with InstanceOf. The new atom carries an enum on the left-hand side that distinguishes which kind of entity is being instantiated.

#![allow(unused)]
fn main() {
pub enum EntityRef {
    Individual(u64),  // an instance assertion in the ABox
    Concept(u64),     // a concept in the TBox (MLT case)
    Statement(u64),   // a reified statement (future; for higher-order reflection)
}

pub struct InstanceOfAtom {
    pub instance: EntityRef,
    pub type_concept: u64,
}
}

One atom expresses every instantiation. Existing emit sites pass EntityRef::Individual(id) and continue to work; new emit sites for concept-to-concept pass EntityRef::Concept(id).

Statement(_) is reserved for higher-order reflection (reified statements as entities). No surface admits it in v1; the variant exists so the IR doesn’t need a second generalization when that day comes.

D2 — Surface syntax admission

RFD-0040 D5 commits to : always meaning instantiation. This RFD extends the parser to admit : in concept declaration heads where today only individual-of-concept is recognized.

pub kind AnimalSpecies { order: 2 }
pub kind Dog : AnimalSpecies                    // Dog is an instance of AnimalSpecies
pub kind Husky <: Dog : DogBreed                // specialization + instantiation

Multi-instantiation follows RFD-0040 D9 (line-broken for multi):

pub kind Dog
    : AnimalSpecies, RegistrationCategory       // two instantiation targets

Mixed multi-specialization + multi-instantiation:

pub kind Husky
    <: Dog, WorkingAnimal
    : DogBreed, RegistrationCategory

The grammar admission is local — the parser already accepts : in declaration heads under RFD-0015’s specialization-sugar interpretation. RFD-0040 D5 replaces that interpretation with the correct one (instantiation); this RFD’s surface change is the lowering: when the right-hand side resolves to a concept (not a metatype primitive), emit InstanceOf instead of the old Meta atom.

Substrate / vocabulary boundary. Three layers:

A modeler writes:

use std::mlt::*        // MLT primitives (decorators + reflection on them)
use ufo::{kind, category}   // UFO metatypes

@[categorizes(Currency)]
pub category CurrencyType { }

pub kind USD : CurrencyType { … }

BFO, DOLCE, and any future ontology that does not adopt MLT skip std::mlt. Their vocabularies declare their own metatypes against std::meta directly. MLT is one standard-library module among many — opt-in.

RFD-0002 (foundational-ontology neutrality) holds at every layer: the substrate ships no UFO-specific content; MLT is its own discrete bundle; UFO is one foundational ontology among several. The categorization/partitioning relations originated in MLT (Carvalho & Almeida 2017), not UFO — UFO adopted them. std::mlt honors that lineage by keeping them separate from std::meta (universal) and from ufo (vocabulary-specific).

D3 — Order is derived

Order is not stamped at declaration. The elaborator computes order as a fixpoint over the instantiation closure. The direction follows Carvalho & Almeida (2017): types are strictly higher-order than their instances.

order(c) = 1 + max(order(x) for x in instances_of(c))

where instances_of(c) = { x | x : c }   (i.e., x where InstanceOf(x, c) holds)

Concretely: Dog : AnimalSpecies gives instances_of(AnimalSpecies) ⊇ { Dog, Cat, … }, so order(AnimalSpecies) = 1 + max(order(Dog), order(Cat)) = 1 + 1 = 2. AnimalSpecies is higher-order than Dog, which is higher-order than the individuals (fido, rex).

Base case: individuals are order 0; types with no instances yet are order 1 (the sup over an empty set contributes 0). The fixpoint terminates in at most |concepts| iterations (the longest possible instantiation chain).

Vocabularies can assert an order via metatype decorators:

@[order(=2)]
pub metatype higher_order_type = { … }

The elaborator validates the asserted order against the derived value. If they disagree, OE0890 fires.

For convenience, the metatype can also declare a bound:

@[bounded_order(2)]
pub metatype species = { … }

This caps the order of any concept of this metatype at 2; deeper instantiation chains through such a concept produce OE0891.

D4 — Elaboration phase

A new phase phase_mlt runs after phase_resolve (name resolution) and before phase_recognize (shape recognition). The phase:

1. Walks all emitted InstanceOf atoms and builds the instantiation graph.
2. Detects cycles. Reports OE0892 InstantiationCycle for each cycle.
3. Computes order via the fixpoint above.
4. Stores derived order in CoreConcept.derived_order: Option<u32>.
5. Validates user-asserted orders (@[order(=N)], @[bounded_order(N)]) against derived values.

The phase is per-package per RFD-0034’s composition boundary. Cross-package instantiation chains resolve at ox compose time when the workspace-level instantiation graph is assembled; the same fixpoint and acyclicity check run against the global graph.

D5 — Lean extension

A new file argon-formal/ArgonFormal/Schema/MLT.lean:

import ArgonFormal.Schema.TypeGraph
import Mathlib.Data.Finset.Lattice

namespace ArgonFormal.MLT

variable {C A : Type} [Fintype C] [DecidableEq C] [Fintype A] [DecidableEq A]

/-- The instances of `d` under an instantiation relation — concepts that instantiate `d`. -/
def instancesOf (instantiates : C → C → Prop) [DecidableRel instantiates] (d : C) : Finset C :=
  Finset.univ.filter (fun c => instantiates c d)

structure TypeGraphMLT extends TypeGraph C A where
  -- `instantiates c d` reads as "c is an instance of d" (c : d in the surface).
  instantiates : C → C → Prop
  instantiates_dec : DecidableRel instantiates
  instantiates_acyclic : Acyclic instantiates
  order : C → ℕ
  -- Types are strictly higher-order than their instances
  -- (Carvalho & Almeida 2017 axiom A-3):
  order_increases : ∀ c d, instantiates c d → order d > order c
  -- `order(d)` equals one plus the supremum of the orders of `d`'s instances.
  -- For types with no instances, `Finset.sup` on an empty set returns `⊥ = 0`
  -- in ℕ (via `OrderBot ℕ`), giving `order = 1` for leaves.
  -- This axiom is what makes `order` the canonical MLT order assignment rather
  -- than an arbitrary `ℕ`-valued function satisfying `order_increases`.
  order_minimal : ∀ d, order d
                       = 1 + ((@instancesOf C _ instantiates instantiates_dec d).image order).sup id

end ArgonFormal.MLT

The empty-Finset.sup base case uses Mathlib’s OrderBot ℕ instance (⊥ = 0), not a default := named argument. instancesOf is defined outside the structure (parametric over the instantiation relation) and referenced inside order_minimal via the structure’s own instantiates and instantiates_dec fields. Promoting order_minimal to a structural axiom (rather than an external theorem) is necessary: without it, order would be a free ℕ-valued function constrained only by strict monotonicity over instantiates, which permits arbitrary inflations like order c = 42 for all c. The axiom binds order to the canonical fixpoint.

The Lean PR that mechanizes this will need to discharge a non-emptiness or termination obligation — the well-foundedness of instantiates (guaranteed by instantiates_acyclic) ensures the fixpoint exists.

Theorems to prove:

• order_well_defined: order is the least fixpoint of the closure starting from order 1.
• order_bounded: ∀ c, order c ≤ |C| (instantiation chains are bounded by concept count).
• order_consistent_with_specialization: c <: d → order c = order d (specialization preserves order).
• instantiates_specializes_independence: instantiation and specialization are independent relations; a concept’s specializations and instantiations can be reasoned about separately.

The Rule machinery, fixpoint algorithm, and decidability theorems in the existing Lean files are reused unchanged. Rules can reference instantiates as just another relation; no rule-category extension is needed.

D6 — Diagnostic codes

• OE0890 OrderMismatch — user-asserted order via @[order(=N)] disagrees with derived order.
• OE0891 InstantiationChainTooLong — concept’s derived order exceeds a metatype’s @[bounded_order(N)] cap.
• OE0892 InstantiationCycle — concept-to-concept instantiation graph contains a cycle.
• OE0893 InstantiationOfPrimitiveMetatype — pub kind Foo : kind (instantiating the kind primitive metatype). The metatype calculus handles classification; instantiation of metatype primitives is Meta not InstanceOf.
• OE0894 InconsistentMixedDeclaration — declaration mixes inline <: and : clauses without line-break per RFD-0040 D9.
• OE0895 InstantiationFieldNotInTarget — body of pub <metatype> X : Y { … } contains field = value where field is not declared on Y and not reachable via Y’s categorization chain (D12). See D11.
• OE0896 InstantiationFieldShadows — body of pub <metatype> X : Y { … } contains field: Type that shadows a field declared on Y or on any concept in Y’s categorization chain. See D11.
• OE0897 CategorizationViolation — CL-1 fired: an instance of a higher-order type is explicitly declared disjoint from the categorized base type, contradicting CL-4’s derived specialization. Reserved in v1 (no explicit-disjointness surface yet); fires once explicit disjointness ships. See D13.
• OE0898 PartitionDisjointnessViolation — CL-2 fired: an individual is classified by two distinct instances of a partition. See D13.
• OE0899 OrderInconsistency — CL-3 fired: a concept of order N is instantiated by a concept of order ≥ N. See D13.

D7 — Migration of existing emit sites

InstanceOf replaces Instantiates. The emit sites enumerated in the IR audit:

• phase_elaborate.rs:3970 — bare variable in rule body → InstanceOf { instance: Individual(local_id), type_concept }.
• lower.rs:648, 1035, 1963 — pattern matches replaced with InstanceOf pattern matches; the EntityRef::Individual(_) arm preserves existing behavior.
• stratify.rs:113 — stratum classification reads type_concept directly.
• test_runner.rs:885, 914 — test execution dispatches on the new variant.

The old Meta lowering for Person :: Kind is kept (it’s still meta-property classification, not concept-to-concept instantiation). The :: operator continues to lower to Meta; the : operator in concept declaration heads lowers to InstanceOf. The two operators now carry distinct semantics, as RFD-0040 D5 commits.

D8 — Tonto compatibility

Tonto’s kind Dog (instanceOf AnimalSpecies) and Argon’s pub kind Dog : AnimalSpecies are semantically identical. Both lower to one InstanceOf atom with instance: Concept(dog_id), type_concept: animal_species_id.

A future ox import tonto tool can mechanically translate Tonto source into Argon source by rewriting kind X (instanceOf Y) to pub kind X : Y and similar for other Tonto syntactic forms.

D9 — @[bounded_order(n)] and unbounded chains

Practical ontologies use bounded-order MLT: order 0 (individuals), 1 (types), 2 (types of types), occasionally 3 (DogBreed : Species : Kingdom). RFD-0040 calls out tier:mlt as a reserved decidability tier; bounded-order MLT is decidable (Carvalho & Almeida 2017 prove this), and the elaborator stays within the bound for any vocabulary that uses @[bounded_order(n)].

Unbounded MLT is not decidable in general; the elaborator emits OW0420 UnboundedOrderChain as a warning when a chain exceeds a heuristic depth (default: 8) without a bound annotation. Vocabularies that want unbounded MLT can suppress the warning via @[allow_unbounded_order] on the relevant metatype.

D10 — meta() intrinsic still works

The meta(c) intrinsic — which lifts a concept’s metatype name to a queryable value — is unchanged. It returns the primitive metatype of the concept (kind, phase, relator, etc.), not the concept-of-which-c-is-an-instance. The two questions are different:

• meta(Dog) == "kind" — Dog is classified by the kind metatype primitive.
• Dog : AnimalSpecies — Dog is an instance of the concept AnimalSpecies.

A meta_concept(c) intrinsic that returns the concept(s) c instantiates is a small additional surface; it can ship in this RFD or be deferred. Deferring.

D11 — Body semantics for cross-level instantiation

The body of pub <metatype> X : Y { … } admits two statement kinds, distinguished syntactically by = vs ::

• field = value — X provides a kind-level value for field. The field must be declared on Y or on any base type Y categorizes (transitively via the @[categorizes] / @[partitions] chain — see D12). The type of value must match the declaring type’s field type. Fires OE0895 InstantiationFieldNotInTarget if the field is not declared on Y or any concept reachable through Y’s categorization chain.
• field: Type — X declares a new field on its own instances. Fires OE0896 InstantiationFieldShadows if Y already declares field, or if any concept in Y’s categorization chain declares field (no implicit shadowing through the chain either).

The two forms can mix freely in a single body. The parser distinguishes them on the = / : token. The elaborator’s field-lookup pass walks the categorization closure once before checking each assignment (the closure is finite and cached per type).

Concretely: pub kind USD : CurrencyType { iso_code = "USD", … } succeeds because CurrencyType @[categorizes(Currency)] and Currency declares iso_code. The kind-level value is recorded on USD; access via USD.iso_code (kind-level lookup) yields "USD". Without the categorization-chain lookup, this assignment would be rejected since CurrencyType itself declares no fields — that’s exactly the OE0895 false-positive D11 must avoid.

pub category Currency {
    iso_code: Text,
    decimal_places: Nat,
    symbol: Text,
}

@[categorizes(Currency)]
pub category CurrencyType { }

pub kind USD : CurrencyType {
    // kind-level values (provide values for Currency's fields, via CL-4 specialization)
    iso_code = "USD",
    decimal_places = 2,
    symbol = "$",

    // instance-level field declarations (each USD bill carries these)
    serial_number: Text,
    denomination: Nat,
    series_year: Nat,
}

Fields do not propagate downward through instantiation: an individual x : X has only the fields X declared via : (plus the fields X’s specializations carry). Kind-level fields are accessed through the type, not through the individual:

• USD.iso_code returns "USD" (kind-level lookup).
• my_twenty.serial_number returns "L12345678A" (instance-level field).
• my_twenty.iso_code is a type error — bills do not have an iso_code field at the individual level.

Kind-level field access USD.iso_code resolves directly from the kind_level_values map on CoreConcept (see Consequences for the wire-type extension). The meta() intrinsic — which returns the primitive metatype (kind, category, etc.) per D10 — does not expose kind-level field values; it answers a different question. Programmatic kind-level reflection uses a kind_level_field(c, name) operation (or the deferred meta_concept(c) intrinsic, also D10, for navigating the instantiation chain). The categorization-chain lookup ensures USD.iso_code resolves even though iso_code is declared on Currency, not on USD directly (D11 field-lookup rule).

D12 — Categorization and partitioning as substrate relations

MLT’s cross-level relations beyond instantiation are categorization (A-108) and partitioning. Both are substrate-level — they’re MLT primitives, not vocabulary-specific concepts. Add two new IR atoms:

#![allow(unused)]
fn main() {
Categorizes { higher_order: u64, base: u64 }     // A-108
Partitions  { higher_order: u64, base: u64 }     // categorizes + complete + disjoint
}

Surface admission via decorators on the higher-order type’s declaration:

@[categorizes(Animal)]
pub category AnimalSpecies { }

@[partitions(Person)]
pub category LifePhasePartition { }

Decorator form aligns with RFD-0040 D7 conventions: one block, before, comma-separated args. The decorator takes one or more concept identifiers naming the base type(s) that the declared higher-order type categorizes or partitions.

The decorators ship in std::mlt — the standard library’s MLT module. Modelers use std::mlt::* to access them. UFO and any other MLT-adopting vocabulary depends on std::mlt; vocabularies that don’t adopt MLT (BFO, DOLCE) don’t import it. The metatype assignments (category, kind, subkind, etc.) remain vocabulary-provided (ufo, bfo, etc.).

The compiler validates categorization at elaboration time:

• The categorizing type must be of strictly higher order than the categorized type (after D3 order derivation).
• Each instance of the categorizing type must specialize the categorized type (enforced by CL-1, see D13).

Partitioning extends categorization with two additional semantic claims:

• Disjointness: no individual is simultaneously an instance of two distinct subtypes that participate in the partition (enforced by CL-2).
• Completeness: every individual that’s an instance of the base type must be an instance of some subtype in the partition. Completeness is the only MLT primitive that interacts with the closed-world / open-world assumption; this RFD defers completeness enforcement to RFD-0038 (runtime capability advertisement) — runtimes that advertise CWA enforce completeness; OWA runtimes treat the partition as a witness without completeness obligation.

D13 — Cross-level enforcement rules

Four Datalog-style rules ship in the kernel as built-in cross-level inference. They fire automatically when concepts declare Categorizes or Partitions IR atoms. The rules are stratified below the user-rule fixpoint per RFD-0034 composition order.

Predicate split. The rules use distinct predicates for declared vs. derived specialization to avoid stratified-NAF deadlock between CL-4 (constructive) and CL-1 (negative check):

• declared_subclass(X, Y) — populated only from explicit X <: Y declarations.
• derived_subclass(X, Y) — populated by CL-4 from categorization.
• subclass(X, Y) :- declared_subclass(X, Y). and subclass(X, Y) :- derived_subclass(X, Y). — the union, used by queries.

The vault’s original CL-1/CL-4 pair shared a single subclass predicate, which would have made CL-1 vacuous (CL-4 fires first, CL-1’s NAF antecedent is always false). The split fixes this.

CL-4 — Categorization propagation (positive inference):

derived_subclass(?X, ?T1) :-
    categorizes(?T2, ?T1),
    has_type(?X, ?T2).

When X is an instance of T2 and T2 categorizes T1, X specializes T1 (via the derived relation). This is the rule that makes the <: Currency clause unnecessary when USD : CurrencyType and CurrencyType categorizes Currency — CL-4 derives derived_subclass(USD, Currency) automatically. CL-4 runs in the constructive stratum, before any NAF rule.

CL-1 — Categorization-disjointness conflict (A-108 violation form):

violation_categorization(?X, ?T2, ?T1) :-
    categorizes(?T2, ?T1),
    has_type(?X, ?T2),
    declared_disjoint(?X, ?T1).

Fires when CL-4 would derive a specialization but the user has explicitly declared X disjoint from T1 via an explicit disjointness declaration. Reports OE0897 CategorizationViolation as a genuine contradiction (not a missing inference). The declared_disjoint predicate is populated from explicit disjointness declarations.

Note: explicit disjointness syntax is not in the v1 surface — it’s reserved for a future RFD. Until that syntax ships, CL-1 has no firing trigger in v1; the rule structure is present so the diagnostic and rule machinery don’t need to be re-wired when disjointness lands. The NAF-vs-derivation tension is resolved by construction (CL-1 reads declared_disjoint, not subclass).

CL-2 — Partition disjointness:

violation_partition_disjoint(?Ind, ?T3a, ?T3b) :-
    partitions(?T2, ?T1),
    has_type(?T3a, ?T2),
    has_type(?T3b, ?T2),
    ?T3a != ?T3b,
    has_type(?Ind, ?T3a),
    has_type(?Ind, ?T3b).

Reports a OE0898 PartitionDisjointnessViolation when a single individual is classified by two distinct instances of a partition.

CL-3 — Order consistency:

violation_order(?X, ?T) :-
    concept_order(?T, ?N),
    has_type(?X, ?T),
    concept_order(?X, ?M),
    ?M >= ?N.

Reports a OE0899 OrderInconsistency when a concept of order N is instantiated by a concept of order ≥ N.

Wiring (per the vault’s MLT design options evaluation):

• crates/nous/src/reasoning/encoding.rs — at schema load, emit ground facts:
  • has_type(X, T) for every InstanceOf { instance: X, type_concept: T } IR atom. Both EntityRef::Individual(_) and EntityRef::Concept(_) variants produce has_type facts — this is what lets CL-rules fire on both the ABox (individual-of-concept) and the TBox (concept-of-concept) cases.
  • declared_subclass(X, Y) for every explicit Specializes { sub: X, sup: Y } IR atom (from <: declarations).
  • declared_disjoint(X, Y) for every explicit disjointness declaration (reserved for the future disjointness surface; emits nothing in v1).
  • categorizes(T2, T1) and partitions(T2, T1) for every Categorizes / Partitions IR atom (D12).
  • concept_order(T, N) for every concept whose derived order is N (D3 fixpoint).
• crates/nous/src/reasoning/rule_gen.rs — generate CL-1 through CL-4 plus the subclass := declared_subclass ∪ derived_subclass union rule.
• crates/nous/src/reasoning/profile.rs — new CompletionPhase::CrossLevelInference stratum, ordered after schema-fact emission and before user-rule fixpoint.

The existing crates/nous/src/multilevel.rs A-108 enforcement is the prototype that informed this design; it gets retired in favor of the rule-based version which composes with the existing Datalog pipeline.

D14 — Subordination reserved

MLT’s third type-of-type relation is subordination: instances of t1 specialize instances of t2, where t1 and t2 are both higher-order (same order). Formally:

$$\text{isSubordinateTo}(t_1,t_2)\leftrightarrow \forall x_1,x_2(\text{iof}(x_1,t_1)\wedge \text{iof}(x_2,t_2)\to x_1⊑x_2)$$

The decorator surface:

@[subordinate_to(VehicleType)]
pub category SportsCarType { }

Reserves the IR atom and decorator name, with no enforcement rule shipped in v1. The domain-pattern census (vault: Orca Multi-Level Domain Requirements) found zero use cases across the six order-2 patterns Orca needs. Future vocabularies that need subordination can introduce the enforcement rule incrementally — the substrate slot is held now to prevent a future syntax conflict.

Rationale

One atom, parameterized. The alternative — adding a sibling InstantiatesConcept atom alongside Instantiates — duplicates pattern-matching everywhere Instantiates is used. Generalizing the LHS to an EntityRef enum makes every pattern-match exhaustive over the cases and lets new variants (statements, reified facts) join later without further duplication.

Order derived, not stamped. Stamping order at declaration creates a maintenance burden: every concept needs an explicit order, every instantiation chain edit risks order drift. Deriving from the graph means correctness by construction. Vocabularies can still assert constraints via @[order(=N)] / @[bounded_order(N)] when they need to lock the level.

Vocabulary-neutral substrate. UFO, BFO, GFO, DOLCE have different opinions about how many levels are admitted, what powertype semantics mean, what the categorization vs instantiation distinction looks like. The substrate provides the relation and the derivation; the vocabularies layer their axioms on top via decorators (@[bounded_order(2)], @[categorizes(...)], etc.). This matches RFD-0002’s foundational-ontology-neutrality principle.

Statement(_) reserved. Higher-order reflection (querying statements about statements, e.g., RDF reification) is a real future case. Reserving the variant now means the IR doesn’t need a second generalization when that surface ships.

Cycle detection lives in the elaboration phase. Lifting it to lowering or kernel execution costs nothing in the common case (no cycles) and avoids a class of footguns. The check runs whether or not bounded-order is asserted.

Categorization and partitioning live in std::mlt, not std::meta or ufo. They are MLT primitives (Carvalho & Almeida 2017) — they originated in MLT and UFO adopted them. Putting them in std::meta would ship unused machinery for non-MLT vocabularies (BFO, DOLCE, GFO don’t have powertypes). Putting them in ufo would force any future MLT-aware vocabulary to depend on UFO or re-declare them. std::mlt honors the actual lineage: MLT is the theory, UFO is one of several vocabularies that adopt it, the stdlib bundles the MLT primitives as their own opt-in module.

The four CL rules ship in the kernel because they’re MLT theorems, not vocabulary choices. A-108 (categorization → specialization) is a theorem of MLT (Carvalho & Almeida 2017); it holds independent of UFO, BFO, DOLCE. Same for partition disjointness, order consistency, and categorization propagation. The kernel applies them universally. Vocabularies that disagree with MLT can opt out per concept via @[mlt_off] (not in v1; reserved if a real use case emerges).

Body semantics make the powertype pattern usable. The field = value form at the kind level + field: Type form at the instance level is what makes the type itself a bearer of data at the kind level — Currency’s iso_code is a property of the kind USD, not of any individual bill. Without this, MLT collapses to “instantiation as a typed relation” without the powertype-bearer structure that UFO ontologies actually use.

Subordination reserved. No domain pattern requires it. Reserving the slot now (decorator name, IR atom) prevents a future syntax conflict and signals to readers of the RFD that the MLT primitive set is complete: instantiation + specialization + categorization + partitioning + subordination, with their respective relations. Future use is additive.

Consequences

Wire types. oxc-protocol adds EntityRef, replaces Instantiates with InstanceOf, and adds the Categorizes, Partitions, and SubordinateTo IR atoms (per D12 and D14). The dual-body content for cross-level instantiation (D11) extends CoreConcept with kind_level_values: BTreeMap<FieldId, Value> alongside the existing fields: BTreeMap<FieldId, FieldDecl>. SDK regeneration via oxc-codegen is mechanical.

Storage. kernel-storage schemas referring to Instantiates in axiom-event bodies migrate. CBOR-encoded bodies for existing events continue to deserialize via a compatibility shim that wraps the old Instantiates shape in InstanceOf { instance: Individual(id), … }. No data migration required.

Lean. New file Schema/MLT.lean. No changes to existing Lean files except adding instantiates : C → C → Prop to the TypeGraph extension in MLT.lean.

crates/nous/src/multilevel.rs retires; cross-level reasoning moves to Datalog. The hand-coded A-108 enforcement is replaced by the four CL rules (D13) emitted into the standard reasoning pipeline. encoding.rs emits the categorizes, partitions, and concept_order facts; rule_gen.rs produces CL-1 through CL-4; profile.rs adds CompletionPhase::CrossLevelInference. Test cases that previously simulated cross-level via the metaxis-only path migrate to using : declarations + @[categorizes(...)] decorators.

Three-layer stdlib split. std::meta ships only the universal substrate primitives (Metatype sealed top, reflection operators meta() / ancestors() / order(), the : and <: operators). std::mlt ships the MLT primitives — the @[categorizes], @[partitions], @[subordinate_to] decorators, the cross-level IR atoms, and the four CL inference rules (D13). Vocabulary-specific metatypes (UFO’s kind, subkind, phase, role, relator, category, mixin, roleMixin; BFO’s universals; DOLCE’s perdurants/endurants) live in their respective packages. Modelers import: use std::mlt::*; use ufo::{kind, category}. Non-MLT vocabularies (BFO, DOLCE) skip std::mlt.

Book. New chapter ch02-10-multi-level-types.md. Covers the powertype pattern, the : operator in declaration heads, derived order, vocabulary constraints (@[bounded_order], @[order(=N)]), the worked example Dog : AnimalSpecies and Husky : DogBreed, and the tier:mlt decidability ladder reservation. The orphaned mlt.ar example becomes a tested showcase.

Examples. argon/examples/lease-story/packages/ufo/src/mlt.ar extends to use the new surface — pub kind GoldenRetriever <: Dog : DogBreed etc. The argufo-consolidation-fixed-kernel/v1 branch can migrate its hand-written ordering rules to derived-order constraints.

Issue tracking. A new issue tracks the Tonto import path; another tracks meta_concept(c) intrinsic if/when needed. Henrique’s MLT diagnosis (the IR audit) is the canonical closure for this work.

Tier ceiling. tier:mlt (per RFD-0040 D-references) is the reserved tier for bounded-order MLT reasoning. The decidability ladder gains this as a separate stratum from tier:fol (full first-order logic) — bounded MLT is decidable; unbounded is not.

Lean extension grows. Beyond the instantiates relation added in D5, the Lean adds categorizes, partitions, and subordinate_to as relations on the TypeGraphMLT structure, along with theorems for the four CL rules: CL-1 soundness (categorization implies specialization), CL-2 soundness (partition disjointness), CL-3 soundness (order monotonicity), CL-4 termination (the propagation rule reaches fixpoint in $|C|$ iterations). These are MLT theorems proper; the proofs follow Carvalho & Almeida (2017) directly.

Historical lineage

• RFD-0002 (foundational-ontology neutrality) — committed. MLT support stays vocabulary-neutral; no UFO axioms baked in.
• RFD-0015 (PL idiom over proof-assistant idiom) — committed. The : overload removed by RFD-0040 D5 is what unblocks the : admission this RFD specifies in concept declaration heads.
• RFD-0034 (composition pipeline) — committed. The new phase_mlt elaboration phase fits within the per-package boundary; cross-package instantiation resolves at ox compose.
• RFD-0040 (substrate atoms and the explicit-writes principle) — discussion. Commits to the IR atom generalization (D12); this RFD specifies grammar, elaboration, Lean, diagnostics, migration.

This RFD does not supersede any committed RFD.

References

• Carvalho, V. A., & Almeida, J. P. A. (2017). Multi-level ontology-based conceptual modeling. Data & Knowledge Engineering. Defines the formal MLT primitives (instantiation, specialization, categorization, partitioning, subordination, order).
• Fonseca, C. M., et al. (2021). Multi-level conceptual modeling: theory, language and application. DKE. Extends MLT with MLT* and orderless types. Orca needs only the stratified MLT fragment (max order = 2).
• Jeusfeld, M. A., & Neumayr, B. (2016). DeepTelos: multi-level modeling with most general instances. The DeepTelos approach: MLT realized as 5 Datalog rules + 1 integrity constraint (Most General Instance pattern).
• Jeusfeld, M. A., & Almeida, J. P. A. (2020). Deductive reconstruction of MLT for multi-level modeling. Proves the bridge from DeepTelos’s Datalog primitives to MLT*’s richer vocabulary.
• Brasileiro, F., et al. (2016). Applying multi-level modeling theory to assess Wikidata. Empirical evidence: 14,320+ anti-pattern instances from level confusion in a major knowledge graph; demonstrates the cost of leaving cross-level enforcement to honor-system.
• Tonto language (OntoUML DSL): https://github.com/matheuslenke/Tonto
• Issue #390 (higher-order types epic, priority:medium) — adjacent but orthogonal; this RFD addresses the foundational MLT gap.