ZFC in Lean

Stream: general

[Jiatong Yang]

I know that mathlib has formalized a model of ZFC in Lean. But I want to show the construction of the math world only using ZFC and logic. So I want to add a constant type Set and several axioms to achieve that. The problem is that classical.choice is too strong but I need to use its corollary em, and I still want the automatic tactics about classical logic. What should I do?

[Violeta Hernández]

Mathlib as a whole uses choice freely and carelessly. If you want to explicitly avoid choice, then mathlib and its tactics are not for you.

[Violeta Hernández]

By the way, I presume that by "tactics about classical logic" you mean tauto!? I've only found it useful in a few situations, I don't think you'll lose out on much by not having it.

[Jiatong Yang]

Thank you. I will not use mathlib then. And I may use Lean4 instead.

[Mario Carneiro]

lean itself is already stronger than ZFC in axiomatic strength

[Jiatong Yang]

Btw, how strong is the lean's axioms? Are there any statements about its consistency?

[Huỳnh Trần Khanh]

Why are you interested in this? As a normal person, I write proofs and couldn't care less about foundations. Foundations are too high, not yet for me.

[Mario Carneiro]

#leantt has the full breakdown. The short answer is that Lean's type theory is equiconsistent with ZFC + n inaccessibles for all n < omega

[Mario Carneiro]

That includes the 3 standard axioms though. No-axioms lean is less well studied, but I believe it to still have approximately the same strength (intuitionistic logic is well known to be equiconsistent with classical logic via double negation translation, and similarly ZF and ZFC are equiconsistent because you can construct L as an inner model in which choice holds)

[Kevin Buzzard]

@Huỳnh Trần Khanh different people are interested in different things

[Patrick Johnson]

Jiatong Yang said:

I know that mathlib has formalized a model of ZFC in Lean. But I want to show the construction of the math world only using ZFC and logic. So I want to add a constant type Set and several axioms to achieve that.

You may be interested in a small project of mine, in which I stated ZFC axioms and constructed some data structures and proved things about them (unordered/ordered pairs, natural numbers, induction principle, set functions as cartesian products, classical propositions, conditionals, etc). It's not written according to the recommended Lean 4 style guide though.