14
$\begingroup$

I'm a big fan of the idea of fully formalizing mathematics. So the Lean proof checker appeals to me.

Relating to this, one of the biggest appeals of mathematics to me is that there is a (largely) agreed upon finite list of axioms which we all agree to use. Those being the ZF(C) set theory axioms. Anyone can find a complete explicit list of these written in first-order logic by googling it and opening the first link on wikipedia.

The Lean proof checker seems to use a version of "type theory" for its foundations, which I would like to learn more about. In particular I would like to be able to convert between "type theory" proofs and the set theory proofs I'm already familiar with so that I can get Lean to check stuff for me.

Here is a page on the axioms of lean 4: https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html

It doesn't appear to me that the axioms described here form a complete list of those used in lean. Without such a list, I don't really have any appeciation for what lean is "proving" and it is difficult for me to know how to convert between lean proofs and the set theory proofs I know.

My main questions are:

  1. Is it true that the Lean model of mathematics is bi-interpretable with ZFC?

  2. Does there exist a compresensive list of all the axioms used by lean in the same vein as this wikipedia page: https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory

Improve this question
$\endgroup$
7
  • 7
    $\begingroup$ Side remark: Two of the axioms of ZF(C) are actually axiom schemas - the axiom schema of specification and the axiom scheme of replacement - each of which generates an infinite class/set of axioms. So the number of actual axioms of ZF(C) is not finite, but infinite. $\endgroup$
    – Alexis Hazell
    Commented Oct 19, 2023 at 11:31
  • 2
    $\begingroup$ Related: How true are theorems proved by Coq? $\endgroup$
    – Timothy Chow
    Commented Oct 19, 2023 at 13:42
  • 7
    $\begingroup$ This question might be more appropriate for the Proof Assistants Stack Exchange. $\endgroup$
    – Timothy Chow
    Commented Oct 19, 2023 at 15:59
  • 3
    $\begingroup$ Mario Carneiro's thesis is also relevant. The executive summary is that Lean is equiconsistent with ZFC + infinitely many inaccessibles. $\endgroup$
    – Timothy Chow
    Commented Oct 19, 2023 at 20:01
  • 2
    $\begingroup$ @TimothyChow If my memory serves right, what Carneido proved is "ZFC + $\omega$ many inaccessibles" interprets Lean, but it does not give a precise strength for Lean: Lean proves for each $n$, the theory "ZFC + $n$ many inaccessibles" is consistent, but ZFC + "$\omega$ many inaccessibles" proves the consistency of ZFC + "$n$ many inaccessibles for each (standard) $n$." See Dorais' answer for a more detail. $\endgroup$
    – Hanul Jeon
    Commented Oct 19, 2023 at 23:26

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .