Live data from Hacker News

What Gödel Discovered

stopa.io

131–140 of 271 posts

Re: What Gödel Discovered

#133

Earlier quoted context omitted.

Another example of why I don't like the word "truth" because I think it does more to muddy the situation than clarify it. Let's drop "truth" for a sec. Let's say I come up with a series of axioms about cows. They describe spots on cows, how many legs cows have, etc. Now I come up with a sentence "all cows have spots." There are two ways of proving this sentence. One is a "semantic proof." That is I go and round up ev…

"True" in this context is a technical definition, not some hand-waving thing. A sentence X being true means every model satisfies X. Provable means logical deduction within the theory proves X. So actually, Godel's theorems are exactly about truth and provability.

Yes if you appeal to model theory you're on firm ground with truth. But that's not how most informal introductions to the incompleteness theorems go (and indeed not how this article went about it).

More to the point, Godel's incompleteness theorems are theorems of proof theory, not model theory. Their proofs can be carried out with no recourse to models at all. And I think they are far less prone to being misunderstood when carried out without recourse to models and by extension without recourse to semantic truth.

You can of course choose to interpret them in model theory if you're working in a semantically complete logical system such as first-order logic with the usual semantics or second-order logic under Henkin semantics, and it is often illuminating to do so once you have those fundamentals. But I think in an informal setting those will tend only to confuse rather than clarify. And importantly the incompleteness theorems still hold in contexts where you don't really have a meaningful model theory to speak of.

Re: What Gödel Discovered

#134
post #7

I’m a mathematician who spent many hours thinking about Goedel theorem and adjacent topics. The author in a self-deprecating way says that he’s not a mathematician, but just a programmer. Bear no mind to that: this is one of the best popular expositions of Goedel theorem I’ve seen. Everything is very accurately explained, there are no silly mistakes and untruths one often sees mentioned in context of Goedel theorem,…

This brought a big smile to read, thank you :)

There is an extraordinarily minor typo: “PM-LIsp”

I point it out only because your work here is so good that it feels wrong not to smooth out any small splinters.

Thank you for making this!

Re: What Gödel Discovered

#135
Very interesting. I'm wondering if this has implications in physics ? Since "the book of nature is written in mathematical language", does this mean that attempts to find a unified theory of everything are doomed ? I'm thinking not necessarily, since we wouldn't need to prove all possible physical phenomena, only those that actually happen, but how do we know if they are among the one that can be proven ?

Re: What Gödel Discovered

#136
post #30

> For example, a gentleman called Frege discovered that he could craft a theory of sets, which could represent just about everything. For numbers, for example, he could do something like this: [ 0 is {}, 1 is {{}}, 2 is { {{}} {} }, etc. ] I don’t know Frege too well, but believe this is due to von Neumann, not Frege: https://en.wikipedia.org/wiki/Ordinal_number#Von_Neumann_def...

You might be correct, Frege defined it (roughly) in a similar way, you can read his original publication here: https://ia800207.us.archive.org/22/items/diegrundlagende00fr... It starts on book page 87, or PDF page 125. Basically, what he seems to be doing is to define 0 as the number of "everything that is not equal to itself" ("die Anzahl, welche dem Begriffe 'sich selbst ungleich' zukommt"), and 1 to be the number…

Ah, yep, interesting! Thanks for the direct link.

Ok, I wrote a long reply trying to figure out what exactly 2 is for him in terms of modern set theory notation, but I got really muddled. German’s not my mother-tongue/the pdf isn’t searchable, and when he says “Anzahl”/“Zahl” I’m never sure if he’s talking about size or abstract property, and would have to read a lot more of the book to figure out!

[but naively: in §76 “n folgt in der natürlichen Zahlenreihe unmittelbar auf m.” is defined as “es giebt einen Begriff F und einen unter ihn fallenden Gegenstand x der Art, dass die Anzahl, welche dem Begriffe F zukommt, n ist, und dass die Anzahl, welche dem Begriffe ““unter F fallend aber nicht gleich x” zukommt, m ist””. “ is ‘n follows directly after m’ is defined as: there’s a preposition F and an object satisfying F such that the number of objects satisfying F is n and the number of objects satisfying “satisfying F but not x” is m. This really looks von Neumann like!]

He also talks about numbers in §56 (but Zahlen, not Anzahlen)...with the problem of deciding in Julius Caesar is an (ordinal?) number or not, or whether anything has Julius Caesar as a number.

