3 ms·
Mathematical foundations are indeed incomplete, that is, there are true propositions, which are unprovable. However, [Gödel 1931] failed to prove incompletene
by ProfHewitt 5y ago
Mathematical foundations are indeed incomplete, that is,
there are true propositions, which are unprovable.
However, [Gödel 1931] failed to prove incompleteness of
foundations using the nonexistent proposition
I'mUnprovble. The [Gödel 1931] attempt to construct
I'mUnprovable using fixed points fails because it violates
restrictions on orders of propositions. The Gödel number of a
proposition left out its order.
Furthermore, existence of I'mUnprovable would have the
unfortunate consequence that foundations are inconsistent.
It is worth noting that the proposition I'mUnprovable is of
no practical importance in mathematical foundations.
Consequently its nonexistence does not much matter.
See the following for further explanation:
https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
- jkhdigital 5y agoNice to hear from you again, Carl. Your comments about inconsistent foundations brings to mind the Univalent Foundations approach to mathematics--can you comment on how your research relates to univalent foundations and homotopy type theory?
- ProfHewitt 5y agoThanks jkhdigital! Of course, mathematical foundations must not be inconsistent. Homotopy type theory is an attempt address issues of equality in type theory.
- rssoconnor 5y agoFor the record, Gödel proposition can be constructed[1] in the same manner that Quines[2] can be constructed. I myself have formalized[3] the first incompleteness theorem in the Coq proof assistant, and many others have as well in various proof assistants. You can find specific and concrete instance of a Gödel proposition written by Stephen Lee at <http://tachyos.org/godel/Godel_statement.html http://tachyos.org/godel/Godel_statement.html>. It really is not that large of a proposition. I'm not sure how you can claim that proposition that I can see with my own eyes does not exist. [1] http://r6.ca/blog/20190223T161625Z.html http://r6.ca/blog/20190223T161625Z.html [2] https://en.wikipedia.org/wiki/Quine_(computing) https://en.wikipedia.org/wiki/Quine_(computing) [3] https://github.com/coq-community/goedel https://github.com/coq-community/goedel
- ProfHewitt 5y agoGödel proposition I'mUnprovable cannot be constructed in foundations because fixed-point construction violates orders on propositions. Existence of I'mUnprovable would render foundations inconsistent. See the following; https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
- rssoconnor 5y agoSince you allege the existence of I'mUnprovable propositions renders Peano Arithmetic (see <http://tachyos.org/godel/Godel_statement.html http://tachyos.org/godel/Godel_statement.html> cited above), Coq, HOL Light, Isabelle and every other proof assistant that has proven the incompleteness theorem inconsistent, I look forward to you facilitating the development of a formal contradiction in any one of these systems. In particular a proof of False in Coq[1] would greatly aid me in getting through some of my troublesome proofs. [1]http://r6.ca/blog/20061211T203500Z.html http://r6.ca/blog/20061211T203500Z.html
- ProfHewitt 5y agoProposition I'mUnprovable must not exist in foundational theories. A proof of inconsistency for a foundational theory that has I'mUnprovable appeared here: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
- rssoconnor 5y agoVery good. Then surely the paper proof can be translated into an inconsistency of Coq, Isabelle or HOL-light, since all of these proof assistants already prove the existance of such an "I'mUnprovable" proposition.
- ProfHewitt 5y agoCoq, Isabelle, and HOL-light are inadequate for the foundations of mathematics. See discussion in related work section of the following: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021