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

241–250 of 271 posts

Re: What Gödel Discovered

#241

Post by stopachka »

drran wrote: post #240
stopachka wrote: post #239

Earlier quoted context omitted.

The point of Godel’s idea, is that he proved “ Lisivka's numbers", has a formula that can’t be proven. Try going through the essay, and point out where the “incorrect” numbers were formed. You may be surprised to find that all statements were “correct” in the definition you are thinking of. The mathematical term is “primitive recursive” and “well-formed”

You missed the point. Any "bad" Godel's number can be interpreted as "good" Lisivka's number. We have ambiguity here, because a number can refer to any formula in infinite number of sets. > We can go further. We can even construct PM-Lisp formulas in PM-Lisp! No, we cannot.

When you say "You missed the point.", and "No, we cannot" -- your words come off as though you are supremely confident, and a bit condescending. This makes me not want to engage deeper with you.

To see how it feels:

No, drran, you have missed the point. Read it again, maybe you'll get it.

Re: What Gödel Discovered

#242

Post by odonnellryan »

piyh wrote: post #33

I read stuff like this on HN and feel like I'm an child watching dad work on a car. Except papa Godel was younger than me when he wrote his paper.

I am certain there are things you are better at then he was, and I'm certain there are things that could be found that you can do that he wish he could have done.

Re: What Gödel Discovered

#243

Post by drran »

stopachka wrote: post #241
drran wrote: post #240

Earlier quoted context omitted.

You missed the point. Any "bad" Godel's number can be interpreted as "good" Lisivka's number. We have ambiguity here, because a number can refer to any formula in infinite number of sets. > We can go further. We can even construct PM-Lisp formulas in PM-Lisp! No, we cannot.

When you say "You missed the point.", and "No, we cannot" -- your words come off as though you are supremely confident, and a bit condescending. This makes me not want to engage deeper with you. To see how it feels: No, drran, you have missed the point. Read it again, maybe you'll get it.

4667698044567788679899973453457778678980909855464564564578787890665467786780909875744564756867978980890785745635646767586445454536665474747746767457575890112345678999077554344567787923424234234234246566797899707980980983453453454353453453453534534534534

This number is equivalent to the proof that I'm right. Godel was genius!

Re: What Gödel Discovered

#244

Post by ProfHewitt »

mike00632 wrote: post #230
ProfHewitt wrote: post #212

Earlier quoted context omitted.

Hi Ethn! Existence of the [Gödel 1931] proposition I'mUnprovable is inconsistent with the following theorem to the effect that theorems can be used in proofs: ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ

For a statement so short it would be easy to avoid using jargon...

Just to be clear

      ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ
is not jargon. Instead, it is standard mathematics.

Re: What Gödel Discovered

#245

Post by ProfHewitt »

AndrewKemendo wrote: post #237
ProfHewitt wrote: post #193

Earlier quoted context omitted.

Dear xyzzy, Unfortunately, you missed that the author's proof does not actually prove inferential undecidability (sometimes called "inferential incompleteness") of Russell's Principia Mathematica for the following reason: The [Gödel 1931] proposition *I'mUnprovable* does **not** exist in Principia Mathematica because it violates restrictions on orders of propositions that are necessary to avoid paradoxes (such as Rus…

Is case anyone is wondering this is MIT professor Emeritus Carl Hewitt https://en.wikipedia.org/wiki/Carl_Hewitt

Wikipedia is contentious and often potentially libelous.

See the following for more up-to-date information:

https://professorhewitt.blogspot.com/

Re: What Gödel Discovered

#246

Post by kazinator »

ProfHewitt wrote: post #212
ethn wrote: post #207

Earlier quoted context omitted.

Secondly, in the PM-Lisp it doesn't necessarily prove that theorem a proves b, it just shows that b can be a successor of the formulas in a

Hi Ethn! Existence of the [Gödel 1931] proposition I'mUnprovable is inconsistent with the following theorem to the effect that theorems can be used in proofs: ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ

Axioms can be used in proofs, and they are not provable.

If a proposition is not provable, yet raises no issues if regarded as true, then it can be added as an axiom and used in theorems.

Re: What Gödel Discovered

#247

Post by ProfHewitt »

AndrewKemendo wrote: post #237
ProfHewitt wrote: post #193

Earlier quoted context omitted.

Dear xyzzy, Unfortunately, you missed that the author's proof does not actually prove inferential undecidability (sometimes called "inferential incompleteness") of Russell's Principia Mathematica for the following reason: The [Gödel 1931] proposition *I'mUnprovable* does **not** exist in Principia Mathematica because it violates restrictions on orders of propositions that are necessary to avoid paradoxes (such as Rus…

Is case anyone is wondering this is MIT professor Emeritus Carl Hewitt https://en.wikipedia.org/wiki/Carl_Hewitt

A whole bunch of previous posts have be reposted to this discussion (maybe by a bot?).

Instead of plowing through the disjointed repostings,

readers may be better off looking at the articles linked in https://professorhewitt.blogspot.com/.

Also, there is a video here:

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

Re: What Gödel Discovered

#248

Post by ProfHewitt »

kazinator wrote: post #246
ProfHewitt wrote: post #212

Earlier quoted context omitted.

Hi Ethn! Existence of the [Gödel 1931] proposition I'mUnprovable is inconsistent with the following theorem to the effect that theorems can be used in proofs: ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ

Axioms can be used in proofs, and they are not provable. If a proposition is not provable, yet raises no issues if regarded as true, then it can be added as an axiom and used in theorems.

It turns out that for powerful theories of Computer Science,

there must exist infinitely many propositions that are

inferentially undecidable, that is, can be neither proved nor disproved.

However, the propositions cannot be specified constructively

and so are not very interesting.

Currently, there seem to be no propositions interesting to

practical Computer Science that are provably inferentially

undecidable.

Re: What Gödel Discovered

#249

Post by ProfHewitt »

Liron wrote: post #180

People act like Godel’s Incompleteness Theorem is all about how formal systems are limited in their level of “insight about truth”. But actually it’s just the same observation as the Halting Problem: you have a system that tries to reason about the behavior of other systems (like Turing Machines or axiomatic set theory), but it can’t possibly always introspect about its own behavior because you can also configure it…

Hi Liron,

Your intuition is pretty good.

A correct proof of inferential incompleteness of Russell's

Principia Mathematica can be constructed using the

computational undecidability of the halting problem.

See https://papers.ssrn.com/abstract=3603021

   However, the [Gödel 1931] proof is incorrect for reasons
   mentioned elsewhere in this discussion.

Re: What Gödel Discovered

#250

Post by ProfHewitt »

Liron wrote: post #218
green_on_black wrote: post #204

Earlier quoted context omitted.

While this is true, it is surprising that is it impossible to engineer a system to be complete and consistent about arithmetic, as opposed to systems which are not engineered well, like your 2nd paragraph. If I take "1 is even", "1 is odd" and "no number can be even and odd" as my axioms, then there is obviously a problem, but of my own doing.

Russel and Whitehead's system is well-engineered; that's why it doesn't prove a contradiction (presumably) while your badly engineered system does. The issue is that R&W made their system powerful enough that it's also incomplete, due to the fact that their system contains smartass statements like G that are hell-bent on creating paradoxes if given the chance. Before Godel's time, people just didn't have enough exper…

Russell's Principia Mathematica (PM) is indeed better

engineered than its predecessor by Frege because it has orders

on propositions. Because of orders on proportions, PM does

not allow the [Gödel 1931] proposition I'mUnprovable.

Furthermore, adding the proposition I'mUnprovable would

make PM inconsistent.

    The Gödel number of a proposition in PM is itself
    "incomplete" because it *doesn't* include the order of the
    proposition.  Allowing its Gödel number to represent a
    proposition is indeed a kind of "code injection" attack,
    which if allowed would make PM inconsistent.
Post reply on HN