Talk:Gödel's incompleteness theorems

Adding a proof generalization based on The Hilbert–Bernays conditions

I think it is in place to add a generalization of the proof of both theorems, based on the Hilbert–Bernays conditions and the diagonal lemma, due to the following reasons:

1. These are arguably important generalizations and the proof do not depend on the details of the specific theory.
2. As for the question whether it is too detailed, proof sketches are given in the article anyway, and the one given for the 1st theorem is already quite elaborated. However, using the the Hilbert–Bernays conditions and the diagonal lemma the proof is much much shorter than the proof sketch.
3. These proofs give a good idea of how to use the language/notations of the Hilbert–Bernays conditions in this context.

I have made such an edit which was reverted by User:Trovatore, which I am not sure was the best way to handle the issue.

Opinions? Dan Gluck (talk) 22:52, 13 July 2020 (UTC)

One possibility is to write the proof in the very short Hilbert–Bernays provability conditions article, which then shows how these conditions are actually used, and only refer to that here. As the current (Gödel's incompleteness theorems) article is quite lengthy and might actually need a severe diet, this could be a good idea. But I'ld love to hear other opinions as well. Dan Gluck (talk) 22:57, 13 July 2020 (UTC)

It shouldn't say most mathematical proofs are written in natural language

They're not, they're written in "mathese", where even relatively simple things are so obsfucated by postsecondary education-level (or almost) jargon that even an educated young adult genius (non math-major) might need many multiples of the reading time just to translate it. i.e. what does nu subscript xi2 stand for, what's this symbol, what's this word, what's the math-only meaning of this word? Etc, etc. Even legalese is probably closer to natural language than modern math proofs and some legaleses come with a (non-binding) natural language "translation". The purpose of that text portion seems to be to make a distinction between proofs by humans and computer-assisted proofs (presumably ones so painstaking to check well (machine code too!) that it wasn't done). There must be a good way to state that without claiming that most mathematical proofs are written in natural language. Sagittarian Milky Way (talk) 19:07, 25 February 2021 (UTC)

The definition of "natural language" is: a language that has developed naturally in use (as contrasted with an artificial language or computer code) (Oxford). Wikipedia describes it as "any language that has evolved naturally in humans through use and repetition without conscious planning or premeditation. Natural languages can take different forms, such as speech or signing. They are distinguished from constructed and formal languages such as those used to program computers or to study logic." What you describe as "mathese" is in fact a natural language under this definition. You seem to be suggesting that "natural language" is supposed to means something like "language that can be easily understood". Alas, that is not what it means. Magidin (talk) 21:52, 25 February 2021 (UTC)

Why are the equations not natural language if they are logic but are always natural language if they are a different field of mathematics? Okay I'm being too harsh, there are still sentences in math proofs but (correct me if I'm wrong) the equations are needed to follow what's going on right? Maybe not every last equation but often (the simplest alienese I've seen is an entire glyph-dense article on the tautology that an ordered set member or real number is either above, equal to or below another one, there was a long string of Byzantine glyphs just to say "if {x, y} in ℝ, x<y or x=y or x>y". What's wrong with saying something more Englishy like that instead of alienese?) Sagittarian Milky Way (talk) 00:30, 26 February 2021 (UTC)

They're written in natural language as opposed to, say, first-order logic. I think this is a reasonable distinction to make, and a reasonable way of putting it. I wouldn't object to an explanatory footnote pointing out that this is not the same thing as layman's language, if you really think this is a likely confusion on a reader's part. --Trovatore (talk) 01:02, 26 February 2021 (UTC)

Ah I see, it's not that this is one of the few where they took the effort to check for human bugs with computer and presumably painstakingly checked the binary maybe even hardware for bugs. They rewrote anything not in fundamentalest-possible logic into a thing so basic logic-y and probably verbose that an algorithm can spit out true or false just fromfollowing logic equations and making sure none of those Greek philosophy laws and stuff are violated. Not everyone would be interested enough to follow the links like automated theorem proving thus this interesting point could be unrealized by them. Could you say something to the effect of this is one of the few theorems that have been broken down into raw first-order logic for automated proving most are written in traditional human-friendly/-readable mathematics while most (including the original) are written in traditional human-friendly/-readable mathematics? Maybe natural language is a traditional phrase in mathematics (?) and likely most readers have seen enough alienese to not think it's just sentences at the highest level but they will think your idea of how dense a natural language can be is weird. Even if natural language is very barely technically correct, a correctness that is ironically not the plain English meaning of natural language. Sagittarian Milky Way (talk) 02:10, 26 February 2021 (UTC)

