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

51–60 of 271 posts

Re: What Gödel Discovered

#51

Post by Konohamaru »

Here's how I interpret Gödel's landmark result:

> semantic properties, except for the most trivial systems, can't be inferred from syntactic properties.

E.g. you can't type a program by seeing everything is using the correct literals and syntactic objects: you need to, sooner or later, know what the program /actually does/.

But the problem is that mathematicians do, in fact, reason about semantics. So saying that "it's uncomputable" ignores the elephant in the room, which is that mathematicians compute theorems for a living. What do mathematicians have that enables them to compute the uncomputable: well-aligned chakras, magic, coffee grounds, the zodiac, etc...?

Re: What Gödel Discovered

#53

Post by dwohnitmok »

Konohamaru wrote: post #51

Here's how I interpret Gödel's landmark result: > semantic properties, except for the most trivial systems, can't be inferred from syntactic properties. E.g. you can't type a program by seeing everything is using the correct literals and syntactic objects: you need to, sooner or later, know what the program /actually does/. But the problem is that mathematicians do, in fact, reason about semantics. So saying that "it…

Argh... this is the nuance I was talking about in another post. Godel's Completeness Theorem (which applies to many systems that Godel's Incompleteness Theorem also applies to) shows that in a sense semantic properties coincide with syntactic properties and so in fact can exactly be inferred from syntactic properties.

What instead Godel's Incompleteness Theorems show is that you cannot exhaustively list all the semantic properties of what you care about, but combined with Godel's Completeness Theorems, only the ones "relevant" to your syntactic axioms.

Re: What Gödel Discovered

#54

Post by 1970-01-01 »

Very off-topic, but long ago when Albert Einstein went for a car ride with Mr. Gödel to become U.S. citizens, Einstein was trying very hard to think of ways to shut him up about a Constitution loophole he discovered. Things didn't go exactly as planned, and in front of the naturalization examiner, Mr. Gödel started blabbing about how he had found a way the U.S could be transformed into a fascist regime...

Sources: https://robert.accettura.com/wp-content/uploads/2010/10/Morg...

https://en.wikipedia.org/wiki/Kurt_Gödel#cite_note-23

Re: What Gödel Discovered

#55

Post by Corazoor »

vannevar wrote: post #38
lqet wrote: post #19

Earlier quoted context omitted.

From Wikipedia [0]: > The proof constructs a particular Gödel sentence for the system F, but there are infinitely many statements in the language of the system that share the same properties, such as the conjunction of the Gödel sentence and any logically valid sentence. [0] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

Yes, but the "such as..." example incorporates the original "this statement is not provable" statement, so it seems a bit of a cheat. If you could exclude that statement, it would also by definition exclude any compound versions of it. It seems to me that the issue boils down to, can "this statement is not provable" be leveraged to get to something like 1 + 1 = 3?

https://en.m.wikipedia.org/wiki/List_of_statements_independe...

What Gödel did prove was that the above list of statements (and infinitely more) must exist.

The special thing about his proof is indeed that it is recursive, i.e. adding another axiom can't fix the problem. But that was only necessary to prove that no formal system can be perfect, ever.

Most undecidable problems can indeed be "fixed" by adding another axiom, but if you go beyond the ones of ZFC it becomes less clear which of the two alternatives is the "right" one...

Re: What Gödel Discovered

#56

Post by kkylin »

cyphar wrote: post #26
vannevar wrote: post #16

Something I've always been curious about: does Gödel's theorem imply an infinity of inconsistent statements, or is the "this statement cannot be proven..." statement the only one? If it's the latter, then of what practical significance is the singularity? If a system is incomplete only in that regard, couldn't one redefine incompleteness to exclude it, and render the system complete for all practical purposes?

Others have explained why you can't wave away inconsistency (principle of explosion) nor incompleteness (adding new axioms just creates a new axiomatic system with its own Godel sentences). However you might also find it interesting what incompletenesses exist in our own mathematical system (ZFC) -- the most well-known example is the Continuum Hypothesis[1]: > There is no set whose cardinality is strictly between tha…

