4 ms·
Dear xyzzy, Unfortunately, you missed that the author's proof does not actually prove inferential undecidability (sometimes called "inferential incompleteness
by ProfHewitt 6y ago
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 Russell's Paradox). Gödel numbers (and in the author's case Lisp expressions) leave out the order of a proposition with the consequence that the Diagonal Lemma **cannot** be used to construct the proposition *I'mUnprovable*.
Furthermore, existence of the proposition I'mUnprovable contradicts the following fundamental theorem of provability that goes all the way back to Euclid:
A theorem can be used in other proofs.
See the following article for further details:
https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
- derangedHorse 6y agoSo 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?
- greatquux 6y agoI'm going to need someone to come along and write up a layman's summary of this article. :) Does it change the end result of Gödel? Or is it basically the equivalent of saying what some restricted programming languages are doing, that we can get "good enough" results and not have these problems by restricting what we can do in the language?
- ProfHewitt 6y agoHi 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 https://papers.ssrn.com/abstract=3603021 However, the article linked above does have a correct proof of inferential undecidability (also known as "inferential incompleteness"). Would be happy to respond to any questions that you might have.
- mike00632 6y agoWhat do you mean by "inferential" and why are there restrictions on what statements are valid?
- ProfHewitt 6y agoHi 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.
- mike00632 6y agoThat doesn't explain why there must be such a restriction.
- ethn 6y agoSecondly, 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
- ProfHewitt 6y agoHi 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 Ψ] (⊢Ψ)⇒Ψ
- mike00632 6y agoFor a statement so short it would be easy to avoid using jargon...
- ProfHewitt 6y agoThe following theorem says that every theorem can be used in another proof: ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ The above theorem is completely standard mathematical notation.
- vfclists 6y agoWhat character set or input method is used in creating this mathmatical characters?
- ProfHewitt 6y agoJust to be clear ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ is not jargon. Instead, it is standard mathematics.
- mike00632 6y agoIt 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.
- deleted 6y ago[deleted]
- AndrewKemendo 6y agoIs case anyone is wondering this is MIT professor Emeritus Carl Hewitt https://en.wikipedia.org/wiki/Carl_Hewitt https://en.wikipedia.org/wiki/Carl_Hewitt
- ProfHewitt 6y agoWikipedia is contentious and often potentially libelous. See the following for more up-to-date information: https://professorhewitt.blogspot.com/ https://professorhewitt.blogspot.com/
- ProfHewitt 6y agoA 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/ https://professorhewitt.blogspot.com/. Also, there is a video here: https://www.youtube.com/watch?v=PJ4X0l2298k https://www.youtube.com/watch?v=PJ4X0l2298k