The Argon Book

Argon is a typed knowledge graph, a rule engine, and a bitemporal store, in one language. It models a domain precisely — its concepts, the relations between them, the rules that classify and derive — and runs that model as a database that answers questions and accepts changes. Three commitments separate it from a database with a schema: the classifying vocabulary is declared in the language rather than built in, knowledge is four-valued so a missing or disputed fact has its own answer, and every model’s reasoning cost is a tier the compiler computes and bounds.

The Reference fixes the exact rules — terse, complete, anchored to the Lean mechanization; where it and this book disagree on a rule, the Reference is correct. Argon by Example holds the runnable programs, compiled and run in CI.

The model

Argon distinguishes values from individuals. A value is data — an integer, a string, a record (struct), a variant of an enum. Two values are equal when their contents are equal. An individual is an entity with identity — a person, a lease, a shipment. It keeps that identity as its data changes, and two individuals may carry identical data and remain distinct. Values are compared by structure, individuals by identity, and the type system tracks which a given position holds.

Concepts

A concept names a class of individuals and fixes the fields its members carry. Person, Employer, Obligation are concepts; Person declares that every person has a name and an age.

pub type Person {
    name: String,
    age: Nat,
}

An individual is classified by the concepts it instantiates. x : Person asks whether x instantiates Person — whether x is in that concept’s extent. Membership is either asserted as a ground fact or derived by a rule; there is no third source.

pub fact Person(alice);   // alice instantiates Person

One individual instantiates several concepts at once. The same alice can be a Person, an Employee, and a Manager simultaneously, and nothing forces those classes apart. Two concepts overlap freely unless a partition declares them disjoint — Argon never infers that membership in one excludes membership in another. A modeler who needs the exclusion states it; absent that statement, an individual sitting in two concepts at once is a fact about the data, not a contradiction.

This is the consequence that shapes everything downstream. A concept is a predicate over individuals, not a slot an individual is filed into. Reading the world means reading extents — the set of individuals each concept classifies — so rules and queries range over concepts the way they range over any relation. The fields are the data each member is guaranteed to carry; the extent is who carries it. Relations gives the relation form of the same idea, and Subtyping the rule that orders concepts by <:.

The meta-calculus

Argon ships no classifying vocabulary. There is no built-in Person, no built-in Kind, no upper ontology — only the means to declare them. A program, or a package it imports, declares the vocabulary it needs.

Three declarations form the meta-calculus:

• a metatype classifies concepts — kind, role, phase are metatypes a vocabulary might declare;
• a metaxis declares an axis along which a metatype’s concepts vary, with named values — a rigidity axis with values anti_rigid < semi_rigid < rigid;
• a metarel classifies relations, as a metatype classifies concepts.

type and rel, the introducers for a plain concept and a plain relation, are not keywords. They are declared in std::core and brought into scope with use std::core::{type, rel} or a package prelude. A program that wants the vocabulary of a foundational ontology imports the package that declares it; the language stays neutral.

The compiler never reads a vocabulary name. It does not know what kind or rigid mean. It enforces the structure the meta-calculus fixes — that a concept’s metatype is in scope, that an axis value is one the axis declares, that a relation’s endpoints carry the metatypes its metarel requires — and nothing about the names. Two metatype-level marks are the exception it acts on: abstract, which forbids direct instances, and fixed, which forbids changing an individual’s instantiation after construction. A metatype binds its axes with : — kind = { rigidity: rigid, sortality: sortal } — giving, for each axis, the value this metatype takes.

Relations

A relation is a first-class citizen, declared with rel the way a concept is declared with type. It is an n-ary edge that carries its own data, bounds its endpoints, specializes other relations, and takes part in rules — every affordance a concept has.

The data lives on the edge. An employment has a salary; the salary belongs to neither endpoint but to the relationship between them.

// A relationship that is the thing holding the data: an employment HAS a
// salary. The salary belongs to the relation, not to either endpoint.
pub rel Employment(employee: Person, employer: Org) {
    mut salary: Int,
}

Most data languages cannot say this directly. A foreign key has no identity and no fields of its own; to attach a salary you reify the relationship into a stand-in individual that exists only to hold it. Argon does not reify — the relation is the thing that holds the data.

Cardinality bounds each endpoint independently, read as UML association-end multiplicity:

// Cardinality is per endpoint, read as UML association-end multiplicity: the
// i-th bracket bounds the distinct position-i values for a fixed combination
// of the other endpoints. `[0..1]` on the owner slot means an asset has at
// most one owner; `[0..*]` on the asset slot means a person may own any
// number. The maximum is enforced at the write path; see the README on minimums.
pub rel Owns(owner: Person, asset: Asset) [0..1] [0..*];

[0..1] on the owner slot says an asset has at most one owner; [0..*] on the asset slot says a person may own any number. The maximum is enforced on every write.

Relations are not limited to two endpoints. A sale relates seller, buyer, and item at once — no intermediate SaleRecord to carry the third leg:

// Relations are n-ary. A sale relates three participants at once — no
// intermediate "SaleRecord" node is needed to hold the third leg.
pub rel Sale(seller: Person, buyer: Person, item: Asset);

And a relation specializes another, exactly as a concept does — every Internship is an Employment — so a rule that ranges over Employment tuples sees internships too. The consequence is uniformity: a relation appears in a rule body the way a concept’s extent does, with no special case for “edges.”

// Relations specialize just like concepts: every Internship is an Employment.
pub rel Internship(employee: Person, employer: Org) <: Employment;
// And relations take part in rules. `colleagues` reads the `Employment`
// relation in a rule body exactly as it would read a concept's extent.
pub derive colleagues(a: Person, b: Person) :- Employment(a, o), Employment(b, o);

colleagues reads the Employment relation as a body atom and joins it to itself on the shared employer. The full program runs in Argon by Example at first_class_relations; the precise endpoint and cardinality rules are in Relations.

Relation ends are immutable unless marked mut. An immutable binding is lifetime-bound: it leaves only through the dependent-context cascade triggered by retracting one of its individuals. The mutation forms (retract x; and the atomic set retract {x, y};), the OE1404 coverage refusal, and the remediation for a wrongly named binding are in mutate and the mutation chapter.

Specialization and instantiation

Two orderings run through the model, and conflating them is the common error.

Specialization, A <: B, holds between concepts: every instance of A is an instance of B. It is a statement about classes, reflexive and transitive.

pub type Person { name: String, age: Nat }
pub type Employee <: Person { employer: String }
pub type Manager  <: Employee;

Manager <: Employee <: Person, so by transitivity every manager is a person. <: orders the vocabulary: it lays out which classes refine which, before any individual exists.

Instantiation, x : A — equivalently iof(x, A) — relates an individual to a concept. It is not transitive, and it is what populates the order <: lays out.

pub fact Manager(dana);

dana : Manager holds by assertion. dana : Employee and dana : Person hold too — not because instantiation chains, but because specialization carries membership upward: an individual in a subclass is in every superclass. The two orderings meet exactly here. <: is the rule; instantiation is the consequence of applying it.

The extent of a concept is the set of individuals that instantiate it. extent(Person) includes dana, because Manager <: Person lifts her into it. This is the distinction that matters for reasoning: rules and queries compute over extents — sets of individuals — never over the subtype relation itself. <: decides who is in an extent; it is not a thing the engine ranges over. The subtyping rules and the upward closure of membership are specified in Subtyping; the intrinsics that read both orderings are in Reflection.

Reflection

The model is reflective: a program reads its own classification. Four intrinsics expose what would otherwise be the compiler’s private bookkeeping, as predicates a rule can range over.

• iof(x, T) tests whether x instantiates T. The rule-atom form x : T is sugar for it.
• meta(x) yields the <:-minimal type or types x instantiates — its immediate classifier.
• specializes(a, b) is the reflexive-transitive <: closure; the rule-atom form is a <: b.
• extent(T) enumerates the individuals that instantiate T.

A type used in value position is a value — a TypeRef — so these intrinsics take types as arguments and pass types as results. That is what makes them first-class predicates rather than compiler queries: a rule can quantify across types, count over them, and join them to data.

// reclassify any employee who manages someone, reading the catalog in a rule body
pub type Person   { name: String }
pub type Employee <: Person;
pub type Manager  <: Employee;

pub rel Supervises(boss: Employee, report: Employee);

