search

metamath / set.mm

Metamath source file for logic and set theory
Creative Commons Zero v1.0 Universal
237 stars 86 forks source link

New PART 17 MODEL THEORY #3599

Open avekens opened 8 months ago

avekens commented 8 months ago

In PR #3596, it was discussed to move section "Godel-sets of formulas" from MC's mathbox to the main body of set.mm.

I think a new "part" (as PART 17, following PART 16 GRAPH THEORY) would be required for it, which could be titled "MODEL THEORY" (according to @digama0's comment in PR #3572). Its (currently one and only) section would be "Gödel-sets of formulas", containing the subsections "Primary Gödel-sets", "The Satisfaction predicate", "Gödel formulas", "The "proves" relation", "Additional Gödel-sets".

Additional candidates for this new PART would be the following sections in MC's mathbox:

I also detected section "Provability logic" in BJ's mathbox, where a "provability predicate" is defined and theorems for Gödel's second incompleteness theorem ( ~ bj-babygodel ) and Löb's theorem ( ~ bj-babylob ) are provided. Would this also fit into this new PART?

Side remark:

digama0 commented 8 months ago

Sounds good to me. I would shorten goedel the label segment to just goe although I don't think we have any examples of such other than bj-babygodel?

Regarding the usage of the umlaut, feel free to put it everywhere you see Godel, I was just being lazy when I wrote those sections.

benjub commented 8 months ago

Maybe you could do a first PR with only the first subsection, "Gödel codes of formulas" ? (I think "Gödel code" is more explanatory and less confusing than "Gödel set", as I wrote in https://github.com/metamath/set.mm/pull/3572#issuecomment-1763494610). Maybe that subsection could contain both the primary definitions of Gödel codes, and also the definitions for derived formulas.

Maybe gc for "Gödel code" could be used in labels ?

As for bj-babygodel, bj-babylob, these can stay in my mathbox for now. They are really the tiny final part of the proof, once everything has been established, whereas the part you are working on about Gödel codes ("arithmetization of logic") is really about building the infrastructure for that proof (among other applications).

digama0 commented 8 months ago

TBH I think we could just take Gödel out of the name altogether. This is just a straightforward encoding of an inductive type / discriminated union, it's not even really a "code". I don't think there are any other reasonable ways to represent a syntax object than something roughly isomorphic to this, and one may wish to reserve the name "Gödel code" for an encoding in natural numbers specifically.

benjub commented 8 months ago

I was having a look at https://github.com/metamath/set.mm/pull/3613 and I noticed that df-prv says it defines the "proves predicate", but I think this is a peculiar use of "proves". @digama0, did you use it on purpose ? Since we are on the semantic side, the use of "proves" seems out of place here, and may confuse readers. I would say :

The satisfaction predicate is more important, so we use the short name for it. The second, and even more the third, are more technical steps, so can be given longer names (the ones I propose here or others). I think this proposal follows standard terminology more closely.

digama0 commented 8 months ago

No, I think it was a poor choice of name, it's closer to "validity" for formulas than "provability" (since there is no axiomatic theory under consideration) and most likely originated from my tendency to read/speak the symbol |= as "proves" even though "models" is more accurate.

Regarding the relative importance of the notions, df-sate is the one you would normally be working with when proving theorems, but df-prv is better for top level results. The formula height bound in df-sat is of course very artificial and hopefully we should not need to deal with it outside the foundational theorems.