However, [Gödel 1931] fails to prove inferential undecidability of foundations of computer science because it violates restrictions on orders of propositions that were introduced in [Russell 1908] to block inconsistencies in foundations. The crucial issue with the proof in [Gödel 1931] is that the Gödel number of a proposition does not capture its order. In strongly-typed theories, the Diagonal Lemma [Gödel 1931] fails to construct the proposition I’mUnprovable such that I’mUnprovable⇔⊬I’mUnprovable.
If the proposition I’mUnprovable existed, it would be a monster in the sense of [Lakatos 1976] because adding it results in inconsistency in foundations of computer science that have the following fundamental principle: ByTheoremUse {⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ} [Euclid approximately 300 BC]
Proof of a contradiction in foundations of computer science: First prove *I’mUnprovable* using proof by contradictions as follows:
In order to obtain a contradiction, hypothesize ¬*I’mUnprovable*.
Therefore, ⊢*I’mUnprovable* (using *I’mUnprovable*⇔⊬*I’mUnprovable*).
Consequently, *I’mUnprovable* using ByTheoremUse, which is a contradiction.
Using proof by contradiction, ⊢*I’mUnprovable* meaning *I’mUnprovable* by ByTheoremUse.
However, ¬*I’mUnprovable* using *I’mUnprovable*⇔⊬I’mUnprovable, which is a contradiction in foundations.
Also, adding I’mUnprovable results in inconsistency in foundations of computer science that have the following fundamental principle: ByAdequacy {⊢∀[Proposition Ψ] (⊢Ψ)⇒⊢⊢Ψ}:
Proof of a contradiction in foundations of computer science: First prove *I’mUnprovable* using proof by contradictions as follows:
In order to obtain a contradiction, hypothesize ¬*I’mUnprovable*.
Therefore ⊢*I’mUnprovable* (using *I’mUnprovable*⇔⊬*I’mUnprovable*).
Consequently, ⊢⊢*I’mUnprovable*using ByAdequacy.
However, ⊢¬*I’mUnprovable*(using I’mUnprovable ⇔⊬I’mUnprovable), which is a contradiction.
Using proof by contradiction, ⊢*I’mUnprovable* meaning ⊢⊢*I’mUnprovable*using ByAdequacy.
However, ⊢¬*I’mUnprovable* (using *I’mUnprovable*⇔⊬*I’mUnprovable*), which is a contradiction in foundations.
Existence of relevant fixed points is extremely important because they enable recursive definitions. Without restrictions, fixed points can be used to construct monsters. For example, without orders on propositions, the “self-referential” proposition I’mFalse (such that I’mFalse⇔¬I’mFalse) could be constructed as the fixed point of the mapping Ψ↦¬Ψ (↦ notation from [Bourbaki 1939–2016]). Since Ψ is a propositional variable in the mapping, ¬Ψ has order one greater than the order of Ψ. Thus because of orders on propositions, there is no paradoxical fixed point I’mFalse for the mapping Ψ↦¬Ψ.
Gottlob Frege made major advances in notations in foundations [Frege 1884]. In Frege’s system, Russell developed a paradox using the mapping NotSelfApplicable[x]⇔¬x[x], which when applied with NotSelfApplicable for x has the following self-contradictory consequence: NotSelfApplicable[NotSelfApplicable]⇔¬NotSelfApplicable[NotSelfApplicable]. With orders on predicates, construction of the monster NotSelfApplicable is blocked because NotSelfApplicable[NotSelfApplicable] is not a well-formed proposition because if NotSelfApplicable is a predicate of order α substituted for x then ¬x[x] has order α+1 since x is a predicate variable of order α meaning that NotSelfApplicable is not a predicate of order α. In this way, Russell continued the logicism programme [Frege 1884] to base the foundations solely on the untyped predicate calculus writing that abstractions “are merely symbolic or linguistic conveniences, not genuine objects” [Russell and Whitehead 1927].
Attaching orders to abstractions enabled blocking the construction of monster such a NotSelfApplicable. However, attaching orders to all abstractions made Russell’s system unsuitable for standard mathematical practice, such as analysis [Russell in Appendix B of Principia Mathematica 2nd Edition, Church 1976, Quine 1966] because every abstraction is an abbreviation for a proposition with an order. Making types (where only propositional types have orders) explicit is a better solution for Computer Science.
References can be found here: https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3603021
However, [Gödel 1931] fails to prove inferential undecidability of foundations of computer science because it violates restrictions on orders of propositions that were introduced in [Russell 1908] to block inconsistencies in foundations. The crucial issue with the proof in [Gödel 1931] is that the Gödel number of a proposition does not capture its order. In strongly-typed theories, the Diagonal Lemma [Gödel 1931] fails to construct the proposition I’mUnprovable such that I’mUnprovable⇔⊬I’mUnprovable.
If the proposition I’mUnprovable existed, it would be a monster in the sense of [Lakatos 1976] because adding it results in inconsistency in foundations of computer science that have the following fundamental principle: ByTheoremUse {⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ} [Euclid approximately 300 BC]
Also, adding I’mUnprovable results in inconsistency in foundations of computer science that have the following fundamental principle: ByAdequacy {⊢∀[Proposition Ψ] (⊢Ψ)⇒⊢⊢Ψ}: Existence of relevant fixed points is extremely important because they enable recursive definitions. Without restrictions, fixed points can be used to construct monsters. For example, without orders on propositions, the “self-referential” proposition I’mFalse (such that I’mFalse⇔¬I’mFalse) could be constructed as the fixed point of the mapping Ψ↦¬Ψ (↦ notation from [Bourbaki 1939–2016]). Since Ψ is a propositional variable in the mapping, ¬Ψ has order one greater than the order of Ψ. Thus because of orders on propositions, there is no paradoxical fixed point I’mFalse for the mapping Ψ↦¬Ψ.Gottlob Frege made major advances in notations in foundations [Frege 1884]. In Frege’s system, Russell developed a paradox using the mapping NotSelfApplicable[x]⇔¬x[x], which when applied with NotSelfApplicable for x has the following self-contradictory consequence: NotSelfApplicable[NotSelfApplicable]⇔¬NotSelfApplicable[NotSelfApplicable]. With orders on predicates, construction of the monster NotSelfApplicable is blocked because NotSelfApplicable[NotSelfApplicable] is not a well-formed proposition because if NotSelfApplicable is a predicate of order α substituted for x then ¬x[x] has order α+1 since x is a predicate variable of order α meaning that NotSelfApplicable is not a predicate of order α. In this way, Russell continued the logicism programme [Frege 1884] to base the foundations solely on the untyped predicate calculus writing that abstractions “are merely symbolic or linguistic conveniences, not genuine objects” [Russell and Whitehead 1927].
Attaching orders to abstractions enabled blocking the construction of monster such a NotSelfApplicable. However, attaching orders to all abstractions made Russell’s system unsuitable for standard mathematical practice, such as analysis [Russell in Appendix B of Principia Mathematica 2nd Edition, Church 1976, Quine 1966] because every abstraction is an abbreviation for a proposition with an order. Making types (where only propositional types have orders) explicit is a better solution for Computer Science.