pub derive promote(e) :- iof(e, Employee), Supervises(e, r), not iof(e, Manager);

promote ranges over the Employee extent, reads the Supervises relation, and tests membership with iof — including a negated membership test, not iof(e, Manager), which a non-reflective model could not phrase at all. Classification has become data the rule joins against, on the same footing as Supervises.

The consequence is that the catalog is queryable. extent(Manager) is a set a rule can count; specializes(Manager, Person) is a fact a rule can branch on. A program reasons about which types exist and how they relate, not only about the individuals under them — the foundation higher-order modeling builds on. The full signatures, the TypeRef sort, and the lowering to catalog relations are in Reflection.

Types and refinement

Every position in an Argon program has a type, and the type system answers one question at a time: may a value of type A stand where a value of type B is expected? The answer is governed by subtyping. On top of subtyping sits refinement — carving a concept into a narrower one by attaching a predicate — where the type system’s central choice falls: whether that predicate defines membership or merely constrains it.

Subtyping

A <: B reads “A is a subtype of B”: every value of A is acceptable where a B is wanted. The relation is reflexive and transitive, and two bounds frame it for every type — A <: Top and Bot <: A. Top is the greatest type, the position that accepts anything; Bot is the least, the type with no values.

Subtyping has three sources beyond the <: edges a program declares. The numeric tower is one: Nat <: Int <: Real and Nat <: Int <: Decimal hold built in, so an Int flows where a Real is expected. Collections are covariant — List<A> <: List<B> and Option<A> <: Option<B> exactly when A <: B, written [A] and A?. Everything else subtypes by equality alone: tuples, function types, and generic applications match only their own shape.

The exact numeric tower

Real, Decimal, and Money are arbitrary-precision rationals, not floating point. A source literal parses to an exact rational with no f64 round-trip, so 0.1 + 0.2 == 0.3 holds — the equality that silently fails in most languages. A sum of decimal amounts is the exact sum; division is the field operation, not a truncation.

Money sits apart from the tower. There is no implicit Int → Money: a count is not a currency amount, and the type system refuses to treat one as the other. Money arises only through monetary arithmetic, whose result-side widening runs the other way — Money ▷ Decimal ▷ Real ▷ Int — so that multiplying a Money by a rate yields Money, and the unit is never lost in a coercion. Rounding, when a domain needs it, is explicit: round_half_even(x, 2) rounds to cents banker’s-style, and like every numeric operation it stays exact — a Decimal rounds to a Decimal, never by way of a binary float.

Defined versus primitive

A refinement attaches a predicate to a concept, producing a subtype whose members satisfy that predicate. The keyword chooses what the predicate means for membership, and the two readings are not interchangeable. This is the description-logic split between a defined class and a primitive one — necessary-and-sufficient conditions against necessary-only — and Argon makes the modeler pick.

iff { P } is defined. P is necessary and sufficient: a value of the supertype is a member if and only if it satisfies P. Membership is derived. The substrate reads the underlying state, evaluates P, and classifies — the modeler never asserts membership directly.

pub type Adult <: Person iff { self.age >= 18 };

Any Person whose age is at least 18 is an Adult, automatically. To make someone an Adult you change their age; the classification follows. Asserting membership by hand — insert iof(p, Adult) — is rejected (OE0211), because for a defined concept the predicate is the source of truth, and a manual assertion could contradict it.

where { P } is primitive. P is necessary only: every member satisfies it, but satisfying it does not confer membership. Membership is asserted — conferred by construction or by an explicit insert iof — and P is enforced as an invariant at each membership write, never as a filter that widens the extent.

pub type Cleared <: Person where { self.clearance_score >= 50 };

A score of 50 or more does not make a Person Cleared. Clearance is granted by an authority; the where predicate is the standing guarantee that anyone granted it meets the bar. A grant to someone below the threshold is rejected (OE0668) — the invariant holds on every member — but a qualifying score sitting in the data confers nothing on its own. This is Rust’s where bound lifted from a function to a concept’s members: a constraint, not a definition.

The contrast is sharpest on a single population. Give four people ages over 18 and a clearance_score field; one of them, never granted clearance, carries a score of 70. The Adult extent is all four — iff classifies from state. The Cleared extent is only those granted — where confers nothing from the qualifying score alone. The same data, two opposite disciplines, chosen by one keyword. Argon by Example works this through in primitive_refinement.

A predicate may read several fields and combine them with &&, ||, and comparisons — iff { self.age >= 18 && self.status == "active" } defines an active adult — and it evaluates on the same exact value tower as every other value position: exact rationals for Real, Decimal, and Money, chronological comparison for dates.

Three-valued field access

A refinement predicate reads a field, but a field may have no recorded value, and Argon does not pretend otherwise. How a missing field reads is fixed by how the field is declared.

A required field f: T that has no recorded value reads unknown — the third truth value, distinct from both true and false. A predicate that reads it cannot evaluate to a definite verdict, so it too is unknown. An optional field f: T? reads None when absent, a positive value the predicate can match on. An epistemic field f: Truth4Of<T> carries its own uncertainty and reads unknown directly when unrecorded.

What that unknown then does depends on the concept’s world assumption, and the two refinement disciplines read it as exact mirror images:

• Under a defined iff, membership requires positive evidence that the predicate holds. An unknown predicate does not classify — a value whose deciding field is unrecorded is neither in the extent nor an error, simply not yet a member. This matches SHACL’s violation discipline and SQL’s three-valued NULL.
• Under a primitive where, the invariant rejects only on positive evidence of violation. A write is refused when P evaluates to a definite false; an unknown permits it, because absence of information is not a violation.

Under the closed-world default, that unknown collapses to false — the regime that makes “not in the extent” mean “false”. A concept that models incomplete knowledge, where absence means unknown rather than false, opts into the open-world reading, where unknown is preserved as its own answer.

One distinction the substrate keeps sharp: unknown means information absent — a field with no value. A predicate that cannot be evaluated at all — an unsupported form, or a type-mismatched comparison like ordering a date against an integer — is not unknown. Unsupported forms are refused at build (OE0660); anything that reaches runtime fails loudly. The system never silently permits a where write or silently empties an iff extent on a predicate it could not run.

Narrowing

Inside a rule body, a guard that establishes a fact about a value refines that value’s type for the rest of the body. After x.field is not unknown, subsequent atoms read x.field as present; after a type test x: Employee succeeds, x carries Employee thereafter. This is occurrence typing — the type at a use site reflects what has been proven about the value on the path that reaches it.

The discipline is sound because narrowing predicates are upward-closed in information: once established at a state, a narrowing survives every state that carries more information. Gaining facts can extend what is known; it can never retract a narrowing already in force. The mechanization proves exactly this — every narrowing predicate holds monotonically as the state grows — which is what lets the type system trust a narrowed type through the rest of a body.

Reasoning

A store that only holds the facts you put in it is a database. Argon derives new facts from stored ones, answers questions over both, and changes stored state — all through one atom, the rule, which comes in five modes. The modes form a ladder from pure computation to the single mode that writes:

• fn — pure computation over its arguments, no state at all.
• derive — defines a derived relation by a rule.
• query — reads stored and derived facts, returns a typed value.
• check — observes the state and emits diagnostics, writes nothing.
• mutate — changes stored facts. The only writer.

derive and check are written in the Datalog register — :- reads “if”, a comma reads “and”. fn, query, and mutate use ordinary expression syntax. The reference fixes the exact grammar of all five in the rule atom.

Derivation

derive

A derive rule defines a relation by a condition instead of by listing its members. The head holds for any binding of the variables that makes the body hold:

senior(p) :- p: Person, p.age >= 65;

senior(p) holds for every Person whose age is at least 65. Two properties take this past a stored view.

A rule may name itself, so a relation can recurse. Transitive closure is the canonical case — reachability over a directed graph, computed from a base case and a recursive step:

reach(x, y) :- edge(x, y);
reach(x, z) :- reach(x, y), edge(y, z);

The first rule is the base case: a direct edge is reachable. The second recurses — if x reaches y and an edge runs from y to z, then x reaches z. Rules with the same head and arity combine by union, so the two clauses together define reach as “a direct edge, or one edge past something already reachable.” Over the chain a → b → c → d the closure is the six reachable pairs, including the three the base edges never state. This is the computation plain SQL joins cannot express and recursive SQL strains to.

