Carl Hewitt

Alonzo Church

Richard Dedekind

Stanisław Jaśkowski

Ludwig Wittgenstein

Inconsistency Robustness in Foundations: Mathematics self proves its own formal consistency and other matters

de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

A current common understanding is that Gödel proved "Mathematics cannot prove its own consistency, if it is consistent." However, the formal consistency of mathematics can be proved by a simple argument using standard rules of Mathematics including the following:  rule of Proof by Contradiction, i.e., (Φ⇒(ΘΘ))├ Φ  the rule Theorem Use, i.e., (├Φ)├ Φ [START_REF]Y:Set β τ]→ X∈Y QED by induction hypothesis 75 Proof: Suppose S:Setsτ and therefore ∃[α:O]→S:Sets α τ S:Sets α τ Show: Boolean s :Setsτ Boolean s :Sets α+1 τ QED 76 by induction on P[α:O]:Proposition1 ≡ ∀[S:Sets α τ]→ ⋃S:Setsτ Assume[END_REF] Formal Proof.

By definition, Consistent⇔∃[Ψ]→├ (ΨΨ). By Existential Elimination, there is some proposition Ψ0 such that Consistent⇒├ (Ψ0 Ψ0) which by Theorem Use and transitivity of implication means Consistent⇒(Ψ0Ψ0). Substituting for Φ and Θ, in the rule for Proof by Contradiction, it follows that (Consistent⇒(Ψ0Ψ0))├ Consistent. Thus, ├Consistent.

The above theorem means that formal consistency is deeply embedded in the architecture of classical mathematics. Please note the following points:

 The above argument formally mathematically proves the theorem that mathematics is consistent  It is not a premise of the theorem that mathematics is consistent. Classical mathematics was designed for consistent axioms and consequently the rules of classical mathematics can be used to prove formal consistency regardless of the axioms, e.g., Euclidean geometry. [START_REF] ⊨ℕ  | ℕ]→ (∀[:StringExpressionPropositionω ℕ ] → Length[END_REF] By formally consistent, it is meant that a consistency is not inferred. The proof is remarkably tiny consisting of only using proof by contradiction. In fact, it is so easy that one wonders why this was overlooked by so many great logicians in the past. The above proof of formal consistency is also remarkable that it does not use knowledge about the content of mathematical theories (plane geometry, integers, etc.). The proof serves to formalize that formal consistency is built into the very architecture of classical mathematics saying nothing about the possibility of bugs in the rules of inference and axioms of Direct Logic.. Consequently, the proof of formal consistency does not provide any assurance that there are no dangerous security holes in Direct Logic

In particular, the proof of formal consistency does not prove constructive consistency, which provides that the rules of Classical Direct Logic themselves do not derive a contradiction. Proof of constructive consistency requires a separate inductive proof using the axioms and rules of inference of Classical Direct Logic. The upshot is that, contra Gödel, there seems to be no inherent reason that mathematics cannot prove constructive consistency of Classical Direct Logic (which formalizes classical mathematical theories). However, such a proof seems far beyond the current state of the art. 4 The usefulness of Classical Direct Logic depends crucially on its consistency because otherwise it cannot be used freely to reason about inconsistent information without introducing further inconsistencies. Fortunately, Classical Direct Logic directly builds on classical mathematics. Good evidence for the consistency Classical Direct Logic derives from how it blocks the known paradoxes of classical mathematics. Humans have spent millennia devising paradoxes for classical mathematics. Having a powerful system like Direct Logic is important in computer science because computers must be able to formalize all logical inferences (including inferences about their own inference processes) without requiring recourse to human intervention. Any inconsistency in Classical Direct Logic would be a potential security hole because it could be used to cause computer systems to adopt invalid conclusions.

It is very important to distinguish between the following:  using the Y untyped fixed point operator for propositions [START_REF]⊨ℕ Length[END_REF]  using recursive definitions that are strongly typed to construct propositions.

Gödel based his incompleteness results on the thesis that mathematics necessarily has the proposition I'm unprovable. using what [Carnap 1934] later called the "Diagonal Lemma" which is equivalent to the Y untyped fixed point operator on propositions. Using strong parameterized types, it is impossible to construct the Gödel's proposition because the Y untyped fixed point operators does not exist for strongly typed logic. 6 In this way, formal consistency of mathematics is preserved without giving up power because there do not seem to be any practical uses for the proposition I'm unprovable.

A procedure definition G could be attempted as follows: G[p] ≡ ⊬p. With strong types, the attempted definition becomes:

G[p:Propositionn:ℕ]:Propositionn+1 ≡ ⊬p

Consequently, there is no fixed point I'm unprovable for G such that G[I'm unprovable] ⇔ I'm unprovable Thus Gödel's proposition "I'm unprovable" does not exist in strongly-typed mathematics. Consequently, it became an open question to find an intuitive inferentially undecidable proposition. 7 Later in this article, it will be shown that [Church 1934] had a very important clue.

Mathematical Foundation for Computer Science

Computer Science brought different concerns and a new perspective to mathematical foundations including the following requirements: 8 [Arabic numeral superscripts refer to endnotes at the end of this article]

 provide powerful inference machinery so that arguments (proofs) can be short and understandable and all logical inferences can be formalized  establish standard foundations so people can join forces and develop common techniques and technology  incorporate axioms thought to be consistent by the overwhelming consensus of working professional mathematicians, e.g., natural numbers [Dedekind 1888], real numbers [Dedekind 1888], ordinals, sets of integers, reals, etc.  facilitate inferences about the mathematical foundations used by computer systems.

Classical Direct Logic is a foundation of mathematics for Computer Science, which has a foundational theory (for convenience called "Mathematics") that can be used in any other theory. A bare turnstile is used for Mathematics so that ├Ψ means that Ψ is a mathematical proposition that is a theorem of Mathematics and Φ├Ψ means that Ψ can be inferred from Φ in Mathematics.

Mathematics self proves its own formal consistency

A mathematically significant idea involves: "…a very high degree of unexpectedness, combined with inevitability and economy." 9 The following rules are fundamental to classical mathematics: Please note the following points:  The above argument formally mathematically proves that mathematics is formally consistent and that it is not a premise of the theorem that mathematics is consistent. 12  Classical mathematics was designed for consistent axioms and consequently the rules of classical mathematics can be used to prove formal consistency regardless of other axioms. 13 The above proof means that "Mathematics is consistent" is a theorem in Classical Direct Logic. This means that the usefulness of Classical Direct Logic depends crucially on the consistency of Mathematics. Good evidence for the consistency of Mathematics comes from the way that Classical Direct Logic avoids the known paradoxes. Humans have spent millennia devising paradoxes.


Computer Science needs very strong foundations for mathematics so that computer systems are not handicapped. It is important not to have inconsistencies in mathematical foundations of Computer Science because they represent security vulnerabilities.

The recently developed self-proof of formal consistency (above) shows that the current common understanding that Gödel proved "Mathematics cannot prove its own consistency, if it is consistent" is inaccurate. Wittgenstein developed the proof below [lines 5) thru 7)] 14 that contradiction in mathematics results from allowing the proposition I'm unprovable. 15 used in the incompleteness results of [Gödel 1931]: // Using 1) 4) ├⊬ I'mUnprovable i // Classical Proof by Contradiction using 2) and 3) 5) ├ I'mUnprovable // from 4) using 1) 6) ├├ I'mUnprovable // from 5) using adequacy 7) ├ I'mUnprovable // from 6) using 1)

Wittgenstein's proof above shows that if the proposition I'm unprovable. is allowed, then Mathematics is inconsistent because of proving lines 5) and 7).

Fortunately, using strongly typed propositions, it can be proved that the Gödel's proposition I'm unprovable. cannot be constructed because required Y untyped fixed points on propositions used in its construction do not exist.

Consequently, using strong types, formal consistency of mathematics can be preserved without giving up power.

Gödel and other theoreticians developed the First-order Thesis that weakened the foundations of mathematics in order to allow the Y fixed point operator for propositions. 16 The weakened foundations (based on first-order logic) enabled some limited meta-mathematical theorems to be proved. However, as explained in this article, the weakened foundations are cumbersome, unnatural, and unsuitable as the mathematical foundation for Computer Science.

By the above formalized proof, Mathematics (├) proves its own formal consistency. However, the proof does so without regard to the content of Mathematics. For example, Mathematics includes the Dedekind categorical axiomatization of the natural numbers.

The proof formal consistency doesn't lead to any technical problems as long as there are no inconsistencies, e.g.,  Categorical axiomatizations of integers and ordinals don't infer any contradictions/  Propositions in Mathematics cannot be constructed using the Y fixed point operator on propositions. The Euler formula for polyhedra is Vertices-Edges+Faces=2, which can be proved in a variety of different ways.

Monster-Barring

But the hollow cube below is a counterexample because Vertices-Edges+Faces=4.

Counterexample to Euler's Formula

