Lesson 10
Constructive and classical assumptions
Why can two formal proofs of familiar mathematics have different axiom footprints?
Constructive and classical foundations accept different general principles. Axeyum reports those assumptions per declaration instead of assigning one label to an entire library.
After this lesson, you should be able to
- Explain constructive existence and unrestricted excluded middle.
- Identify the roles of choice, propositional extensionality, and quotient soundness.
- Interpret an empty axiom footprint without overstating what it proves.
10.1
Constructive existence contains a witness
A constructive proof that an object exists provides enough information to obtain that object. A constructive proof of P or not P determines which side holds. These requirements give proofs computational content.
Classical logic permits unrestricted excluded middle and proof by contradiction in cases where no decision method is known. These methods are standard and useful, but they can produce existence proofs without a construction.
10.2
Lean exposes several trusted principles
Choice selects values from nonempty types without requiring a definable selection procedure. Propositional extensionality turns logical equivalence into equality between propositions. Quotient soundness identifies related representatives after quotient construction.
These principles do different work and should not be grouped under a vague classical label. A declaration's dependency walk can identify the specific trusted names it reaches.
10.3
mathlib cannot be classified by one word
Many mathlib declarations are constructive or have an empty measured footprint. Others use classical reasoning because it shortens proofs or supports definitions that depend on choice, extensionality, or quotients.
A useful comparison therefore works per declaration and per formal statement. Similar theorem names can use different carriers, definitions, hypotheses, or conclusions, so footprint counts alone do not establish equivalence.
10.4
Axeyum's pure base is measured per declaration
Axeyum includes constructed mathematical carriers and kernel-checked declarations whose recorded axiom footprints are empty. Classical imports remain available on routes that identify their assumptions.
An empty footprint means that the dependency analysis reached no recorded axiom, opaque declaration, or quotient primitive for that declaration. The kernel, its primitive calculus, the formal statement, and the import or construction process still require review.
Worked example
Compare two forms of an existence argument
Prove that some integer has square 9.
- Construct a witness
Choose 3.
- Check the property
Compute 3² = 9.
- Package the proof
Return the witness 3 together with the equality proof.
- Compare methods
A contradiction argument that denies all witnesses could prove existence classically, but it would not by itself supply the integer.
Result. The witness 3 and its checked square form constructive evidence for the existence claim.
10.5
Check your understanding
Answer each question before opening the explanation.
1 Does an empty axiom footprint prove that the theorem is stated correctly in prose?
No. It reports the trusted declarations reached by the formal dependency route, not the accuracy of a prose summary.
2 Why is propositional extensionality stronger than proving P if and only if Q?
It converts the logical equivalence into equality of the proposition objects P and Q.
Concept wiki
Terms in this lesson
- Axiom A proposition accepted without a proof term in the current formal environment.
- Axiom footprint The set of trusted axioms reached by a declaration's dependencies.
- Constructive mathematics Mathematics that requires explicit constructions or evidence for existence claims.
- Classical logic Logic that permits principles such as excluded middle for every proposition.
- Law of excluded middle The principle that P or not P holds for every proposition P.
- Axiom of choice A principle that selects an element from each set in a family of nonempty sets.
- Propositional extensionality The principle that logically equivalent propositions are equal as propositions.
- Quotient soundness A trusted rule that identifies quotient representatives related by the chosen relation.