Executable epistemology

What a claim knows about itself

In most languages a fact is just a value. In Axioma every stored fact also carries its own epistemic bookkeeping — a grounding tier (how it was derived) and a kind (what it draws on) — and those travel through every inference. Provenance is a first-class value you can read, walk, and defend.

▶ Press Run or /Ctrl+Enter. WebAssembly interpreter — same as the playground. interpreter: loading…
GROUNDING · TWO ORTHOGONAL AXES

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 onlogical, 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).

ladder.axOpen in Playground ↗

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.

proof.axOpen in Playground ↗

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.

cancel.axOpen in Playground ↗

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.