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

21–30 of 39 posts

Re: What Gödel Discovered (2020)

#21

Post by DarkNova6 »

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…

As a non-mathematician I always wondered about one thing. Because the way I interpret the Incompleteness Theory is that "you cannot have a universal system of infinite expressiveness, because you will need a more expressive one to prove it".

In other words, you can't have a top-down universal system. But you very well can have well described ones perfectly describe observable behaviour without defects.

Or is this too reductive?

Re: What Gödel Discovered (2020)

#22

Post by ghywertelling »

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…

Godel's 1st Incompleteness Theorem - Proof by Diagonalization

https://www.youtube.com/watch?v=PpSxqde0af4

This is another good exposition.

Re: What Gödel Discovered (2020)

#23

Post by coldtea »

bazoom42 wrote: post #12

I’m confused by this jump to the natural world: > could you encode in pure logic how a dog behaves Assuming we knew enough about how a dog behaves (or less ambitiously, a more primitive organism) I would assume this could be described in a formal language. But why would Principia be needed for this? Math have been used to model natural phenomena a long time before Principia.

>Assuming we knew enough about how a dog behaves (or less ambitiously, a more primitive organism) I would assume this could be described in a formal language. But why would Principia be needed for this?

It explains this directly before that phrase:

"Their language was dense and the work laborious, but they kept on proving a whole bunch of different truths in mathematics, and so far as anyone could tell at the time, there were no contradictions. It was imagined that at least in theory you could take this foundation and eventually expand it past mathematics: could you encode in pure logic how a dog behaves, or how humans think?"

>Math have been used to model natural phenomena a long time before Principia.

Which means little in this context. The question posed wasn't if you can use some math to describe some natural phenomenon.

The question posed was whether one could model the whole thing (e.g. how a dog behaves) in a formal language - not just take some isolated equations and apply it to this or that aspect of phenomenon (especially if it's a mere approximation). That they already knew, e.g. the equations for planetary motion.

Re: What Gödel Discovered (2020)

#24

Post by coldtea »

bazoom42 wrote: post #16
ergonaught wrote: post #15

Earlier quoted context omitted.

> I would assume this could be described in a formal language The assumption is the first problem, no? If the formal language is complete, it must be inconsistent. If it is consistent, it must be incomplete. If the language is incomplete or inconsistent, you may be unable to encode dog behavior in it.

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.

>This is what I don’t get. Was this thought impossible before Principia? On what grounds?

Even the full formalization of mathematics wasn't considered certain (*) before Hilbert/Principia and those 20th century attempts. Much less the formalization being applied everything in the physical world or even animal behavior.

* in retrospect rightly so, because it wasn't, at least not without inconsistency/incompleteness.

Re: What Gödel Discovered (2020)

#26

Post by bazoom42 »

coldtea wrote: post #23
bazoom42 wrote: post #12

I’m confused by this jump to the natural world: > could you encode in pure logic how a dog behaves Assuming we knew enough about how a dog behaves (or less ambitiously, a more primitive organism) I would assume this could be described in a formal language. But why would Principia be needed for this? Math have been used to model natural phenomena a long time before Principia.

> Assuming we knew enough about how a dog behaves (or less ambitiously, a more primitive organism) I would assume this could be described in a formal language. But why would Principia be needed for this? It explains this directly before that phrase: "Their language was dense and the work laborious, but they kept on proving a whole bunch of different truths in mathematics, and so far as anyone could tell at the time,…

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?

Re: What Gödel Discovered (2020)

#27

Post by manofmanysmiles »

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…

Do you recommend reading "Gödel, Escher, Bach: an Eternal Golden Braid"?

Re: What Gödel Discovered (2020)

#28

Post by dvt »

DarkNova6 wrote: post #21
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…

As a non-mathematician I always wondered about one thing. Because the way I interpret the Incompleteness Theory is that "you cannot have a universal system of infinite expressiveness, because you will need a more expressive one to prove it". In other words, you can't have a top-down universal system. But you very well can have well described ones perfectly describe observable behaviour without defects. Or is this too…

The easiest way to think about it is like this:

We have these things called systems: a "system" is anything that follows rules: a board game, traffic, the English language, math, C++, etc. Some systems are smart and they can talk about themselves, but others can't. For example, Tic-Tac-Toe can't talk about Tic-Tac-Toe, but English can talk about English.

Gödel is interested in smart systems because dumb systems are boring.

Some systems are useful: they are "useful" if they always say true things. So math is more useful than English. I can lie in English, but I can't lie in math. (Formally, this is what we call consistency).

So here's a problem for you: suppose we have a smart-useful-system, call it SUS. SUS should be able to say "SUS is useful." It can talk about itself and it can't lie, so we should have no problem, right?

Gödel showed that if our system can actually say that about itself, it wasn't useful to begin with. For a few centuries, philosophers and mathematicians were trying to come up with the "one perfect system": useful, smart, and also complete (it can say all true things), and a few more properties. Turns out such a system is impossible.

NB: I use the words "say" or "talk about" in a very hand-wavy fashion, sometimes I mean Prove(), sometimes I mean Entail(). The details are very nuanced, and this isn't meant to be a deep dive.

Re: What Gödel Discovered (2020)

#29

Post by coldtea »

bazoom42 wrote: post #26
coldtea wrote: post #23

Earlier quoted context omitted.

> Assuming we knew enough about how a dog behaves (or less ambitiously, a more primitive organism) I would assume this could be described in a formal language. But why would Principia be needed for this? It explains this directly before that phrase: "Their language was dense and the work laborious, but they kept on proving a whole bunch of different truths in mathematics, and so far as anyone could tell at the time,…

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?

Re: What Gödel Discovered (2020)

#30

Post by jb1991 »

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…

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..
Post reply on HN