Your naive ideas of what computer proof assistants can handle have caused your description of this process to be inaccurate, so you're kind of missing the point. It is not necessarily broken down into more basic steps; it is, however, written in a more formalized and artificial language. It's like if I said, in English, that it doesn't matter what order you add two real numbers, their result will be the same, or if I wrote using logical notation $\forall x\in \mathbb {R} :\forall y\in \mathbb {R} :x+y=y+x$. The two things I might say mean more or less the same thing as each other, at similar levels of detail, but one is in a precise formalized language more easily read by computers and one is in natural language more easily read by people. You might also note that the formalized version is actually less verbose than the human version, not more. The point that you're missing is, this computer verification step leads to greater belief in the reliability of the same proof, because it's not the proof that had to be changed to make it verifiable, it's just the language it was written in. —David Eppstein (talk) 02:58, 26 February 2021 (UTC)

I see, a flaw does seem to have a slightly higher chance of sneaking through when the proof is partly words than when it's fully in logic glyphs and checked by computers. And now I know what upside-down A and tridents ∈ ∉ ∋ mean, heck if they're all this easy then maybe they're not so bad, maybe I could learn a few of the ones under the edit box a day. Sagittarian Milky Way (talk) 04:14, 26 February 2021 (UTC)

"Maybe natural language is a traditional phrase in mathematics (?)" Actually, the term comes from linguistics, not mathematics. Again, it is to distinguish regular languages that arise and evolve naturally, from artificial and created languages, like elvish, klingon, or esperanto; and from computer languages. The term includes technical, even highly technical, discourse, provided it takes place in the context of a natural language (like technical medical language being spoken in English; but not technical medical language being spoken in Esperanto). It does not mean "jargon free and accessible to a layman without any effort or knowledge". Magidin (talk) 17:27, 26 February 2021 (UTC)

That does expose a possible flaw in the presentation, though — we really aren't trying to distinguish mathematical English from mathematical Esperanto. Esperanto would also count as a "natural language" in the meaning we're trying to get at here. The point we want to make is that proofs are appeals to human reasoning, presented in human language, showing the reader/listener a path of reasoning that (barring mistakes or bad initial assumptions) leaves no room for doubt. This is as opposed to formal string manipulations in (say) Hilbert-style or Gentzen-style predicate calculus, which do not require thinking about their meaning at all in order to verify them. I'm not sure what the best way to get this across is. I don't quite agree with David that it's just a different language. --Trovatore (talk) 19:19, 26 February 2021 (UTC)

Mathematicians don't have a term of art or traditional word or phrase for logic element crunching in general? Like Boolean algebra, those Greek logic laws transcribed to formal p's, q's, if symbols etc... Sagittarian Milky Way (talk) 19:45, 26 February 2021 (UTC)

What does "logic element crunching" mean? For that matter, what does "logic element" mean? And what does this have to do with your initial request/complaint/edit suggestion? It all seems to be rooted in you misunderstanding the phrase "natural language" to mean "non-technical and jargon-free". Having cleared up this misunderstanding, is this just devolving into whether mathematics uses symbols and words that don't mean what you think they do or should mean? Also, that's not what "Boolean algebra" means, either. Magidin (talk) 21:07, 26 February 2021 (UTC)

It's clear SMW is not a mathematician; I don't think we need to keep pointing that out. Let's see if we can clarify the point being made. Do we first agree what point we actually want to make? I really don't think that point, whatever we agree on, would make any distinction between English and Esperanto, which possibly makes the phrase "natural language" problematic. --Trovatore (talk) 21:51, 26 February 2021 (UTC)

I called the logic symbols "logic elements" cause I don't know the answer to numeral:number::logic symbol:(proper mathematical name for these things). Operations (or manipulations or whatever the proper term is) being done on numbers is sometimes informally called number crunching so whatever the proper analogous term is for operations that can be done on logic thingies seems to be the important point Trovatore is mentioning rather than constructed vs natural language. And Boolean algebra is only one kind of logic symbol crunching, one of the few I've heard of, I do not know if the proof even used Boolean. Sagittarian Milky Way (talk) 22:47, 26 February 2021 (UTC)

".... were written in a way intended for human readers"? Magidin (talk) 22:10, 26 February 2021 (UTC)

Works for me. --Trovatore (talk) 22:12, 26 February 2021 (UTC)

Sounds good. Sagittarian Milky Way (talk) 22:47, 26 February 2021 (UTC)

The Paulson 2013 reference makes a stronger related point, that Gödel himself was philosophically opposed to exactly the sort of formalization of proof that was done in this case to his proof. —David Eppstein (talk) 23:58, 26 February 2021 (UTC)

Unicode and ASCII

I've just removed the following from the article

(Note: Computer programs typically represent sentences in Unicode rather than ASCII, and convert them more efficiently to produce smaller numbers. But we only need to choose some method and then apply it consistently to every sentence, and joining together the decimals is simpler to describe.)

The reason being that it is not correct. To start with unicode is not an encoding, so computer programs do not generally represent anything in unicode. Rather they use a specific encoding, which is usually compliant with some version of the Unicode standard. This might seem like a nitpick, and it is something that I could have just fixed. UTF-8, the most common encoding on the internet, is probably what is meant. However, the real issue with this claim is that UTF-8 is backwards compatible with the US-ASCII standard. So to say that UTF-8 is used "rather than ASCII" would be misleading at the very least. Additionally the second clause

Computer programs typically [...] convert them more efficiently to produce smaller numbers.

does not have a very clear meaning to me. However it seems to imply that UTF-8 is a more dense encoding than US-ASCII which is just not true; a character in US-ASCII encoded in UTF-8 is still the same byte, because UTF-8 is backwards compatible with US-ASCII.

So given that, if someone still wants to put a version of this claim into the article I would strongly recommend getting a reliable source for the claim.

AquitaneHungerForce (talk) 10:14, 1 November 2021 (UTC)

In fact, there is an issue here: Unicode has problems with numerical encoding of strings that ASCII doesn't, since the proposed encoding was essentially base-1000, which is works for ASCII and coding up the byte array representation of any encoding but is not collision-free if you work with Unicode codepoints. But while a gesture at practical encoding is appropriate, discussion of the technicalities facing actual computer systems quickly distracts the reader from grappling with the topic of the article. I'm against explicit treatment of this point at any length, regardless of sourcing. I'm wondering if the discussion can readably be made more concise.— Charles Stewart (talk) 11:34, 1 November 2021 (UTC)

If the issue of ASCII vs Unicode ever comes up in this article, then the text in which it comes up should be reworded to remove the need for it. Considerations like that are far off-topic for this article. I understand the desire to make the ideas accessible to readers whose shortest path may be through their computer knowledge, but if specific character encodings ever come up, then we've lost the thread. --Trovatore (talk) 16:31, 1 November 2021 (UTC)

I think that a short mention in a footnote, along the lines of "Actual computer systems use more complex or specialized methods to encode strings e.g. UTF-8" would be fine. But I agree that this article does not need to get in the details and I think it should not be in a parenthetical but rather a footnote because this is not the point. AquitaneHungerForce (talk) 19:02, 1 November 2021 (UTC)

First-order vs. higher-order version