[there’s also an english translation here http://www.naturalthinker.net/trl/texts/Frege,Gottlob/Frege,... but honestly it’s not much easier there :P ]

ALL of this is confusing with what wikipedia says on the matter of defining natural number “Gottlob Frege and Bertrand Russell each proposed defining a natural number n as the collection of all sets with n elements.” - which may also be the case, but lacks a citation alas. https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na...

I don’t know if I have it in me to straighten this all out (that is, to RTFM).

Re: What Gödel Discovered

#137

Earlier quoted context omitted.

I am trying to follow, but I feel I am hanging Goedel incompleteness theorem -> apply this to "theories" Goedel completeness theorem -> apply this to a specific "model", of the theory So there can be "something true but not provable" in the theory, and "we cannot describe all true things about specific models", but ....what?

The answer you got from lmm and others is wrong (I am a professional mathematician and did research in logic). The completeness theorem says simply: if T is a first-order theory (list of axioms in first-order logic), any sentence true in every model of T is provable by logical deduction in T. The first incompleteness theorem says: if T is a consistent recursively enumerable theory that can contains a sufficient amoun…

Ah... this also has nuances. Although perhaps the unspoken assumption of your post is that you are trying to explain the incompleteness theorems through the lens of first-order logic? In which case your definitions are completely fine.

But just to be clear, your summarization of the first incompleteness theorem is through the lens of model theory and therefore predicated on the completeness theorem and doesn't hold in its absence. The canonical example is second-order PA under full second-order semantics, which has only one model (this is also true of second-order ZFC). Hence there do not exist sentences of second-order PA which are true in some models and false in others.

To fully flesh out the syntactic results of Godel's incompleteness theorems and their semantic consequences when Godel's completeness theorem holds, there's the following syntactic -> semantic chains.

1st incompleteness: there exist sentences which cannot be proved within any theory containing enough arithmetic. Therefore by Godel's completeness theorem there are sentences in the theory which are satisfied by some models and whose negation are satisfied by other models.

2nd incompleteness: the sentence Con(T) corresponding to the informal sentence "the theory T is consistent" cannot be proved within the theory T itself assuming T contains enough arithmetic. Therefore by Godel's completeness theorem there are models of T where Con(T) is satisfied and models of T where Not(Con(T)) is satisfied.

As I said in another post while Godel's completeness theorem is an essentially model-theoretic result (and it is the foundation that all other model theory builds on), Godel's incompleteness theorems are fundamentally syntactic results that live in the realm of proof theory, rather than semantic ones that live in the realm of model theory, although they have deep implications for the latter.

(Also to be extraordinarily pedantic, as you point out elsewhere, a sentence is true if it is satisfied by all models. Hence technically it is a misnomer to say that a sentence is true in a given model. Rather a sentence is satisfied by a given model. But it's a common enough bit of informal terminology, but I just want to point it out for people who aren't familiar with model theory so that they don't get tripped up trying to square different formal definitions of "true.")

Re: What Gödel Discovered

#138
Nice article, I do like the way it's explained in a way that a programmer like myself can understand it.

I did note a few typos that I will take the opportunity to report here, in order to make an already great article a little better:

Under "PM-Lisp Axioms": Looking at the code "(when (or p q) (or (q p))". I don't think the (q p) should have parens around it.

Under "(proves a b)": There is no ending quote at the end of the last sentence.

Under "(subst a b c)": I find the text "PM-LIsp". I guess the I should be lower case.

Re: What Gödel Discovered

#139

Earlier quoted context omitted.

This brought a big smile to read, thank you :)

There is an extraordinarily minor typo: “PM-LIsp” I point it out only because your work here is so good that it feels wrong not to smooth out any small splinters. Thank you for making this!

Oi, thanks for the kind words and the catch! Updated (should take a few minutes to show up)

Re: What Gödel Discovered

#140

Nice article, I do like the way it's explained in a way that a programmer like myself can understand it. I did note a few typos that I will take the opportunity to report here, in order to make an already great article a little better: Under "PM-Lisp Axioms": Looking at the code "(when (or p q) (or (q p))". I don't think the (q p) should have parens around it. Under "(proves a b)": There is no ending quote at the end…

Thank you for taking the time! Updated -- should take a few mins to show up :)
Post reply on HN