25 ms·
Proposition I'mUnprovable must not exist in foundational theories. A proof of inconsistency for a foundational theory that has I'mUnprovable appeared here:
by ProfHewitt 5y ago
Proposition 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