I've read Godel, Escher, Bach, and I've read this. It's a very nice explanation.
But everywhere I see, Godel's theorem is touted as some kind of deep philosophical insight, whereas from what I understand, informally it could be rephrased as "if you have a usable language for mathematical proofs, some phrases in that language must be neither true nor false (i.e. nonsensical)".
Nonsensical phrases in our human languages in nothing new, so the conclusion becomes that much less exciting. Though I'm sure it's valuable for fundamental math theory.
Wasn't that proof using a paradox, though? Then that basically really proves the existence of paradoxes. It doesn't disprove the existence of all other kinds of statements, of course.
A statement 'x == 1' might be contextual (with a free variable x), but I think the theory is talking more about statements like
for all x
(x + 1)^ 2 == x^2 + 2*x + 1
which is true and does not depend on x. Contrast that with
for all x
x == 1
which is obviously false.
But the proof outlined in the article constructed a statement with a free variable, where a substitution with a certain value leads to a statement which is neither true, nor false. That means that the general statement in the proof's example is neither true nor false either.
Sorry about the awkward terminology, BTW, my engineering degree was a decade ago and in a language other than English.
No, the statements in Gödel’s proofs are not paradoxes.
Substitutions of variables are not the same as interpretations. The interpretation tells you what the nonlogical symbols like *, +, ^, 1, 2, 3 etc mean.
To me reading this article it was striking to consider the relationship between language and (mathematicsl/logical) truth this way. In my mind it correlates with the quantum phenomenon that observing something fundamentally alters its state.
But everywhere I see, Godel's theorem is touted as some kind of deep philosophical insight, whereas from what I understand, informally it could be rephrased as "if you have a usable language for mathematical proofs, some phrases in that language must be neither true nor false (i.e. nonsensical)".
Nonsensical phrases in our human languages in nothing new, so the conclusion becomes that much less exciting. Though I'm sure it's valuable for fundamental math theory.