Examples of distinct "axiom sets"

Stream: new members

[Isak Colboubrani]

For educational purposes, I’m collecting examples of the distinct “axiom sets” that proofs can depend on (assuming we’re only using the axioms already defined in Lean/Mathlib).

So far, I’ve been able to construct examples with the following sets of axiom dependence:

• $\emptyset$
• $\{ \operatorname{prop ext} \}$
• $\{ \operatorname{Quot.sound} \}$
• $\{ \operatorname{prop ext}, \operatorname{Classical.choice}, \operatorname{Quot.sound} \}$

Which other sets of axioms might appear and what are some examples of each?

For the examples I’ve identified (see below), are there better or more canonical ones that I might use instead?

Below are minimal working examples illustrating each of the axiom sets above:

-- axioms = ∅
import Mathlib
lemma depends_on_no_axioms : 1 + 1 = 2 := by rfl
#print axioms depends_on_no_axioms

-- axioms = {propext}
import Mathlib
lemma depends_on_propext₁ (p q : Prop) (h : p ↔ q) : p = q := propext h
#print axioms depends_on_propext₁
lemma depends_on_propext₂ : 1 + 1 = 2 := by norm_num
#print axioms depends_on_propext₂

-- axioms = {Quot.sound}
import Mathlib
lemma depends_on_quot_sound (f g : ℕ → ℕ) (h : ∀ n, f n = g n) : f = g := funext h
#print axioms depends_on_quot_sound

-- axioms = {propext, Classical.choice, Quot.sound}
import Mathlib
-- Classical.not_not : ¬¬a ↔ a
#print axioms Classical.not_not
-- Classical.em : p ∨ ¬p
#print axioms Classical.em
-- peirce : ((a → b) → a) → a
#print axioms peirce
-- Nat.prime_two : Nat.Prime 2
#print axioms Nat.prime_two

[Isak Colboubrani]

Found three more:

-- axioms = {Lean.trustCompiler}
import Mathlib
lemma depends_on_trust_compiler : Lean.reduceBool true = Lean.reduceBool true := rfl
#print axioms depends_on_trust_compiler

-- axioms = {Lean.ofReduceBool}
import Mathlib
lemma depends_on_of_reduce_bool : 1 + 1 = 2 := by native_decide
#print axioms depends_on_of_reduce_bool

-- axioms = {propext, Classical.choice, Lean.ofReduceBool, Quot.sound}
import Mathlib
lemma depends_on_of_reduce_bool_etc (x y z : BitVec 1) : x < y → y < z → x < z := by bv_decide
#print axioms depends_on_of_reduce_bool_etc

[Aaron Liu]

docs#Quotient.exact maybe?

[Isak Colboubrani]

@Aaron Liu Do you mean as a better or more canonical axioms = {propext} example?

import Mathlib
#print axioms Quotient.exact
-- 'Quotient.exact' depends on axioms: [propext]

[Aaron Liu]

It's a more obviously useful statement

[Isak Colboubrani]

After some additional experimentation, I’ve found seven distinct axiom sets that can be triggered (as reported by #print axioms …).

Should I expect to find any additional combinations of axioms, or is this the complete set of possible axiom requirements for proofs (assuming we’re only relying on the axioms already defined in Lean/Mathlib)?

1. axioms = ∅
2. axioms = {propext}
3. axioms = {propext, Classical.choice, Quot.sound}
4. axioms = {propext, Classical.choice, Lean.ofReduceBool, Quot.sound}
5. axioms = {Lean.ofReduceBool}
6. axioms = {Lean.trustCompiler}
7. axioms = {Quot.sound}

[Yaël Dillies]

Why would you expect only some sets to be triggerable? I expect every single set can be triggered

[Aaron Liu]

#print axioms Classical.choice will probably just be {Classical.choice}

[Aaron Liu]

And you can combine these arbitrarily with PProd

[Isak Colboubrani]

@Yaël Dillies That's a good question! I wasn't sure whether any of the axioms were "absorbed" by others when reported by #print axioms […] — in the sense that, for example, a combination like Lean.ofReduceBool and Lean.trustCompiler might be reported simply as Lean.trustCompiler by #print axioms […].

[Yaël Dillies]

No, that doesn't happen. #print axioms reports all the axioms that are used. There is no subsumption

[Isak Colboubrani]

@Yaël Dillies Thanks! (TIL the word "subsumption" too. Thanks again!)

Is my understanding correct here:

• For sorry-free theorems in a third-party Lean project, the five "core axioms" that a given theorem can depend on are {propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound}, leading to 32 possible combinations ($2^5$). This excludes any user-defined axioms or axioms "internal" to the main Lean code base (such as axioms defined in the tests).
• In Mathlib specifically, the policy is to restrict the axiom use to subsets of {propext, Classical.choice, Quot.sound}, resulting in 8 possible combinations ($2^3$) for a given Mathlib theorem.

Does that sound correct?

[Yaël Dillies]

Both points sound correct, yes. But there might be more core axioms than the ones I am aware of