What a claim knows about itself

Provenance, tracked automatically

Axioma records two distinct axes on stored facts. The tier records how a fact arrived — axiom, postulate, theorem, conjecture, hypothesis, or datum — and affects operations such as cancellation. The kind records the declared or propagated basis of a claim: logical, empirical, motive, transcendental, or metalogical. The author supplies the starting assertions and their tags; the interpreter records and propagates their consequences.

A theorem is a strict consequence of the supplied premises and rules. Its label is not a probability or a credibility score, and does not establish that those premises are true of the world. A strict conclusion from a hypothesis still has tier theorem; its proof retains the hypothesis. The six examples below include executable expect checks of these distinctions.

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 two derivations. A bare assert lands at datum. A strict rule <= yields a theorem; a defeasible rule <~~ yields a conjecture. The tier records the route taken, while the premise retains its original status. Read it back with grounding(rel, args).

The proof chain — walk a theorem back to its premises

A conclusion can be traced back through its premises. proof(rel, args) returns the recorded chain as (fact, tier, depth) tuples; why renders it as prose. This example bottoms out at an axiom. A different proof can end at a hypothesis, postulate or datum — inspecting the chain tells you which assumptions the conclusion actually depends on.

Grounding-aware cancel — the tier is load-bearing

cancel can defeat a conjecture, but refuses a theorem. This protects a strict derivation from direct cancellation; it does not make its premises immune to revision. force_cancel explicitly overrides that protection. To withdraw a premise and reconsider its dependents, use forget_cascade, demonstrated below. The Stoic interpretation here is a modeling choice: the author supplies the rules relating judgment, disturbance and tranquility.

Kind propagation — the a priori / empirical seam

The kind axis propagates separately from the tier. Here, a conclusion drawing on an empirical premise is empirical; the strict conclusion from the motive premise has kind logical. Both have tier theorem. These are consequences of the supplied tags and inference rules: the interpreter does not independently decide whether a report is accurate or an initial claim is a priori.

When a premise changes

First derive a conclusion from a hypothesis and inspect that hypothesis in its proof. Withdraw the only premise: the conclusion disappears from the query result. Then give the same conclusion two supporting paths. Withdrawing one leaves the other intact; withdrawing both removes the conclusion. Multiple derivations provide alternate support within the model — they do not, by themselves, establish that real-world sources are independent.

The empty results above concern these declared relations and rules. They report what this model derives; they do not prove that the corresponding claim is false in the world. Each card starts with a fresh environment, and its assertions are checked directly from this page before publication and in the production test suite.