What can we prove - what are the underlying axioms?

Stream: general

[Axel Boldt]

I'm trying to understand what axioms the Lean system and Mathlib use. For instance: which first-order theorems about (Nat,+,*) can we prove in Lean? Do they coincide with the ones provable from Peano's first-order axioms, or with the ones provable in ZFC, or with some other class?

[David Sampson]

The reference manual discusses the fundamental axioms Lean uses a bit: https://lean-lang.org/doc/reference/latest/Axioms/

A lot of things that would need to be axioms in other systems are baked in to the type system in Lean. For example, the existence of 0 and S x for all x : Nat are part of the definition of Nat, whereas in Peano they are explicit axioms. See: https://github.com/leanprover/lean4/blob/cdd38ac5115bdeec5f609e9126cce00f51ae88b3/src/Init/Prelude.lean#L1185-L1206

For more information it would be good to read up on the Calculus of Inductive Constructions, which is the type theory Lean is based on.

See also: https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Computation/#axioms-and-computation

https://rocq-prover.org/doc/V8.9.1/refman/language/cic.html
^^^ This is about Rocq, but Lean's type system is very similar.

[Aaron Liu]

Probably I would guess coincides with ones provable in "ZFC + { there are at least n inaccessible cardinals | n < ω }"

[Matt Diamond]

#leantt (Mario Carneiro's thesis on the type theory of Lean) might be informative (I assume it still applies to Lean 4?)

[James E Hanson]

One thing to note with this discussion is that type theory as a field uses the word 'axiom' in a technical sense that's not really consistent with the way it's used in most conversations about 'axioms' and 'axiomatic systems'. (Specifically an axiom in type theory is an assumption without in-built computational content.)

This results in sort of odd things like being able to prove a statement like $\mathrm{Con}(\mathsf{PA})$ in Lean 'without any axioms.'

[James E Hanson]

David Sampson said:

A lot of things that would need to be axioms in other systems are baked in to the type system in Lean. For example, the existence of 0 and S x for all x : Nat are part of the definition of Nat, whereas in Peano they are explicit axioms.

I don't get why you're saying this. Neither of these are axioms of first-order Peano arithmetic in the modern sense.

[James E Hanson]

The constant 0 and the successor function are part of the syntactic specification of Peano arithmetic.

[Snir Broshi]

James E Hanson said:

The constant 0 and the successor function are part of the syntactic specification of Peano arithmetic.

But the fact that successor is injective and that 0 is not in its image are axioms in PA, whereas Lean gets them as part of the inductive construct itself

[Aaron Liu]

It comes from the recursor and its equations

[James E Hanson]

Snir Broshi said:

James E Hanson said:

The constant 0 and the successor function are part of the syntactic specification of Peano arithmetic.

But the fact that successor is injective and that 0 is not in its image are axioms in PA, whereas Lean gets them as part of the inductive construct itself

Sure but the whole axiom/rule distinction is somewhat arbitrary, which is why I find it a little bit annoying when people use it as a selling point of type theory over and above first-order logic. I could just take ordinary $\mathsf{PA}$ and decree that all of the axioms are rules and then I would be able to prove things in $\mathsf{PA}$ 'without axioms' too.

[Aaron Liu]

The difference is the computational content, which if you're just making proofs then it isn't really meaningful

[Aaron Liu]

But Lean can also make definitions

[Aaron Liu]

so that's why we distinguish them, the computation rules let you compute, and the axioms don't reduce on anything

[James E Hanson]

I understand the computational content aspect, but it doesn't change the fact that 'type theory is able to prove things without axioms' is a really misleading way of saying 'type theory has computational content baked into its formalism.' If you ask an average mathematician on the street what an 'axiom' is, they're not going to say 'an assumption without computational content.'

[James E Hanson]

(deleted)

[Axel Boldt]

James E Hanson said:

the whole axiom/rule distinction is somewhat arbitrary,

Agreed. In any event: one would hope that a complete and formalized list of Lean's rules and axioms is available somewhere. How else are we to compare its theorems with those of other systems?

[Riccardo Brasca]

As mentioned above, the standard reference is #leantt