Open david-a-wheeler opened 7 years ago
david-a-wheeler
commented
7 years ago Norm noted that an arxiv article posted in 2016 includes a summary of 6 different proofs; It may be helpful towards selecting one to formalize: https://arxiv.org/abs/1612.02549
avekens
commented
1 year ago Is there currently any activity here? I had a look at the Google group, and I've found the following posts:
https://groups.google.com/g/metamath/c/if0T9w1k5Sc/m/7GwilZhsTa4J (di....@gmail.com Jun 12, 2015, 12:56:41)
Interesting that you should mention this: just yesterday I read http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf which seems like a pretty good blueprint for an implementation of the Incompleteness theorem (or other model theory for that matter), even if Isabelle/ZF is a little different from Metamath. It looks like that reference in turn borrows a lot from Swierczkowski (http://journals.impan.gov.pl/dm/Inf/422-0-1.html), which might also be a good reference.
On Fri, Jun 12, 2015 at 6:03 AM, Scott Fenton sct...@gmail.com wrote: I'm working (long-term) on the Incompleteness Theorem
https://groups.google.com/g/metamath/c/QPOfJEnRqmU/m/9d7MpggJEAAJ
On Fri, 9 Dec 2016 05:14:09 -0800 (PST), Norman Megill n...@alum.mit.edu wrote: An arxiv article posted just yesterday includes a summary of 6 different proofs. It may be helpful towards selecting one to formalize (Goedel's). https://arxiv.org/abs/1612.02549
https://groups.google.com/g/metamath/c/rhpkuHra_ic/m/uymZNIaJBgAJ (di....@gmail.com Apr 8, 2017, 8:13:52)
On Sun, Apr 2, 2017 at 10:50 PM, Paul Chapman igb...@gmail.com wrote: (2) Has anything been done on Gödel numbers? Is there an nth prime function, or more generally an nth member in increasing order of a countable well-ordered set?
Nothing has been done on Godel numbers AFAIK. ...
I'm sure that Mario will answer that eventually. But meanwhile here are some simple answers.
I would like to understand first order logic, ZFC and Gödel's completeness theorem. I'm thinking, I can't really say I understand those things if I can't implement a proof checker for FOL and ZFC and prove Gödel's completeness theorem using that checker.
That's what I'm planning to do at some point. Not that theorem in particular, but I'd like to formalize some beginning of arithmetic and calculus using some particular textbooks of my preference. But you shouldn't underestimate its complexity. It's sufficient to say that Godel's incompleteness theorem is still not in Metamath database which is much more advanced than MM0's with many more people working on it. I think that completeness theorem is missing as well but not sure.
Hey, I didn't say that was all it's for. It's not on the top of my list of priorities, but I believe that the project will be in a good position to formalize Godel's incompleteness theorem once the main goal is finished. Already we have enough to formalize inductively defined structures like expression trees and Godel numbering; if I recall the proof correctly there isn't that much more to do to diagonalize it.
On Mon, Apr 27, 2020 at 8:46 PM Jim Kingdon kin...@panix.com wrote:
it is being used in order to define the input language of MM0 so that I can make a claim about an MM0 verifier
Ah, and here I had let my hopes get up that it was for formalizing Gödel's Incompleteness Theorem (which is in the Metamath 100, after all).
There are some new hints in the posts written in 2019 and 2020, and some people claimed/announced that they are/will be working on it.
I tried to start a proof, but got stuck already at assigning Gödel Numbers to formulars (how can a set/class of wffs be defined? How can a function from the set/class of wffs to the positive integers be defined?) @digama0 is there something already available in mm0 which can be transfered to mm/set.mm?
tirix
Prove Gödel's Incompleteness Theorem (metamath 100 #6). 4 other formalization tools have done so.
Mario: Model theory. So many ways to do this one, and all of them require a lot of preparation and potential incompatibilities down the line, so I've been indecisive about this.