In the face of this counterexample, it becomes important to characterize polyhedra more rigorously. For example,  A Regular solid  A convex solid with polyhedral faces  A surface consisting of a system of polygons  etc. That mathematics self proves its own formal consistency contradicts [Gödel 1931] that claim (using the proposition i I'm unprovable.) that mathematics cannot prove its own consistency.

However using strong types, Gödel's proposition cannot be constructed. ii Note that there is a crucial difference between how Russell used types and the method used in Direct Logic. Russell attempted to use types as the fundamental mechanism for preventing inconsistencies by restricting the domain of mathematics to objects that can be described by a strict hierarchical type system. However, he ran into trouble because his type mechanism was too strict and prevented ordinary mathematical reasoning. iii

In this paper, strong types are used in the mathematical foundation of computer science to prevent the construction of paradoxical contradictory sentences and to provide the foundations for sets.

i constructed using what [Carnap 1934] later called the "Diagonal Lemma" which is equivalent to the Y untyped fixed point operator on propositions. ii It is important that types for propositions do not place restrictions on types of other mathematical objects so that Y fixed points can be used elsewhere when they exist, for example in topology, etc.. iii In order to be able to carry out ordinary mathematical reasoning, Russell introduced an (unmotivated) patch called "ramified types" that collapsed the type hierarchy.

Bertrand Russell

The difficulties encountered by Russell are avoided as follows:  having the integers 18 and ordinals as primitives categorically axiomatized  sets axiomatized as the characteristic functions of strongly typed functions

The above approach provides a very usable foundation for ordinary mathematical reasoning and for the mathematical foundations of computer science.. Science is in relatively good shape and is coming to a consensus around using strong parameterized types for the mathematical foundations of Computer Science and also using them in the foundations of their programming languages.

So where does this leave some theoreticians who previously thought that they owned this subject matter because of their previous publications? There are at least two possibilities:

 The field splits and some theoreticians try to ignore the Computer Scientists' prestigious published volume and its reviews. i.e., the sentence that for every ℕ there is a larger ℕ

In Direct Logic, a sentence is a grammar tree (analogous to the ones used by linguists). Such a grammar tree has terminals that can be constants. And there are uncountably many constants, e.g., the real numbers:

Of course, because the digits of 3.14159... are computable, there is a expression1 such that expression1 = 3.14159... that can be used to create the sentence (expression1 < (expression1 + 1)).

However the sentence (expression1 < (expression1 Suppose to obtain a contradiction that it is possible to prove closure, i.e., ⊢ProofsComputationalyEnumerable. Then there is a provably computable total procedure ProofsEnumerator:

[ℕ]↦Proof such that it is provable that ∀[p:Proof]→ ∃[i:ℕ]→ProofsEnumerator∎[i]= p ∀[i:ℕ]→ProofsEnumerator∎[i]:
Proof A subset of the proofs are those proving that certain procedures [ℕ]↦ℕ are total. Consequently, there is a

ProvedTotalsEnumerator:[ℕ]↦([ℕ]↦ℕ) that enumerates the provably total computable procedures [ℕ]↦ℕ that can be used in the implementation of the following procedure:

Diagonal∎[i:ℕ]:ℕ ≡ 1+ (ProvedTotalsEnumerator∎[i]) ∎[i] Consequently:
 Diagonal is a proved total procedure because it is implemented using computable proved total procedures.  Diagonal is not a proved total procedure because it differs from every other computable proved total procedure. The above contradiction completes the proof.

[Franzén 2004] argued that mathematics is inexhaustible because of inferential undecidability ii of mathematical theories. The above theorem that mathematics is open provides another independent argument for the inexhaustibility of mathematics.

Mathematical provability is computationally undecidable

Mathematics proves that provability in mathematics is computationally undecidable: 24

Theorem ⊢Mathematical provability is computationally undecidable, i.e., ⊢ProvablityComputationalyDecidable Proof. If provability in Mathematics 25 were computationally decidable then, the halting problem would be computationally decidable.

Completeness of inference versus inferential undecidability of closed mathematical theories

A closed mathematical theory is an extension of mathematics whose proofs are computationally enumerable. For example, group theory is obtained by adding the axioms of groups to Classical Direct Logic. Similarly, the closed mathematical theory Nat has the usual Dedekind axioms including the induction axiom: For each order:ℕ+ and P:Propositionorder ℕ the following Dedekind induction axiom holds:

(P⟦0⟧  ∀[i:ℕ]→ P⟦i⟧⇨P⟦i+1⟧) ⇨ ∀[i:ℕ]→ P⟦i⟧
Theorem The proposition ProofsComputationalyEnumerable Nat is true but unprovable in Nat, i.e., both of the following hold:

 ⊨ℕ ProofsComputationalyEnumerable Nat  ⊬ Nat ProofsComputationalyEnumerable Nat Proof:
Mathematics can make use of its types (i.e., Proposition Nat ω 26 , Sentence Nat ω 27 and Domain Nat ω 28 ) in the enumeration of proofs of Nat without violating the type rules of Mathematics. Consequently, ⊨ℕ ProofsComputationalyEnumerable Nat Suppose to obtain a contradiction that ⊢ Nat ProofsComputationalyEnumerable Nat Then there is a provable in Nat computable total procedure ProofsEnumerator

Nat :[ℕ]↦Proof Nat such that it is provable in Nat that ∀[p:Proof Nat ]→ ∃[i:ℕ]→ ProofsEnumerator Nat ∎[i]= p ∀[i:ℕ]→ ProofsEnumerator Nat ∎[i]:
Proof Nat A subset of the proofs in Nat are those proving that certain procedures [ℕ]↦ℕ are total. Consequently, there is a procedure ProvedTotalsEnumerator Nat :[ℕ]↦([ℕ]↦ℕ) that enumerates the provable in Nat total computable procedures [ℕ]↦ℕ that can be used in the implementation of the following procedure:

Diagonal∎[i:ℕ]:ℕ ≡ 1+ (ProvedTotalsEnumerator Nat ∎[i]) ∎[i]
Consequently:  Diagonal is a provable in Nat total procedure because it is implemented using computable provable in Nat total procedures.  Diagonal is not a provable in Nat total procedure because it differs from every other computable provable in Nat total procedure. The above contradiction completes the proof. Proof by contradiction in Nat : Suppose to derive an inconsistency that Consistent Nat . By the definition of inconsistency for Nat, there is some proposition Ψ of the theory Nat such that ├ Nat (Ψ  Ψ). By Existential Elimination, there is some proposition Ψ0 such that ├ Nat (Ψ0  Ψ0) which theorem can be used to infer in Nat that (Ψ0  Ψ0). The above contradiction completes the proof.

Note that the closed mathematical theory

Theorem. Sets τ is categorical via a (unique) isomorphism with the unique model Setsτ.

Theorem 31 The proposition ProofsComputationalyEnumerable Sets τ is true but unprovable in Sets τ, that is, both of the following hold:

 ⊨SetsτProofsComputationalyEnumerable Sets τ  ⊬ Sets τ ProofsComputationalyEnumerable Sets τ Proof:
Mathematics can make use of the types definable in Sets τ in the enumeration of proofs of Sets τ without violating the type rules of Mathematics. Consequently, ⊨ℕ ProofsComputationalyEnumerable Sets τ The proof of ⊬ Sets τ ProofsComputationalyEnumerable Sets τ is the same as the corresponding proof for Nat.

Theorem 32 ⊢ Sets τ Consistent Sets τ , that is, Sets τ proves its formal consistency Information Invariance 33 is a fundamental technical goal of logic consisting of the following: [START_REF]CurryΨ├ (CurryΨ├ Ψ)) // substituting 1) into 2)[END_REF] 1. Soundness of inference: information is not increased by inference 35 2. Completeness of inference: all information that necessarily holds can be inferred

Classical Provability Direct Logic

Classical Provability Direct Logic is an improvement over Provability Logic [Verbrugge 2010] as follows:

 Propositions are directly represented as opposed to being represented as Gödel numbers.  Theorems can be used directly in proofs, that is (⊢)⇒.  Adequacy is directly expressed as follows: (⊢) ⇔ ⊢(⊢).  Deduction is directly expressed as follows: (⊢) ⇔ ⊢(⇒).  ⊨ is directly expressed with the following:

o (⊢) ⇒ (⊨) o (⊨)(⇒) ⇒ (⊨)  A goal (⊩) is directly expressed with the following: o Forward: (⇒)(⊩) ⇒ (⊩ ) o Backward: (⇒)(⊩) ⇒ (⊩ )

Overview

Contradiction

Outcome Church discovered to his dismay that if theorems of mathematics are postulated to be computationally enumerable, then mathematics is inconsistent.

Proofs of mathematics cannot be computationally enumerated and mathematics is open and inexhaustible. But theorems of a particular theory can be postulated to be computationally enumerable. Using the proposition I'm unprovable., [Gödel 1931] claimed that mathematics cannot prove its own consistency. However, it is pointed out in this paper that mathematics easily proves its own formal consistency.

The contradiction can be resolved by using strong types for mathematics so that Gödel's proposition does not exist.

Using the Y untyped fixed point operator to construct the proposition I'm unprovable., [Gödel 1931] claimed to prove inferential undecidability (sometimes called "incompleteness") for mathematics. However, Wittgenstein showed that Gödel's proposition leads to inconsistency in mathematics.

In Classical Direct Logic, the following sentence is true but unprovable in Nat assuming that Nat is consistent:

ProofsComputationalyEnumerable Nat
In Computer Science, it is important that the Natural Numbers (Nat) be axiomatized in a way that does not allow integers (e.g. infinite ones) in models of the axioms. However, it is impossible to properly axiomatize Nat using first-order logic.

Using Classical Direct Logic, Nat can be axiomatized in such a way that all models are uniquely isomorphic to Nat. Consequently, there are no infinite integers in models of the axioms.

First-order logic is unsuitable as the foundation of mathematics for Computer Science:

 Some theorems of ordinary mathematics cannot be proved.

Conclusion

"The problem is that today some knowledge still feels too dangerous because our times are not so different to Cantor or Boltzmann or Gödel's time. We too feel things we thought were solid being challenged; feel our certainties slipping away. And so, as then, we still desperately want to cling go a belief in certainty. It makes us feel safe. ... Are we grown up enough to live with uncertainties or will we repeat the mistakes of the twentieth century and pledge blind allegiance to another certainty." Malone [2007] "The world always needs heretics to challenge the prevailing orthodoxies.

We are lucky that we can be heretics today without any danger of being burned at the stake. But unfortunately I am an old heretic. Old heretics do not cut much ice. When you hear an old heretic talking, you always say, 'Too bad he has lost his marbles.' What the world needs is young heretics. I am hoping that one or two of you people in the audience may fill that role." Dyson [2005] The closed mathematical theory Nat has the usual Dedekind axioms including the induction axiom. Consequently, the proposition ProofsComputationalyEnumerable Nat is true but unprovable in Nat .

Information Invariance is a fundamental technical goal of logic consisting of the following: 1. Soundness of inference: information is not increased by inference 2. Completeness of inference: all information that necessarily holds can be inferred. That the closed mathematical theory Sets τ is inferentially undecidable i with respect to ProofsComputationalyEnumerable Nat does not mean incompleteness with respect to the information that can be inferred because

 ⊢ ⊬ Sets τ ProofsComputationalyEnumerable Sets τ  ⊢ ⊬ Sets τ ProofsComputationalyEnumerable Sets τ  ⊢ ⊨Setsτ ProofsComputationalyEnumerable Sets τ
Computer Science needs a rigorous foundation for all of mathematics that enables computers to carry out all reasoning without human intervention. 36 [Frege 1879] was a good start, but it foundered on the issue of consistency.

i sometimes called "incomplete" [Russell 1925] attempted basing foundations entirely on types, but foundered on the issue of being expressive enough to carry to some common mathematical reasoning. [Church 1932, 1933] attempted basing foundations entirely on untyped higher-order functions, but foundered because it was shown to be inconsistent [Kleene and Rosser 1935]. Presently, Isabelle [Paulson 1989] and Coq [Coquand and Huet 1986] are founded on types and do not allow theories to reason about themselves. Classical Direct Logic is a foundation for all of mathematical reasoning based on strong types (to provide grounding for concepts) that allows general inference about reasoning.

[ Gödel 1931] claimed inferential undecidability i results for mathematics using the proposition I'm unprovable. In opposition to Wittgenstein's correct argument his proposition leads to contradictions in mathematics, Gödel later claimed that his results were for a cut-down first-order theory of natural numbers. However, first-order logic is not a suitable foundation for Computer Science because of the requirement that computer systems be able to carry out all reasoning without requiring human intervention (including reasoning about their own inference systems).

i sometimes called "incompleteness"

Following [Frege 1879, Russell 1925, and Church 1932-1933], Direct Logic was developed and then investigated propositions with the following results. 1941] and [Löb 1955] also lead to inconsistency in mathematics. Consequently, mathematics had to be rescued against these uses of the Y untyped fixed point operator for propositions.  Self-proof of the formal consistency of mathematics. Consequently, mathematics had to be rescued against the claim [Gödel 1931] that mathematics cannot prove its own consistency. Also, it became an open problem whether mathematics proves its own formal consistency, which was resolved by the author discovering an amazing simple proof. 37 A solution is to require strongly typed mathematics to bar use of the Y untyped fixed point operator for propositions. 38 However, some theoreticians have very reluctant to accept the solution.

According to [Dawson 2006]: 39  Gödel's results altered the mathematical landscape, but they did not "produce a debacle".  There is less controversy today over mathematical foundations than there was before Gödel's work. However, Gödel's writings have produced a controversy of a very different kind from the one discussed by Dawson:  Gödel's claim that mathematics cannot prove its own consistency i has been disproved.

 Consequently, Gödel's writings have led to increased controversy over mathematical foundations.

The development of Direct Logic has strengthened the position of working mathematicians as follows: ii  Allowing freedom from the philosophical dogma of the First-Order Thesis  Providing usable strong types for all of Mathematics that provides theories that have categorical models  Allowing theories to freely reason about theories  Providing Inconsistency Robust Direct Logic for safely reasoning about theories of practice that are (of necessity) pervasively inconsistent. i Gödel's writing was accepted doctrine by some theoreticians for over eight decades.

ii Of course, Direct Logic must preserve as much previous learning as possible.

Sociology of Foundations

"Faced with the choice between changing one's mind and proving that there is no need to do so, almost everyone gets busy on the proof.  The formal presentation of a demonstration (proof) has not lead automatically to consensus. Formal presentation in print and at several different professional meetings of the extraordinarily simple proof in this paper have not lead automatically to consensus about the theorem that "Mathematics is Consistent". New results can sound crazy to those steeped in conventional thinking. Paradigm shifts often happen because conventional thought is making assumptions taken as dogma. As computer science continues to advance, such assumptions can get in the way and have to be discarded.  There has been an absence of universally recognized central logical principles. Disputes over the validity of the Principle of Excluded Middle led to the development of Intuitionistic Logic.  There are many ways of doing logic. One view of logic is that it is about truth; another view is that it is about argumentation (i.e. proofs). 41  Argumentation and propositions have be variously (re-)connected and both have been re-used. Church's paradox is that assuming theorems of mathematics are computationally enumerable leads to contradiction. In this papers, the paradox is transformed into the fundamental principle that "Mathematics is Open" (i.e. it is a theorem of mathematics that the proofs of mathematics are not computationally enumerable) using the argument used in Church's paradox.  New technological developments have cast doubts on traditional logical principles. The pervasive inconsistency of modern large-scale information systems has cast doubt on some logical principles, e.g., Excluded Middle. 42  Political actions have been taken against views differing from the establishment theoreticians. According to [Kline 1990, p. 32],

Hippasus was literally thrown overboard by his fellow Pythagoreans "…for having produced an element in the universe which denied the…doctrine that all phenomena in the universe can be reduced to whole numbers and their ratios." Fearing that he was dying and the influence that Brouwer might have after his death, Hilbert fired 43 Brouwer as an associate editor of Mathematische Annalen because of "incompatibility of our views on fundamental matters" 44 e.g., Hilbert ridiculed Brouwer for challenging the validity of the Principle of Excluded Middle. Gödel's original results were for Principia Mathematica (and not first-order logic) as the foundation for the mathematics of its time including the Dedekind axiomatization of the natural numbers. In face of Wittgenstein's devastating criticism, Gödel insinuated 45 that he was crazy and retreated to first-order logic in an attempt to salvage his results. Some theoreticians turned first-order logic into a philosophical dogma in part it facilitated their careers. Since theoreticians couldn't prove anything significant about practical mathematical theories, they cut them down to unrealistic first-order theories where results could be proved (e.g. compactness) that did not hold for practical mathematical theories. In the famous words of Upton Sinclair: "It is difficult to get a man to understand something, when his salary depends on his not understanding it." Some theoreticians have ridiculed dissenting views and attempted to limit their distribution by political means. 46

Acknowledgments

"All truth passes through three stages: First, it is ridiculed. Second, it is violently opposed. If f:τ 2 𝛔 1 and x:τ1, then f[x]:τ2. iii Setτ is a type parametrized by the type τ. In Java and C++, parametrized types are called "generics", "<" is used for , and ">" is used for . The following axiom holds: ∀[τ::,s:Setτ,x∈s] → x:τ iv Propositionorder is the parametrized type consisting of type Proposition parametrized by order. v The type of p⟦x⟧ means that the Y untyped fixed point operator cannot be used to construct propositions in Direct Logic.

Grammar (syntax) trees (i.e. expressions and sentences) are defined as follows: i The type of (x) means that the Y untyped fixed point operator cannot be used to construct sentences in Direct Logic.

 Expressions, i.e.,
ii if t then s1 else s1

iii The type of (p⟦x⟧) means that the Y untyped fixed point operator cannot be used to construct sentences in Direct Logic.

Foundations with strong parameterized types

"Everyone is free to elaborate [their] own foundations. All that is required of [a] Foundation of Mathematics is that its discussion embody absolute rigor, transparency, philosophical coherence, and addresses fundamental methodological issues." 61

Classical Direct Logic develops foundations for mathematics by deriving sets 62 from types 63 to encompass all of standard mathematics including the reals, analysis, geometry, etc. 64 For each order:ℕ+ and P:Propositionorder ℕ , the following strongly-typed categorical Dedekind induction axiom holds:

(P⟦0⟧  ∀[i:ℕ]→ P⟦i⟧⇨P⟦i+1⟧) ⇨ ∀[i:ℕ]→ P⟦i⟧
Another fundamental axiom of Mathematics is for each order:ℕ+ and P:Propositionorder O the following strongly-typed categorical ordinal induction axiom holds:

(∀[α:O]→ (∀[β<α:O]→ P⟦β⟧)⇨P⟦α⟧) ⇨ ∀[α:O]→ P⟦α⟧ Type Choice Choiceτ1,τ2:τ2 τ2 τ1 ∀[f:τ2 τ1 ]→ ∀[x:τ1] → (∃[z:τ1] → f[z]:τ2) ⇨ Choiceτ1,τ2[f][x]:τ2
Categoricity "If the mathematical community at some stage in the development of mathematics has succeeded in becoming (informally) clear about a particular mathematical structure, this clarity can be made mathematically exact ... Why must there be such a characterisation? Answer: if the clarity is genuine, there must be a way to articulate it precisely. If there is no such way, the seeming clarity must be illusory ... for every particular structure developed in the practice of mathematics, there is [a] categorical characterization of it." 65 Classical Direct Logic is much stronger than first-order axiomatizations of set theory in that it provides categoricity for ℕ, ℝ, and O. Categoricity is very important in Computer Science so that there are no nonstandard elements in models of computational systems, e.g., infinite integers and infinitesimal reals.

Theorem (Categoricity of

Theorem (Categoricity of Ordinals O):

If X be a type satisfying the axioms the theory of the ordinals Ord, then X is (uniquely) isomorphic to O. 71 Theorem (Model Soundness of Ord ):

(⊢ Ord ) ⇨ ⊨ O 
Proof: Suppose ⊢ Ord . The conclusion immediately follows because the axioms for the theory Ord hold in the model O .

Richard Dedekind

Theorem. Sets τ is categorical via a (unique) isomorphism. Proof: 79 Suppose that X satisfies the axioms for Sets τ.

By ordinal induction, the isomorphism I:X Setsτ as follows: I is a unique isomorphism:

 I is one to one  The range of I is X  I is a homomorphism: o I [{ }Setsτ] = { }X o ∀[S1,S2:Setsτ] → I [S1 ∪ S2] = I[S1] ∪X I [S2] o ∀[S1 S2:Setsτ] → I[S1 ∩ S2] = I[S1] ∩X I[S2] o ∀[S1,S2:Setsτ] → I[S1 -S2] = I[S1] -X I[S2] o ∀[S:Setsτ] → I[⋃S] = ⋃X {I[x] | x∈S}  I -1 :Setsτ X is a homomorphism  I is a unique isomorphism: If g:X Setτ is an isomorphism, then g= I
According to [Monk 2007]: 82 Wittgenstein hoped that his work on mathematics would have a cultural impact, that it would threaten the attitudes that prevail in logic, mathematics and the philosophies of them. On this measure it has been a spectacular failure.

Unfortunately, recognition of the worth of Wittgenstein's work on mathematics came long after his death. For decades, many theoreticians mistakenly believed that they had been completely victorious over Wittgenstein.

According to [Gödel 1972]: "Wittgenstein did not understand it [Gödel's 1931 article on Principia Mathematica] (or pretended not to understand it). He interpreted it as a kind of logical paradox, while in fact it is just the opposite, namely a mathematical theorem within an absolutely uncontroversial part of mathematics (finitary number theory or combinatorics)."

In the above passage, Gödel retreated from Principia Mathematic to the First-Order Logic theory FirstOrderNatualNumbers to defend his proposition I'mUnprovableInFirstOrderNatualNumbers. However, the following incompleteness result is not very impressive because FirstOrderNatualNumbers is a very weak theory: Chaitin [2007] The thesis of Chaitin's criticism above is that incompleteness is a fundamental issue for formal systems that is not adequately addressed by Gödel's proof based on his proposition. 83 Gödel's derived his proposition using what [Carnap 1934] later called the "Diagonal Lemma" which is equivalent to the Y untyped fixed point operator on propositions. His results were for Principia Mathematica, which was intended as the foundation of all of Mathematics. Unfortunately, Principia Mathematica had some defects in its types that have been corrected in Direct Logic..

 ⊨ℕ I'mUnprovableInFirstOrderNatualNumbers  ⊬ FirstOrderNatualNumbers I'mUnprovableInFirstOrderNatualNumbers Furthermore,
[Church 1935] correctly proved inferential incompleteness (sometimes called the "First Incompleteness Theorem") without using Gödel's proposition. The Church theorem and its proof are very robust. After Church proved inferential undecidabilty of closed mathematical theories using computational undecidablity, Gödel claimed more generality and that his results applied to all consistent mathematical systems that incorporate axioms for the natural numbers. However, when he learned of Wittgenstein's devastating proof of inconsistency, 84 Gödel retreated to claiming that his results applied to the very weak first-order theory of natural numbers. 85 The upshot is that Gödel never acknowledged that his proposition i I'm unprovable. implies inconsistency in mathematics.

Also, the ultimate criteria for working mathematicians of correctness theorems of the natural numbers provability using the categorical set theory described in this article. In this sense, Wittgenstein was correct in his identification of ultimate "truth" with provability. On the other hand, Gödel obfuscated the important identification of provability as the touchstone of ultimate correctness in mathematics.

Paul Cohen [2006] wrote as follows of his interaction with Gödel: 86 "His [Gödel's] main interest seemed to lie in discussing the 'truth' or 'falsity' of these questions, not merely in their undecidability. He struck me as having an almost unshakable belief in this "realist" position, which I found difficult to share. His ideas were grounded in a deep philosophical belief as to what the human mind could achieve. I greatly admired this faith in the power and beauty of Western Culture, as he put it, and would have liked to understand more deeply what were the sources of his strongly held beliefs. Through our discussions, I came closer to his point of view, although I never shared completely his 'realist' point of view, that all questions of Set Theory were in the final analysis, either true or false."

i constructed using the Y untyped fixed point operator on propositions von Neumann [1961] had a very different view from Gödel:

"It is not necessarily true that the mathematical method is something absolute, which was revealed from on high, or which somehow, after we got hold of it, was evidently right and has stayed evidently right ever since."

Provability Logic

One kind of Provability Logic (called PL) is a cut-down theory of deduction that has been used to investigate provability predicates for languages that allow use of the Y untyped fixed point operator for propositions [Verbrugge 2010]. PL is very weak; even for proving theorems about integers because PL is first-order.

[ Löb 1955] proposed the following conditions that became the basis of Provability Logic:

i 1. (⊢ PL ) ⇨ ⊢ PL ⊢ PL  87 2. ⊢ PL ((⊢ PL (⇨)) ⇨ (( ⊢ PL ) ⇨ ⊢ PL ))) 88 3. ⊢ PL ((⊢ PL ) ⇨ ⊢ PL ⊢ PL ) 89
Gödel's construction of the proposition I'm unprovable in PL ii using the Y fixed point operator can be carried out in Provability on propositions about the natural numbers with the following results:

 ⊬ PL I'mUnprovableInPL iii  ⊬ PL I'mUnprovableInPL iv  Consistent[PL] ⇨ ⊨ℕ I'mUnprovableInPL v
i His formulation actually used a convoluted coding of propositions into integers called Gödel numbers.

ii I'mUnprovableInPL ≡ ⊬ PL I'mUnprovableInPL

iii Proof by contradiction in PL iv Proof by contradiction in PL v If Consistent[PL], then I'mUnprovableInPL is true in the model ℕ by proof above in theory Nat .

John von Neumann

However, PL is a weak theory. For example, the principle of natural deduction Logic that allows theorems to be used in subproofs is not allowed in PL: 90 (⊢ )⊢

In summary, Provability Logic (although a useful historical development step) is too weak and fragile to serve in the mathematical foundation of Computer Science.

Limitations of first-order logic

"By this it appears how necessary it is for nay man that aspires to true knowledge to examine the definitions of former authors; and either to correct them, where they are negligently set down, or to make them himself. For the errors of definitions multiply themselves, according as the reckoning proceeds, and lead men into absurdities, which at last they see, but cannot avoid, without reckoning anew from the beginning; in which lies the foundation of their errors..."

[Hobbes Leviathan, Chapter 4] 91

It turns out that first-order logic is amazing weak. For example, first-order logic is incapable of characterizing even the natural numbers, i.e., there are infinite integers in models of every first-order axiomatization of the natural numbers. Furthermore, there are infinitesimal real numbers in models of every first-order axiomatization of the real numbers. i Of course, infinite integers and infinitesimal reals are monsters that must be banned from the mathematical foundations of Computer Science.

However, some theoreticians have found first-order logic to be useful for their careers because it is weak enough that they can prove theorems about first-order axiomatizations whereas they cannot prove such theorems about stronger practical systems, e.g., Classical Direct Logic. 92 Zermelo considered the First-Order Thesis to be a mathematical "hoax" because it necessarily allowed unintended models of axioms. 93 [Barwise 1985] critiqued the First-Order Thesis that mathematical foundations should be restricted to first-order logic as follows:

The reasons for the widespread, often uncritical acceptance of the first-order thesis are numerous. The first-order thesis ... confuses the subject matter of logic with one of its tools. First-order language is just an artificial language structured to help investigate logic, much as a telescope is a tool constructed to help study heavenly bodies. From the perspective of the mathematics in the street, the firstorder thesis is like the claim that astronomy is the study of the telescope. 94 Computer Science is making increasing use of Model Analysis i in the sense of analyzing relationships among the following:  concurrent programs and their Actor Model denotations  domain axiom systems and computations on these domains i a restricted form of Model Checking in which the properties checked are limited to those that can be expressed in Linear-time Temporal Logic has been studied [Clarke, Emerson, Sifakis, etc. ACM 2007 Turing Award].

Jon Barwise

Ernst Zermelo

In Computer Science, it is important that the natural numbers be axiomatized in a way that does not allow non-numbers (e.g. infinite ones) in models of the axioms. Unfortunately, every consistent first-order axiomatization of the natural numbers has a model with an infinite integer: The infinite integer ∞ is a monster that must be banned from the mathematical foundations of Computer Science.

Theorem: If ℕ is
A similar result holds for the standard theory ℝ of real numbers [Dedekind 1888] compared to a cut-down, first-order theory 95 , which has models with infinitesimals: . It can be shown that M is a model of T with an infinitesimal ε, which is a monster that must be banned from the mathematical foundations of Computer Science.

Theorem: If ℝ is
On the other hand, since it is not limited to first-order logic, Classical Direct Logic characterizes structures such as natural numbers and real numbers up to isomorphism. i There are theorems for integers that cannot be proved from the first-order versions of the Dedekind axioms [Goodstein 1944, Simpson 1985, Wiles 1995, Bovykin 2009, McLarty 2010].

i proving that software developers and computer systems are using the same structures Of greater practical import, First-order logic is not a suitable foundation for the Internet of Things in which specifications require a device respond to a request. i The specification that a computer responds can be formalized as follows: ∃[i:ℕ]→ ResponseBefore[i].. However, the specification cannot be proved in a first-order theory.

Proof: In order to obtain a contradiction, suppose that it is possible to prove in a first-order theory T ∃[i:ℕ]→ ResponseBefore [i]. Therefore the infinite set of propositions {ResponseBefore[i] | i:ℕ} is inconsistent. By the compactness theorem of first-order logic, it follows that there is finite subset of the set of propositions that is inconsistent. But this is a contradiction, because all the finite subsets are consistent since the amount of time before a server responds is unbounded, that is,

∄[i:ℕ]→ ⊢ T ResponseBefore[i].
The following is an example of an Actor system can provides a service that is impossible to implement using nondeterministic Turing Machines because:

There is a bound on the size of integer that can be computed by an always halting nondeterministic Turing Machine starting on a blank tape.

Plotkin [1976] gave an informal derivation as follows:

Now the set of initial segments of execution sequences of a given nondeterministic program P, starting from a given state, will form a tree.

The branching points will correspond to the choice points in the program. Since there are always only finitely many alternatives at each choice point, the branching factor of the tree is always finite. That is, the tree is finitary. Now König's lemma says that if every branch of a finitary tree is finite, then so is the tree itself. In the present case this means that if every execution sequence of P terminates, then there are only finitely many execution sequences. So if an output set of P is infinite, it must contain a nonterminating computation.

i An implementation of such a system is given below in this article.

First-order logic is not a suitable foundation for specifications in the Internet of Things.

above concurrent algorithm for Unbounded∎[ ] cannot be implemented using nondeterministic abstract state machines or using the nondeterministic λcalculus.

The above program illustrates how nondeterministic branching is not a good model for message reception in IoT

As a foundation of mathematics for Computer Science, Classical Direct Logic provides categorical 96 numbers (integer and real), sets, lists, trees, graphs, etc. which can be used in arbitrary mathematical theories including theories for categories, large cardinals, first-order axiomatizations, etc. These various theories might have "monsters" of various kinds. However, these monsters are not imported into the foundations of Computer Science.

Computer Science needs stronger systems than provided by first-order logic in order to weed out unwanted models. In this regard, Computer Science doesn't have a problem computing with "infinite" objects (i.e. Actors) such as π and uncountable sets such as the set of real numbers Setℝ. However, the mathematical foundation of Computer Science is very different from the general philosophy of mathematics in which the infinite integers and infinitesimal reals allowed by models of first-order theories may be of some interest. Of course, it is always possible to have special theories that are not part of the foundations with infinite integers, infinitesimal reals, unicorns, etc. 97 Of course some problems are theoretically not computable. However, even in these cases, it is often possible to compute approximations and cases of practical interest. i

The mathematical foundation of Computer Science is very different from the general philosophy of mathematics in which infinite integers and infinitesimal reals may be of some interest. Of course, it is always possible to have special theories with infinite integers, infinitesimal reals, unicorns, etc.

Church's Paradox

[ Church 1932, 1933] attempted basing foundations entirely on untyped higher-order functions, but foundered because contradictions emerged because 1. His system allowed the use of the Y untyped fixed point operator for propositions [Kleene and Rosser 1935] 2. Theorems in his system were computationally enumerable.

[Church 1934] expounded on the following profound issues, which is designated " Church's Paradox":

"in the case of any system of symbolic logic, the set of all provable theorems is [computationally] enumerable... any system of symbolic logic not hopelessly inadequate ... would contain the formal theorem that this same system ... was either insufficient [theorems are not computationally enumerable] or over-sufficient [that theorems are computationally enumerable means that the system is inconsistent]... This, of course, is a deplorable state of affairs... Indeed, if there is no formalization of logic as a whole, then there is no exact description of what logic is, for it in the very nature of an exact description that it implies a formalization. And if there no exact description of logic, then there is no sound basis for supposing that there is such a thing as logic."

The above issues can be addressed as follows: 1. Requiring Mathematics to be strongly typed 2. Mathematics self proves that it is "open" in the sense that proofs are not computationally enumerable (i.e. not "closed"). 98

Gödel, Curry, and Löb Paradoxes

Allowing use of the Y untyped fixed point operator for propositions results in contradictions.

For example, consider the diagonal construction used in [Gödel 1931]:

The proposition I'm unprovable. that was used by Gödel cannot be constructed as follows: Gödel thought that he demonstrated ⊢⊬Gödel. Therefore ⊢Gödel using Gödel⇔⊬Gödel. ⊢⊢Gödel follows using adequacy. But the contradiction ⊢Gödel follows using Gödel⇔⊬Gödel.

Alonzo Church

Also, the following paradoxes cannot prove every proposition because the Y untyped fixed point operator for propositions cannot be used in a strongly typed logic:

The Liar Paradox [Eubulides of Miletus] is an example of using untyped propositions to derive an inconsistency. However, strong typing prevents an inconsistency as follows: [1999]. 12 A prominent logician referee of this article suggested that if the proof is accepted then consistency should be made an explicit premise of every theorem of classical mathematics! 13 As shown above, there is a simple proof in Classical Direct Logic that Mathematics (├) is consistent. If Classical Direct Logic has a bug, then there might also be a proof that Mathematics is inconsistent. Of course, if such a bug is found, then it must be repaired. The Classical Direct Logic proof that Mathematics (├) is consistent is very robust. One explanation is that consistency is built in to the very architecture of classical mathematics because it was designed to be consistent. Consequently, it is not absurd that there is a simple proof of the formal consistency of Mathematics (├) that does not use all of the machinery of Classical Direct Logic.

Ψ i hypothesis ... Φ i inference Ψ⇨Φ i conclusion Ψ i premise ... Ψ⇨Φ i premise ... Φ i conclusion ΨΦ i premise … Ψ├ Θ i premise ... Φ├ Θ i premise ... Θ i conclusion Ψ i premise … ΨΦ i conclusion Ψ i premise … ΨΦ i premise … Φ i conclusion (Ψ├ Φ)├ (Ψ⇨Φ) Ψ ├ (ΨΦ) (ΨΦ), (Ψ├ Θ), (Φ├ Θ) ├ Θ Ψ, (Ψ⇨Φ) ├ Φ Ψ, (ΨΦ) ├ Φ  Introduction  Elimination  Cases Ψ i premise … Φ i premise ... ΨΦ i conclusion ΨΦ i premise … Ψ i conclusion … Φ i conclusion Ψ, Φ ├ (ΨΦ) (ΨΦ) ├ Ψ, Φ  Introduction  Elimination (├ Ψ) ⇨ Ψ Soundness (Φ├ Ψ) ⇔ (├ (Φ├ Ψ
In reaction to paradoxes, the dogma of strict separation of "object theories" (theories about basic mathematical entities such as numbers) and "meta theories" (theories about theories) was developed. This linguistic separation can be very awkward in Computer Science. Consequently, Direct Logic does not have the separation in order that some propositions can be more "directly" expressed. For example, Direct Logic can use ├├Ψ to express that it is provable that P is provable in Mathematics. It turns out in Classical Direct Logic that ├├Ψ holds if and only if ├Ψ holds. By using such expressions, Direct Logic contravenes the philosophical dogma that the proposition ├├Ψ must be expressed using Gödel numbers. 14 Wittgenstein in 1937 published in Wittgenstein 1956, p. 50e and p. 51e] 15 using what [Carnap 1934] later called the "Diagonal Lemma" which is equivalent to the Y untyped fixed point operator on propositions. 16 Classical Direct Logic is different from [Willard 2007], which developed sufficiently weak systems that the proposition I'm unprovable. does not exist.

17 Delta, student in [Lakatos, 1976, pg. 14].

18 specified by axioms [Dedekind 1888] that characterize them up to a unique isomorphism 19 It is worth going to a lot of trouble to make sure that Classical Direct Logic is consistent so that it can be freely used in an inconsistent theory without introducing additional inconsistencies into the theory. Any bugs found in Classical Direct Logic must be repaired to restore consistency. where ProgressionS i ⇾ ProgressionS i+1 In this way, S can be mathematically characterized in terms of all its possible behaviors (including those involving unbounded nondeterminism). The denotations of the Computational Representation Theorem form the basis of procedurally checking programs against all their possible executions. 21 According to [Gödel correspondence with Ernst Zermelo October 30, 1931 in Kurt Gödel Collected Works Volume V Correspondence H-Z, Oxford University Press, 2003. pp. 420-431.]: Without Gödel's restriction "you obtain an uncountable system of possible statements, among which only a countable subset are `provable', and there must certainly be `undecidable' statements." 22 e.g. [Shulman 2012, nLab 2014] 23 [cf. Church 1934, Kleene 1936] 24 [Church 1936, Turing 1936] 25 Since Mathematics has all the power of Nat. 30 The formal consistency theorem contradicts the claim in [Raatikainen 2015] which states: "For any consistent system [formal system] F within which a certain amount of elementary arithmetic can be carried out [for example, the formal system ℕ], the consistency of F cannot be proved in F itself." where "Roughly, a formal system is a system of axioms equipped with rules of inference, which allow one to generate new theorems. The set of axioms is required to be finite or at least decidable, i.e., there must be an algorithm (an effective method) which enables one to mechanically decide whether a given statement is an axiom or not. If this condition is satisfied, the theory is called "recursively axiomatizable", or, simply, "axiomatizable". The rules of inference (of a formal system) are also effective operations, such that it can always be mechanically decided whether one has a legitimate application of a rule of inference at hand. Consequently, it is also possible to decide for any given finite sequence of formulas, whether it constitutes a genuine derivation, or a proof, in the system-given the axioms and the rules of inference of the system."

and "A formal system is consistent if there is no statement such that the statement itself and its negation are both derivable in the system."

The reason for the contradiction is that [Raatikainen 2015] implicitly assumed that a formal system must be able construct Gödel's proposition I'm unprovable. 31 Same proof as for Nat 32 Same proof as for Nat 33 Closely related to conservation laws in physics [START_REF]CurryΨ├ (CurryΨ├ Ψ)) // substituting 1) into 2)[END_REF] That the closed mathematical theory Nat is inferentially undecidable [START_REF]CurryΨ├ (CurryΨ├ Ψ)) // substituting 1) into 2)[END_REF] with respect to ProofsComputationalyEnumerable Nat does not mean incompleteness with respect to the information that can be inferred because  ⊢ ⊬ Nat ProofsComputationalyEnumerable Nat  ⊢ ⊬ Nat ProofsComputationalyEnumerable Nat 35 For example, inconsistent information does not infer nonsense. 36 Consequently, there can cannot be any escape hatch into an unformalized "meta-theory." 37 The claim also relied on Gödel's proposition I'm unprovable. 38 Formal syntax was invented long after [Gödel 1931]. 39 emphasis in original 40 cf. [Rosental 2008] 41 According to [Concoran 2001]:

"after first-order logic had been isolated and had been assimilated by the logic community, people emerged who could not accept the idea that first-order logic was not comprehensive. These logicians can be viewed not as conservatives who want to reinstate an outmoded tradition but rather as radicals who want to overthrow an established tradition." 42 for discussion see [Hewitt 2010] 43 in an unlawful way (Einstein, a member of the editorial board, refused to support Hilbert's action) 44 Hilbert letter to Brouwer, October 1928 45 Gödel said "Has Wittgenstein lost his mind?" 46 For example:

  Proof by Contradiction, i.e. (Φ⇒(ΘΘ))├ Φ, which says that a proposition can be proved by showing that it implies a contradiction.  Theorem Use (a theorem can be used in a proof), i.e. (├ Φ)├ Φ 10 Theorem: Mathematics self proves its own formal consistency. Formal Proof By definition, Consistent⇔∃ [Ψ]→├ (ΨΨ). 11 By the rule of Existential Elimination, there is some proposition Ψ0 such that Consistent ⇒├ (Ψ0 Ψ0) which by Theorem Use and transitivity of implication means Consistent⇒ (Ψ0 Ψ0). Substituting for Φ and Θ, in the rule for Proof by Contradiction, we have (Consistent⇒(Ψ0Ψ0))├ Consistent. Thus,├ Consistent. A Natural Deduction i proof is given below: 1) Consistent // hypothesis to derive a contradiction just in this subargument ├ Consistent // rule of Proof by Contradiction using 1) and 4) 2) ∃[Ψ]→├(ΨΨ) // definition of inconsistency using 1) 3)├ (Ψ 0 Ψ 0 ) // rule of Existential Elimination using 2) 4) Ψ 0 Ψ 0 // rule of Soundness using 3) Natural Deduction Proof of Formal Consistency of Mathematics i [Jaśkowski 1934] developed Natural Deduction cf. [Barker-Plummer, Barwise, and Etchemendy 2011]

  o x1x2:Proposition1 where x1:τ, e2:τ and τ:: o τ1⊑τ2 56 where τ1:τ3, τ2:τ4 , τ3:: and τ4:: o τ1:: 57 where τ1:τ2 and τ2:: o (x:τ):Proposition1 where τ::, x:τ1 and τ1:: o f[x]:Proposition1 where x:τ, f:Boolean τ and τ:: o p⟦x⟧:Propositionorder+1 v where x:τ, p:Propositionorder τ and order:ℕ+ o (1, …, n-1├ 𝐩 𝐓 n):Propositionorder 58 where p:Proof, T:Theory, 1 to n:Propositionorder and order:ℕ+ o s:Propositionorder where s:Sentenceorder with no free variables and order:ℕ+ i Type of computable procedures from τ1 into τ2. If f:([τ1]↦τ2) and x:τ1, then f ∎[x]:τ2. ii Type of functions from τ1 into τ2.

  Natural Numbers ℕ): 66 If X be a type satisfying the Dedekind categorical axioms for the natural numbers Nat , then X is isomorphic to ℕ 67 , which is strictly more powerful than what a first-order theory can express. 68 Theorem (Categoricity of Real Numbers ℝ): 69 If X is a type satisfying the Dedekind categorical axioms for the real numbers Real, then X is (uniquely) isomorphic to ℝ, which is strictly more powerful than what a first-order theory can express. 70 Theorem (Model Soundness of Nat ): (⊢ Nat ) ⇨ ⊨ℕ Proof: Suppose ⊢ Nat . The conclusion immediately follows because the axioms for the theory Nat hold in the model ℕ .

  Set α+1 τ Z∈XI[S] ⇔ ∃[Y:Set α τ]→ I[Y]∈XZ 3. S:Set α τ and α is a limit ordinal Z∈XI[S] ⇔ ∃[β<α:O,Y:Set β τ]→ I[Y]∈XZ

  a model of a first-order axiomatization T, then T has a model M with an infinite integer. Proof: The model M is constructed as an extension of ℕ by adding a new element ∞ with the following atomic relationships: {∞<∞}  { m<∞ | m:ℕ} It can be shown that M is a model of T with an infinite integer ∞.

  a model of a first-order axiomatization T, then T has a model M with an infinitesimal. Proof: The model M is constructed as an extension of ℝ by adding a new element ∞ with the following atomic relationships: {∞<∞}  {m<∞ | m:ℕ} Defining ε to be 1 ∞ , it follows that ∀[r:ℝ]→ 0<ε< 1 𝑟

5720

  The Computational Representation Theorem[Clinger 1981; Hewitt 2006] characterizes computation for systems which are closed in the sense that they do not receive communications from outside:The denotation DenoteS of a closed system S represents all the possible behaviors of S as 20

From

  Davis @cs.nyu; Dana Scott @cmu; Eric Astor @uconn; Mario Carneiro @osu; Dave Mcallester @ttic; Joe Shipman Subject: Re: Parameterized types in the foundations of mathematics Not if I have anything to say about it! Harvey On Apr 20, 2016 at 11:25 AM, Carl Hewitt wrote: > Hi Martin, > > Please post the message below to FOM [Foundations of Mathematics forumHarvey Friedman on the FOM Wiki: "I have not yet seen any seriously alternative foundational setup that tries to be better than ZFC in this [categoricity of models] and other respects that isn't far far worse than ZFC in other even more important respects." > > Of course, ZFC is a trivial consequence of parameterized types with the following definition for set of type τ: > > Setτ ≡ Boolean τ > > Also of course, classical mathematics can be naturally formalized using parameterized types. For example, see "Inconsistency Robustness in Foundations: Mathematics self proves its own Consistency and Other Matters" in HAL Archives. > > Regards, > Carl 47 Arthur Schopenhauer (1788-1860) 48 For every type there is a larger type, i.e.., ∀[τ1::] → ∃[τ2::] → τ1⋤τ2 49 True≠False ∀[x:Boolean]→ x=True  x=False 60 50 The theory of the natural numbers Nat is axiomatized as follows where S is the successor function: 0:ℕ  +1:ℕ ℕ  ∀[i:ℕ]→ +1[i]≠0  ∀[i, j:ℕ]→ +1[i]=+1[j] ⇒ i=j For each order:ℕ+ and P:Propositionorder ℕ :(P⟦0ℕ⟧  ∀[i:ℕ]→ P⟦i⟧⇨P⟦+1[i]⟧) ⇨ ∀[i:ℕ]→ P⟦i⟧ 51The theory of the ordinals Ord is axiomatized as follows: 0:O  ∀[α:O]→ α≧0  Successor ordinals: +1:O O o ∀[α:O]→ +1[α]>α o ∀[α,β:O]→ β>α ⇒ +1[α]≦β o ∀[α:O]→ α:SuccesorO ⇔ ∃[δ:O]→ α=+1[δ]  Limit ordinals: ∀[α:O,f:O O ]→ ⊍αf:O o ∀[α:O]→ α:LimitO ⇔ α>0  ∄[δ:O]→ α=+1[δ] o ∀[α,β<α:O,f:O O ]→ f[β]≦⊍αf o ∀[α,β:O,f:O O ]→ (∀[δ<α]→ f[δ]≦β) ⇨ ⊍αf≦β  Omega ordinals: ∀[α:O]→ ωα:O o ω0 = ℕ o ∀[α:O]→ ⇨ |ωα+1| ≅ |𝐁𝐨𝐨𝐥𝐞𝐚𝐧 𝛚 α | ∀[α,β:O]→ |β|≅|ωα+1| ⇨ ωα+1≦β where |τ1| ≅ |τ2| ⇔ ∃[f:τ 2 τ 1 ]→ OneToOneOntoτ1,τ2[f] o ∀[α:LimitO]→ ωα = ⊍ β<α 𝛚 β Trichotomy: ∀[α,β:O]→ α<β ⊻ α=β ⊻ β<α  For each order:ℕ+ and P:Propositionorder O the following ordinal induction axiom holds: (∀[α:O]→ ∀[β<α:O]→ P⟦β⟧⇨P⟦α⟧) ⇨ ∀[α:O]→ P⟦α⟧

  Lakatos has called this strategy "monster-barring."

contra Gödel et. al "Men… think in herds … they only recover their senses slowly, and one by one." Charles Mackay

] is the result of sending the Actor CreateReal the message [ ]  (0 either 1) is the nondeterministic choice of 0 or 1,  [first, rest] is the list that begins with first and whose

	Classical Direct Logic
	There are uncountably many propositions (because there is a different
	"The point of foundations is not to arbitrarily restrict inquiry but proposition for every real number). Consequently, there are propositions that
	to provide a framework wherein one can legitimately perform those are not the abstraction of any element of a denumerable set of sentences. For
	constructions and operations that are mathematically interesting example, p[x:ℝ] ≡ λ[y:ℝ] → (y=x) defines a different predicate p[x] for each
	and useful." real number x, which holds for only one real number, namely x. i
	-Herrlich and Strecker [1973]
	It is important to distinguish between sentences, and propositions. Sentences ii
	Direct Logic must meet the following challenges: (which without free variables) can be abstracted into propositions that can be
	 Consistent to avoid security holes asserted. Furthermore, terms iii can be abstracted into Actors (i.e. objects in
	 Powerful so that computer systems can formalize all logical inferences mathematics).
	 Principled so that it can be easily learned by software engineers
	 Coherent so that it hangs together without a lot of edge cases Abstraction and parsing are becoming increasingly important in software
	 Intuitive so that humans can follow computer system reasoning engineering. e.g.,
	 The execution of code can be dynamically checked against its  Comprehensive to accommodate all forms of logical argumentation documentation. Also Web Services can be dynamically searched for  Inconsistency Robust to be applicable to pervasively inconsistent theories and invoked on the basis of their documentation. of practice using  Use cases can be inferred by specialization of documentation and from o Inconsistency Robust Direct Logic for logical inference about inconsistent information code by automatic test generators and by model checking.
	o Classical Direct Logic for Mathematics used in inconsistency-robust  Code can be generated by inference from documentation and by
	theories 19 generalization from use cases.
	In Direct Logic, unrestricted recursion is allowed in programs by using
	strongly typed recursive definitions.
	There are uncountably many Actors. 20 For example, CreateReal∎[ ] is a
	nondeterministic procedure that can return any real number i between 0 and 1
	where ii
	CreateReal∎[ ] ≡ [(0 either 1), ⩛Postpone CreateReal∎[ ]]
	where  Some younger logicians join with the Computer Scientists pushing forward with strong parameterized types in foundations. At this point, the above Computer Scientists are firmly ensconced in their field and have a head start in that they have held two international symposia at  CreateReal∎[ remainder Stanford and published a well-regarded volume of articles on their is rest, and results in what is arguably the most prestigious academic series of  Postpone expression delays execution of expression until the volumes in the area. But there is still much work to be done! value is needed.
	Each CreateReal∎[ ] could be any one of uncountably many numbers between
	0 and 1.
	i using binary representation.
	ii Typically, a result returned by the non-deterministic procedure Real is not
	computable in the sense there is no computable deterministic procedure that can
	compute its digits.

Abstraction and parsing are needed for large software systems so that that documentation, use cases, and code can mutually speak about what has been said and their relationships.

	For example:
	Propositions
	e.g. ∀[n:ℕ]→ ∃[m:ℕ]→ m>n
	i.e., for every ℕ there is a larger ℕ
	Sentences
	e.g. (∀[n:ℕ]→ (∃[m:ℕ]→ (m>n)))
	i For example (p[3])[y] holds if and only if y=3.
	ii which are grammar tree structures
	iii which are grammar tree structures

Types in Classical Direct Logic are much stronger than those in constructive logic 22 because Classical Direct Logic has all of the power of Classical Mathematics. Mathematics self proves that it is open

		+ 1)) is not the same
	as (3.14159... < (3.14159... + 1)) because it does not have the same
	vocabulary and it is a much larger sentence that has many terminals
	<
	+
	3.14159...
	3.14159...	1
	3.14159...	1

whereas

(3.14159.

.. <

(3.14159.

.. + 1)) has just 3 terminals: Consequently, sentences cannot be enumerated. 21 Note: "Although everything mathematical is formalizable, it is nonetheless impossible to formalize all of mathematics in a single formal system."

[Gödel 1935]

13 Mathematics proves that it is open in the sense that it can prove that its proofs cannot be provably computationally enumerated: 23 Theorem ⊢Mathematics is Open, i.e., ⊢ProofsComputationalyEnumerable Proof. i

  Nat is inferentially undecidable 29 with respect to ProofsComputationalyEnumerable Nat does not mean Mathematical incompleteness with respect to the information that can be inferred about theory Nat because  ⊨ℕ ProofsComputationalyEnumerable Nat  ⊬ Nat ProofsComputationalyEnumerable

Nat

Theorem 30 ⊢ Nat Consistent Nat , i.e., Nat proves its formal consistency



  Formalization of Wittgenstein's proof that Gödel's proposition I'm unprovable. leads to contradiction in mathematics. So the consistency of mathematics had to be rescued against Gödel's proposition constructed using what [Carnap 1934] later called the "Diagonal Lemma" which is equivalent to the Y untyped fixed point operator on propositions. Use of the Y untyped fixed point operator on propositions in results of [Curry

  The inherently social nature of the processes by which principles and propositions in logic are produced, disseminated, and established is illustrated by the following issues with examples:40

	"
	John Kenneth Galbraith [1971 pg. 50]
	"Max Planck, surveying his own career in his Scientific Autobiography
	[Planck 1949], sadly remarked that 'a new scientific truth does not
	triumph by convincing its opponents and making them see the light,
	but rather because its opponents eventually die, and a new generation
	grows up that is familiar with it.' "
	[Kuhn 1962]

  Third, it is accepted as being self-evident."47 Extensive discussions with Tom Costello, Eric Kao, Ron van der Meyden and other members of the Stanford CS Logic Group helped the development of this paper. Tom suggested that more conventional terminology be used in the formal proof of consistency of mathematics. Martin Davis kindly provide the reference for[Gödel 1933]. Comments by James Lottes, Pat Suppes, Daniel Raggi, Eric Winsberg, John Woods, and Ming Xiong helped improve the presentation. Dan Flickinger suggested including an overview table. Alan Bundy pointed out many crucial places where the presentation needed improvement. John Woods served ably as the senior referee by compiling an excellent synopsis of anonymized conference referee reports for this article. Discussions with Michael Beeson helped improve the section on how mathematics self-proves its own formal consistency. Correspondence with Monroe Eskew helped clarify the relationship of Classical Direct Logic with first-order logic. Also, Monroe suggested looking at the Berry Paradox. i Correspondence with Jack Copeland helped clarify the relationship of the work reported in this article with previous work by Gödel et. al. Also, Jack suggested inclusion of the closely related natural deduction proof that mathematics proves its own formal consistency in addition to the linear proof. Discussions on the FriAM electronic mailing list were very helpful in improving this article. J.J. Meyer participated in Inconsistency Robustness 2011 and subsequently wrote an excellent review of the resulting book. Conversations with Dana Scott were very helpful in clarifying the discussion of the issue of the provability of the formal consistency of Mathematics. Natarajan Shankar was extremely helpful in clarifying how Gödel's proposition I'm unprovable. leads to inconsistency in Mathematics. Setτ:: iii and Expressionτ:: 54 where τ::  Propositions, i.e., a Proposition is a discrimination of the following: o :Propositionorder where :Propositionorder iv and order:ℕ+ o ,,⇨,⇔:Propositionorder where ,:Propositionorder and order:ℕ+ o (p � True⦂ 1, False⦂ 2):Propositionorder where p:Boolean, ,:Propositionorder 55 and order:ℕ+ o x1=x2 where x1,x2:τ and τ:: o x1x2 where x1,x2:Setτ and τ::

	Appendix 1. Notation of Classical Direct Logic
	 Type i.e., a type is a discrimination 48 of the following:
	o Boolean:: 49 , ℕ:: 50 and O:: 51
	o Propositionorder:: and Sentenceorder:: where order:ℕ+
	o τ1⦶τ2:: 52 , [τ1,τ2]:: 53 , [τ1]↦τ2:: i and 𝛕 𝟐	𝛕 𝟏 :: ii where τ1:: and τ2::
	o

  Constantτ where x:τ and τ:: o x:Expressionτ where x:Constantτ and τ:: o x:Expressionτ where x:Variableτ and τ:: o (Let f1[x1:𝛕 𝟏 ]:𝛔 𝟏 ≡d1, ... , fn[xn:𝛕 𝐧 ]:𝛔 𝐧 ≡dn 59 。y):Expressionτ where for i in 1 to n, fi:Variable𝛔 𝐢 𝛕 𝒊  in di and y, xi:Variable𝛕 𝐢  in di,di:Expression𝛔 𝐢 , y:Expressionτ, and 𝛕 𝐢 :: o (Let x1:𝛕 𝟏 ≡d1, ... , xn≡dn 60 。y):Expressionτ where for i in 1 to n, xi:Variable𝛕 𝐢  in di and y, di:Expression𝛔 𝐢 , y:Expressionτ, and if e1 then e2 else e3  Sentences, i.e., a Sentence is a discrimination of the following:

	an Expressionτ is a discrimination of the o Constantτ:: where τ:: following: o (x):𝛕 𝐢 :: o (e1⦶e2):Expressionτ1⦶τ2, ([e1, e2]):Expression[τ1, τ2], ([e1]↦e2):Expression[τ1]↦τ2 and (𝐞 𝟐 𝐞 𝟏 ):Expression𝛕 2 𝛕 1  where e1:Expressionτ1, e2:Expressionτ2 , τ1:: and τ2:: o (e1 � True⦂ e2 , False⦂ e3):Expressionτ i where e1:ExpressionBoolean, e2,e3:Expressionτ and τ:: o (λ[x:τ1]:τ2 → e):Expression𝛕 𝟐 𝛕 𝟏  where e:Expressionτ2, x:Variableτ1 in e, and τ1,τ2:: o (e[x]):Expressionτ2 where e:Expression𝛕 𝟐 𝛕 𝟏 , x:Expressionτ1, τ1:: and τ2:: o (e∎[x]):Expressionτ2 where e:Expression[τ1]↦τ2, x:Expressionτ1, τ1:: and τ2:: o Sentenceorder⊑ExpressionSentenceorder where order:ℕ+ and order:ℕ+ o (s):Sentenceorder where s:Sentenceorder and order:ℕ+ o (s1s2),(s1s2),(s1⇨s2),(s1⇔s2):Sentenceorder where s1,s2:Sentenceorder and order:ℕ+ o (e � True⦂ s1, False⦂ s2) ii :Sentenceorder where e:ExpressionBoolean, s1,s2:Sentenceorder and order:ℕ+ o (e1=e2):Sentence1 where e1,e2:Expressionτ and τ:: o (e1⊑e2):Sentence1 where e1,e2:Expressionτ1, τ1:τ2 and τ2:: o (e1e2):Sentence1 where e1,e2:ExpressionSetτ and τ:: o (e1e2):Sentence1 where e1:Expressionτ, e2:ExpressionSetτ and τ:: o (e1:e2):Sentence1 where e1:Expressionτ1, e2:Expressionτ2 τ1:τ3, τ2:τ4 and τ3,τ4:: o (e::):Sentence1 where e:Expressionτ and τ:: o o (x):Sentenceorder+1 i where x:VariableSentenceorder o (∀[x:τ1]→ s),(∃[x:τ1]→ s):Sentenceorder where x:Variableτ1

e:τ where e:Expressionτ with no free variables and τ:: o s:Expressionτ where s:StringExpressionτ and τ:: i in s, s:Sentenceorder and order:ℕ+ o (f[x]):Sentence1 where x:Expressionτ, f:ExpressionBoolean τ  and τ:: o (p⟦x⟧):Sentenceorder+1 iii where x:Expressionτ, p:ExpressionSentenceorder τ , τ:: and order:ℕ+ o (s1,…,sn-1├ 𝐩 𝐓 sn):Sentenceorder where T:ExpressionTheory, s1 to n:Sentenceorder, p:ExpressionProof and order:ℕ+ o s:Sentenceorder where s:StringSentenceorder and order:ℕ+

  [START_REF]formalizing Gödel's proof[END_REF]



  Liar Paradox[Eubulides of Miletus] 101 Liar:Nonexistent ≢ Liar // above definition is illegal because Liar is of // type order greater than Liar Proposition of any order // because the type of CurryΨ├Ψ is a Proposition of higher // order than CurryΨ

	Appendix 4. Classical Natural Deduction
	Below are schemas for nested-box-style Natural Deduction i for Classical
	Mathematics:
	1)	Liar ⇔ Liar	// definition of Liar
	2)	Liar	// proof by contradiction from 1)
	3)	Liar	// from 1) and 2)
	Also, the following paradoxes cannot prove every proposition because the Y
	untyped fixed point operator for propositions cannot be used in a strongly
	typed logic:

 Curry's Paradox [Curry 1941] Suppose Ψ:Propositionorder:ℕ+. CurryΨ:Nonexistent ≢ CurryΨ├ Ψ // illegal definition because CurryΨ is not a i Evolved from classical natural deduction [Jaśkowski 1934]. See history in Pelletier

  Consistent with the general practice in Computer Science, there is no way to identify propositions with integers.

	Classical Provability Direct Logic,	Terminator, 45
	15	Theorem Use, 49  A theorem of Mathematics can be used in a step of a sub-proof to
	Pythagoreans, 1 prove a theorem in Mathematics regardless of the assumptions of the Transitivity of ∈
	Replacement sub-proof.	sets, 34
	sets, 34 11 The definition of formal inconsistency, i.e., Type, 29
	⇨ Elimination universe Union Consistent⇔∃[Ψ]→├ (ΨΨ) ⇨ Introduction Russell, B., 7 sentence Scott, D., 22 sets, 34 is not per se about numbers.
	Direct Logic, 31	sets, 34
	Sentence, 31	Verbrugge,
	Set, 29	Wittgenstein, L., 1, 36
	Sets τ, 17	Y untyped fixed point operator,
	Setsτ, 14, 34	39, 45, 47
	Setsτ, 14, 34	Zermelo, E., 1, 41
	categorical, 14, 17	ZFC
	soundness, 15	sets, 34
	soundness of inference, 15
		Proof by Contradiction
		Ψ	i hypothesis
		...
		ΦΦ	i inference
		Ψ	i conclusion
		(Ψ├ (ΦΦ))├ Ψ
			Adequacy
			))

i This is Gödel's argument formalized for the foundations of mathematics, à la Principia Mathematica

i This argument appeared in[Church 1934] expressing concern that the argument meant that there is "no sound basis for supposing that there is such a thing as logic." ii See section immediately below.

i Please see section on the Berry Paradox in the historical appendix.

i Likewise, first-order set theory (e.g. ZFC) is very weak. See discussion immediately below.

i e.g. see Terminator[START_REF] Knies | Terminator Tackles an Impossible Task Microsoft Research[END_REF]], which practically solves the halting problem for device drivers

i This is a stronger form of a theorem in[START_REF] Gödel | On formally undecidable propositions of Principia Stephen Kleene[END_REF]

Proposition Nat ω ≡ Proposition Nat 1 ⦶ Proposition Nat 2 ⦶ ...

Sentence Nat ω ≡ Sentence Nat 1 ⦶ Sentence Nat 2 ⦶ ...

Domain Nat ω ≡ Domain Nat 1 ⦶ Domain Nat 2 ⦶ ... where Domain Nat 1 ≡ ℕ Domain Nat n+1 ≡ Domain Nat n ℕ

sometimes called "incomplete"

Bibliography Anthony Anderson and Michael Zelëny (editors). Logic, Meaning and Computation: Essays in Memory of Alonzo Church Springer. 2002. Jeremy Avigad and John Harrison. Formally Verified Mathematics. CACM. April 2014. Steve Awodey and Erich Reck. Completeness and Categoricity. Parts I and II: Nineteenth-century Axiomatics to Twentieth-century Metalogic. History and Philosophy of Logic. Vol. 23. 2002. Steve Awodey, Álvaro Pelayo, and Michael A. Warren. Voevodsky's Univalence Axiom in Homotopy Type Theory Notices of AMS. October 2013. Alan Anderson. Mathematics and the "Language Game" (1958) in Philosophy of Mathematics Selected Readings. Prentice Hall. 1964. David Barker-Plummer, Jon Barwise and John Etchemendy. Language, Proof, and Logic: Second Edition Stanford Center for the Study of Language and Information. 2011. Jon Barwise. Model-Theoretic Logics: Background and Aims in "Model Theoretic Logics" Springer-Verlag. 1985. Hamid Berenji, et. al. A reply to the paradoxical success of Fuzzy Logic AI Magazine. Spring 1994. Francesco Berto. The Gödel Paradox and Wittgenstein's Reasons Philosophia Mathematica. February, 2009. Errett Bishop. The Crisis in Contemporary Mathematics Historia Mathematica. 2. 1975. George Boolos. On second-order logic Journal of Philosophy. Vol. 72. 1975. Nicolas Bourbaki. Univers. In Séminaire de Géométrie Algébrique du Bois Marie -1963-64 -Théorie des topos et cohomologie étale des schémas -(SGA 4)vol. 1. Springer-Verlag. 1972 Andrey Bovykin. Brief introduction to unprovability. Logic Colloquium 2006. Lecture Notes in Logic 2009 Bernd Buldt. The Scope of Gödel's First Incompleteness Theorem. Logica Universalis. Volume 8. December 2014. Andrea Cantini, Paradoxes and Contemporary Logic, Stanford Encyclopedia of Philosophy. Winter 2012 Edition. Rudolph Carnap. Logische Syntax der Sprache. (The Logical Syntax of Language Open Court Publishing 2003) 1934. Walter Carnielli and João Marcos. Ex Contradictione Non Sequitur Quodlibet Bulletin of Advanced Reasoning and Knowledge. 2001. Hasok Chang. Inventing Temperature: Measurement and Scientific Progress Oxford University Press. 2007. Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang Ranking Abstractions ESOP'08. Gregory Chaitin. Interview in "Dangerous Knowledge" BBC4 documentary. 2007. Gregory Chaitin. Thinking about Godel and Turing: Essays on Complexity 1970-2007. World Scientific Publishing. 2007. Alonzo Church. A Set of postulates for the foundation of logic (1) Annals of Mathematics. Vol. 33, 1932. Alonzo Church. A Set of postulates for the foundation of logic (2) Annals of Mathematics. Vol. 34, 1933. Alonzo Church. The Richard Paradox. Proceedings of American Mathematical Society. 1934. Alonzo Church. An unsolvable problem of elementary number theory Bulletin of the American Mathematical Society 19, May, 1935. American Journal of Mathematics, 58 (1936), Alonzo Church: A Formulation of the Simple Theory of Types, Journal of Symbolic Logic. vol. 5. 1940. Alonzo Church The Calculi of Lambda-Conversion Princeton University Press. 1941. Alonzo Church. Introduction to Mathematical Logic Princeton University Press. 1956. Paul Cohen. The Independence of the Continuum Hypothesis I and II Proceedings of the National Academy of Sciences of the United States of America, Vol. 50, No. 6. Dec. 15, 1963. John Corcoran. Second-order Logic. Logic, Meaning and Computation. Kluwer. 2001. Thierry Coquand and Gérard Huet: The calculus of constructions. Technical Report 530, INRIA, Centre de Rocquencourt, 1986.John Corcoran. Gaps between logical theory and mathematical practice in The methodological unity of science. 1973.John Corcoran. Categoricity. History and Philosophy of Logic. Vol. 1. 1980 Will Clinger. Foundations of Actor Semantics MIT Mathematics Doctoral Dissertation. June 1981. Jack Copeland. The Essential Turing Oxford University Press. 2004. Haskell Curry "Some Aspects of the Problem of Mathematical Rigor" Bulletin of the American Mathematical Society Vol. 4. 1941.

Mathematica in "A Source Book in Mathematical Logic, 1879-1931" Translated by Jean van Heijenoort. Harvard Univ. Press. 1967. Kurt Gödel (1933) Kurt Gödel Collected Works, Vol. III. Oxford University Press. Page 47. Kurt Gödel. Review of Logical Syntax of Language. 1935. Godfrey Hardy, A Mathematician's Apology Cambridge: University Press. 1940. Reuben Goodstein. On the restricted ordinal theorem Journal of Symbolic Logic. 1944. Mandy Hale. The Single Woman: Life, Love, and a Dash of Sass. Thomas Nelson. 2013. Horst Herrlich and George Strecker. Category theory Allyn and Bacon. 1973. Carl Hewitt, Peter Bishop and Richard Steiger. A Universal Modular Actor Formalism for Artificial Intelligence IJCAI-1973. Carl Hewitt Inconsistency Robustness for Logic Programs in Inconsistency Robustness. College Publications. 2015. Carl Hewitt Formalizing common sense for inconsistency-robust information integration using Direct Logic™ Reasoning and the Actor Model Inconsistency Robustness 2010. Carl Hewitt ActorScript™ extension of C#™, Java™ , JavaScript™ and Objective C™ in Inconsistency Robustness. College Publications. 2015. Carl Hewitt Actor Model of Computation: Many-core Inconsistency-robust Information Integration Inconsistency Robustness 2011. Carl Hewitt. What is computation? A Computable Universe: Understanding Computation & Exploring Nature as Computation. Edited by Hector Zenil. World Scientific Publishing Company. 2012. David Hilbert Mathematical Problems Lecture delivered before the International Congress of Mathematicians at Paris in 1900. Translation by Newson: http://aleph0.clarku.edu/~djoyce/hilbert/problems.html David Hilbert. Neubegründung der Mathematik: Erste Mitteilung Abhandlungen aus dem Seminar der Hamburgischen Universität. 1. 1922. English translation in From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s Oxford University Press. 1998. Immaculee Ilibagiza. Left to Tell: Discovering God Amidst the Rwandan Holocaust Hay House. 2014. Daniel Isaacson. The reality of mathematics and the case of set theory. Truth, Reference, and Realism. Central European University Press. 2008. Stanisław Jaśkowski On the Rules of Suppositions in Formal "Logic Studia Logica" 1, 1934. (reprinted in: Polish logic 1920-1939, Oxford University Press, 1967. Stephen Kleene and John Barkley Rosser The inconsistency of certain formal logics Annals of Mathematics Vol. 36. 1935. Stephen Kleene General recursive functions and natural numbers Mathematical Annuals. 1936. Stephen Kleene On the Notation of Ordinal Numbers Journal of Symbolic Logic 1938.

Sets τ defined using strong parameterized types

The type Setτ can be defined as follows:

Setτ ≡ Boolean τ

Of course set membership is defined as follows: ∀[x:τ:, S:Setτ] → xS ⇔ S[x]=True

Inductive definition:

1. Set 0 τ ≡ Boolean τ The properties below mean that Setsτ is a "universe" of mathematical discourse. 72  Foundation: There are no downward infinite membership chains. 73  Transitivity of Appendix 2. Historical Background "The powerful (try to) insist that their statements are literal depictions of a single reality. 'It really is that way', they tell us. 'There is no alternative.' But those on the receiving end of such homilies learn to read them allegorically, these are techniques used by subordinates to read through the words of the powerful to the concealed realities that have produced them." [Law 2004]

Gödel was certain

" 'Certainty' is far from being a sign of success; it is only a symptom of lack of imagination and conceptual poverty. It produces smug satisfaction and prevents the growth of knowledge." [Lakatos 1976] According to John von Neumann, Gödel was "the greatest logician since Aristotle." 80 Gödel based his incompleteness results on the thesis that mathematics necessarily has the proposition I'm unprovable. i Wittgenstein was granting the supposition that Gödel had proved inferential undecidability (sometimes called "incompleteness") of Russell's system, that is., ⊢⊬ P. However, inferential undecidability is easy to prove using the proposition P where P⇔⊬P: Proof. Suppose to obtain a contradiction that ⊢ P. Both of the following can be inferred:

1) ⊢ ⊬ P from the hypothesis because P⇔⊬P 2) ⊢ ⊢ P from the hypothesis by Adequacy. But 1) and 2) are a contradiction. Consequently, ⊢⊬ P follows from proof by contradiction.

By contrast, the following Actor system can compute an integer of unbounded size:

The above Actor system can be implemented as follows using ActorScript™:

Unbounded∎[ ]:Integer ≡ Of course, it is completely unacceptable for every proposition to be provable and so measures must be taken to prevent this.

Berry Paradox

The Berry Paradox [Russell 1906] can be formalized as follows:

Consider the following definition:

Length [s]<100 ⇨ Characterize⟦s, n⟧))"

BExpression:ExpressionPropositionω+1 The following logical equivalences hold:

Theorem. Allowing the proposition I'm unprovable. [ii] used in the incompleteness results of [Gödel 1931] leads to inconsistency in Classical Provability Direct Logic. 106

Proof: 107

// Proof by Contradiction using 2) and 3) i

5) ├ I'mUnprovable

// from 4) using 1)

6) ├├ I'mUnprovable

// from 5) using adequacy 7) ├ I'mUnprovable // from 6) using 1)

Inconsistency in Classical Provability Direct Logic means that there is some Ψ such that ├ (ΨΨ).

Theorem. Classical Provability Direct Logic proves its formal consistency

Proof: Consistent ⇒ ├ (ΨΨ) "Second-order quantification is significant for philosophy of mathematics since it is the means by which mathematical structures may be characterized. But it is also significant for mathematics itself. It is the means by which the significant distinction can be made between the independence of Euclid's Fifth postulate from the other postulates of geometry and the independence of Cantor's Continuum hypothesis [conjecture] from the axioms of set theory. The independence of the Fifth postulate rejects the fact, which can be expressed and established using second-order logic, that there are different geometries, in one of which the Fifth postulate holds (is true), in others of which it is false." 67 For each type X that satisfies the Dedekind axioms there is a (unique) isomorphism I:X ℕ and inductively defined as follows:

] Using proofs by induction on ℕ and X, the following follow:

1. I is defined for every ℕ 2. I is one-to-one:

Base : Suppose k=0ℕ. QED.

To show: [j]]] by definition of I 5. I -1 :ℕ X is a homomorphism:

To show:

Base : To show: [j]]] by definition of I 6. I is the unique isomorphism: If g:X ℕ is an isomorphism then g=I Proof: Induction on P[j:ℕ]:

To show:

For example, there are nondeterministic Turing machines that the theory ℕ proves always halt that cannot be proved to halt in the cut-down first-order theory. 69 [Dedekind 1888] The following can be used to characterize the real numbers (ℝ 69 ) up to isomorphism with a unique isomorphism:

where

64 71 For each type X that satisfies the theory Ord there is a (unique) isomorphism I:X O inductively defined as follows:

Using proofs by ordinal induction on O and X, the following follow: 1. I is defined for every O

x I⚬f⚬I -1 5. I -1 :O X is a homomorphism 6. I is the unique isomorphism: If g:X O is an isomorphism then g=I 72 [Bourbaki 1972; Fantechi, et. al. 2005] 73 This implies, for example, that no set is an element of itself. [Zermelo 1930, van Dalen 1998, Ebbinghaus 2007] 94 First-order theories fall prey to paradoxes like the Löwenheim-Skolem theorems (e.g. any first-order theory of the real numbers has a countable model). First-order theorists have used the weakness of first-order logic to prove results that do not hold in stronger formalisms such as Direct Logic [Cohen 1963, Barwise 1985]. 95 e.g. the theory RealClosedField [Tarski 1951] 96 unique up to isomorphism via a unique isomorphism 97 Rejection of the First-Order Thesis resolves the seeming paradox between the formal proof in this article that Mathematics formally proves its own formal consistency and the formal proof that 'Every "strong enough" formal system that admits a proof of its own consistency is actually inconsistent.' [Paulson 2014]. Although Mathematics is "strong enough" the absence of propositions (constructed using the Y untyped fixed point operator on propositions) blocks the proof of formal inconsistency to which Paulson referred. 98 In other words, the paradox that concerned [Church 1934] (because it could mean the demise of formal mathematical logic) has been transformed into fundamental theorem of foundations! "There is a proposition of order 𝑛 which I affirm and which is false". This is a proposition of order 𝑛+1; hence the man is not affirming any proposition of order 𝑛 102 [Yanofsky 2013 page 328] expressed concern about Löb's paradox: we must restrict the fixed-point machine in order to avoid proving false statements [using Löb 's argument]. Such a restriction might seem strange because the proof that the fixed-point machine works seems applicable to all [functions on untyped statements]. But restrict we must. Yanofsky proposed solving above problem posed by Löb's paradox using systems of logic that are so weak that they cannot abstract their own sentences. Unfortunately, such weak systems are inadequate for Computer Science. Instead of weakening logic, Direct Logic adopted the strategy of using types for mathematics that does not allow the Y fixed point operator for propositions and sentences. 103 using definition of BSet 104 using definition of BExpression 105 substituting BNumber for n [ii] using what [Carnap 1934] later called the "Diagonal Lemma" which is equivalent to the Y the fixed point operator on propositions. 106 Wittgenstein developed the proof below [lines 5) thru 7)] that contradiction in mathematics results from allowing the proposition I'm unprovable. used in the incompleteness results of [Gödel 1931]. 107 [Wittgenstein 1937 published in Wittgenstein 1956, p. 50e and p. 51e]