A rule body may also negate — not P — and may quantify, compare, and aggregate. Every body must be range-restricted: each variable in the head, in a negated atom, or in a comparison must be bound by some positive atom in the body. An unbound variable would project nothing meaningful, so an unsafe rule is refused at build (OE1303) rather than silently producing a wrong answer.

The stratified fixpoint

A set of derive rules computes by a fixpoint, and the substrate proves both that it terminates and that the answer is unique. The engine tracks, for each predicate and individual, a three-valued status — is, not, or can (unknown) — starting with everything can and filling in the other two. Rules fall into three internal categories the modeler never writes but whose separation explains the guarantee:

• Positive rules only ever turn can into is.
• Negation rules — those using not — read a finished positive result and turn can into not.
• Constraint rules observe and emit diagnostics; they change no status.

Predicates are sorted into strata by their dependencies. Within a stratum the engine runs every positive rule to a fixpoint, then applies negation once against that completed result, then moves up. Termination follows from monotonicity: positive work only adds is, negation only adds not, and doing all the positive work before any negation keeps the two from contradicting each other. The count of remaining can values strictly decreases, so the process halts in a bounded number of steps with one answer. The Rust engine runs this as a semi-naive evaluator.

Recursion through negation

Stratification handles negation that crosses between strata — one predicate’s negation reading another, already-finished one. Negation inside a cycle it cannot: p :- not q together with q :- not p has no stratified answer, because whichever rule runs first decides the result. Argon does not reject such a program. It falls to well-founded semantics — the Van Gelder–Ross–Schlipf alternating fixpoint — under which a paradoxical atom comes out undefined: neither asserted nor denied. An undefined atom does not fire.

This is not a corner case to be tolerated; it is how arbitration is modeled. Argon by Example schedules a robot’s plan in robot_plan_execution, where two conflicting actions cannot both run. An action is scheduled when it is applicable and not challenged; an action is challenged when a conflicting action is itself scheduled. So scheduled recurses through its own negation by way of challenged — exactly the win-move game on the conflict graph — and the two predicates form one negation-cyclic component the engine evaluates by well-founded semantics. An asymmetric conflict, where one action has priority, resolves to a definite winner: the uncontested action is scheduled and its rival is challenged and absent. A symmetric conflict, two actions deadlocked with no tiebreak, is undefined under the well-founded model — both are absent from scheduled and from challenged, the observable signature of a standoff.

The well-founded model is three-valued; the current surface is two-valued. The engine materializes the definitely-true extent, the sound projection for conditional obligations. Surfacing undefined as a distinct query result is a later increment, which the reference tracks under derive. A second semantics, stable models behind a #[brave] attribute, is designed but not built — writing the attribute refuses loudly today rather than parsing green and doing nothing.

Bounded universals and aggregates

A rule can demand that every element of a domain satisfy a condition. forall f: Fluent where pre(a, f), holds(f) holds for an action a exactly when every precondition of a holds initially — the genuine universal, not “some precondition holds.” It lowers to a count-equality: the number of preconditions that hold equals the number of preconditions, so an empty domain is vacuously true. The reference gives the encoding under derive.

A body can also count and compare. exists { Person(p) } is the bare Boolean form, true when the body has any solution at all. count { Person(p) } >= 3 binds a cardinality and filters on it. The comprehension forms — sum, min, max, avg, and count with a projection — also run in derive and query bodies, and because an aggregate is a bindable expression, two of them can be compared directly. Argon by Example classifies a workforce by cardinality in aggregate_count_v0 and totals ledger postings in double_entry_v0.

Queries

A query runs a read and returns a typed value; it never writes. The common form names a relation or a concept, and the return type dispatches the read — a query returning a concept returns that concept’s extent:

pub query adults() -> Adult;
pub query closure() -> reach;

adults() returns every individual classified Adult; closure() returns the computed reach relation. Richer projection, filtering, and ordering have a fuller surface under query in the reference.

Mutation

Everything above reasons over a fixed set of facts. mutate changes them, transactionally — it is the only mode that writes. The reliable, widely-used form is a Datalog-style body of operations:

pub mutate openAccount(a: Account, name: String) {
    insert iof(a, Account);
    update a: Account set { name = name };
}

insert iof(a, Account) records that a instantiates Account; update a: Account set { … } writes its fields. The body’s operations are insert iof, inserting a relation tuple, update, delete, and forget. insert iof(a, Account) is permitted because Account’s introducing metatype is not declared fixed: dynamic classification is the default, and the engine enforces the declared fixed and abstract modifier bits rather than reading any axis name.

Argon also has a richer imperative body — require guards that abort the whole mutation on failure, let bindings, an effectful if, typed-literal construction with a system-minted identity, field navigation, exact arithmetic, collection inserts paired with for, and match over constant patterns in both value and statement position. Its core executes today; the build refuses loudly on the forms that do not yet run, so a program never relies on a mutation that would die at runtime. The reference fixes the full imperative surface and its current status under mutate.

A mutation is atomic. A failed require guard, or any error during the body, commits nothing.

Individual retraction uses retract x;; several individuals form one atomic set with retract {x, y};. Retraction ends those individual lifetimes and cascades incident relation bindings when every immutable end’s dependent context is covered by the same set. A retraction is logical cessation, not erasure: the pre-retraction extent stays queryable bitemporally — the store retains what was.

Retraction — when a thing ceases

The right occasion for retract is narrow: an individual has genuinely ceased to exist in the domain. Its constitutive bindings — the immutable-ended relations that were about it — end with it, by cascade. That is the only lawful way an immutable binding leaves the store, and retraction is what fires it.

The canonical case — the passport is destroyed

A passport is issued to exactly one holder for the passport’s whole life: issuedTo fixes the holder end (no mut). The holder never changes; the only honest end of the binding is the passport ceasing to exist. Destroy the passport and its frozen issuedTo binding cascades away with it — the person it was issued to is untouched.

pub type Person;
pub type Passport;

// The passport's holder is constitutive: fixed for the passport's life.
pub rel issuedTo(mut passport: Passport, holder: Person) [0..*] [1];

pub mutate issue(p: Passport, h: Person) {
    insert iof(p, Passport);
    insert iof(h, Person);
    insert issuedTo(p, h);
}

// The passport is destroyed — it leaves the domain.
pub mutate destroy(p: Passport) {
    retract p;
}

Issue passport p1 to alice, then destroy p1. The Passport extent empties; alice survives in the Person extent; the issuedTo(p1, alice) binding cascaded away with the passport it was about:

── before: issue(p1, alice) ────────────────
query passports: 1 row(s)   (p1)
query people:    1 row(s)   (alice)

── after: retract p1 ───────────────────────
query passports: 0 row(s)
query people:    1 row(s)   (alice)

The binding did not have to be deleted — it could not be (delete issuedTo(p1, alice) refuses OE1402, an immutable end). Retracting the passport is the lawful exit, and the history of the issuance remains readable at any prior transaction time.

Notice which individual was retracted. The natural targets of retract are artifacts and dependents — a destroyed passport, decommissioned equipment, a terminated contract, a dissolved marriage — things whose constitutive bindings should die with them and onto which nothing else’s frozen bindings point. Retracting a person is usually the wrong instinct: people are what everything else’s constitutive bindings are frozen onto (a child’s bornTo, a passport’s issuedTo), so a person’s cessation drags every dependent into the retraction set — which is exactly the OE1404 friction below, and it is friction by design. A person who dies, emigrates, or closes an account has changed state, not stopped being an entity the model tracks; those are facts to assert, not retractions.

Nor is retract how you record damage or loss while you still care about the object. If the domain keeps answering questions about the thing in the present — is this passport valid? damaged? when was it reported lost? can it be reinstated? — then the thing is still an entity and its condition is ordinary state: insert iof(p, Damaged) (or a status property), leaving the passport addressable for repair, claims, and audit workflows. retract p is for when the model should stop tracking the identity in the present tense — present-view queries no longer return it, its cardinality slots free up (the holder could be issued a replacement passport where [0..1] would have blocked a second live one), and no future fact can be asserted about it. The pre-retraction history still answers as_of questions either way; the discriminator is whether you need to say new things about the individual going forward. Damaged means yes; destroyed means no.

When the set is incomplete — OE1404 and its remedy

