Provenance, tracked automatically
Axioma keeps two independent axes on every fact. The tier ranks how strongly a fact is held — axiom > postulate > theorem > conjecture > hypothesis > datum — and is set by how the fact arrived: a bare posit, a strict deduction, or a defeasible guess. The kind records what the fact ultimately draws on — logical, empirical, motive, transcendental, metalogical. Every example below reads one or both axes back, walks the proof, or defends a conclusion — none of it bolted on, all of it computed by the interpreter as the facts are derived.
A fact describes itself
The refinement axiom/motive posits a claim at the strongest tier and tags its kind in one token. The fact then answers questions about its own status through the possessive axis — fact's grounding and fact's kind — so the epistemic metadata is not a side table but a property of the claim itself.
The provenance ladder — how a fact arrived sets its tier
The same premise feeds three derivations, and the tier records the manner of each. A bare assert lands at datum. A strict rule <= yields a theorem — a necessary consequence. A defeasible rule <~~ yields a conjecture — a guess that later evidence may unmake. Read it back with grounding(rel, args).
The proof chain — walk a theorem back to its axioms
Because each derived fact remembers the premises it came from, a conclusion can be unwound. proof(rel, args) returns every step as a (fact, tier, depth) tuple; the why keyword renders the same chain as prose. Both bottom out at the originating axiom — a real, inspectable derivation, not a bare truth value.
Grounding-aware cancel — the tier is load-bearing
Retraction respects the ladder. cancel defeats a conjecture — that is exactly what defeasance is for. But it refuses a theorem: a strict consequence cannot be unmade by fiat, only by revising a premise in its proof. force_cancel is the deliberate override. The Stoic reading: the novice's disturbance is a defeasible guess; the sage's tranquility is a necessary consequence.
Kind propagation — the a priori / empirical seam
The kind axis is orthogonal to the tier and travels through inference on its own. A conclusion drawn from an empirical observation inherits empirical content; a chain from a pure a-priori posit stays logical. Crucially the tier is untouched either way — both conclusions are equally theorem-grade deductions. Axioma marks where the a priori ends and the empirical begins, without conflating it with how strongly the fact is held.
Read a claim's ground
Two axes, computed for free on every fact: the tier that ranks how it is held, and the kind that names what it rests on. Fork any snippet, add a premise, and watch the provenance move with it.