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

What Gödel Discovered (2020)

stopa.io

Post reply on HN
Print view View original

31–39 of 39 posts

Re: What Gödel Discovered (2020)

#31

Post by layer8 »

What Gödel showed is that (in any sufficiently powerful formal axiomatic system) the set of provable statements isn’t the same as the set of true statements. This means that either there are true statements that aren’t provable (incompleteness), or that there are provable statements that aren’t true (inconsistency), or both.

One way to see this is via the halting problem. For any program (with a fixed input), there is a truth of the matter of whether it will eventually halt or not. In the formal system, for every (Turing-machine) program P we can define a function s_P(n) that gives us the state of the program after n steps (by recursive definition). Then we can write for any program P the statement H(P) = “there exists a natural number n such that s_P(n) is a halting state”. Furthermore, we can write a program R that, given any program P as input, enumerates all proofs of the formal system (this is possible because proofs are strings, and we can write a program that enumerates all strings) and that for each proof checks if it is a proof of H(P) or of not H(P), and if it finds such a proof, stops and outputs the result (P halts or doesn’t halt). If such a proof exists, then R will eventually find it. And if R would find a proof for any P, then this would solve the halting problem.

But we know that the halting problem is undecidable, which means that there must be programs P for which there is neither a proof of H(P) nor of not H(P). This shows that there are truths (the program will halt or won’t halt) for which there is no proof in the formal system; or alternatively, that the formal system is inconsistent and proves falsities.

Re: What Gödel Discovered (2020)

#32

Post by mjh2539 »

cousin_it wrote: post #8
annie511266728 wrote: post #7

Earlier quoted context omitted.

Yeah, I think that's the tradeoff. Löb gets you to the main idea faster, but Gödel numbering is the part that makes it feel like the system is actually doing it itself. Without that step, it can start to feel a bit too close to the liar paradox.

Yeah. I'd say half of the work is Gödel numbering and the other half is the diagonal lemma.

This is the most apt answer I've read thus far.

Re: What Gödel Discovered (2020)

#33

Post by Nevermark »

jb1991 wrote: post #30
Nevermark wrote: post #11

Earlier quoted context omitted.

Other names for Gödel encoding: Digital. Binary. Zorros and Unos. Today Gödel encoding is so pervasive, it’s easy to miss that everything is trivially Gödel encladed. Because like most everything invisible, it’s right in front of us. We Gödel our memes and gift cards, and (pick your poison) pr0ns. Colors and AI’s, lax ASMR’s and our (sneaky don’t read me) terms of service. Even this very small humble . Gödel isn’t ea…

You are suggesting Godel created the punctuation mark known as a period? Obviously not. But I'm not sure what you are trying to say..

That period was encoded in a symbol string, i.e. it is a bit string.

Today we encode everything in bi-symbol strings.

This was not common when Gödel crafted his incompleteness theorem. And at the time it was a novel approach for setting up a context for testing the limits of computing.

Some people can still be struck by it as novel when reading the proof, because in context it was, and still feels that way. But today "symbol string" representation is ordinary and pervasive.

Re: What Gödel Discovered (2020)

#35

Post by bazoom42 »

Nevermark wrote: post #11
dvt wrote: post #2

This blog post gets way too caught up in Gödel numbers, which are merely a technical detail (specifically how the encoding is done is irrelevant). A clever detail, but a detail nonetheless. Author gets lost in the sauce and kind of misses the forest for the trees. In class, we used Löb's Theorem[1] to prove Gödel, which is much more grokkable (and arguably even more clever). If you truly get Löb, it'll kind of blow y…

Other names for Gödel encoding: Digital. Binary. Zorros and Unos. Today Gödel encoding is so pervasive, it’s easy to miss that everything is trivially Gödel encladed. Because like most everything invisible, it’s right in front of us. We Gödel our memes and gift cards, and (pick your poison) pr0ns. Colors and AI’s, lax ASMR’s and our (sneaky don’t read me) terms of service. Even this very small humble . Gödel isn’t ea…

Gödel did not invent encoding. Morse was widely used before Gödel.

Re: What Gödel Discovered (2020)

#36

Post by bazoom42 »

coldtea wrote: post #29
bazoom42 wrote: post #26

Earlier quoted context omitted.

So would it be just as correct to use an electrical circuit as example, i.e. before Principia it was not believed possible to model an electrical circuit in a formal language?

I still don't think it's possible to model an electrical circuit in a formal language, except if you mean the very crude high level behavior. Getting to electron flows and even quantum effects though?

So what do you believe can be modeled in a formal language?

Re: What Gödel Discovered (2020)

#37

Post by Nevermark »

bazoom42 wrote: post #35
Nevermark wrote: post #11

Earlier quoted context omitted.

Other names for Gödel encoding: Digital. Binary. Zorros and Unos. Today Gödel encoding is so pervasive, it’s easy to miss that everything is trivially Gödel encladed. Because like most everything invisible, it’s right in front of us. We Gödel our memes and gift cards, and (pick your poison) pr0ns. Colors and AI’s, lax ASMR’s and our (sneaky don’t read me) terms of service. Even this very small humble . Gödel isn’t ea…

Gödel did not invent encoding. Morse was widely used before Gödel.

Morse didn't conceptually extend encoding to self-referential symbolic systems. Morse's insight was pure communication of symbols devoid of meaning.

Important but nowhere near the same.

Today, general symbolic encoding is viewed as trivial. Every symbol we have is pervasively encoded as bits, so of course entire expressions are. So Morse's code might seem comparable.

But what Gödel invented went well beyond Morse. We are just jaded with regard to his insight now.

Re: What Gödel Discovered (2020)

#38

Post by bazoom42 »

roxolotl wrote: post #17
bazoom42 wrote: post #16

Earlier quoted context omitted.

The article use “describing the behavior of a dog” as something people began to think was possible because of Principia. This is what I don’t get. Was this thought impossible before Principia? On what grounds? What about describing an electrical circuit formally? Surely this was thought possible before Principia was published.

The assumption made by many in the early 20th century, spurred on by the recent successes of unification and formalization, was essentially that we could formally describe the entire universe. Godel’s proof shows that if you attempt to formally describe something there’s either an inconsistency or it’s incomplete. That doesn’t mean you cannot describe the behavior of a dog formally but it does mean the same formula w…

> Godel’s proof shows that if you attempt to formally describe something there’s either an inconsistency or it’s incomplete.

The “something” Gödels proof talks about is axiomatic systems. It doesn’t talk about physical objects.

Re: What Gödel Discovered (2020)

#39

Post by bazoom42 »

Nevermark wrote: post #37
bazoom42 wrote: post #35

Earlier quoted context omitted.

Gödel did not invent encoding. Morse was widely used before Gödel.

Morse didn't conceptually extend encoding to self-referential symbolic systems. Morse's insight was pure communication of symbols devoid of meaning. Important but nowhere near the same. Today, general symbolic encoding is viewed as trivial. Every symbol we have is pervasively encoded as bits, so of course entire expressions are. So Morse's code might seem comparable. But what Gödel invented went well beyond Morse. We…

Of course you can encode self-references in morse code, how could morse prevent that? Just use the same lisp syntax as in the article and then encode using morse code instead of Gödel numbering.

The purpose of Gödel numbering is to represent an arbitrary-length string of symbols as a single integer which allows you to manipulate it using Peano arithmetic.

But it is not like Gödel invented binary as you seem to suggest. Baudot code (a 5-bit character encoding) was in use in 1870’s.

In any case, Gödel-numbering is the least interesting part of the the theorem. The groundbreaking idea is creating statements about theorems.

Post reply on HN