Retract too little and the build refuses. A child’s birth-mother is constitutive (bornTo fixes the mother end); a mother’s set of children grows over her life (mut child). Retract the mother alone while a child survives, and her child’s frozen bornTo binding would strand — the individual it depends on, the child, is still here:

pub rel bornTo(mut child: Person, mother: Person) [0..*] [1];

pub mutate retractMother(m: Person) {
    retract m;              // OE1404 while a live bornTo(child, m) child survives
}

The refusal names the stranded end and the surviving dependent context, and hands you the completed retraction verbatim as a remedy: line:

OE1404: retracting `alice` would strand the immutable `mother` end of
`bornTo` — its dependent context (child=`childB`) still survives — an
immutable end stays fixed for the life of its dependent individuals, so
ending it needs at least one dependent-context individual to cease in the
same operation. Retract the dependent individual(s) so the binding retracts
by cascade; or, if this end is genuinely rebindable, declare it `mut`.
remedy: retract {alice, childB};

The remedy: line is the completed set — the individual you named plus every dependent-context individual its retraction would strand, iterated to the fixed point (if pulling in childB stranded her dependents, they would be in the line too). Paste it back to say exactly what the coverage rule needs:

pub mutate retractBoth(m: Person, c: Person) {
    retract {m, c};        // one atomic set covers the mother AND her child's context
}

The set is atomic: coverage is checked once over the whole set, so mother and child cease together and no binding strands. This is what makes the OE1404 message legible — it is asking you to complete the set, and retract {…} is how you say it.

These are invocation-dependent examples (OE1404 needs a pre-existing live tuple, so they are marked ignore), but the coverage rule they show is live: forget m; will not sidestep it either — erasure runs the same coverage gate and refuses while the dependent context survives.

A retraction set may span several statements

Two retract statements in one mutate body union into one cessation set, checked by one coverage gate — the remedy above must be expressible compositionally (a retract inside an if branch, a for body, or a match arm joins the same union):

pub rel bindsSpouse(mut marriage: Marriage, spouse: Person) [0..1] [2];

// A marriage's two spouse bindings are constitutive; the marriage is their
// shared dependent context. Retracting the marriage and both spouses in
// separate statements is ONE set — coverage holds over the union.
pub mutate dissolve(m: Marriage, s1: Person, s2: Person) {
    retract {m, s1};
    retract s2;
}

Retract is one of four lifecycle verbs

retract is not the tool for most changes. Reach for it only when an individual has ceased. The sibling verbs cover the other three shapes. The four occupy exactly one cell each of a 2×2 — grain (what the verb removes) against the nature of the removal: delete and amend work at the fact grain (a tuple that was true-then vs. one that was never-true), while retract and forget work at the entity grain (logical removal from the model vs. physical removal from the store).

amend targets a directly-asserted relation tuple — never a derived conclusion (you amend the premises, not the conclusion: a derived target refuses OE1406), and, as implemented, never a classification or property value. It corrects an asserted fact, not a relation: it never touches the relation’s declaration, its other tuples, or the participating individuals. All four verbs — delete, amend, retract (with its OE1400 guard), and forget — are enforced on this toolchain; amend is specified in RFD 0076 and realized by this change. The four differ in which view changes: delete moves valid time, amend corrects the belief record — both at the fact grain, both retaining queryable history — retract ends a lifetime and its cascade, and forget alone removes bytes from the served store.

The entity-grain cell has two verbs, not one, and the split is deliberate — retract exists in addition to forget on three axes. History: retract is logical, so the pre-cessation extent stays bitemporally queryable — audits and as_of reconstructions read the retained trail, and in regulated domains retaining superseded records is a legal requirement; were forget the only removal, ordinary cessation would destroy the very trail audits exist to read. forget physically erases the served record (leaving a tombstone in the durable journal). Privilege: forget is capability-gated as the right-to-erasure / compliance channel; retract is an ordinary statement, because ending an entity’s lifecycle is ordinary domain logic — were forget the only removal, every workflow that ends an entity would need the erasure capability, a privilege-escalation antipattern. Meaning: a retract is an event in the record (“ceased, and here is when”), so derived views and the amendment plane’s corrected view compose with it; forget removes the record-keeping itself (“no longer allowed to know”), and those same views are definitionally blind to a forgotten individual afterward. The two are not rivals: forget runs the same OE1404 coverage gate as retract, so it is strictly retract + physical destruction + a permission check — never a bypass of retraction’s semantics.

Everything in the system is bitemporal except what forget has touched, on two layers. At the query surface, forget destroys its target’s bitemporality by design: the axiom events and their bitemporal history are gone from the served store, so an as_of reconstruction — “what did we believe about x last March?” — returns nothing. That is the erasure contract, not a limitation: right-to-erasure requires that historical reconstructions stop answering, which a bitemporal retraction cannot deliver — after retract x, the same as_of query still answers in full, because a retraction is an ordinary event in the bitemporal record. At the storage substrate, the durable replay journal retains the erased events’ bytes closed alongside a tombstone — an append-only-durability necessity, not queryable history: no query path reaches those bytes, and replay reads the tombstone to re-erase so crash recovery is deterministic. (A regime requiring physical destruction of even those closed bytes is a storage-lifecycle / compaction concern, not language semantics.)

Retraction is not death. Ceasing to be alive is ordinary state — a fact you assert (insert iof(alice, Deceased)), and it leaves every proposition that was true of her, bornTo included, standing in both history and the present view: a dead mother is still someone’s mother. Ceasing to be an entity — the identity itself leaving the domain — is retract. The two are orthogonal, and only the second fires the cascade.

One record, four fates. A single bornTo fact routes to a different verb depending on what went wrong:

• The record was wrong — the birth was logged with a mother who was never this child’s mother (or was never a real individual at all). It was never true, so it is a belief-time correction: amend bornTo(child, wrong) => bornTo(child, right), or a standalone withdrawal amend bornTo(child, wrong) when there is no replacement. The child is untouched; the amended proposition returns to unknown — an uninitialized fiber is the legal “not yet recorded”, not a refutation — and the end-freeze releases as if it had never been set, so a later insert bornTo(child, right) admits where it would have refused OE1403. With the false tuple withdrawn, retract wrong alone is now admitted: coverage reads the net corrected view, where the amended tuple is no longer incident, so nothing strands — the exact refusal (OE1404) that retracting the mother alone drew before the amendment. Retraction without the amendment would be a lie (the child did not cease; nothing ended).
• The thing ceased — the mother genuinely leaves the domain, taking that whole branch with her: retract {mother, child} (the set covers her child’s constitutive context, per OE1404; her other constitutive bindings need their contexts in the set too). If she died but the child lives on, this is not the case — that is the Deceased fact above, not a retraction.
• The subject invoked erasure — a compliance request to remove a person’s data: forget subject, under #[allow_forget]. This is capability-gated physical erasure, reserved for privacy/compliance — not the everyday cessation channel.
• An association simply changed — a toy is given away. ownedBy(mut toy, mut owner) is a pure association, both ends mut, so it is neither retraction nor amendment: delete ownedBy(toy, kid); insert ownedBy(toy, newKid);. Direct tuple rebinding is admitted precisely because every end is mut.

The amend semantics described above are not sketch: they are fixed by the canonical design record — RFD 0076 and its mechanized amendment suite in the Lean substrate — so the belief-time reading, the OE1405/OE1406/OE1407/OE1409 refusals, and the net-corrected-view coverage stated here are specified, not provisional. The surface implementation that enforces them is present on this toolchain, so the amend-dependent steps above run. Because the design record governs the semantics, this description cannot silently drift from the shipped behavior.

The resurrection guard — OE1400

Retract an individual and then re-introduce it in the same transaction — re-classify it, name it at a relation endpoint, or write a property of it — and the whole transaction refuses:

pub mutate resurrect(p: Passport) {
    retract p;
    insert iof(p, Passport);   // OE1400 — p was retracted earlier in this transaction
}

OE1400: retracted individual `p1` was re-introduced: still classified as `Passport`.

The cascade released p’s constitutive bindings on the premise that p was gone; naming p again after that, in the same commit, would falsify that premise after the fact. (An assert-then-retract nets clean and is admitted — the retraction sweeps the earlier assertion.) The lawful form is a later transaction: once p is genuinely retracted, a subsequent transaction may re-introduce the identity, where the ordinary immutable-fiber freeze — not the resurrection guard — governs any re-asserted binding as a replacement assertion.

