Zulip Chat Archive

Stream: maths

Topic: ZFC in Lean


view this post on Zulip James Palmer (Jun 27 2020 at 11:39):

Hi guys, where can I find the ZFC axioms in Lean? What is there currently in terms of theorems? I want to spend the better part of this week trying to expand on that and maybe even some metatheory on LEAN :)

view this post on Zulip Johan Commelin (Jun 27 2020 at 11:40):

The metatheory of lean and zfc don't have that much to do with each other, I think

view this post on Zulip Johan Commelin (Jun 27 2020 at 11:40):

But see src/set_theory/zfc.lean

view this post on Zulip Johan Commelin (Jun 27 2020 at 11:40):

Note that mathlib doesn't use zfc anywhere.

view this post on Zulip Kenny Lau (Jun 27 2020 at 11:41):

Lean uses dependent type theory

view this post on Zulip Alistair Tucker (Jun 27 2020 at 11:46):

There's this as well https://github.com/flypitch/flypitch/blob/master/src/zfc.lean

view this post on Zulip James Palmer (Jun 27 2020 at 11:50):

Forgive me I meant metatheory as in First order logic/predicate logic metatheory

view this post on Zulip Johan Commelin (Jun 27 2020 at 12:00):

@James Palmer In that case the Flypitch link that Alistair gave is quite important.

view this post on Zulip Johan Commelin (Jun 27 2020 at 12:01):

It would be really interesting to get some of that stuff in mathlib

view this post on Zulip James Palmer (Jun 27 2020 at 12:10):

many thanks

view this post on Zulip James Palmer (Jun 30 2020 at 20:06):

i.e. we couldn't write constant A: set and then go from there? (permitting that we've write open fol before so that we can make sense of the axioms)

view this post on Zulip Mario Carneiro (Jun 30 2020 at 20:10):

what are you trying to accomplish exactly?

view this post on Zulip Mario Carneiro (Jun 30 2020 at 20:12):

There are two main ways to talk about systems like ZFC: as a model, a set Set of sets with a binary operation called elementhood, or as a syntactic theory, where you have a definition of formulas and axioms and can define the set of provable theorems of ZFC. The former is done in set_theory.zfc, and the latter is done in flypitch

view this post on Zulip Mario Carneiro (Jun 30 2020 at 20:14):

Your comment seems to involve elements of both approaches

view this post on Zulip James Palmer (Jun 30 2020 at 20:18):

where do I find these?

view this post on Zulip Mario Carneiro (Jun 30 2020 at 20:18):

src#Set

view this post on Zulip James Palmer (Jun 30 2020 at 20:18):

I was hoping to look at it with regards to its links to module theory

view this post on Zulip Mario Carneiro (Jun 30 2020 at 20:18):

flypitch was linked above

view this post on Zulip Mario Carneiro (Jun 30 2020 at 20:18):

module theory?

view this post on Zulip James Palmer (Jun 30 2020 at 20:19):

*model theory

view this post on Zulip James Palmer (Jun 30 2020 at 20:19):

forgive me my computer is not having the best time communicating things atm

view this post on Zulip Mario Carneiro (Jun 30 2020 at 20:23):

I don't think the general notion of a model of ZFC is defined, but https://github.com/flypitch/flypitch/blob/master/src/bfol.lean defines a boolean valued model of a FOL extension

view this post on Zulip Jesse Michael Han (Jul 01 2020 at 01:58):

@James Palmer basic model theory is in flypitch/src/fol.lean and flypitch/src/completeness.lean

you can see on this branch how the API is used to state the theorem that Set, the canonical model of ZFC in Lean, is formally a model of the ZFC axioms

view this post on Zulip James Palmer (Jul 01 2020 at 09:24):

thanks Jesse, good work on the Continuum Hypothesis project btw!

view this post on Zulip James Palmer (Jul 01 2020 at 09:24):

(deleted)

view this post on Zulip James Palmer (Jul 01 2020 at 09:25):

(deleted)


Last updated: May 11 2021 at 16:22 UTC