Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

What Gödel Discovered

stopa.io

Post reply on HN
Print view View original

191–200 of 271 posts

Re: What Gödel Discovered

#191

Post by nmadden »

hvis wrote: post #189

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 language…

It’s not so much that they’re neither true nor false (they’re not paradoxes), but that they can be true in some interpretations and false in others. I wrote up some notes about this here: https://neilmadden.blog/2020/11/17/some-incomplete-thoughts-...

Re: What Gödel Discovered

#192

Post by praptak »

hvis wrote: post #189

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 language…

No, it is not about nonsensical phrases. Godel proved that there are some sentences that are true, but they have no proof in the system.

Re: What Gödel Discovered

#193

Post by ProfHewitt »

xyzzyz wrote: 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,…

Dear xyzzy,

Unfortunately, you missed that the author's proof does not actually prove inferential undecidability (sometimes called "inferential incompleteness") of Russell's Principia Mathematica for the following reason:

     The [Gödel 1931] proposition *I'mUnprovable* does **not** exist in Principia Mathematica because it violates restrictions on orders of propositions that are necessary to avoid paradoxes (such as Russell's Paradox). Gödel numbers (and in the author's case Lisp expressions) leave out the order of a proposition with the consequence that the Diagonal Lemma **cannot** be used to construct the proposition *I'mUnprovable*.
Furthermore, existence of the proposition I'mUnprovable contradicts the following fundamental theorem of provability that goes all the way back to Euclid:

     A theorem can be used in other proofs.
See the following article for further details:

https://papers.ssrn.com/abstract=3603021

Re: What Gödel Discovered

#194

Post by JesseMeyer »

"This meant that no formal system, could prove by itself, that it could only produce true statements. "

I see this generalization often, that Godel showed that all formal systems share this restriction, but doesn't the formal system have to be at least be able to express the properties of integers?

Is the ability to formally express integers relatively a particularly demanding constraint on choice of axioms?

Re: What Gödel Discovered

#195

Post by ProfHewitt »

dwohnitmok wrote: post #60

I thought I replied to this post, but I guess not and my reply ended up being a top-level reply, which is just as well. I will just mention my main two quibbles to this otherwise excellent post and others like it so that other people who embark on introductory posts to Godel's results don't fall into the same trap. 1. Please don't bring the notion of truth into an introductory explanation (such as in the section "Pow…

Dear dwohnitmok,

Actually, powerful strongly-typed theories used in Computer Science can prove their own consistency!

See the following article for for how this is done:

https://papers.ssrn.com/abstract=3603021

As you pointed out, such a proof does not mean that it is not operationally possible to derive a contradiction using axioms and rules of inference.

Instead our confidence in the consistency of a powerful strongly-typed theory is because there is just one model of the axioms of the theory up to a unique isomorphism, which formalizes the concept of "truth" that you mentioned in your post.

For example, see the following article:

https://papers.ssrn.com/abstract=3457802

Re: What Gödel Discovered

#196

Post by greatquux »

ProfHewitt wrote: post #193
xyzzyz wrote: 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,…

Dear xyzzy, Unfortunately, you missed that the author's proof does not actually prove inferential undecidability (sometimes called "inferential incompleteness") of Russell's Principia Mathematica for the following reason: The [Gödel 1931] proposition *I'mUnprovable* does **not** exist in Principia Mathematica because it violates restrictions on orders of propositions that are necessary to avoid paradoxes (such as Rus…

I'm going to need someone to come along and write up a layman's summary of this article. :) Does it change the end result of Gödel? Or is it basically the equivalent of saying what some restricted programming languages are doing, that we can get "good enough" results and not have these problems by restricting what we can do in the language?

Re: What Gödel Discovered

#197

Post by daralthus »

Liron wrote: post #180

People act like Godel’s Incompleteness Theorem is all about how formal systems are limited in their level of “insight about truth”. But actually it’s just the same observation as the Halting Problem: you have a system that tries to reason about the behavior of other systems (like Turing Machines or axiomatic set theory), but it can’t possibly always introspect about its own behavior because you can also configure it…