Checks

A check observes and reports; it never changes state. When its body holds, it emits the diagnostic on the right of =>. This is how an integrity rule flags a violation instead of silently repairing it. Double-entry accounting has one invariant — within every journal entry, total debits equal total credits — and it is a single check comparing two aggregates:

pub check EntryNotBalanced(e: Entry) :-
    e: Entry,
    debits  = sum(p.amount for p in Posting, inEntry(p, e), p.side == "D"),
    credits = sum(p.amount for p in Posting, inEntry(p, e), p.side == "C"),
    debits != credits
    => Diagnostic {
        severity: Severity::Error,
        code:     "Ledger::E001",
        message:  "journal entry is not balanced",
    };

Each sum totals one side of the entry; debits != credits fires the diagnostic. A balanced entry derives nothing.

Where a check discharges is decided by what its body reads, not by an annotation the author writes. A catalog-level check — every variable reflective-sorted, reading declaration structure like specializes or implements — discharges at ox check and ox build, because the declared catalog is closed at build and evaluation there is final. This is the user-extensible compiler-diagnostic mechanism: a vocabulary package ships its modeling constraints as check rules, and they surface under the package’s own codes like any built-in diagnostic. An instance-level check — any variable ranging over individuals — discharges at runtime, on every mutation boundary, as a delta guard: it rejects a mutation that creates a violation while leaving a pre-existing one to be reported, not blocked. The guard is over the change, not the absolute state.

Severity decides the consequence. Because EntryNotBalanced carries Severity::Error, an unbalanced posting is rejected, not merely reported — at build a firing error writes no artifact, and at runtime it aborts the offending mutation atomically. Double-entry is enforced at the rule layer, not left to a downstream report. The mechanization proves the two halves that make this trustworthy: a catalog-closed check evaluates identically at build and against any extending store, and the runtime guard passes exactly when the mutation introduces no new violation. Argon by Example carries the worked check packages — double_entry_v0 and check_constraints.

Traits

A trait names a contract a type can implement, in the style of Rust traits — but its implementations are rules, not methods. The fourth atom is a rule-plane construct: a trait declares one or more rule heads, and each impl … for T supplies a clause for a specific type. The clauses for a given head union exactly as same-head derive clauses do, so the implementations behave as one rule with per-type behavior:

pub trait Inspectable {
    derive Due(Self);
}

impl Inspectable for Truck { derive Due(t: Self) :- t.hours >= 100; }
impl Inspectable for Crane { derive Due(c: Self) :- c.hours >= 50;  }
impl Inspectable for Drone { derive Due(d: Self) :- d.hours >= 10;  }

Dispatch is not a vtable lookup; it is derivation. The reasoner fires whichever per-type clauses match, so a query over Due returns every asset past its own kind’s threshold — three clauses, one head, per-kind thresholds. A trait may require another, Rust’s supertrait bound: trait Serviceable: Inspectable makes implements(t, Serviceable) entail implements(t, Inspectable), and the reflective surface — implements(t, Trait) as a body atom — ranges over the catalog like any other relation.

Conformance is checked at the catalog layer. A #[static] check whose variables are all reflective-sorted — a TypeRef ranging over the type catalog, reading specializes and implements — discharges totally at ox check and ox build, with no instances. So a package can demand that every kind under a category implement a contract and have the demand settled at build:

#[static]
pub check EveryAssetKindIsInspectable(t: TypeRef) :-
    specializes(t, Asset), t != Asset,
    not implements(t, Inspectable)
    => Diagnostic { severity: Severity::Error, code: "Fleet::E010",
                    message: format!("{} must implement Inspectable", t) };

The check fires on any asset kind left uncovered and refuses the build before an artifact is written; #[static] makes instance-vocabulary drift a hard error rather than a silent reclassification. A trait is not a concept — it carries no extent and classifies no individual — so a bare trait-head atom over a type only partially covered is itself a build error unless the author writes the coverage-can-fail branch explicitly, never by silence. Argon by Example works a fleet under trait contracts in trait_contracts. The reference fixes the trait surface and its conformance discipline under the trait atom.

Truth under incompleteness

A model assembled from partial, sometimes-conflicting sources cannot answer every question true or false. Some facts are unrecorded; some sources disagree. Argon does not paper over either case. An answer is one of four values, the world a concept lives in decides what a missing fact means, and a rule may carry exceptions without ever lying about what it derives.

Four values

A query returns is (true), not (false), can (unknown), or both (two sources disagree). The four are the values of the FDE bilattice — Belnap’s four-valued logic, the Truth4 carrier of the reference, truth values. They order two ways at once: by truth, not < can,both < is, and by information, can < is,not < both. is and not are the classical pair; can is the absence of evidence; both is the presence of conflicting evidence.

can and both are answers, not errors. If a model does not record Alice’s age, “is Alice an adult?” is can — unknown, a value a query can return and a caller can match on, distinct from a definite not. If one registry asserts she is a person and another denies it, a query that combines them is both. Neither collapses into a guess.

A single coherent line of reasoning never produces both. A derive fixpoint (Reasoning) tracks the three consistent values is, not, and can; both arises only where federation joins disagreeing standpoints, below. At a Boolean decision point — a where guard, a Boolean projection — can collapses fail-closed to false, the closed-world reading. To keep can and both distinct at the surface, a query declares its return type as Truth4Of<T>; otherwise the projection folds them away.

Worlds

The closed world

A world assumption decides what the absence of a fact means. Under the closed-world assumption an absent fact is false: if a membership is not derivable, it does not hold. Under the open-world assumption an absent fact is unknown: absence is the lack of evidence, not its denial. The reference fixes both under world assumptions.

Argon is closed-world by default. A program is a data system whose extents are the authority for what is true, and closed-world is the regime that makes “not in the extent” mean “false” rather than “not yet known”. With Alice’s hours unrecorded, “is Alice a FullTime?” is not — she is not a full-timer until her hours say so. A package may set its default_world in the manifest, but every concept without an explicit mark inherits the closed default.

A concept whose knowledge is incomplete by nature opts out, one concept at a time, with #[world(open)]:

#[world(open)]
pub type LegalAgent { mut name: String }

The attribute is executed, not decorative. The elaborator reads the policy word — open or closed, any other word a loud refusal — records the concept’s world on a per-concept map keyed by its qualified path, and the reasoner stamps that map onto every evaluation. Each negated membership atom is then read under its own concept’s world. The attribute is concept-only; placing it elsewhere is rejected.

World-honest negation

Negation-as-failure is the closed-world inference: not P succeeds when P is not derivable. Under an open-world concept that inference is unsound — an absent P(x) is unknown, not a definite not, so reading the absence as false would assert more than the evidence supports.

Argon refuses to draw the unsound conclusion rather than draw it silently. A closed-world not H whose derivation depends on an open-world concept’s negation does not get to read that unknown as false; the substrate refuses the shape at ox check and ox build with OE1367. The fix is stated in the diagnostic: mark H’s concept open-world too, so not H tolerates the unknown, or restructure so the open-world negation never flows into a closed-world-negated head. The default stays closed-world for every concept without the mark. R(args) is unknown reads only R’s completed well-founded-undefined rows; it does not enumerate ordinary open-world absence. A recursive read before R completes refuses with OE1441. This is world-honest negation-as-failure: the engine honors each concept’s mark instead of evaluating closed-world unconditionally.

The same honesty reaches the test surface. assert derivable F(x) and assert not derivable F(x) read F’s world directly. A present row is a definite pass or fail; an absent row under the closed world is definite non-derivability; an absent row under an open-world concept is unknown, so closed-world non-derivability is not assertable — the runner reports a distinct, loud INCONCLUSIVE, never a silent pass.

A CWA-true result lifts safely into an open-world consumer: positive evidence stays positive when more information may yet arrive. The Lean mechanizes this transfer (cwa_owa_transfer, cwa_isCwa_preserved_under_info_increase) and proves the reverse unsound (owa_to_cwa_not_sound) — a conclusion that holds only by collapsing an unknown to false does not transfer the other way. The full three-valued lift of open-world membership into downstream derive heads — letting an open-world can row materialize in a derived extent — is the well-founded-semantics catch-up; today the substrate refuses the unsound interaction rather than evaluating it. The wired surface is negation-as-failure, the structural write-side guards, and the derivability test.

Defeasibility

