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

251–260 of 271 posts

Re: What Gödel Discovered

#251

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…

Model Theory formalizes the notion of "truth" in foundational

mathematics of computer science. The axioms of powerful

foundational theories of computer science have just one model

up to a unique isomorphism. See

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

    The [Gödel 1930] "completeness theorem" is *false* for the
    foundational theories of Computer Science because these
    theories are inferentially incomplete, that is, not every
    proposition can be proved or disproved.

Re: What Gödel Discovered

#252

Post by ProfHewitt »

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…

In foundational theories that are strongly typed (such as

https://papers.ssrn.com/abstract=3457802, which is much

more powerful than first-order ZFC), one version of

the Continuum Hypothesis is still open although other

versions have been proved or disproved.

    It has *not* been proved that the open version cannot be   
    proved and it has *not* been proved that the open
    version cannot be disproved.

Re: What Gödel Discovered

#253

Post by ProfHewitt »

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?

There are an infinitely many propositions that cannot be proved

or disproved in foundational theories of Computer Science.

    However, foundational theories exclude the [Gödel 1831] 
    proposition *I'mUnprovable* because including it would 
    make the theories inconsistent for reasons mentioned 
    elsewhere in this discussion.

Re: What Gödel Discovered

#254

Post by ProfHewitt »

Bud wrote: post #52

This is an exceptionally good explanation of Gödel's incompleteness theorem for the general reader.

Hi Bud!

What is actually needed is a correct exposition (such as

https://papers.ssrn.com/abstract=3603021) of how

inferential incompleteness of Russell's Principia

Mathematica follows from the computational undecidability of

the Halting Problem.

    Prior to https://papers.ssrn.com/abstract=3603021, 
    attempts to proof inferential incompleteness were 
    *incorrect* for foundational theories because of the 
    incorrect assumption that theorems of a foundational 
    theory can be computationally enumerated.

Re: What Gödel Discovered

#255

Post by ProfHewitt »

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…

Hi Hvis!

Inferentially undecidable sentences of Russell's Principia

Mathematica are not nonsensical. However, they are obscure

because no particular example is known because no one knows

how to present them constructively.

Re: What Gödel Discovered

#256

Post by ProfHewitt »

dwohnitmok wrote: post #47

There are two things I will argue with on this otherwise great explanation. First, I've said this before and I'll bang this drum across every Godel post I see. Please don't introduce the notion of truth into an introductory post on Godel's Incompleteness Theorems (the Power of Numbers section). Introductory posts on Godel's Incompleteness Theorems like to say things like "there are true things you cannot prove" or in…

Dear Dwohnitmok,

    1: Model theory, which formalizes "truth", is very 
       important for understanding inferential 
       incompleteness. Axioms of foundational theories of 
       Computer Science have just *one* model up to a unique 
       isomorphism, which defines "truth".
          The theorems of foundational theories of Computer 
       Science are *not* computationally enumerable. 
       Consequently, even the provable proposition's 
       *cannot* be computationally enumerated, much less the 
        ones true in the unique model.

    2. Foundational theories of Computer Science can prove 
       their own consistency because they *disallow* the 
       [Gödel 1931] proposition *I'mUnprovable*, which if it 
        were allowed would make the theories inconsistent.

Re: What Gödel Discovered

#257

Post by ProfHewitt »

ko27 wrote: post #34

Just to be clear. This implies that it's possible to write some specific statement (using PM axioms) that contradicts itself? Is there a readable example of this statement without using Gödel numbers but instead just with the axiom statements?

Yes, PM would be made inconsistent by including the

[Gödel 1931] proposition I'mUnprovable for reasons

explained elsewhere in this discussion.

Fortunately, the rules on orders of propositions make it

impossible to construct proposition I'mUnprovable in PM.

Re: What Gödel Discovered

#258

Post by ProfHewitt »

cmonnow wrote: post #102

I never understood the fascination people have with self-referential 'paradoxes' like : "This statement is False". Pronouns do not have an independent existence. Until the pronoun 'This' resolves to an actual statement which has a valid true/false property, it is a recurrence without termination i.e. a infinite loop, that has no meaning. Suppose I say: 1. Sky is blue. 2. Previous statement is True. 3. Previous statem…

Foundational theories of Computer Science would be rendered

inconsistent if they allowed the construction of the

proposition I'mFalse or the [Gödel 1931] proposition

I'mUnprovable using fixed points.

    Fortunately, orders on propositions prohibit the 
    construction of the proposition *I'mFalse* and also 
    prohibit the construction of the [Gödel 1931] 
    proposition *I'mUnprovable*.

Re: What Gödel Discovered

#259

Post by ProfHewitt »

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…

No extra restriction is required because Russell's Principia

Mathematical already excludes construction of the [Gödel 1931]

proposition I'mUnprovable because of orders on propositions.

Re: What Gödel Discovered

#260

Post by ProfHewitt »

arc0 wrote: post #187
drran wrote: post #178

Earlier quoted context omitted.

Well, I disliked it. I see proof that every valid formula can be converted into a Godel number. However, every invalid formula can also be converted into a Godel number. So, if we are able to construct a number, then it proves what?

The conversion of formulae to Gödel numbers is basically an implementation detail, the fact it can be done allows us to define theorems on the natural numbers that describe properties of the logical system. Encoding an invalid formula is of course possible, but I don't see why that would be a problem, it doesn't inherently 'prove' anything.

The Gödel number a proposition in Russell's Principia

Mathematica does not correctly represent the proposition

because it leaves out the order of the proposition.

Post reply on HN