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.
Mario On Mon, Apr 27, 2020 at 8:46 PM Jim Kingdon <[email protected]> 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). > > On April 27, 2020 6:10:05 PM PDT, Mario Carneiro <[email protected]> > wrote: >> >> >> >> On Mon, Apr 27, 2020 at 7:35 AM Norman Megill <[email protected]> wrote: >> >>> On Monday, April 27, 2020 at 1:01:56 AM UTC-4, Mario Carneiro wrote: >>> ... >>> >>>> >>>> I know, and this is a bigger issue for set.mm than in the mm0 >>>> databases because these are smaller and more purpose driven. One reason I >>>> went with _c notations for characters is because it is easier to read >>>> >>> >>>> _h : _e : _l : _l : _o : __ : _w : _o : _r : _l : _d >>>> >>>> than >>>> >>>> 'h' : 'e' : 'l' : 'l' : 'o' : 'sp' : 'w' : 'o' : 'r' : 'l' : 'd' >>>> >>> >>> Maybe I missed something in this thread, but what is the purpose of >>> formalizing ASCII? Is this something that eventually might be added to >>> set.mm?. >>> >> >> I didn't explain this, but I am already using a formalization of ASCII in >> MM0, for example >> https://github.com/digama0/mm0/blob/master/examples/mm0.mm0#L405-L459 . >> As you can see there, it is being used in order to define the input >> language of MM0 so that I can make a claim about an MM0 verifier. While I >> have no immediate plans to move this to set.mm, this is a possibility, >> and it also shows an example of a mathematically reasonable use of ASCII >> formalization, which may come up in set.mm in another form (e.g. >> metamath in metamath). >> >> Our informal convention has been to prefix non-italic letters with >>> underscore, like _i, so _<letter> will clash with a few that already >>> exist. How about a single quote prefix, 'a 'b 'c ... like in Lisp 'foo to >>> abbreviate (quote foo)? That would not clash with anything in set.mm >>> except ''' in AV's mathbox (for alternate function value) which could be >>> changed. >>> >>> 'h : 'e : 'l : 'l : 'o : 'sp : 'w : 'o : 'r : 'l : 'd >>> >> >> This also works for me. I don't think it is essential to commit to a >> notation right now since I'm not actually adding these characters to >> set.mm, but I wanted to make sure that others keep this use in mind. >> >> Mario >> >> -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSseUgZOphZO0wkoTLaB-Q%2Bzs38KLYoupY1oVJmHzdsJWQ%40mail.gmail.com.
