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

231–240 of 271 posts

Re: What Gödel Discovered

#231

Post by ir123 »

Some things that were not clear to me, can some one help me out with them?

1) While representing 1+1 = 2 i.e (= (+ (next 0) (next 0)) (next (next 0))) which comes at the start of this article, is this considered to be just a statement? Or a true statement that follows from the axioms?

2) On formulas, this example is shown (there-is a (= (next 0) a)). It is not clear whether this is a necessarily true statement or some symbols relating a and 0.

3) He says that proofs are a sequence of formulas but colloquially they are sequence of "implications". That "implication" is introduced later on and it is shown that this "implication" symbol also needs to be proved (successor). Didn't he use the fact that one thing implies another multiple times previously?

I need the distinction amongst "statement", "formula" and "axioms".

Apologies if the above looks like a vegetable soup but I'd love some explanation for this.

Re: What Gödel Discovered

#233

Post by ProfHewitt »

mike00632 wrote: post #229
ProfHewitt wrote: post #211

Earlier quoted context omitted.

Hi GreatQuux! The article linked below explains why [Gödel 1931] did not prove inferential undecidability of Russell's Principia Mathematica and likewise why the formalization of [Gödel 1931] in Lisp proof being discussed is also invalid: https://papers.ssrn.com/abstract=3603021 However, the article linked above does have a correct proof of inferential undecidability (also known as "inferential incompleteness"). Woul…

What do you mean by "inferential" and why are there restrictions on what statements are valid?

Hi Mike!

The word "inferential" has to do with being able to be logically inferred, that is, deduced.

Russell's Principia Mathematica specified that each proposition must have an order to block paradoxes such as Russell's paradox.

See the article linked above for further explanation.

Re: What Gödel Discovered

#234

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

The following theorem says that every theorem can be used in another proof:

         ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ
The above theorem is completely standard mathematical notation.

Re: What Gödel Discovered

#235

Post by arc0 »

drran wrote: post #224
arc0 wrote: post #187

Earlier quoted context omitted.

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.

For me, it looks like use a program in C to generate a C code, and then prove that a C program can generate an invalid C code, so the C compiler must be invalid. Compilation step is missed. Compiler will refuse to compile the invalid code. IMHO, the same situation is for Godel numbers. We can use math to generate numbers, which are equivalent to formulas, BUT why these formulas must be accepted? Initial set of axioms…

Gödel's proof does not apply to any single axiomatic system, it applies to any computable set of axioms that can talk about numbers, quantifiers, addition and multiplication. This isn't arbitrary, it's a set of properties required for just about any interesting mathematics to take place.

The formulae are accepted because Gödel gives us a mapping, he proves that we can convert any formula into a number without losing information.

Re: What Gödel Discovered

#236

Post by [deleted] »

ProfHewitt wrote: post #193
xyzzyz wrote: post #7

I’m a mathematician who spent many hours thinking about Goedel theorem and adjacent topics. The author in a self-deprecating way says that he’s not a mathematician, but just a programmer. Bear no mind to that: this is one of the best popular expositions of Goedel theorem I’ve seen. Everything is very accurately explained, there are no silly mistakes and untruths one often sees mentioned in context of Goedel theorem,…

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…

[deleted]

Re: What Gödel Discovered

#237

Post by AndrewKemendo »

ProfHewitt wrote: post #193
xyzzyz wrote: post #7

I’m a mathematician who spent many hours thinking about Goedel theorem and adjacent topics. The author in a self-deprecating way says that he’s not a mathematician, but just a programmer. Bear no mind to that: this is one of the best popular expositions of Goedel theorem I’ve seen. Everything is very accurately explained, there are no silly mistakes and untruths one often sees mentioned in context of Goedel theorem,…

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

Re: What Gödel Discovered

#238

Post by drran »

arc0 wrote: post #235
drran wrote: post #224

Earlier quoted context omitted.

For me, it looks like use a program in C to generate a C code, and then prove that a C program can generate an invalid C code, so the C compiler must be invalid. Compilation step is missed. Compiler will refuse to compile the invalid code. IMHO, the same situation is for Godel numbers. We can use math to generate numbers, which are equivalent to formulas, BUT why these formulas must be accepted? Initial set of axioms…

Gödel's proof does not apply to any single axiomatic system, it applies to any computable set of axioms that can talk about numbers, quantifiers, addition and multiplication. This isn't arbitrary, it's a set of properties required for just about any interesting mathematics to take place. The formulae are accepted because Gödel gives us a mapping, he proves that we can convert any formula into a number without losing…

Ok, we converted formulas into unique numbers. Now, we can range these numbers, then we can remap these numbers back to natural numbers: 1 is first formula, 2 is second formula, and so on. We can produce these numbers with just «next» operator.

However, some formulas are incorrect, so we filter out them and then remap remaining functions again: 1 is first correct formula, 2 is second correct formula, and so on. Now, we can produce correct formulas with just «next» operator.

However, some formulas can contradict our system of rules, so we filter out them, and remap remaining functions again: 1 is the first correct formula which doesn't contradict the system of rules, and so on. Let's call them "Lisivka's numbers".

So, Godel's numbers can contradict axiomatic system, while Lisivka's numbers cannot.

Do you see the problem?

Re: What Gödel Discovered

#239

Post by stopachka »

drran wrote: post #238
arc0 wrote: post #235

Earlier quoted context omitted.

Gödel's proof does not apply to any single axiomatic system, it applies to any computable set of axioms that can talk about numbers, quantifiers, addition and multiplication. This isn't arbitrary, it's a set of properties required for just about any interesting mathematics to take place. The formulae are accepted because Gödel gives us a mapping, he proves that we can convert any formula into a number without losing…

Ok, we converted formulas into unique numbers. Now, we can range these numbers, then we can remap these numbers back to natural numbers: 1 is first formula, 2 is second formula, and so on. We can produce these numbers with just «next» operator. However, some formulas are incorrect, so we filter out them and then remap remaining functions again: 1 is first correct formula, 2 is second correct formula, and so on. Now,…

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”

Re: What Gödel Discovered

#240

Post by drran »

stopachka wrote: post #239
drran wrote: post #238

Earlier quoted context omitted.

Ok, we converted formulas into unique numbers. Now, we can range these numbers, then we can remap these numbers back to natural numbers: 1 is first formula, 2 is second formula, and so on. We can produce these numbers with just «next» operator. However, some formulas are incorrect, so we filter out them and then remap remaining functions again: 1 is first correct formula, 2 is second correct formula, and so on. Now,…

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.

Post reply on HN