Zulip Chat Archive

Stream: maths

Topic: ZFC in Lean

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 :)

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

Johan Commelin (Jun 27 2020 at 11:40):

But see src/set_theory/zfc.lean

Johan Commelin (Jun 27 2020 at 11:40):

Note that mathlib doesn't use zfc anywhere.

Kenny Lau (Jun 27 2020 at 11:41):

Lean uses dependent type theory

Alistair Tucker (Jun 27 2020 at 11:46):

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

James Palmer (Jun 27 2020 at 11:50):

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

Johan Commelin (Jun 27 2020 at 12:00):

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

Johan Commelin (Jun 27 2020 at 12:01):

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

James Palmer (Jun 27 2020 at 12:10):

many thanks

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)

Mario Carneiro (Jun 30 2020 at 20:10):

what are you trying to accomplish exactly?

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

Mario Carneiro (Jun 30 2020 at 20:14):

Your comment seems to involve elements of both approaches

James Palmer (Jun 30 2020 at 20:18):

where do I find these?

Mario Carneiro (Jun 30 2020 at 20:18):

src#Set

James Palmer (Jun 30 2020 at 20:18):

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

Mario Carneiro (Jun 30 2020 at 20:18):

flypitch was linked above

Mario Carneiro (Jun 30 2020 at 20:18):

module theory?

James Palmer (Jun 30 2020 at 20:19):

*model theory

James Palmer (Jun 30 2020 at 20:19):

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

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

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

James Palmer (Jul 01 2020 at 09:24):

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

James Palmer (Jul 01 2020 at 09:24):

(deleted)

James Palmer (Jul 01 2020 at 09:25):

(deleted)

Last updated: Dec 20 2023 at 11:08 UTC