Zulip Chat Archive

Stream: maths

Topic: Gödel completeness theorem


Xin Huajian (Jul 02 2022 at 04:09):

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 (Jul 02 2022 at 04:15):

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

Xin Huajian (Jul 02 2022 at 12:58):

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

Junyan Xu (Jul 02 2022 at 13:31):

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 (Jul 02 2022 at 13:50):

@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 (Jul 02 2022 at 17:01):

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 (Jul 03 2022 at 02:51):

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

Junyan Xu (Jul 03 2022 at 02:55):

Apparently this is it? completeness is here.

Xin Huajian (Jul 03 2022 at 02:59):

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 (Jul 03 2022 at 03:01):

(deleted)

Xin Huajian (Jul 03 2022 at 03:01):

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 (Jul 03 2022 at 03:05):

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 (Jul 03 2022 at 03:07):

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 (Jul 04 2022 at 06:22):

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 (Jul 04 2022 at 06:25):

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 (Jul 04 2022 at 06:28):

Yeah that is a little misleading!


Last updated: Dec 20 2023 at 11:08 UTC