03 / Truth & provability
Choose your mathematical world.
A statement.
The assumptions beneath it.
Current framework
◇ Curated dependenciesZFC
These are proof statuses relative to assumptions, not absolute truth values. No consistency checker or automated foundations prover is running.
Dependency graph / selected statement
Provable
Every vector space over every field admits a Hamel basis.
An AC-equivalent theorem over ZF; Choice is assumed.
The theorem quantifies over all vector spaces and all fields, not only finite-dimensional spaces or one fixed field. Over classical ZF it is equivalent to Choice.
References & scope for this relation
- University of Toronto · The Axiom of Choice ↗
§11.6: equivalence of Choice, well-ordering and the basis theorem over ZF.
- John L. Bell · The Axiom of Choice ↗
Independence and mathematical applications of Choice.
The relations are curated; software deterministically selects the applicable rule. They are not Lean-checked. Independence claims carry an explicit consistency assumption.
When a proof disappears, has the object disappeared with it?
Withhold Choice, then assert its negation. Observe how the status changes. What did you change: the statement, the available proof, or the world you intend to describe?