3 ms·
Gödel proposition I'mUnprovable cannot be constructed in foundations because fixed-point construction violates orders on propositions. Existence of I'mUnprova
by ProfHewitt 5y ago
Gö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