Learn · Logic and foundations
Axeyum for logicians and foundations researchers
Axeyum's kernel, trust accounting, and constructive models make the foundations of each result available for direct inspection.
a103b3db3 Measured Source Axeyum fact ledger and implementation documentation After reading this guide, you should be able to
Learning objectives
- Identify the parts of Axeyum that are relevant to logic and foundations.
- Distinguish implemented results from the current research frontier.
- Open a lesson or artifact that provides the underlying definitions and evidence.
Current state
What exactly does the kernel assume and check?
The pure-Rust kernel checks universes, dependent terms, definitional equality, inductive types, strict positivity, recursors, and selected well-founded recursion. Its quotient package contains Quot, Quot.mk, Quot.lift, and Quot.ind, but not Quot.sound.
The logic development includes an intuitionistic natural-deduction system and a machine-checked result that excluded middle is not derivable in it. The environment computes each theorem's axiom footprint from its actual dependency closure.
Why it matters
What the current work makes possible
- Trust claims are outputs of the environment rather than labels attached by authors.
- Constructive carrier models show how much mathematics can be built with an empty trusted surface.
- Classical principles appear as explicit declarations or formal boundary theorems.
- Selected Lean imports expose differences between elaboration acceptance and independent kernel admission.
Results to inspect
Open the evidence
What comes next
Extend the present base
Kernel work can extend the admitted Lean construct matrix, strengthen metatheory and mutation tests, and narrow the remaining import boundary without turning source elaboration into trusted checking.
The formal library can add more independence and non-derivability results, including precise studies of which mathematical principles require which extensions.
Where to begin