Real rules have exceptions. Adults may vote, unless they are felons, except for certain special classes. A node is presumed flagged, unless something clears it. Classical Datalog has no room for this; Argon makes it first-class without letting any rule lie about what it derives. The reference fixes the design under defeasible reasoning on three commitments: a rule derives exactly what its head says, the attack between rules is a directive rather than a clause, and the meaning of a defeasible program is its compilation onto the core fixpoint. RFD 0028 — Defeasibility redesign: honest heads, the defeat-directive plane, and strategy as a compilation scheme records the design decision.

A rule comes in one of three strengths. An unmarked derive rule is strict — classical Datalog, unattackable; adding more rules can only add its conclusions. #[default] marks a clause defeasible — it holds unless an applicable attacker blocks it, the reading of Rust’s default fn. A defeater is an ordinary rule whose body, when it fires, blocks a target conclusion; it carries #[defeats(target(args))], and in the degenerate case where no one reads its own head it does nothing but block. #[label(name)] gives a clause an identity so an attack can name it.

The franchise model reads true at every line. Special-class members vote by a strict clause; adults vote by a defeasible one; felons are an exception with its own honest head:

pub derive can_vote(p) :- SpecialClass(p);          // strict, unattackable

#[default]
#[label(adult)]
pub derive can_vote(p) :- Adult(p);                 // defeasible default

#[defeats(can_vote(p))]
pub derive disenfranchised(p) :- Felon(p);          // the attack is a directive

No rule spells out the head it denies. The exception lives under its own name, disenfranchised, and the attack rides the directive above it. Because the #[defeats] argument resolves against the attacker’s own variables, the block is per-tuple: disenfranchised(p) blocks can_vote for exactly the p it derives, not the whole head. A #[defeats] argument bound in neither head nor body is a loud error, never a fresh variable. The strict clause is out of reach — a special-class felon still votes, because the attack resolves only against the defeasible adult clause. Targets are resolution-checked at elaboration, so an unresolvable or strict target refuses rather than misfiring, and a cycle in the attack graph is refused outright rather than resolved by a silent choice.

A tuple survives when some clause not attacked on it derives it — team defeat: an unbeaten teammate keeps the conclusion. A blocked tuple is simply absent from the extent; it does not propagate a third truth value downstream. Every later rule reads that post-defeat extent, even through strict intermediate rules. Marking a later reader #[default] makes that reader overridable; it does not restore blocked input rows. With no attacker on the reader, it returns the same rows as an otherwise identical strict reader. Defeaters can themselves be defeated. A pardon that defeats a disenfranchisement restores the vote: the #[defeats] rule is itself #[default] and attacked in turn, and as long as the chain bottoms out the pardoned felon’s can_vote returns. The block is computed from each attacker’s surviving extent, so a defeated defeater stops blocking exactly where it was beaten.

The strategy that runs is Governatori-style defeasible logic with explicit superiority and ambiguity blocking, compiled in three strata — support, then blocking from surviving attackers, then a team-defeat fold — onto the same stratified and well-founded engine of Reasoning. No separate reasoner runs; the engine stays strategy-blind, and the strategy’s identity is recorded in the built artifact so it is honest about which compilation gave it its meaning. The Lean proves the defeat algebra over each clause’s converged contribution: the team-defeat fold equals the declarative warranted set (compiled_extent_eq_warranted), strict clauses are unattackable, ambiguity blocking holds, and a defeated defeater no longer blocks (defeated_defeater_does_not_block). What the Lean does not yet re-prove is the correspondence for a recursive clause’s fixpoint under defeat; that rests on the differential-oracle corpus, where a transitive closure under a live defeat plane returns its full extent and a pardoned felon regains the vote.

Proof tags

Every derived fact carries a proof tag, surfaced through the provenance channel by ox derive --explain. +Δ marks a conclusion definitely provable — supported by a strict, unattackable clause. +∂ marks one defeasibly provable — supported by a surviving default clause after defeat resolution. Their negatives, −Δ and −∂, mark definite and defeasible refutation. The tag is the difference between a fact that holds come what may and one that holds only because nothing beat it:

$ ox derive examples/legal_norms_can_vote can_vote --explain
  +Δ (dave)     // strict special-class clause
  +∂ (alice)    // surviving adult default

A defeasible model reports not only what survived but on what strength, so an answer that looks wrong is something to investigate rather than accept.

Composition

A model is rarely one file by one author. It draws on vocabulary from a foundational ontology, regulations from one source and facts from another, viewpoints that need not agree. Argon composes these along two axes. Standpoints hold viewpoints that may disagree and join them by the four-valued logic. Modules and packages carry code and vocabulary across boundaries, with the imported theory shaken down to what the importer actually uses and proven to preserve every conclusion about it.

Standpoints and federation

Standpoints

A standpoint is a named viewpoint. Items declared inside a standpoint s { … } block belong to s and are addressed as s::Item. Standpoints form a lattice ordered by <: — California <: USFederalTax places California below federal tax in the lattice. The order declares federation membership, the set a query may draw across; it is not namespace inheritance, so a child standpoint sees a parent’s items only through an explicit use. The reference fixes the surface under standpoints and federation.

A fact asserted inside a standpoint block is local to that standpoint. A not_fact is strong negation — an explicit denial, not the mere absence of an assertion. Two registries can hold flatly contradictory records:

pub standpoint historical {
    pub fact Person(alice);
    pub fact Person(bob);
}

pub standpoint public_record {
    pub not_fact Person(alice);
    pub not_fact Person(carol);
    pub fact Person(dave);
}

Federation

across [...] on a query federates the listed standpoints. Federation is the information-join of the four-valued logic: for each individual it combines what every standpoint says, and where two disagree the join is both. A query that federates the two registries above returns four answers — Alice both (asserted by historical, denied by public_record), Bob is (asserted once), Carol not (only ever denied), and Dave is (asserted once). Disagreement becomes a value the caller can match on, not a crash and not a silent choice of winner. The Lean characterizes exactly when the join is both (federate_eq_both_iff over the infoJoin of the Truth4 carrier).

This is the one place both arises. A single standpoint, evaluated on its own, stays within is, not, and can; only federation across disagreeing standpoints produces conflict. Federation conflict policy is chosen per query, not per standpoint: a federated query is paraconsistent by default, surfacing both, and may instead request a strict projection.

Visibility

A standpoint also bounds what a query can see, and the rule is a sheaf reading of scope. A fact declared at module scope — outside any standpoint block — sits in the default layer and restricts into every view. A fact declared inside a standpoint is local and visible only by selecting that standpoint. So an unfederated query reads exactly the default layer; across [s] reads the default layer unioned with s’s own facts; across [s1, s2] info-joins those per-standpoint views.

Four queries over one default-layer widget and two standpoint-local ones separate the cases cleanly. The default-layer dfl appears in all four. A query scoped to s1 adds only_s1; a query scoped to s2 adds only_s2; neither local fact leaks into the other’s view or into the unscoped base. The unscoped base returns one row, each single-standpoint view two, the federation across both three. Cross-standpoint reads require explicit federation; a scoped fact never silently becomes global truth, and derive rules, checks, and the mutation delta-guard all evaluate over the default-layer view. A federated query naming a standpoint with no declaration is refused rather than contributing an empty extent that would mask the typo.

The sheaf reading is exact. Treat the standpoint lattice as a space and assign each open set the knowledge available to the standpoints in it. The default layer is a global section — it restricts to every open set, which is why an unscoped fact is visible everywhere. A standpoint-scoped fact is a local section — defined only on its own open set. Irreducible disagreement, the both outcome, is the obstruction to gluing local sections into a global one: it lives in a first cohomology that no global section can flatten. The Lean proves the visibility laws directly (view_of_base_eq_default_layer, scoped_view_eq_default_union_own, and the three (in)visibility lemmas) and proves the federated system’s bottom-up evaluation is an equilibrium that is a minimal global section of the sheaf (bottom_up_is_equilibrium, equilibrium_is_global_section, equilibrium_is_minimal_section), over a finite model with no axioms. The full categorical construction — a genuine Grothendieck topology with general restriction maps — is open research; the finite-model theorems are what the substrate commits to.

Bridge rules

