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

261–270 of 271 posts

Re: What Gödel Discovered

#261

Post by ProfHewitt »

daralthus wrote: post #197
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…

Because of the halting issue you cannot summarise reality into a set of axioms and rules. Which is the original purpose of mathematics. Therefore you cannot say mathematics is right or true without adding at the end: "this actually could all be wrong".

Dear Darlthus,

The predicate HaltaType>[anExpression] is true if and only

if anExpression of type aType halts.

The predicate Halt is inferentially undecidable, that is, it

is not the case that for every expression anExpression of type aType that

|- HaltaType>[anExpression] or |- ~HaltaType>[anExpression].

Inferential undecidability does not mean that mathematics

is wrong.

Of course, it is possible to have incorrect

mathematical proofs, such as the incorrect proof in

[Gödel 1931] for the inferential undecidability of Russell's

Principia Mathematica. (There is a correct proof here:

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

Re: What Gödel Discovered

#262

Post by ProfHewitt »

ajnin wrote: post #135

Very interesting. I'm wondering if this has implications in physics ? Since "the book of nature is written in mathematical language", does this mean that attempts to find a unified theory of everything are doomed ? I'm thinking not necessarily, since we wouldn't need to prove all possible physical phenomena, only those that actually happen, but how do we know if they are among the one that can be proven ?

A very comprehensive theory of physics including the physics of

computation can be developed. However, such a foundational

theory will be inferentially undecidable.

Re: What Gödel Discovered

#263

Post by ProfHewitt »

The author of "What Gödel Discovered" has a good point that

Gödel numbers are not a convenient representation of a

proposition of Russell's Principia Mathematica (PM). (Nor

are Gödel numbers adequate because they omit the order of a

proposition.)

Lisp expressions are an improvement. However, a Lisp

expression, as used in the article, is also not adequate

because it also omits the order of the proposition.

See the following for a high-level representation of

propositions of PM that includes the crucial orders on

proportions: https://papers.ssrn.com/abstract=3459566

Re: What Gödel Discovered

#264

Post by ProfHewitt »

amboo7 wrote: post #124

Lispers learned marketing, bravo! The only issue is the missing credit to the Quanta article https://www.quantamagazine.org/how-godels-incompleteness-the... .

Hi Amboo7!

The article "What Gödel Discovered" improves on the Quanta

article linked above by using Lisp expressions instead of

Gödel numbers.

The proof in "What Gödel Discovered" is still incorrect

because the Lisp expressions it uses leave out the crucial

orders on propositions in Russell's Principia Mathematica.

Re: What Gödel Discovered

#265

Post by vfclists »

ProfHewitt wrote: post #234
mike00632 wrote: post #230

Earlier quoted context omitted.

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.

What character set or input method is used in creating this mathmatical characters?

Re: What Gödel Discovered

#266

Post by mike00632 »

ProfHewitt wrote: post #244
mike00632 wrote: post #230

Earlier quoted context omitted.

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.

It absolutely is jargon. The fact that you explained it by saying it's "mathematics" instead of "English" suggests as much. Jargon means that it's technical language specific to a field and not used in everyday vernacular. What you wrote can't even be typed on a standard keyboard. It's jargon.

I'm pointing it out because its use is not so innocent. Jargon is often used to obfuscate meaning, especially when it means something that would otherwise be easy to say plainly.

Re: What Gödel Discovered

#267

Post by mike00632 »

ProfHewitt wrote: post #233
mike00632 wrote: post #229

Earlier quoted context omitted.

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.

That doesn't explain why there must be such a restriction.

Re: What Gödel Discovered

#268

Post by daralthus »

ProfHewitt wrote: post #261
daralthus wrote: post #197

Earlier quoted context omitted.

Because of the halting issue you cannot summarise reality into a set of axioms and rules. Which is the original purpose of mathematics. Therefore you cannot say mathematics is right or true without adding at the end: "this actually could all be wrong".

Dear Darlthus, The predicate Halt aType >[ anExpression] is true if and only if anExpression of type aType halts. The predicate Halt is inferentially undecidable, that is, it is not the case that for every expression anExpression of type aType that |- Halt aType >[ anExpression ] or |- ~Halt aType >[ anExpression ]. Inferential undecidability does not mean that mathematics is wrong. Of course, it is possible to have…

Thank you for the paper.

Of course proofs can be still correct, it's just that we cannot cope with infinites very well without talking about computational limits.

My argument was hyperbolic, I regret, but it was less about what's incorrect and more about what's incomplete. The aspirations of early mathematicians was to discover a platonic ideal. Instead of that we only got useful tools that are always* up for re-interpretation depending on context.

An example of this is that Euclid's fifth postulate, which be consistent with many other interpretations of geometry too, not just the single one originally intended. It turned into a tool of formal scaffolding instead of an omnipotent "truth". Going from absolute to relative in power.

*In cases where they involve infinites. Including simple expressions like "take N to be an integer"

Re: What Gödel Discovered

#269

Post by derangedHorse »

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…

So in layman's terms you're saying the system the author tries to prove incomplete by definition removed the parts that would prove it's inconsistent?

Re: What Gödel Discovered

#270

Post by ProfHewitt »

Although [Gödel 1931] failed to proved inferential

undecidability of Russell's Principia Mathematica, there is a

fairly simple undecidable proposition namely, the proposition

   *Undecidable*≡Halt>[RunOne.[]]
where RunOne.[]≡Eval.[SelectOne.[0]] such that

   SelectOne.[i:Natural]≡ExpressionFromString.[i] *finishesFirst* SelectOne.[i+1]
Eval.[anExpression] evaluates anExpression and where the expression

    (expression1 *finishesFirst* expression2)
returns the value of whichever of the expressions expression1

and expression2 evaluation finishes first.

The procedure SelectOne selects one of the expressions

created from strings.

For details see: https://papers.ssrn.com/abstract=3603021

Post reply on HN