(The following discussion was started by a side remark at Talk:Peano_axioms#Downgrade_the_quality_level_of_the_article_to_B. It has been moved to here in order to disrupt the main discussion at Talk:Peano_axioms.)

@Vkuncak: Maybe you are the right person to explain to me why Gödel's incompleteness theorem is considered to refer to first-order logic in Wikipedia, while his original 1931 article (e.g. [1]) refers to Principia Mathematica, and, in particular, higher-order logic (in sect.2, p.176, variable symbols of arbitrary high order are introduced before fn.17; on p.177, axiom I.3 is the classical 2nd-order induction axiom, with x₂ a predicate variable, ".", "Π", and "⊃" meaning "and", "for all", and "implies", respectively). I guess I'm unaware of some modern treatment of Gödel's result which transcribed it to FOL. Maybe you could even devise a clarifying remark for the page Gödel's incompleteness theorems? Many thanks in advance - Jochen Burghardt (talk) 19:06, 31 January 2022 (UTC)

Jochen: I'm not Vkuncak, but if I could mix in, I think that may be more of a Principia Mathematica question than a general math-logic question. The notation and terminology used by Russell turned out to be pretty much of a dead end; hardly anyone learns it anymore for mathematical reasons (though historians may still be interested). And yes, I suppose it's probably good to know about if you want to read Gödel's original paper, but the same remarks apply — Gödel was doing something for the first time, and putting it in the context of the day, but there are much more efficient ways to learn the content now.

I'm not competent to answer the question directly because I've never bothered to put in the effort needed to understand Principia Mathematica, but I could offer a guess. It likely has to do with two different senses of the phrase "second-order logic". In the context of this article, for example, second-order logic with "full semantics", plus the original Peano axioms, is enough to make the theory categorical — there is only one model up to isomorphism. "Full semantics" means that you have first-order variables that range over natural numbers and second-order variables that range over sets of natural numbers, and the latter really range over all sets of natural numbers.

On the other hand, you can take exactly the same theory but interpret it with Henkin semantics, which means that you give it an interpretation by specifying what both the first-order and second-order variables range over. That is, you limit the second-order variables to ranging over a pre-specified class of sets of naturals, rather than all of them. Now the theory is no longer categorical. It's actually a theory of first-order logic, though it has second-order variables.

Does that help? It might be a nice thing to bring up at the refdesk if you want more details. We could use some good questions like that. --Trovatore (talk) 19:42, 31 January 2022 (UTC)

Jochen: Thank you for pointing out to this historical development, of which I was not aware of! I was merely following the expositions in several textbooks, including Mendelson and the handbook by Samuel Buss. These all refer to FOL formulation of the problem. What matters for the incompleteness theorem is to have a system where provability is recursively enumerable. Strong enough FOL theory with decidable axiom schemas is one typical way to get recursively enumerable definition of provability. Second order logic with full semantics is not such an effective definition: there is no way to enumerate all true facts according to such semantics. Vkuncak (talk) 20:25, 31 January 2022 (UTC)

Trovatore: Henking semantics for second order (and higher-order) logic could be applied to the question of models of Peano arithmetic and provability, but do we actually have interesting facts to mention in that direction (other than it is a valid thing to consider)? If yes, this line of thinking could be used to expand and clarify analogously the paragraph on categoricity proof carried out in first-order axiomatization of ZFC. I thought how to clarify that paragraph, but I am not entirely sure about the intention was with it originally, so I left it as it is. Vkuncak (talk) 20:25, 31 January 2022 (UTC)

@Trovatore and Vkuncak: Thanks for your answers. I moved the discussion path to here in order not to distract the quality level discussion at Talk:Peano_axioms#Downgrade_the_quality_level_of_the_article_to_B.

My point with Principia Mathematica is just that it admits arbitrary high order quantifications, independent of the uncommon notation.

As for Henkin semantics (of which I was unware - thanks for the hint!), categoricity would depend on the choice of the domain sets for first- and second-order variables; if they are chosen to be the full sets, Henkin semantics coincides with standard semantics, doesn't it? - Jochen Burghardt (talk) 10:04, 1 February 2022 (UTC)

Yes, the standard interpretation will almost always be a model in the Henkin semantics. I've rewritten the paragraph at second-order logic making this clear. We really should have a full article on Henkin semantics: the details are a little tricky but make the picture much clearer. — Charles Stewart (talk) 10:15, 1 February 2022 (UTC)

Second theorem in terms of the first

The first theorem states that there exists a true statement F cannot prove. A few months ago I added an edit stating that the second theorem in particular provides a concrete example of one of the true statements that F cannot prove, namely Cons(F). It was reverted, with edit summary "how do you know it [Cons(F)] is true?" But since one of the premises of the theorem is that F is consistent, Cons(F) is true, so I believe Cons(F) is a concrete example of a true statement not provable from F. If this reasoning is correct, should the specification be re-added to the article? I think it may be helpful to see the second theorem as providing a specific example of the first theorem, even if the first theorem already involves the Godel sentence. C7XWiki (talk) 08:02, 27 October 2022 (UTC)

I have a source that I think claims the second theorem provides an example of the first:

"He [Godel] followed this with his First and Second Incompleteness Theorems. The first one asserts that every sufficiently extensive, consistent formal system (and almost all formal systems are sufficiently extensive) is incomplete in the sense that there exist sentences expressed within the system that cannot be decided within it. The second one provides additional information that consistency of such a system is a sentence of this kind."

From Harvey Friedman's Research on the Foundations of Mathematics (1985), Studies in Logic and the Foundations of Mathematics vol. 117. p.viii. C7XWiki (talk) 09:45, 8 November 2022 (UTC)

Image

Regarding Jochen's addition of an image, here.

Jochen says in the edit summary "no idea how to illustrate the theorem itself", and I basically agree. Oh, someone could probably come up with something, maybe some sort of block diagram, but I doubt it would actually be helpful.

But to be honest I don't think the proffered image is particularly helpful either.

So my vote would be just not to have an image. I don't think there's any great value in having an image purely pro forma. If there's no image that genuinely helps direct the reader to the point of the article, then why have one at all? --Trovatore (talk) 20:25, 20 February 2023 (UTC)