Where across [...] composes standpoints lattice-wise, a bridge rule moves a conclusion in one direction between two standpoints, optionally through a domain mapping — a directional, named, typed inference rather than a symmetric join. A bridge from s₁ to s₂ does not imply one from s₂ to s₁; that asymmetry is what keeps bridges from collapsing standpoints into equivalence and erasing their separation.

The design is committed and the surface is real: bridge declarations parse, lower to the wire format, resolve, and pass well-formedness checks. The federation fixpoint does not yet fire them, so a built artifact’s bridge bodies would never contribute to their target. Rather than ship that inert surface, a pub bridge is refused loudly at ox check and ox build (OE1102); model the cross-standpoint inference with an explicit derive or fact until evaluation lands. The parse, lower, and wire path is kept intact so the work resumes without a grammar or format change.

Modal operators

box(P) and diamond(P) read “necessarily” and “possibly” over a frame of worlds — either the standpoints in scope, ordered by <:, or the configurations an individual passes through as the store mutates. Over the classification frame the two connect back to fixed classification. A type introduced by a fixed metatype carries forward rigidity: once an individual is a member, the mutation gate preserves that membership forward. So box(x : T) over a fixed-introduced T reduces to x : T — necessity is the property itself. The discharge is polarity-asymmetric: forward rigidity grips the positive box(x : T) but gives no grip on box(¬(x : T)), since a current non-member may still be constructed into the type later. The Lean proves both the discharge (box_fixed_discharge) and its asymmetry (isRigidIn_does_not_discharge_box_neg).

The engine evaluates this static-discharge case under fixed-default semantics: box and diamond parse, classify at the modal tier, and evaluate by stripping the wrapper and reading the inner atom. That is exact for fixed-introduced types — the common case — and conservative for dynamic ones, which a full Kripke evaluator would settle precisely. The evaluator, the desugaring to quantification over a World carrier, and the interaction of modal operators with federation are designed in the reference under standpoints and modal operators, and not yet wired.

Modules and packages

Modules

A module is a unit of scope. A .ar file is a module named for its stem; a directory with a mod.ar is a module whose siblings are its submodules; mod Name { … } nests one inline. A bare mod Name; declares that a sibling Name.ar exists and attaches it — Rust’s child-module declaration, and the only meaning the form carries. A file does not rename itself, and a content-bearing file whose mod Name; resolves to no sibling is refused rather than silently relabeling its own contents.

Visibility follows Rust. A default-visibility item is private to the module that declares it and every descendant, so a private item at the package root is visible package-wide; pub exposes it to dependents, pub(pkg) limits it to the package. use brings names into scope — single, brace-list, glob, and aliased forms — and a pub use re-exports, joining the importer’s public surface. A qualified path walks from a root: pkg:: is the current package’s self-reference, stable across a rename; self:: and super:: step through the module tree; a leading dependency name resolves into that dependency; std:: is always available. Resolution of a bare name tries local scope, then imports and the package prelude, then the language substrate — the primordial types and built-in forms that are always in scope and not a library. Nothing else is ambient: even the type and rel introducers are brought in explicitly, by use std::core::{type, rel} or a package prelude, which is how the language stays vocabulary-neutral.

Packages

A package is a module tree with a manifest. ox.toml is Cargo-flavored — a [package] with a name, version, and edition, a [dependencies] table, an optional [lattice] ceiling that caps the decidability tier the package may reach, and an optional prelude of use-tails auto-prepended to every module. The prelude is empty by default and carries no vocabulary; a package opts its introducers in.

When one module imports another, the elaborator does not pull the whole imported theory in. It extracts a ⊥-locality module: the smallest subset of the imported axioms that stays non-trivial once every concept outside the used signature is reinterpreted as the empty concept. Extraction is a fixpoint, linear per iteration, terminating in a bounded number of steps. Its guarantee is Σ-scoped conservativity: every entailment about the used signature survives. Argon strengthens the classical result for its own semantics — closed-world conclusions are preserved, ghost individuals reachable only through unused concepts are pulled in, defeasible rules drag in their defeaters (a classical extractor is unsound under non-monotone semantics), and extraction composes across an import chain. All of it is mechanized in the Lean’s locality layer. Extraction is also how decidability tiers compose across heterogeneous modules: each extracted module is classified on its own, and conservativity guarantees no entailment is lost in the seam.

A dependency is a path or a registry reference. A path dependency loads a local checkout and folds its pub surface into the workspace under the dependency name; a vocabulary package is consumed exactly this way, with vocab = { path = "../vocab" } in the manifest and use vocab::{ kind, Substantial }; bringing its introducers and categories into scope, so the consumer writes pub kind Person <: Substantial against vocabulary it does not own and a check shipped with that vocabulary fires on the consumer’s catalog. A registry dependency resolves against a content-addressed registry served over the toolchain CDN: blobs are keyed by hash, a package name resolves to a single version across the whole graph — nominal type identity admits no two — and resolution runs PubGrub over the version constraints, reporting an unsolvable conflict with its derivation chain rather than guessing. A registry dependency with no configured index is refused with a diagnostic that names the fix rather than silently resolving to nothing. The reference fixes the manifest and resolution surface under modules and packages.

Realization

A model that type-checks is not yet a running system. Two things stand between the source and a database that answers questions: the executor must know it can evaluate the program at all, with a cost it can name, and the program must become an artifact a runtime loads and replays. Argon settles the first before the second. A program declares how hard it is to reason about, the classifier verifies that claim, and only a program the executor can run reaches the artifact.

The decidability ladder

Expressiveness and cost trade against each other, and Argon makes the trade visible. Every module sits on one of seven tiers, ordered by what its rules are allowed to say:

Each rung admits everything the rung below admits and one form more — closure adds transitive closure, recursive adds recursion through negation, fol adds unrestricted quantification — and pays for the added power in worst-case cost. The bottom two tiers run in polynomial time. expressive is still decidable but can cost exponential time in the worst case. fol is only semi-decidable: a query may run forever, which is why it is reachable only through the explicit unsafe logic escape and never by default.

The default tier is structural. A program that only declares concepts, subtypes them, and asks membership questions stays at the bottom of the ladder and runs in polynomial time, no annotation required.

The classifier reads the program, not the author

A module’s tier is computed, not asserted. The classifier walks every rule, assigns each atom the lowest tier that admits it, and takes the maximum across the program — a module lands on the lowest tier sufficient to admit everything it contains. A single recursive-through-negation rule pulls the whole module to recursive; without it the module stays lower. The mechanization proves the assignment sound: if the classifier reports tier t, every atom in the program is admitted at t, so the cost bound for t holds for the whole program. An author may annotate a module’s intended tier with #[dec(tier: …)], but the annotation is checked against the computed tier, not trusted in its place — a module that claims structural while containing a recursive rule is refused, not quietly promoted.

A second axis runs alongside the main ladder for temporal operators, classified the same way, and a package may cap the tier it will admit with a [lattice] ceiling in its manifest. Reaching past the ceiling is a build error, which is how a package that means to stay tractable keeps a contributor from silently raising its cost. The reference fixes the full ladder, the temporal sub-tiers, and the annotation surface under Decidability.

The polynomial floor is proven

The base tier’s cost claim is not an estimate. The Lean mechanization proves that for a fixed predicate at the structural tier, evaluation cost is bounded by a polynomial in the size of the data (d1_polynomial_bound over the D1Pred fragment). The predicate’s own size and quantifier depth are constants for a given program, so the bound is polynomial in the number of individuals — the data complexity that matters when the schema is fixed and the store grows. This is the formal content behind “structural runs in polynomial time”: a theorem about the fragment, carried in the substrate rather than asserted in prose.

Shapes the executor cannot run are refused, never dropped

The classifier’s verdict has teeth. A program at a tier the executor cannot yet evaluate, or a rule shape outside the supported fragment, is refused at ox check and ox build with a coded diagnostic — never accepted and silently skipped. A query touching an unsafe logic first-order rule is refused pending the first-order executor and its time budget; a federated bridge body is refused because the federation fixpoint does not yet fire it. The discipline is uniform: a built artifact is one whose every rule the runtime can evaluate, so a program never compiles green and then dies, or worse, returns a wrong answer, on a form the executor quietly declined to run. What the executor cannot do, it says so, at build, with the fix in the diagnostic.

Build and the artifact

Build, then run

With the tier settled and the shapes accepted, the source becomes an artifact. The shape mirrors compiling to a binary, except the artifact is a database rather than machine code:

$ ox build examples/temporal_promotion
$ ox query examples/temporal_promotion ...

ox build runs the compiler over a package and writes a .oxbin. A separate runtime loads that file the way a database server loads a schema, then answers queries and accepts mutations. The runtime never compiles source — every parse, check, and elaboration step happened at build time — which keeps it small and embeddable. ox is the driver that orchestrates compilation across a package and writes the artifact; oxc is the compiler-only subset it drives.

The build pipeline is a fixed sequence of phases:

lex      -> tokens
parse    -> a lossless syntax tree
expand   -> macros run to a fixed point (below)
resolve  -> every path bound to a definition
check    -> type inference, then the runtime-evaluability gate
elaborate-> one axiom event per declaration
encode   -> the .oxbin

The decisive step is elaboration. It turns every declaration — a concept, a relation, a rule, a fact — into an axiom event: a tagged record with a body. By the time the artifact exists, the whole program is a list of events, which is also the storage model the runtime turns on. The check phase before it is the evaluability gate: it runs the static checks and refuses the unsupported shapes, so a .oxbin that exists is one that passed.

Macros run before the program is a program

The expand phase is where the fifth atom lives. A pub macro is compile-time code generation — a vocabulary library grows the surface syntax without a compiler change, which is what the ontology-neutral design depends on. A macro expands to surface syntax that is re-parsed and flows through the same resolve, check, and elaborate path as hand-written source; it never emits an axiom event directly. Expansion runs to a fixed point, bounded by a fuel cap that errors on exhaustion rather than looping.

Two consequences make macros safe to trust. Because the classifier runs after expansion, on the lowered events, a macro lands the program on its true tier — a macro that emits a recursive rule is classified exactly as if the rule were written by hand, and cannot smuggle a program across a tier boundary. And because the declarative layer is strongly normalizing, has no input or output, and emits in a canonical order, expansion is a deterministic function of its input: the same source yields a byte-identical artifact, with no author discipline required.

The declarative engine — pattern-to-template pub macro with hygiene, repetition, and cross-module import — runs today. A procedural layer, #[procmacro] pub fn computing over reflected syntax, ships its first slice: token pasting, quotation, and light declaration reflection, enough to re-home the #[irreflexive] and #[asymmetric] directives from compiler builtins into genuine library macros. The remaining procedural surface is staged. The reference fixes the macro surface, the hygiene model, and the current status under the macro atom.

The artifact

The .oxbin opens with a fixed-size preamble and a directory of sections. Two properties govern how it is consumed.

It carries four independent version numbers rather than one — the section layout, the set of axiom kinds, the decidability ladder, and the runtime contract — because these evolve at different rates. A consumer accepts a future minor bump on any axis and rejects a major one: strict producers, liberal consumers.

It is content-addressed and deterministic. A composition signature hashes the wiring, the standpoint lattice, and the contract versions, and the artifact hash builds on that. Because the encoding and section order are canonical, the same source always produces a byte-identical .oxbin — reproducible builds for a knowledge base. The reference fixes the artifact layout under the .oxbin section model.

The store

Engine, Module, Store

Loading splits into three objects with distinct ownership.

Engine   the shared, immutable schema; one per process
  Module   one loaded .oxbin: concepts, relations, rules, seed facts; immutable; shared by many stores
    Store    one execution context: the live, mutable set of facts; answers queries, takes mutations

The split between an immutable Module and a mutable Store is what makes many isolated contexts cheap: thousands of stores share one loaded schema, each with its own facts. A query reads a store; a mutate writes one; the module underneath them never changes.

The store is an append-only log

The storage layer has no mutable tables. The whole database is one append-only log of axiom events. A schema declaration, a fact assertion, a retraction — each is a new row, and rows are never edited in place. A retraction closes a row’s time window rather than deleting it; physical erasure happens only through the capability-gated forget operation.

There are 26 kinds of axiom event. The catalog is ontology-neutral — a foundational ontology like UFO contributes zero variants, because its meta-properties are ordinary meta_property events whose body names an axis, target, and value — and the Lean inductive is its canonical source. Each row carries its kind and body, the standpoint and module it belongs to, its valid- and transaction-time ranges, a polarity, its tier, and its provenance. So when a mutate body runs insert iof(p, Person), nothing updates a “persons” table: the runtime appends an instance-of assertion. Asking for the current persons replays the log and keeps the rows live now. The reference fixes the storage model under the storage layer.

Two clocks

Every event carries two independent times, and the log is what makes both queryable.

• Transaction time — when the system recorded a fact. “We entered the lease on March 3; we corrected the rent on April 9.”
• Valid time — when the fact is true in the world. “The lease runs January through December.”

Because the two are independent, a query reads along either. Reading at a past transaction time answers what did we believe then; reading at a past valid time answers how was the world then. A query carries the coordinate with as_of: a transaction stamp pins the read to a past belief state, a date pins it to a past state of the world. After a scenario hires someone as a minor and later corrects their age, the same adults query returns nothing at the early transaction stamp and the now-adult individual at the later one — the read snapshot moved past the correction. Argon by Example carries the worked bitemporal programs, temporal_promotion over transaction time and effective_dated_tax_v0 over valid time. Retroactive correction and “as we knew it then” audits are native to the log, not bolted on as history tables.

Tests, serving, and SDKs

Tests are in the language

A model’s behavior is asserted in the language, not in an external harness. A test "name" { … } block runs against a fresh store seeded with the package’s declared facts, and ox test discovers and runs every block, printing a verdict per test and exiting non-zero on any failure, so it doubles as a CI gate. The positive forms assert what a model derives — assert derivable F(x) succeeds when F(x) holds. The assertion is world-honest: it reads F’s world directly, so an absent row under a closed-world concept is a definite non-derivability, while an absent row under an open-world concept is unknown and the runner reports a distinct INCONCLUSIVE rather than a silent pass. The negative form, assert rejects { … }, runs a write block against an isolated copy of the store and passes exactly when the write is refused — the test that a constraint holds the line. Because the example corpus runs in CI, the tests inside it are part of the language’s own regression surface.

Serving and SDKs

A loaded .oxbin is served over HTTP. ox runtime serve binds a versioned /v1 API that dispatches the package’s declared queries and mutations by descriptor name, with batch and health endpoints alongside. Beyond declared dispatch, the API accepts ad-hoc query and mutation bodies as source text, type-checked against the loaded module by the same checker the build runs and then routed through the same path the declared forms use; the declared forms are a named convenience over this generic path. Ad-hoc submission is on by default and a deployment locks it down with --no-adhoc or restricts it to reads. There is no untyped entity-write surface: every write, declared or ad-hoc, goes through a typed mutate. The first-order tier is not served — a query touching an unsafe logic rule is refused, the same loud refusal the build makes. The reference fixes the runtime surface under the runtime contract.

An artifact also generates client code. ox gen reads the schema and emits a dependency-free TypeScript SDK, a typed runtime client, a JSON Schema, or generated documentation, so a host application calls the knowledge base through types that match its declarations. A schema-hash check rejects an SDK built against a stale artifact.

What runs today

ox build, run, query (with as_of), run-scenario, derive, and test work end to end over the in-memory store, which is the live default every example uses; the .oxbin reader and writer handle the preamble, version negotiation, validation, and all 26 axiom-body codecs. ox runtime serve answers the /v1 API, and ox gen emits the TypeScript and JSON-Schema artifacts. A Postgres backend crate exists behind the same storage trait and is selected explicitly; the in-memory backend is what the runtime exercises by default, durable only for the life of the process. A hosted production registry, the per-context incremental cache, and several optional artifact sections are specified rather than wired. The worked packages in Argon by Example are the live, CI-verified account of what runs; the reference fixes the precise rules under the build pipeline, the runtime contract, and the storage layer.

How the books fit together

Argon’s documentation is three texts.

• The Argon Book — the language in order: the model, its types, its reasoning, incompleteness, composition, and execution.
• The Argon Reference — the exact rules. Terse, complete, canonical for the surface, and anchored to the Lean mechanization, which is canonical for the substrate. Where the Lean and the Reference disagree on something the Lean covers, the Lean wins; where this book and the Reference disagree on a rule, the Reference is correct.
• Argon by Example — runnable programs, compiled and run in CI. A broken example is a failed build, not a stale snippet.

RFDs record design decisions; the Lean mechanization carries the proofs.