For anyone interested in the consistency of CH and Axiom of Choice:

https://www.scottaaronson.com/blog/?p=4974

And (of course) the HN discussion at the time:

https://news.ycombinator.com/item?id=24954695

Re: What Gödel Discovered

#57

Post by pvarangot »

Konohamaru wrote: post #51

Here's how I interpret Gödel's landmark result: > semantic properties, except for the most trivial systems, can't be inferred from syntactic properties. E.g. you can't type a program by seeing everything is using the correct literals and syntactic objects: you need to, sooner or later, know what the program /actually does/. But the problem is that mathematicians do, in fact, reason about semantics. So saying that "it…

I may be wrong here, but don't mathematicians sometimes "compute" in a meta-language that's sometimes more powerful, or less formal, than the system they are inferring things about?

Hence why they need results reviewed and a community to agree upon what's acceptable as a proof. Otherwise reviewing a proof would be an automatic process, if everything was done in the world of syntactic symbols with clear rules that tie one statement to the next.

Re: What Gödel Discovered

#58

Post by madia_leva »

marwan-nwh wrote: post #14
eyeundersand wrote: post #5

This is remarkably well done. I'm reading Hofstadter's Godel, Escher, Bach and found this at the perfect time. Thanks for the write up!

Man, I just searched about that book, and it is like there is a world I don't know anything about. Would you mind sharing the names of your favorite books?

EGB is one of my favourite books ever, but I think it doesn't explain Gödel's theorem as simple as it could. Of course, there are just so many wonderful things in EGB that this is not a fatal flaw by any means.

There is a fantastic book called "The Universal Computer: The Road from Leibniz to Turing" by Martin D. Davis that makes a very good job of explaining the context of Gödel's theorem, the theorem itself and the relation with computing in an accesible way. I'd recommend it to anyone interested either in computers or in Gödel's theorem.

Re: What Gödel Discovered

#59

Post by tshaddox »

a1369209993 wrote: post #48
tshaddox wrote: post #39

Earlier quoted context omitted.

I thought that independent (undecidable) statements are totally different than the Gödel sentences which demonstrate incompleteness. The latter is a statement which is true in the axiomatic system but which cannot be proven using the axiomatic system. The former is just a statement that essentially has no truth value in the axiomatic system.

Something being true in a axiomatic system is the same thing as it being provable; that's what "true" means. While a Godel statement for X can be interpreted as "X does not prove this statement", that interpretation inherently relies on the semantic implied by X. The Godel construction is systematic way of generating independent statements without needing to know anything specific about the axiomatic system.

Ah yes, you're right, and my lazy wording in the former comment is inaccurate. A Gödel sentence is just a statement written in the syntax of whatever formal system we're dealing with: generally, it's a statement that there exists no natural number which satisfies a particular property. The formal system cannot prove or disprove that statement.

As you said, we tend to call the statement "true" because we know that the formal system itself was designed with the intention to describe natural numbers and arithmetic, and the statement was designed intentionally to refer indirectly to itself and claim its own unprovability. Since the statement is formally unprovable, we interpret it as being true. I had forgotten that Gödel actually showed that there are other interpretations of the formal system in which the Gödel statement is false.

Re: What Gödel Discovered

#60

Post by dwohnitmok »

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 "Power of Numbers" or in the short intro to "Hilbert's Program"). It makes it very confusing, especially in light of Godel's other landmark result, i.e Godel's Completeness Theorem which simultaneously applies to many of the same logical systems and can be very very vaguely described as "all true things are provable." Just stick to incompleteness and consistency at a syntactic level instead of appealing to truth, that is respectively the ability to always add new axioms and the lack of syntactic contradictions.

2. The lack of a system S's ability to prove its own consistency is not interesting by itself since we would not trust a proof from a potentially inconsistent system. Hence it is not, in a sense, terribly interesting that we require an infinite tower of increasingly stronger systems to prove the consistency of S and themselves. Rather the interesting direction goes the other way. S cannot prove the consistency of stronger systems, which means we cannot have a "minimal" system we use to explore the consistency of all other systems (again subject to some nuance).

Post reply on HN