Gödel completeness theorem

Stream: maths

[Xin Huajian]

Have Gödel completeness theorem been proven in mathlib? It seems that the proofs of the completeness and compactness of first-order logic do not appear in the mathlib, but they have been given in the flypitch project.

[Violeta Hernández]

We have the power to state such a metatheorem in Lean? That's awesome if true

[Xin Huajian]

Yes, the model_theory in mathlib have given some metatheorems of the first-order logic.

[Junyan Xu]

The Ax-Grothendieck theorem has been proved using model theory. The author just opened #15070 as a step of getting this into mathlib. The ongoing work of migrating flypitch into mathlib seems to be exclusively carried out by Aaron Anderson, at least recently.

(There is also an ongoing project aiming to show the consistency of New Foundations by constructing a model, in which Yaël Dillies is involved, but it doesn't seem (and I think doesn't need) to use the FOL/model theory library.)

[Kevin Buzzard]

@Joseph Hua I see that your Ax Grothendieck repo is public, but will you make your MSc thesis public as well?

Joseph is going to CMU next year for a PhD.

Edit: sorry for the ping Joseph -- the thesis is here.

[Joseph Hua]

Kevin Buzzard said:

Joseph Hua I see that your Ax Grothendieck repo is public, but will you make your MSc thesis public as well?

Joseph is going to CMU next year for a PhD.

Edit: sorry for the ping Joseph -- the thesis is here.

Sorry I didn't see this, yeah I made it public a couple of days ago, to avoid plagiarism scandals

[Xin Huajian]

And has the Gödel incompleteness theorem been proved? Or is anyone working on that?

[Junyan Xu]

Apparently this is it? completeness is here.

[Xin Huajian]

Junyan Xu said:

Apparently this is it? completeness is here.

Thanks! And how about the incompleteness theorem? It seems remain on the unproved list (NO. 6).

[Xin Huajian]

(deleted)

[Xin Huajian]

Joseph Hua said:

Kevin Buzzard said:

Joseph Hua I see that your Ax Grothendieck repo is public, but will you make your MSc thesis public as well?

Joseph is going to CMU next year for a PhD.

Edit: sorry for the ping Joseph -- the thesis is here.

Sorry I didn't see this, yeah I made it public a couple of days ago, to avoid plagiarism scandals

Thanks for your updating the flypitch! It really helps me.

[Junyan Xu]

Xin Huajian said:

Thanks! And how about the incompleteness theorem? It seems remain on the unproved list (NO. 6).

I think theorems are only removed from the list when they get into mathlib, but I can't find formalization (in Lean) of the incompleteness theorems outside of mathlib either. There is reference to a Coq formalization in the flypitch repo.

[Xin Huajian]

Junyan Xu said:

Xin Huajian said:

Thanks! And how about the incompleteness theorem? It seems remain on the unproved list (NO. 6).

I think theorems are only removed from the list when they get into mathlib, but I can't find formalization (in Lean) of the incompleteness theorems outside of mathlib either. There is reference to a Coq formalization in the flypitch repo.

Thanks!

[Alex J. Best]

The unproved list is simply the complement of the proved list (https://leanprover-community.github.io/100.html), which does contain links to things in projects outside of mathlib. So if there is something in a relatively stable state it should no longer appear on the unproved list (there are a few things on there that definitely are Lean-formalized somewhere or other though)

[Johan Commelin]

I guess the text at the top of the page is misleading. Because it suggests that the list is only about stuff in mathlib.

[Alex J. Best]

Yeah that is a little misleading!