What Gödel Discovered • Hacker News Board

Re: What Gödel Discovered

#111

Post by dang » Tue, Nov 17, 2020, 2:02 AM UTC

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…

> 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.

Sorry for the confusion. We detach comments that are replies to the top comment but don't respond to anything specific that that comment said. This is standard moderation. Sometimes we post that we did this (https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...), but not always.

We do this because users often post replies to the top comment on a page that aren't really replies. Sometimes they do that because they want to get their comment higher on the page (so-called topjacking). Of course that's not always the case.

Both of your posts are fine (except for the fact that they duplicate one another) but they are replies to the article, not to anything that the top comment (https://news.ycombinator.com/item?id=25116881) specifically says. Indeed your sentence "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." makes it quite clear that your reply is to the article, not xyzzyz's comment. That's great! But the appropriate level for such a comment is the top level of the thread.

I've therefore done the same again and detached this subthread from https://news.ycombinator.com/item?id=25116881.

Re: What Gödel Discovered

#112

Post by redvenom » Tue, Nov 17, 2020, 2:03 AM UTC

pvarangot wrote: post #57

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…

There are two separate statements here:

1. Mathematicians often use relatively powerful systems, like reasoning in ZFC about Peano arithmetic. The consistency and completeness of axiomatic systems is what this article is about

2. Mathematicians pretty much exclusively use informal systems (compared to formal logic) for reasoning. The reason why that is is because it is just infeasible to reason typical mathematics using formal logic for most cases.

However, it's important to realize that these two are orthogonal.

Re: What Gödel Discovered

#113

Post by redvenom » Tue, Nov 17, 2020, 2:06 AM UTC

irrational wrote: post #8

> This proof showed that “1 + 1”, does indeed equal “2”. It took 2 volumes to get here. I know this seems logical to mathematicians, but it feels to me like having to take 2 volumes to prove something than any child knows intuitively is... I don't know what word I am looking for... obsessive?

The point is not to prove that 1+1=2. The point is to construct mathematics (all of mathematics) directly from the axioms using a formal language. The objective of 1+1=2 is not interesting, but the result is a rigorous foundation of mathematics using formal languages.

The upshot is twofold: (1) we have a rigorous foundation of mathematics in formal logic which CAN be used to prove nontrivial statements, as in the application of model theory to mathematics, and (2) we can now build proof assistants that allow us to use computers to better understand proofs.

Both applications of formal reasoning are equally interesting and have wide ramifications in mathematics.

Re: What Gödel Discovered

#114

Post by musicale » Tue, Nov 17, 2020, 2:07 AM UTC

schoen wrote: post #9

Cf. Douglas Hofstadter's Metamagical Themas : > In March of 1977, I met the great AI pioneer Marvin Minsky for the first time. It was an unforgettable experience. One of the most memorable remarks he made to me was this one: "Gödel should just have thought up Lisp; it would have made the proof of his theorem much easier." I knew exactly what Minsky meant by that, I could see a grain of truth in it, and moreover I kne…

That book helped me reach the conclusion that Hofstadter's self-references were annoying to the point that I wished to avoid them (and his writing in general) in the future.

Re: What Gödel Discovered

#115

Post by dang » Tue, Nov 17, 2020, 2:17 AM UTC

6gvONxR4sf7o wrote: post #45

TheGrassyKnoll wrote: post #42

He used a word I don't see very often (if ever) https://en.wikipedia.org/wiki/Epiphenomenon

If you format it that way (the spaces in front for a code block), we can't click the link.

I've fixed the formatting now.

Re: What Gödel Discovered

#116

Post by redvenom » Tue, Nov 17, 2020, 2:32 AM UTC

itismonday1 wrote: post #96

xyzzyz wrote: post #81

Earlier quoted context omitted.

> 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." If people want to understand how to reconcile this very vague statement with Goedel incompleteness theorem that appears to say that some "true" statements are in fa…

I am trying to follow, but I feel I am hanging Goedel incompleteness theorem -> apply this to "theories" Goedel completeness theorem -> apply this to a specific "model", of the theory So there can be "something true but not provable" in the theory, and "we cannot describe all true things about specific models", but ....what?

The answer you got from lmm and others is wrong (I am a professional mathematician and did research in logic).

The completeness theorem says simply: if T is a first-order theory (list of axioms in first-order logic), any sentence true in every model of T is provable by logical deduction in T.

The first incompleteness theorem says: if T is a consistent recursively enumerable theory that can contains a sufficient amount of Peano arithmetic, then there exists a sentence which is neither true in all models nor false in all models. In other words, there is a sentence which is true in at least one model of T, and false in another.

The second incompleteness theorem says that if T can interpret Peano arithmetic, then we cannot prove the consistency of T within T.

So a tl;dr:

-Completeness: any SENTENCE true in ALL models is PROVABLE - applies to all first order theories

-1st Incompleteness: there EXISTS sentences which are TRUE in some models, FALSE in others. - Applies to theories that contain enough arithmetic

-2nd Incompleteness: if a sufficiently strong system is CONSISTENT, we CANNOT PROVE that CONSISTENCY within the system.

NB: of course, if you have a sufficiently WEAK system, like the axioms of group theory together with "FOR ALL x FOR ALL y (x=y)", then that theory would be COMPLETE and Godel's incompleteness theorem does not apply here.

Re: What Gödel Discovered

#117

Post by redvenom » Tue, Nov 17, 2020, 2:49 AM UTC

lmm wrote: post #105

itismonday1 wrote: post #96

Earlier quoted context omitted.

I am trying to follow, but I feel I am hanging Goedel incompleteness theorem -> apply this to "theories" Goedel completeness theorem -> apply this to a specific "model", of the theory So there can be "something true but not provable" in the theory, and "we cannot describe all true things about specific models", but ....what?

The way I see it is that both theorems are statements about the relationship between a theory and models of that theory. Goedel's completeness theorem tells you that for a theory in first-order logic, there's a model that corresponds exactly to that theory: anything that's true in that model can be proven in the theory, and vice versa. Godel's incompleteness theorem tells you that there's no such model for any system…

Just want to point out that your answer is essentially incorrect. Godel's completeness theorem has nothing to do with the existence of models. It is about the provability of sentences that are true within all models.

Also, the incompleteness theorem doesn't say anything about the nonexistence of a model. It gives the existence of at least one sentence X (for sufficiently nice theories that include enough arithmetic) such that there ARE two models where X is true in one and false in the other.

Re: What Gödel Discovered

#118

Post by redvenom » Tue, Nov 17, 2020, 2:55 AM UTC

jlokier wrote: post #43

cyphar wrote: post #26

Earlier quoted context omitted.

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…

> being able to prove the CH is an incompleteness in ZFC. It's only incompleteness if the CH is true or false at the semantic level, "outside" of the logic system under discussion. But the CH may be neither true or false, semantically, if the meaning of "existence of a set whose cardinality is strictly between that of the integers and the real numbers" strictly depends on the axioms and logic used to define sets and…

This response is not quite right. "It's only completeness [...]" sentence does not make sense.

CH is independent of ZFC, period, as proved by Cohen. Talking about 'semantic level' does not make sense.

CH is an example of the incompleteness of ZFC. There are models of ZFC in which CH is true and models in which CH is false.

Re: What Gödel Discovered

#119

Post by redvenom » Tue, Nov 17, 2020, 2:57 AM UTC

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?

Excellent question. It implies an infinite number of statements. For if T is such an incomplete theory and X is a statement true in some models of T and false in others, then T+X is also a theory that satisfies the same requirements as T in Godel's theorem. Therefore there is another statement Y that is true in some models of T+X and false in other models of T+X. But any model of T+X is a model of T so Y is true in some models of T and false in others. And it goes on...

Re: What Gödel Discovered

#120

Post by redvenom » Tue, Nov 17, 2020, 3:01 AM UTC

dwohnitmok wrote: post #100

itismonday1 wrote: post #96

Earlier quoted context omitted.

I am trying to follow, but I feel I am hanging Goedel incompleteness theorem -> apply this to "theories" Goedel completeness theorem -> apply this to a specific "model", of the theory So there can be "something true but not provable" in the theory, and "we cannot describe all true things about specific models", but ....what?

Another example of why I don't like the word "truth" because I think it does more to muddy the situation than clarify it. Let's drop "truth" for a sec. Let's say I come up with a series of axioms about cows. They describe spots on cows, how many legs cows have, etc. Now I come up with a sentence "all cows have spots." There are two ways of proving this sentence. One is a "semantic proof." That is I go and round up ev…

"True" in this context is a technical definition, not some hand-waving thing. A sentence X being true means every model satisfies X. Provable means logical deduction within the theory proves X. So actually, Godel's theorems are exactly about truth and provability.