Because of the halting issue you cannot summarise reality into a set of axioms and rules. Which is the original purpose of mathematics. Therefore you cannot say mathematics is right or true without adding at the end: "this actually could all be wrong".

Re: What Gödel Discovered

#198

Post by dwohnitmok »

Konohamaru wrote: post #185
dwohnitmok wrote: post #143

Earlier quoted context omitted.

> The propositions that are undecidable are NOT AT ALL connected to the propositions that are independent. I'm not quite sure what you mean by undecidable propositions, but I assume it to mean something like the following? Propositions which must be true or must be false (i.e. are satisfied/not satisfied respectively by all models which satisfy the overall theory), but for which there is no finite proof that they hol…

> To take a step back, the assertion that there are fundamentally undecidable mathematical propositions in the real sense you're laying out (as opposed to more formal treatments of truth in model theory) is a statement of the Platonist school of mathematical philosophy. To go one step forward, these undecidable/uncomputable statements are computed by humans all the time, which makes the Platonist school of mathematic…

> these undecidable/uncomputable statements are computed by humans all the time

This is a far stronger statement than I think even Platonists would accept. What examples of non-computable statements that are computed by humans do you have in mind?

Even putting on my Platonist hat (which I'll wear for the rest of this reply), I would still argue, in line with xyzzyz's comment, that at most humans deal with computable descriptions of non-computable things. For example, the description of the real numbers is computable even if the real numbers themselves are not. Likewise even if the real numbers are not computable, we can only ever work with computably-definable (indeed only finitely definable) real numbers rather than arbitrary real numbers.

To use the map-territory analogy, while the territory is the thing we care about, the only things we can work with, manipulate, and compute are computable maps.

For example Chaitin's Constant is a non-computable real number. However, we never work with Chaitin's Constant directly, but rather with our finite description of it, from which we deduce all sorts of other facts.

There are therefore many things about Chaitin's Constant we will never know. But that is the Platonist's lot in life.

As an aside, there's in fact a formalization of this that states that a mathematical universe consisting solely of finitely definable entities and nothing else is perfectly reconcilable with ZFC. See https://mathoverflow.net/questions/44102/is-the-analysis-as-...). Now as I continue to wear my Platonist hat I don't believe for a second that this is in fact how the mathematical universe actually operates, but it is a good explanation for why it is beyond the mathematical abilities of humans to distinguish between this definable universe and the real universe we live in.

Re: What Gödel Discovered

#199

Post by skoll43 »

daralthus wrote: post #197
Liron wrote: post #180

People act like Godel’s Incompleteness Theorem is all about how formal systems are limited in their level of “insight about truth”. But actually it’s just the same observation as the Halting Problem: you have a system that tries to reason about the behavior of other systems (like Turing Machines or axiomatic set theory), but it can’t possibly always introspect about its own behavior because you can also configure it…

Because of the halting issue you cannot summarise reality into a set of axioms and rules. Which is the original purpose of mathematics. Therefore you cannot say mathematics is right or true without adding at the end: "this actually could all be wrong".

at the end: maybe not even wrong

Re: What Gödel Discovered

#200

Post by Sharlin »

ozankabak wrote: post #182

So if we have a theory expressive enough to make statements about ordinary (Peano) arithmetic, we can always form a self-referential statement within the framework of this theory which we can not prove or disprove. So far, so good. Here is my question: What happens if we restrict/weaken the theory to preclude self-referential statements? Obviously, we will lose our ability to express certain arithmetic statements whi…

We lose the ability to reason about sets of unbounded size. As long as we only restrict ourselves to some bounded subset of integers, Gödel can't do the trick with his numerals. Equivalently, on the CS side, we must restrict ourselves to total functions, that is, all valid programs must provably halt after some bounded number of steps.
Post reply on HN