For 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>. 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.
Since you allege the existence of I'mUnprovable propositions renders Peano Arithmetic (see <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.
Very 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.
Nice 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?
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