Carl Hewitt

Alonzo Church

Richard Dedekind

Stanisław Jaśkowski

Bertrand Russell

Ludwig Wittgenstein

Strong Types for Direct Logic

Mathematics in this article means the precise formulation of standard mathematical theories that axiomatize the following up to a unique isomorphism: booleans, natural numbers, reals, ordinals, sets, lambda calculus procedures, and Actors.

Mathematical Foundations for Computer Science

All mathematical entities are instances of types. Computer Science brought different concerns and a new perspective to mathematical foundations including the following requirements (building on [Maddy 2018]):  Practicality is providing powerful machinery so that arguments (proofs) can be short and understandable and  Generality is formalizing inference so that all of mathematics can take place side-by-side. Direct Logic provides a generality by formalizing theories of the natural numbers, reals, ordinals, set theory, groups, lambda calculus, and Actors side-by-side.  Shared Standard of what counts as legitimate mathematics so people can join forces and develop common techniques and technology. According to [Burgess 2015]:

To guarantee that rigor is not compromised in the process of transferring material from one branch of mathematics to another, it is essential that the starting points of the branches being connected ... be compatible. ... The only obvious way ensure compatibility of the starting points ... is ultimate to derive all branches from a common unified starting point. Direct Logic provides such a common unified starting point including natural numbers, reals, ordinals, set theory, group theory, geometry, algebra, lambda calculus, and Actors that are axiumatized up to a unique isomorphism.  Abstraction so that fundamental mathematical structures can be characterized up to a unique isomorphism including natural numbers, reals, ordinals, set theory, groups, lambda calculus, and Actors. 10  Guidance is for practioners in their day-to-day work by providing relevant structures and methods free of extraneous factors. Direct Logic provides guidance by providing strong parameterized types and intuitive categorical inductive axiomatizations of natural numbers, ordinals, sets, lambda calculus, and Actors.  Meta-Mathematics is the formalization of logic and rules of inference. Direct Logic facilitates meta-mathematics because it is its own meta-theory.  Automation is facilitated in Direct Logic by making type checking very easy and intuitive along as well as incorporating Jaśkowski natural deduction for building an inferential system that can be used in everyday work.

In a strongly typed mathematical theory, every proposition, term, and expression has a type where there is no universal type Any. Types are constructed bottom up from types that are categorically axiomatized. 1 Strong types are extremely important in Direct Logic because they block all known paradoxes including Berry [START_REF] Russell | Les paradoxes de la logique Revue de métaphysique et de morale[END_REF]], [START_REF] Burali-Forti | Una questione sui numeri transfiniti Rendiconti del Circolo Matematico di Palermo[END_REF], Church [Church 1934], Curry [Curry 1941], Girard [Girard 1972], and Liar [Eubulides of Miletus], Löb [START_REF] Löb | Solution of a problem of Leon Henkin[END_REF]], and Russell [START_REF] Russell | Letter to Gottlob Frege[END_REF]]. 2 Blocking known paradoxes makes Direct Logic safer for use in Intelligent Applications by preventing security holes. Consistent strong mathematical theories can be freely used without introducing additional inconsistent information into inconsistency robust empirical theories that will be the core of future Intelligent Applications. Direct Logic 3 is called "direct" because it directly deals with propositions instead of attempting to deal with them indirectly using Gödel numbers as is done in Provability Logic 4 . Because propositions in Direct Logic are uncountable, it is impossible to give a Gödel number to every proposition. 5 Inconsistency Robustness is performance of information systems (including scientific communities) with pervasively inconsistent information. 6 Inconsistency Robustness of the community of professional mathematicians is their performance repeatedly repairing contradictions over the centuries. In the Inconsistency Robustness paradigm, deriving contradictions has been a progressive development and not "game stoppers." Contradictions can be helpful instead of being something to be "swept under the rug" by denying their existence, which has been repeatedly attempted by authoritarian theoreticians (beginning with some Pythagoreans). Such denial has delayed mathematical development. This article reports how considerations of Inconsistency Robustness have recently influenced the foundations of mathematics for Computer Science continuing a tradition developing the sociological basis for foundations. 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.

After [Church 1934], logicians faced the following dilemma:

 1 st order theories cannot be powerful lest they fall into inconsistency because of Church's Paradox.  2 nd order theories contravene the philosophical doctrine that theorems must be computationally enumerable.

The above issues can be addressed by requiring Mathematics to be strongly typed using so that:  Mathematics self proves that it is "open" in the sense that theorems are not computationally enumerable. 7  Mathematics self proves that it is formally consistent. 8  Strong mathematical theories for Natural Numbers, Ordinals, Set Theory, the Lambda Calculus, Actors, etc. are inferentially decidable, meaning that every true proposition is provable and every proposition is either provable or disprovable. 9

 Risk Assessment is the danger of contradictions emerging in classical mathematical theories. In this regard, Direct Logic formalizes longestablished and well-tested mathematical practice while blocking all known paradoxes including Berry [START_REF] Russell | Les paradoxes de la logique Revue de métaphysique et de morale[END_REF]], [START_REF] Burali-Forti | Una questione sui numeri transfiniti Rendiconti del Circolo Matematico di Palermo[END_REF],

Church [Church 1934], Curry [Curry 1941], Girard [Girard 1972], and Liar [Eubulides of Miletus], Löb [START_REF] Löb | Solution of a problem of Leon Henkin[END_REF]], and Russell [START_REF] Russell | Letter to Gottlob Frege[END_REF]].

Intuitive categorical inductive axiomatizations of natural numbers, propositions, types, ordinals, sets, lambda calculus, and Actors promote confidence in operational consistency.

Consistent mathematical theories can be freely used in (inconsistent) empirical theories without introducing additional inconsistency. 11

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." 12 "The aims of logic should be the creation of "a unified conceptual apparatus which would supply a common basis for the whole of human knowledge." [START_REF] Tarski | Introduction to Logic[END_REF] Note: parametrized types 13 in Direct Logic are more intuitive for classical mathematical theories than intuitionistic types [Martin- [START_REF] Martin-Löf | An intuitionistic theory of types in Twenty-Five Years of Constructive Type Theory[END_REF]]. 14 Booleans are Propositions although Propositions are not reducible to Booleans:  True:Boolean  False:Boolean  Boolean ⊑Proposition //each Boolean is a Proposition  Boolean ≠Proposition //some Propositions are not Booleans  (3=3) ≠ True //the proposition 3=3 is not equal to True  (3=3) ≠ (4=4)

//the proposition 3=3 is not equal to the proposition 4=4  (3=4) ≠ False //the proposition 3=4 is not equal to False In Direct Logic, unrestricted recursion is allowed in programs. For example, There are uncountably many Actors. For example, the procedure call Real∎[ ] can output any real number using binary representation between 0 and 1 where 15 Real:([ ]→ R [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] ) // Real is a procedure of // no arguments that returns a R [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] Real∎[ ] ≡ [(0 either 1), ⩛Postpone Real∎[ ]]

where o (0 either 1) is the nondeterministic choice of 0 or 1, o [ first, ⩛rest] is the list that begins with first and whose remainder is rest, and o Postpone expression delays execution of expression until the value is needed.

Also, there are uncountably many propositions (because there is a different proposition for every real number). For example, the function p defined as follows: p[x] ≡ λ[y:R] (y=x) defines a different predicate p [x] for each real number x, which holds for only one real number, namely x. 16 Sentences parse trees are important as a means for constructing propositions. If s is a well formed sentence parse tree with no free variables, then s is a proposition.

Every proposition is the abstraction of some sentence parse tree.

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 Φ.

Direct Logic develops foundations for Mathematics by deriving sets from types and categorical axioms for the natural numbers and ordinals. i.e., sentence parse tree for proposition that for every ℕ there is a larger ℕ

Sentence Parse Trees

Higher Order Logic

"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 characterization? 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." 17 Classical Direct Logic is much stronger than 1 st order axiomatizations of set theory in that it provides categoricity for natural numbers N, reals R, ordinals O. set theory, the lambda calculus and Actors. 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. For example, nonstandard models cause problems in model checking if a model has specified properties.

Natural Number Induction

The mathematical theory 18 Nat that axiomatises the Natural Numbers has the following axioms:

• N ::

// N is a type • 0:N // 0 is of type N • +1:N N // +1 is of type N N • ∄[i:N] +1[i]=0 • ∀[i,j:N] +1[i]=+1[j] ⇨ i=j
In addition Nat has the following induction axiom, which has uncountable instances: 19 ∀[P:

Nat N ] (P[0]  ∀[i:N] P[i]⇨P[+1[i]]) ⇨ ∀[i:N] P[i]
The above induction axiom makes use of the type Proposition Nat which has the following axioms: 20

• Nat ::

// Nat is the type of propositions of theory Nat • ∀[t 1 ,t 2 :Type Nat; x:t 1 ] (x:t 2 ):Nat • ∀[t :Type Nat; x1,x2:t ] (x1=x2):Nat
In addition to the above, propositions of Nat have the following induction axiom:

∀[Q:Nat Nat ] ((∀[t :Type Nat ; x1,x2:t ] Q[x1=x2]) ⋀ (∀[:Nat ] Q[]⇨Q[]) ⋀ (∀[1,2:Nat ] Q[1]Q[2]⇨Q[12]) ⋀ (∀[t :Type Nat ; P:Nat t ] ∀t Q[P])⇨Q[∀t P]) ⇨ ∀[:Nat ] Q[]
The above axioms characterize Proposition Nat up to a unique isomorphism. 21 The following theorem states that each proposition is the abstraction of a sentence parse tree. 22 Theorem. 23

∀[:Nat ] ∃[s:Sentence Nat]  = s Proof Checkers in Nat ∀[1,2:Nat ] (1⊢Nat
ForAllElimChecker[c]∎[1,2] ≡ 1 if (∀[x:t ] P[x]) then 2=P[c] else False // If 1 is ∀[x:t ] P[x], then 2=P[c], otherwise False Consequently, (∀[x:t ] P[x]) ⊢ ForAllElimChecker[c] 𝑁𝑎𝑡 P[c]

Computational Undecidability of Provability in Nat

The halting problem is to computationally decide whether a given procedure p halts on a given input x, which is formally expressed as Halt [p,x]. [Church 1935;Turing 1936] proved that the halting problem is computationally undecidable. Whether a proposition is a theorem of Nat is computationally undecidable because the predicate Halt can be formalized in Nat such that:

∀[i:N, p:([N]→N)] Halt[p, i] ⇔ ⊢ Nat Halt[p, i])
Theorem (Indiscernibility for Nat ):

∀[i,j:N] i=j ⇔ ∀[P:Nat N ] P[i]⇔P[j] Proof. Define Same:(Nat N ) N Same[i] ≡ λ[j:N] i=j ∀[i,j:N] (Same[i]⇔Same[j]) ⇨ i=j
Theorem (Proof Soundness of Nat ): (⊢ Nat ) ⇨  Proof soundness of means that a theorem in Nat can be used in proofs. A consequence of Proof Soundness is that unrestricted cut-elimination does not hold for Nat . 24

Axiomatization of ⊨ N

Axioms of ⊨ N are as follows:

 ⊨ N True  ⊨ N False  (⊨ N ) ⇔ (⊨ N )  (⊨ N )  (⊨ N ) ⇔ ⊨ N   ∀[P:Nat N ] (⊨ ∀[i:N ] P[i]) ⇔ (∀[i:N ] ⊨ N P[i]) Theorem (Model Soundness of Nat ): (⊢ Nat ) ⇨ (⊨ N )
Proof: Suppose ⊢ Nat . The theorem immediately follows because the axioms for the theory Nat hold in the type N.

Theorem (Categoricity of Nat ): 25 If X be a type satisfying the axioms for the natural numbers Nat , then there is a unique isomorphism I with N defined as follows:

• I:

X N • I[0 N ] ≡ 0 X • I[+1[j]] ≡ + 1 𝑋 [I[j]] because • I is defined on N • I is 1-1 • I is onto X • I is a homomorphism  I[0 N ] ≡ 0 X  ∀[i:N] I[+1[j]] ≡ + 1 𝑿 [I[j]] • I -1 is a homomorphism  I -1 [0 X ] ≡ 0 N  ∀[z:X] I -1 [+ 1 𝑿 [z]] ≡ [+1[I -1 [z]] • If g is an isomorphism with X, then g=I
Note that the statement of categoricity is not a 1 st order proposition because it quantifies over every type X and over every isomorphism between X, and N. (⇨) ⇨   proof theoretically to say that proving the theorem ⇨ means that  is a theorem:

(⇨) ⇨ ⊢ Nat   in [START_REF] Jaśkowski | On the Rules of Suppositions in Formal Logic[END_REF]] natural deduction to say that ( infers  and ) holds in a subproof 27 of a proof infers that  holds in the proof: That there are proofs that cannot be expressed through text alone, overturns a long-held philosophical dogma about mathematical theories, i.e., that all theorems of a theory can be computationally generated by starting with axioms and mechanically applying rules of inference.  It has been easier to prove meta theorems for 1 st order logic. Since theoreticians found it difficult to prove anything significant about practical mathematical theories, they cut them down to unrealistic 1 st 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.  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 36 Brouwer as an associate editor of Mathematische Annalen because of "incompatibility of our views on fundamental matters" 37 e.g., Hilbert ridiculed Brouwer for challenging the validity of the Principle of Excluded Middle. [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]] results were for Principia Mathematica as the foundation for the mathematics of its time including the categorical axiomatization of the natural numbers. In face of Wittgenstein's devastating criticism, Gödel insinuated 38 that he was crazy and retreated to 1stOrderDedekindPeano in an attempt to salvage his results.

(⊢ Nat )⊢ Nat 

Summary of Nat

The theory Nat can be summarized as follows:

 Indiscernibility for Nat:

∀[i,j:N] i=j ⇔ ∀[P:Nat N ] P[i]⇔P[j]  Instance Adequacy of Nat: ∀[P:Nat N ] (∀[i:N] ⊢ Nat P[i]) ⇨ ⊢Nat ∀[i:N] P[i]  Nat is categorical for N ⊦ Nat ∀[X::] NatX  ⇔ UniquelyIsomorphic[X, N]
 Nat proves its own formal consistency

⊦ Nat (∃[:Nat ] ⊦ Nat )  A proposition is true ⇔ it is provable in Nat ∀[:Nat ] (⊨ N ) ⇔ (⊦ Nat )  Nat is inferentially decidable ∀[:Nat ] (⊦ Nat )  (⊦ Nat )  ⊦ Nat  is computationally undecidable

Actor Model

Concurrent message passing was crucially omitted from the  calculus [Church 1932], Turing Machines (TM) [Turing 1936], Simula-67 [Dahl andNygaard 1967], and Logic Programs [START_REF] Hewitt | Planner: A Language for Proving Theorems in Robots IJCAI[END_REF]] thereby crippling them as a foundation for the Internet of Things (IoT). Actors [Hewitt, et. al 1973] remedied the omission to provide for scalable computation. An Actor message passing machine can be millions of times faster than any corresponding pure Logic Program or parallel nondeterministic  expression. Since the time of this early work, message passing has grown to be one of the most important paradigms in computing [Hewitt and Woods 2018;Hoare 2016;Milner 1993].

Of course, earlier work made huge pioneering contributions:  expressions play an important role in programming languages. TM inspired development of the stored program sequential computer. Simula-67 became the basis for object-oriented programming in Java and C++. Logic Programs are fundamental to Scalable Intelligent Systems. [Hewitt and Woods 2018]

Message Passing in Practice

Concurrency control for readers and writers in a data base is a classic problem that illustrates the power of message passing. The fundamental constraint is that multiple writers are not allowed to operate concurrently in the data base and a writer is not allowed to operate concurrently with a reader. In the figure below for an Actor machine  Yellow is used for the Actor's region of mutual exclusion  Within the region of mutual exclusion, a hole in grey allows other messages to be processed which are of two kinds: ReadersWriter Scheduler

Many different policies could be implemented in the above scheduler including the following:

 Reader priority: When a writer comes out of the database, resume all in ReadersQ.

 Writer priority: When a writer comes out of the database and both WritersQ and ReadersQ are nonempty, resume just one in ReadersQ, and then when it comes of the database resume one in WritersQ.

Computation that cannot be done by  Calculus, TM, or pure Logic Programs

Actor message passing machines can perform computations that a no  expression, nondeterministic Turing Machine, Simula-67 program, or pure Logic Program can implement. Below is an example of a very simple computation that cannot be performed by a nondeterministic TM:

There is an always-halting Actor message passing machine that can compute an integer of unbounded size. This is accomplished using variables count initially 0 and continue initially True. The computation is begun by concurrently sending over the Internet two messages to the Actor machine: a stop request that will return an integer n formalized as Output[n] and a go message that will return

Void.

The Actor machine operates as follows:

 When a go message is received: If continue is True, increment count by 1, send this Actor machine a go message in a hole of the region of mutual exclusion, and afterward return Void. If continue is False, return Void.

 When a stop message is received, return count and set continue to False for the next message received.

continue := False

True False

Theorem. There is no  expression, nondeterministic Turing Machine, Simula-67 program, or pure Logic Program that implements the above computation.

Proof [Plotkin 1976]: "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."

Limitations of 1 st Order Logic for Concurrent Computation

Theorem. It is well known that there is no 1 st order theory for the above Actor machine.

Proof. Every 1 st order theory is compact meaning that every inconsistent set of propositions has a finite inconsistent subset. Consequently, to show that there is no 1 st order theory, it is sufficient to show that there is an inconsistent set of propositions such that every finite subset is consistent. The set of propositions

NoOutput defined to be {Output[i] | i:N} is inconsistent meaning ⊢NoOutput (because ⊢∃[i:N] Output[i], i.e.,
 An Actor's event ordering o ∀[x:Actor, c:Com ] Initialx↷Receivedx[c]↷Afterx[c] 42 o ∀[x:Actor, c1,c2:Com ] c1≠c2 ⇒ Receivedx[c1]↷Receivedx[c2] ⋁ Receivedx[c2]↷Receivedx[c1] 43 o ∀[x:Actor, c1:Com ] ∄[c2:Com ] Receivedx[c1]↷Receivedx[c2]↷Afterx[c1] 44  An Actor's behavior change o ∀[x:Actor, c1:Com ] (∄[c2:Com ] Receivedx[c2]↷Receivedx[c1]) ⇒ x[Receivedx[c1]]=x[Initialx] 45 o ∀[x:Actor, c:Com ] x[Afterx[c]]=(x[Beforex[c]])[c] 46 o ∀[x:Actor, c:Com ] Let processing = Info[Beforex[c]]⊔Info[Receivedx[c]]⊔Info[Createdx[c]] 47 in Info[Afterx[c]]⊑processing 48 ⋀ Info[Sentx[c]]⊑processing 49  Discreteness of Actors event ordering 50 ∀[e1, e2:Event ] Finite[{e:Event | e1↷e↷e2]}] 51  Actor Induction ∀[x:Actor, P:Act Behavior ] (P[x[Initialx]] ∀[c:Com ] P[x[Receivedx[c]]]⇨P[x[Afterx[c]]]) ⇨ ∀[c:Com ] P[x[Receivedx[c]]]  P[x[Afterx[c]]] 52
Note that the above axioms do not require that every communication sent must be received. However, ActorScript provides that every request will either throw a TooLong exception or respond with the response sent to its customer.

Theorem. Computational Adequacy of Actors.

If for each i:N, Fi is a nondeterministic λ expression such that ∀[i:N] Fi⊑Fi+1 ⇨(limiti: N Fi):Actor

Theorem. Categoricity of Act

If X be a type satisfying the axioms for Act , then there is a unique isomorphism between X and Actor.

Theorem: Inferential completeness of the theory

Act ∀[:Act ] (⊨ Actor ) ⇒ (⊢ Act )
Corollary. Equivalence of satisfiability and provability in Act , i.e.,

∀[:Act ] (⊨ Actor ) ⇔ (⊢ Act ) Theorem. Inferential Decidability of Act , i.e., ∀[:Act ] (⊢ Act )  (⊢ Act ) Proof. Follows immediately from (⊨ Actor ) ⇔ (⊢ Act )
Mathematics self proves its own formal consistency (contra [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]])

The following are fundamental to Mathematics 53 :

 By Contradiction, i.e. ├ (¬Φ⇒(Θ¬Θ)) ⇒ Φ, which says that a proposition can be proved showing that its negation implies a contradiction.

 A theorem can be used in a proof 54 , i.e. ├ ((├ Φ)⇒Φ)

Theorem: Mathematics self proves its own formal consistency 55 , i.e., ├Consistent Proof. Suppose to obtain a contradiction, that mathematics is formally inconsistent, i.e., ¬Consistent. By definition of formal consistency, there is some proposition Ψ0 such that├ (Ψ0 ¬Ψ0) which by the Theorem Use means Ψ0¬Ψ0 , which is a contradiction. Thus, ├ Consistent using By Contradiction.

Please note the following points:  The above argument mathematically proves that Mathematics is formally consistent and that it is not a premise of the theorem that Mathematics is formally consistent.  Mathematics was designed for consistent theories and consequently Mathematics can be used to prove its own formal consistency regardless of other axioms. 56  [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]] used formal consistency as the basis of his results. The above theorem does not prove that Mathematics is operationally consistent, i.e., that no contradiction can be derived using the stated axioms and rules.

The above derivation means that "Mathematics is formally consistent" is a theorem in Classical Direct Logic.

The above self-proof of formal consistency shows that the current common understanding that [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]] proved "Mathematics cannot prove its own formal consistency, if it is formally consistent" is inaccurate. 57 1)Consistent // hypothesis to derive a contradiction just in this subargument ├ Consistent // axiom of Proof by Contradiction using 1) and 3)

2) ├(Ψ 0 Ψ 0 ) // definition of inconsistency using 1)

3) Ψ 0 Ψ 0 // axiom of Soundness using 2)

Natural Deduction Proof of Formal Consistency of Mathematics

Mathematics Self Proves that it is Open.

Mathematics proves that it is open in the sense that it can prove that its theorems cannot be computationally enumerated by a provably total procedure: Theorem ⊢Mathematics is Open, i.e., ⊢TheoremsEnumerableByProvableTotalProcedure Proof. 58 Suppose to obtain a contradiction that TheoremsEnumerableByProvableTotalProcedure Then by the definition of TheoremsEnumerableByProvableTotalProcedure Consequently,

⊢TheoremsEnumerator:

[N]→1 Proposition such that  ∀[p:Proposition ] (⊢p) ⇒ ∃[i:N] TheoremsEnumerator∎[i]=p
A subset of the theorems enumerated by TheoremsEnumerator are those stating that certain real numbers are provably computable. Consequently, there is a provably deterministic total procedure ProvablyComputableR [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] Enumerator:([N]→1ProvablyComputableR [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] ) which enumerates provably computable real numbers:

 Total[ProvablyComputableR [0,1] Enumerator]  ∀[i:N] (ProvablyComputableR [0,1] Enumerator∎[i] ]):ProvablyComputableR [0,1]  ∀[r:ProvablyComputableR [0,1] ] ∃[i:N] ProvablyComputableR [0,1] Enumerator∎[i]=r
ProvablyTotalEnumerator can be used to implement the provably deterministic total procedure ⊢Diagonal:([N]→1Boolean) as follows: [START_REF]X:Sets 0t  X:Boolean t[END_REF] because it is the deterministic composition of provably total deterministic procedures.  Diagonal:ProvablyComputableR [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] because Diagonal differs from every provably computable real number enumerated by ProvablyComputableR [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] Enumerator. The above contradiction completes the proof.

Diagonal∎[i] ≡ 1-(ProvablyComputableR [0,1] Enumerator∎[i])∎[i] Consequently:  Diagonal:ProvablyComputableR [0,
Some but not all of the theorems of Mathematics can be computationaly enumerated. [Franzén 2004] argued that Mathematics is inexhaustible because of inferential undecidability of mathematical theories. The above theorem that Mathematics is open provides another independent argument for the inexhaustibility of Mathematics.

Conclusion

Strong Types are extremely important in Direct Logic because they block all know paradoxes.

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.

Computer Science needs a rigorous foundation for all of mathematics that enables computers to carry out all reasoning without human intervention. 59 [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[Church , 1933] ] attempted basing foundations entirely on untyped higherorder 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.

[ [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]] claimed inferential undecidability 60 results for mathematics using the proposition I'mUnprovable In opposition to Wittgenstein's correct argument his proposition leads to contradictions in mathematics, Gödel claimed that the results of [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]] were for 1stOrderDedekindPeano . However, 1 st order theories are not a suitable foundation for Computer Science for reasons explained elsewhere in this article.

Following [Russell 1925, and Church 1932-1933], Direct Logic was developed and then investigated propositions with results below.

Formalization of Wittgenstein's proof that Gödel's proposition I'mUnprovable 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 1941] and [START_REF] Löb | Solution of a problem of Leon Henkin[END_REF]] 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 [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]] that mathematics cannot prove its own formal 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. 61 A solution is to require strongly typed mathematics to bar use of the Y untyped fixed point operator for propositions. 62 However, some theoreticians have very reluctant to accept the solution.

According to [Dawson 2006]: 63 o Gödel's results altered the mathematical landscape, but they did not "produce a debacle". o There is less controversy today over mathematical foundations than there was before Gödel's work. However, [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]] has produced a controversy of a very different kind from the one discussed by Dawson:

 The common understanding that mathematics cannot prove its own formal consistency 64 has been disproved.  Consequently, [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]] has now led to increased controversy over mathematical foundations.

Intelligent Applications need to use higher order logic because moderately strong theories of 1 st order logic are inconsistent. Categorical higher order theories of Natural Numbers, Reals, and Actors are inferentially complete and inferentially decidable.

Although theorems of mathematical theories in higher order logic are not computationally enumerable, proof checking is computationally decidable. Direct Logic with strong types categorically axiomatize up to a mathematical theory T

for the model M for each of the following models: Natural Numbers, Real Numbers, Computable Procedures, and Actors as follows:

 Indiscernibility for theory T:

∀[x1,x2:M] i=j ⇔ ∀[P:T M ] P[x1]⇔P[x2]  Instance Adequacy of T: ∀[P:T M ] (∀[x:M] ⊢ T P[x]) ⇨ ⊢ T ∀[x:M] P[x]  T is categorical for M: ⊦ T ∀[X :Type T ] TX ⇔ UniquelyIsomorphic[X , M]  T proves its own formal consistency ⊦ T (∃[:T ] ⊦ T )  A proposition is true if and only if it is provable in T ∀[:T ] (⊨ M ) ⇔ (⊦ T )  T is inferentially decidable ∀[:T ] (⊦ T )  (⊦ T )  ⊦ T  is computationally undecidable for :T  ⊦ 𝐩 𝑻
 is computationally decidable for p:ProofCheckerT  and :T

The development of Direct Logic has strengthened the position of working mathematicians as follows: 65  Allowing freedom from the philosophical dogma of the "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." [START_REF] Law | After Method: mess in social science research[END_REF]]

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." [START_REF] Lakatos | Proofs and Refutations[END_REF] Paul Cohen [2006] wrote as follows of his interaction with Gödel: 66 "His [Gödel's] "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."

Kurt Gödel

John von Neumann [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]] based incompleteness results on the thesis that mathematics necessarily has the proposition I'mUnprovable.

[This] is what comes of making up such sentences." [emphasis added]

Wittgenstein's proof is valid in Nat, which formalizes standard mathematical practice.

According to [START_REF] Monk | Boshevist or anarchist? The Reception of Wittgenstein's Philosophy of Mathematics in Wittgenstein and his interpreters[END_REF]]: "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. Ludwig Wittgenstein [START_REF] Chaitin | Dangerous Knowledge BBC4 documentary[END_REF] The Church/Turing theorem and its proof are very robust. Afterward Gödel claimed more generality and that his results applied to all consistent mathematical systems that incorporate the Dedekind/Peano axioms for the natural numbers. However, when he learned of Wittgenstein's devastating proof of inconsistency, 70 Gödel retreated to claiming that his results were only for 1stOrderDedekindPeano : "Wittgenstein did not understand it [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF] 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)." 71 However, Gödel engaged in historical revisionism because Wittgenstein's argument that Gödel's I'mUnprovable leads to inconsistency was for the higher order theory in Russell's system, which Gödel used in his famous 1931 article that Wittgenstein criticized. After Wittgenstein's criticism, Gödel retreated i to the position that his 1931 results were only for 1stOrderDedekindPeano , i without mentioning that he was retreating which Gödel called "finitary number theory or combinatorics." The upshot is that Gödel never acknowledged that his "self-referential" proposition i implies inconsistency in mathematics. Retaining Gödel's results for I'mUnprovable requires a very narrow and constricted approach of reducing propositions to strings for sentences and then to Gödel numbers axiomatized in 1stOrderDedekindPeano to avoid Wittgenstein's devastating criticism. This narrow constricted view is intolerable for computer science, which needs to reason about propositions in a more natural and flexible way using Strong Types. Although Gödel's incompleteness results for I'mUnprovable have fundamental problems, the work was extremely significant in further the development of the history of metamathematics. For example, the paradoxes of Curry and Löb were developed following along Gödel's work.

A key difference is that Direct Logic works directly with propositions as opposed to the work of Gödel, Curry, and Löb, which was based on 1 st order theories with propositions from sentence strings coded as integers.

i constructed using fixed points exploiting an untyped notation for mathematics

Attempt to Axiomatize N with Computationally Enumerable Theorems Nat1 described below illustrates failure in attempting to axiomatize the Natural Numbers using a theory whose theorems are computationally enumerable. The primitive of Nat 1 are as follows: 75 • 0:N

• +1:N N // add 1 • :𝑁𝑎𝑡 1 𝑁𝑎𝑡 1 // negation • ⋀:𝑁𝑎𝑡 1 𝑁𝑎𝑡 1 2 // conjunction • ∃:Nat 1 [Type Nat 1 , Nat 1 Type Nat 1  ] // existential quantifier 76  ⫦:Nat 1 Nat 1 // provability in Nat1
Nat1 has the following axiom schemas where s is abstraction of string s as a proposition:

 Induction Schema ∀[P:String Nat1 N ] ⫦ ( P [0]  ∀[i:N] P [i] ⇨ P [i+1]) ⇨ ∀[i:N] P [i]
 Instance Adequacy Schema [START_REF] Hilbert | Die Grundlegung der elementaren Zahlenlehre Mathematische Annalen[END_REF][START_REF] Thau | The -Rule Studia Logica[END_REF]]

∀[P:String Nat1 N ] ⫦ (∀[i:N] ⫦P [i]) ⇨ ∀[i:N] P [i]
Theorem: Axioms and theorems of Nat1 are computationally enumerable Theorem: ∀[:Nat1] (⫦) ⇔(⊢ Nat 1 )

The following defines the Nat1 provable computable real numbers between 0 and 1:

Definition Nat 1 R [0,1] ] ≡ R [0,1] ] ∋λ[x] ⫦x:Total [N]→1 Boolean ] 
Nat1 goes too far Theorems of Nat1 are computationally enumerable by Nat1TheoremsEnumerator where

⊦ Nat 1 Nat1TheoremsEnumerator:Total [N]→1 Theorem Nat1 ]  such that ⊦ Nat 1 ∀[:Theorem Nat1]] ∃[i:N] Nat 1 TheoremsEnumerator∎[i]=
Consequently, there is a Nat1 provably total procedure Nat1ProvablyComputableR [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] Enumerator such that ∀[r:Nat 1 R [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] However, this means that 1934] pointed out that there is no obvious way to remove the inconsistency, which means that that if Nat 1 is taken to be valid mathematical theory of truths of the natural numbers then, "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."

] ⇒ ∃[i:N] Nat1ProvablyComputableR [0,1] Enumerator∎[i]=r also ∀[i:N] ⫦ Nat1ProvablyComputableR [0,1] Enumerator∎[i]:Nat 1 R [0,1] Therefore by Nat1 Instance Adequacy, ⊦ Nat 1 ∀[i:N] Nat1ProvablyComputableR [0,1] Enumerator∎[i]:Nat 1 R
⊦ Nat 1 Nat1ProvablyComputableR[0,1]Enumerator:Total [N]→1 Nat 1 R [0,1]  Nat 1 Total F ]  ≡ F∋λ[p] ⫦ p:Total F ]  Nat 1 Enumerable ≡ Nat 1 Total [N]→1 Nat 1 R [0,1] ∋λ[f] ∀[r:Nat 1 R [0,1] ] ⇒ ∃[i:N] f∎[i]=r [Church
After [Church 1934], logicians faced the following dilemma:  1 st order theories cannot be powerful enough to be a foundation for Intelligent Applications lest they fall into inconsistency because of Church's Paradox.  2 nd order theories contravene the philosophical doctrine that theorems must be computationally enumerable.

Alonzo Church

There Is No 1 st Order Theory That Axiomatizes Actors By the Actor Model of Computation, the above Actor will eventually receive the stop[ ] message and return an unbounded number.

An Actor that Provably Responds

Discussion

Church's Paradox and other paradoxes raise a number of issues that can be addressed by requiring mathematics to be strongly typed and using higher order logic as follows:

1. Requiring Mathematics to be strongly typed using so that  Mathematics self proves that it is "open" in the sense that theorems are not computationally enumerable. 78  Mathematics self proves that it is formally consistent. 79  Strong mathematical theories for Natural Numbers, Ordinals, Set Theory, the Lambda Calculus, Actors, etc. are inferentially decidable, meaning that every true proposition is provable and every proposition is either provable or disprovable. Furthermore, theorems of these theories are not enumerable by a provably total procedure. 2. It was initially thought that mathematics could be based just on character strings. Then diagonalization was discovered and things haven't been the same since. The string for the general 1 st order non-categorical induction schema is as follows for each P:String Proposition 1 N :

( P [0]  ∀[i:N] P [i] ⇨ P [i+1]) ⇨ ∀[i:N] P [i]
which has countably many 1 st order propositions as instances that are abstracted from the countably many character strings of type String Proposition 1 and which differs fundamentally from the character string for the more general 2 nd order categorical induction axiom, which is as follows: 80 ∀[P:

Proposition 1 N ] (P[0]]  ∀[i:N] P[i]⇨P[i+1]) ⇨ ∀[i:N] P[i]
Although the theory Nat has only finitely many axioms, the above string abstracted as a proposition has uncountably many 1 st order propositions as instances. 81 In this way, Nat differs fundamentally from a 1 st order theory because, being uncountable, not all instances of the Nat induction axiom can be obtained by abstraction from character strings. Proofs abstracted from character strings for the axioms of the natural numbers can be computationally enumerated and are valid proofs in Nat, but this does not enumerate all of the proofs of Nat ! What is to be made of the uncountable number of theorems of Nat whose proofs cannot be written down in text?

Ernst Zermelo

Zermelo suggested that the [Godel 1931] incompleteness results relied on an overly restrictive conception of quantification and proof. He took it as crucial that true proposition of set theory must be "provable" and that the validity of a proof can reasonably be decided. To this end, he developed an infinitary logic but did not carry it very far. In 1935 he was dismissed for failing to salute Hitler and his proposal was not pursued by anyone else until, perhaps, the revival of infinitary languages in the 1950s. [START_REF] Shapiro | Foundations without Foundationalism: A Case for Second-Order Logic[END_REF] Additional limitations of 1 st order theories "[F]rom the 1950s onward, classical mathematics had just one deductive system, namely, first-order Zermelo-Fraenkel Set Theory with [the Axiom of] Choice ..." [START_REF] Hodges | [END_REF]]

"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] 82 A 1 st order theory is very weak. For example, a 1 st order theory is incapable of characterizing even the natural numbers, i.e., there are infinite integers in models of every 1 st order axiomatization of the natural numbers. Furthermore, there are infinitesimal real numbers in models of every 1 st order axiomatization of the real numbers. 83 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 1 st order theory to be useful for their careers because it is weak enough that they can prove theorems about 1 st order axiomatizations whereas they cannot prove such theorems about stronger practical higher order systems, e.g., Classical Direct Logic. 84 Zermelo considered the 1 st Order Thesis to be a mathematical "hoax" because it necessarily allowed unintended models of axioms. 85 [START_REF] Barwise | Model-Theoretic Logics: Background and Aims in "Model Theoretic Logics[END_REF]] critiqued the 1 st Order Thesis that mathematical foundations should be restricted to 1 st order theories 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 first-order thesis is like the claim that astronomy is the study of the telescope. 86

Computer Science is making increasing use of Model Analysis 87 in the sense of analyzing relationships among the following:  concurrent programs and their Actor Model denotations  domain axiom systems and computations on these domains

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. . 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.

Jon Barwise

On the other hand, since it is not limited to 1 st order propositions, Classical Direct Logic characterizes structures such as natural numbers and real numbers up to isomorphism. 88 There are many theorems of Nat that cannot be proved from 1 st order axioms [Goodstein 1944[START_REF] Simpson | Nonprovability of certain combinatorial properties of finite trees in Studies in Logic and the Foundations of Mathematics[END_REF][START_REF] Wiles | Modular elliptic curves and Fermat's Last Theorem[END_REF][START_REF] Bovykin | Brief introduction to unprovability[END_REF][START_REF] Mclarty | What Does it Take to Prove Fermat's Last Theorem? Grothendieck and the Logic of Number Theory Journal of Symbolic Logic[END_REF].

Unbounded Nondeterminism

Of greater practical import, 1 st order theory is not a suitable foundation for the Internet of Things in which specifications require a device respond to a request. 89 The specification that a computer responds can be formalized as follows:

∃[i:N] ResponseBefore[i].
However, the specification cannot be proved in a 1 st order theory. Proof: In order to obtain a contradiction, suppose that it is possible to prove in a 1 st order theory ∃[i:N] ResponseBefore[i]. Therefore the infinite set of propositions {ResponseBefore[i] | i:N} is inconsistent. By the compactness theorem of 1 st order theory, 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:N] ⊢ResponseBefore[i].
However, the above specification axiom does not compute any actual output! Instead the above axiom simply asserts the existence of unbounded outputs for Unbounded∎[ ].

Theorem. The nondeterministic function defined by Unbounded (earlier in this article) cannot be implemented by a nondeterministic Logic Program 90 or a nondeterministic Turing Machine: Proof. 91 The task of a nondeterministic Logic Program P is to start with an initial set of axioms and prove Output=n for some numeral n. Now the set of proofs of P starting from initial axioms will form a tree. The branching points will correspond to the nondeterministic choice points in the program and the choices as to which rules of inference to apply. Since there are always only finitely many alternatives at each choice point, the branching factor of the tree is always finite. 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 proof of P proves Output=n for some numeral n, then there are only finitely many proofs. So if P nondeterministically proves Output=n for every numeral n, it must contain a nonterminating computation in which it does not prove Output=n for some numeral n.

The following arguments support unbounded nondeterminism in the Actor model [Hewitt 1985]:  There is no bound that can be placed on how long it takes a computational circuit called an arbiter to settle. Arbiters are used in computers to deal with the circumstance that computer clocks operate asynchronously with input from outside, e.g., keyboard input, disk access, network input, etc. So it could take an unbounded time for a message sent to a computer to be received and in the meantime the computer could traverse an unbounded number of states.  Electronic mail enables unbounded nondeterminism since mail can be stored on servers indefinitely before being delivered.



Communication links to servers on the Internet can be out of service indefinitely

As a foundation of mathematics for Computer Science, Classical Direct Logic provides categorical axiomatizations 92 of numbers (integer and real), sets, lists, trees, graphs, etc. which can be used in arbitrary mathematical theories including 1 st order theory is not a suitable mathematical foundation for Intelligent Applications for the Internet of Things.

theories for categories, large cardinals, etc. These various theories might have "monsters" of various kinds. However, these monsters should not imported into models of computation used in Computer Science.

Computer Science needs stronger systems than provided by 1 st order theory 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R. 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 1 st 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. 93 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. 94 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.

Theorem. Computational Inadequacy of Nondeterministic Lambda Calculus. The nondeterministic lambda calculus is inadequate to implement all computable procedures.

Proof. Fi[j:N] ≡ j>i if True then InfiniteLoop ∎[ ] False then i either Fi[j+1] For each i:N, Fi is a nondeterministic λ expression but (limiti: N Fi) cannot be implemented as a nondeterministic λ expression. However (limiti: N Fi):Actor

Convergence: ∀[f:([t 1 ]→t 2 ),x:t 1 ] f∎[x]↓ ∃[y:t 2 ] f∎[x]=y Approximation: ∀[f1, f2:([t 1 ]→1t 2 )] f1≦f2 ⇔ ∀[x:t 1 ] f1∎[f3]↓ ⇒ f1∎[x]=f2∎[x] Bottom: ∀[f:t ] (⊥t ∎[f])↓ Note: ∀[f:([t ]→t )] ⊥t ≦f
Monotone:

F:Monotone t 1 , t 2  ⇔ F:Functional t 1 , t 2   ∀[g:([t 1 ]→ t 2 )] g≦F∎[g] Limit Theorem: ∀[F:Monotone t ] F=limit 𝑖:𝐍 + F i ∎[⊥t ] 99
Theorem: Some nondeterministic procedures have unbounded nondeterminism 100 ∃[f: ([t ]→t )] f:Λt  Theorem. 101 Lam t  is categorical with only one model up to a unique isomorphism. Proof: Suppose that X satisfies the axioms for Lam t .

By lambda induction, the isomorphism I:X Λ t is defined as follows: 102

 I[Identityt ] ≡ Identity X t   I[1stt 1 , t 2 ] ≡ 1st X t 1 , t 2   I[2ndt 1 , t 2 ] ≡ 2nd X t 1 , t 2   I[Fixt 1 , t 2 ] ≡ Fix X t 1 , t 2   I[Eithert ] ≡ Either X t   I[[x1, x2]] ≡ [I[x1], I[x2]] X  ∀[x:t 1 , f:([t 1 ]→t 2 )] I[f∎[x]] ≡ I[f]∎ X [I[x]]
I is the unique isomorphism: In order to fill out the ordinals, the following limit axioms are included in Ord:

 I is one to one  The range of I is X  I is a homomorphism  I -1 :Λt  X is
• ∀[α:O, f:O O ] ⊍α f:O • ∀[α,β:O; f:O O ] β<⊍αf ⇔ ∃[δ<α] β≦f[δ] • ∀[α,β:O; f:O O ] (∀[δ<α] f[δ]≦β) ⇨ (⊍αf)≦β
In order to guarantee that there are enough ordinals, the following axioms are also included in Ord :

• Theorem. Theory SetTheoryt  is isomorphic to Sets t  with a unique isomorphism.

Proof: 118 Suppose that X satisfies the axioms for SetTheoryt .

By ordinal induction, the isomorphism I:X Sets t  as follows:

1. S:

Sets 0t  I[S] ≡ S 2. S:Sets α+1t  Z∈ X I[S] ⇔ ∃[Y:Sets αt ] I[Y]∈ X Z 3. S:Sets αt and α:LimitO  Z∈ X I[S] ⇔ ∃[β<α:O, Y:Sets βt ] I[Y]∈ X Z 4. I is a unique isomorphism:  I is one to one  The range of I is X  I is a homomorphism: o I[{ } Sets  t ] = { } X o ∀[S1,S2:Sets t ] I [S1 ∪ S2] = I[S1] ∪ X I [S2]
(⊦ SetTheory  t  ) ⇨ ⊨ Sets  t  Proof: Suppose ⊦ SetTheory  t  .
The theorem immediately follows because the axioms for the theory SetTheoryt  hold in the type Sets t .

 Girard [Girard, J. 1972] There is no type Type thereby blocking the paradox. However, the type of a type is a type, e.g. Type N  is the type of N.  Berry [START_REF] Russell | Les paradoxes de la logique Revue de métaphysique et de morale[END_REF]] can be formalized using the proposition Characterize[s, k] meaning that the string s characterizes the integer k as follows:

Characterize Every nondeterministic computable procedure can be obtained by abstraction from an expression:

≡ λ[s:String Proposition anOrder N , k:N] ∀[x:N] s  [x] ⇔ x=k
∀[f:([t 1 ]→t 2 )] Nondeterministic[f]⇨∃[e:Expression [t 1 ]→t 2 ] f=e
However as explained in this article, there are computations that cannot be implemented in the nondeterministic lambda calculus and therefore require Actors for their implementation. 7 In this sense, Mathematics is "incomplete", but nor in the sense of Gödel's results. See below on the inferential completeness of standard theories of mathematics, such as natural numbers, real numbers, ordinal numbers, set theory, lambda calculus, and Actors. 8 Which is not the same as proving the much stronger proposition that no contradiction can be derived from the exact axioms and inference rules of Direct Logic. 9 Furthermore, theorems of these theories are not enumerable by a provably total procedure.

10 Of course, abstraction means that 1 st order logic is not a suitable foundation.

11 cf. [START_REF] Wigner | The unreasonable effectiveness of mathematics in the natural sciences[END_REF] 12 [START_REF] Nielsen | Alternative Foundations/philosophical February 28[END_REF] 13 parametrized types have become very popular in programming languages, e.g., Java where they are called "generics." 14 Classical results can be embedded in intuitionistic logic as follows:

 ⇔  ∃ can be transformed to ∀  1⋁2 can be transformed to (1⋀2) 15 Some of the outputs are conventionally identified as being the same real number, e.g., .0111111.... and .1000000000 16 For example (p[3])[y] holds if and only if y=3. 17 [Isaacson 2007] 18 A theory is defined by a set of propositions in Direct Logic that are taken to be axioms of the theory. 19 There are no sets in the induction axiom. Quine famously criticized 2 nd order theory as nothing more than "set theory in sheep's clothing" [Quine 1970, pg. 66 Above characterizes Type Nat  up to a unique isomorphism. 21 Proof. Suppose that X is propositions of a theory which satisfies the axioms for propositions of Nat. Inductively define I:X Nat as follows: [x]] where t :Type Nat  and P:Nat t I is a unique isomorphism between Nat and X 22 There are uncountable sentence parse trees because the constants which they contain are uncountable.

In reaction to paradoxes, philosophers developed the dogma of the necessity of strict separation of "object theories" (theories about basic mathematical entities such as numbers) and "meta theories" (theories about theories). 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 Ψ 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.

57 [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF] NotProvablen:N + ≡ λ[p:Proposition n] ⊬p Consequently, there is no fixed point I'mUnprovable for the procedure NotProvablen:N +  such that the following holds: NotProvablen:N + [I'mUnprovable]⇔I'mUnprovable Thus Gödel's I'mUnprovable does not exist in Strongly Typed Mathematics.

In arguing against Wittgenstein's criticism, Gödel maintained that his results on I'mUnprovable followed from properties of N using Gödel numbers for strings that are well-formed. The procedure NotProvable could be attempted for strings as follows: NotProvable ≡ λ[s] ""⊬" s"

With strong types, the attempted definition becomes:

  e.g. (∀[n:ℕ] (∃[m:ℕ] (m>n)))

1 .

 1 Queue (shown as rectangle) hole in which the current activity can be suspended until resumed 2. Call-out (shown as oval) hole for a request made outside the region of mutual

  main interest seemed to lie in discussing the 'truth' or 'falsity' of these [mathematical] 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."According to John von Neumann, Gödel was "the greatest logician since Aristotle." 67 However,[von Neumann 1961] expressed a very different mathematical philosophy than Gödel:

  Theorem: If N is a model of a 1 st order axiomatization T, then T has a model M with an infinite integer. Proof: The model M is constructed as an extension of N by adding a new element ∞ with the following atomic relationships: {∞<∞}  { m<∞ | m:N} It can be shown that M is a model of T with an infinite integer ∞. The infinite integer ∞ is a monster that must be banned from the mathematical foundations of Computer Science. Theorem: If R is a model of a 1 st order axiomatization T, then T has a model M with an infinitesimal. Proof: The model M is constructed as an extension of R by adding a new element ∞ with the following atomic relationships: {∞<∞}  {m<∞ | m

  ∀[α:O] ωα:O • Definition by ordinal induction: 1. ω0 = N 2. ωα+1 = Boolean {:O | < ω α } 3. ω α = ⊍α (λ[β:O] ω) Theorem Ordinals have the following properties:  Ordinals are well-ordered: Least[{ }] = 0 O ∀[S:Boolean O ] S≠{ } ⇨ Least[S]∈S ∀[S:Boolean O ] S≠{ } ⇨ ∀[α∈S] Least[S]≦α  Reals can be well-ordered because ω1=R

o

  ∀[S1,S2:Sets t ] I[S1 ∩ S2] = I[S1] ∩ X I[S2] o ∀[S1,S2:Sets t ] I[S1 -S2] = I[S1] -X I[S2] o ∀[S:Sets t ] I[⋃S] = ⋃X {I[x] | x∈S}  I -1 :Sets t X is a homomorphism  I is the unique isomorphism: If g:X Sets t  is an isomorphism, then g= I Theorem (Model Soundness of SetTheoryt ):



  I[x1=x2] ≡ (x1=x2)  I [] ≡ I[]  I[12] ≡ I[1]  I[2]  I[∀[x:t ] P[x]] ≡ ∀[x:t ] I[P

  NotProvablen:N + [String Proposition n]→1 String Proposition n+1NotProvablen:N +  ≡ λ[s:String Proposition n] ""⊬" s"108 The theory of the ordinals Ord can be axiomatised as follows: 0 O :O  Successor ordinals o ∀[α:O] +1[α]:O  +1[α]>α o ∀[α:O] ∄[β:O] α<β<+1[α]  Replacement for ordinals: o ∀[α:O,f:O O ] ⊍αf:O o ∀[α,β:O,f:O O ] β∈⊍αf ⇔ ∃[δ<α] β≦f[δ] o ∀[α,β:O,f:O O ] (∀[δ<α] f[δ]≦β) ⇨ ⊍αf≦β  Cardinal ordinals ω0 = N ∀[α:O] α>0 O ⇨ ω α≐ Boolean {:O | < ω α } ∀[α,β:O] β≐ωα ⇨ ωα=β  ωα∈β where t1≐t2 ⇔ ∃[f: t2 t1 ] 1to1ontot1, t2[f] 1to1t1, t2[f:t2 t1 ] ⇔ ∀[x1,x2:t 1 ] f[x1]=f[x2] ⇨ x1=x2 1to1ontot1, t2[f:t2 t1 ] ⇔ 1to1t1, t2[f:t2 t1 ]  ∀[y:t2] ∃[x:t1] f[x]=y  Tansitivity of < ∀[α,β<α,δ<β:O] α<δ  ∀[α,β:O] α<β  α=β  β<α  ∀[α,β:O] α<β ⇨ β<α  The following ordinal induction axiom holds: ∀[P:Ord O ] (∀[α:O] ∀[β<α:O] P[β]⇨P[α]) ⇨ ∀[α:O] P[α] 109For each type X that satisfies the theory Ord there is a unique isomorphism with O that is I:X O inductively defined as follows:I[0 O ] ≡ 0 X ∀[α:O] I[+1[α]] ≡ + 1 𝑋 [I[α]]∀[α:LimitO ] I[α] ≡ y where y:X  ∀[β<α] y≦ X I[β]  ∀[z:X] (∀[β<α] z≦ X I[β]) ⇒ y≦ X z

  By Contradiction is one of the most fundamental principles of Classical Mathematics (going back to before Euclid), which can be formalized  axiomatically to say that if  implies  and  then:

	By Contradiction in Nat
	"[By Contradiction is] one of a mathematician's first
	weapons . It is a far finer gambit than any chess
	gambit: a chess player may offer the sacrifice of a pawn
	or even a piece, but a mathematician offers the game."
	G. H. Hardy 26
	Richard Dedekind

Corollary There are no infinite numbers in models of the theory Nat , i.e., ∀[X::] Nat X  ⇨ ∄[j:X] ∀[i:X] j<i

By Contradiction is much more powerful than has been supposed by many philosophers of mathematics. As shown in this article, it is sufficient to prove the formal consistency and the inferential completeness of categorical theories of the natural numbers, reals, ordinals, set theory, the lambda calculus, and Actors. Theorem: 28 Inferential completeness of Nat

	Corollary. Equivalence of satisfiability and provability in Nat, i.e.,
	∀[:Nat ] (⊨ N ) ⇔ (⊢ Nat )
	Theorem. Inferential Decidability of Nat 30 , i.e.,
	∀[:Nat ] (⊢ Nat )  (⊢ Nat )
	Proof. Follows immediately from (⊨ N ) ⇔ (⊢ Nat )
	Theorem. Theorems of the theory Nat are not computationally enumerable
	Proof. Suppose to obtain a contradiction that theorems of Nat are
	computationally enumerable. Then whether a proposition is a
	theory of Nat is computationally decidable by enumerating
	theorems until either the proposition or its negation is
	encountered.
	Theorem (
	Proof.
	Suppose in :Nat and ⊨ N . Further suppose to obtain a
	contradiction that . Hence  and , which is a contradiction.
	Therefore ⊢ Nat  using By Contradiction in Nat. 29

∀[:Nat ] (⊨ N ) ⇒ ⊢ Nat 

Instance Adequacy of Nat ): 31

	∀[P:Nat ] (∀[i:N] ⊢ Nat P[i]) ⇨ ⊢ Nat ∀[i:N] P[i]
	Proof: Suppose ∀[i:N] ⊢ Nat P[i] which means by completeness
	∀[i:N] ⊨ N P[i]. Therefore ⊨ N ∀[i:N] P[i] which means by completeness
	⊢ Nat ∀[i:N] P[i]

Theorem (Nat is not compact) 32 Definition Total:Nat [N]→N where Total

	Uneven Progress
	"All truth passes through three stages. First, it is ridiculed. Second, it is
	violently opposed. Third, it is accepted as being self-evident."
	Arthur Schopenhauer [1818]
	"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."
	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]
	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:
	
	[f] ≡ ∀[i:N] ∃[j:N] f∎[i]=j
	Theorem The theory Nat proves that it is formally consistent: 33
	⊢ Nat Consistent[Nat]
	Proof: Suppose to derive an inconsistency that Consistent[Nat ] . By the
	definition of formal inconsistency for Nat , there is some proposition
	Ψ0:Nat such that ⊢ Nat (Ψ0Ψ0) which can be used to infer in Nat that
	Ψ0Ψ0. The above contradiction completes the proof.

The formal presentation of a demonstration (proof) has not led 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 proves that it is formally 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). 34 

Argumentation and propositions have be variously (re-)connected and both have been re-used. Church

	mathematics that the proofs of mathematics are not computationally
	enumerable). See discussion in this article.
	
	's paradox [Church 1934] is that assuming
	theorems of mathematics are computationally enumerable leads to
	contradiction. In this article, Church's Paradox is transformed into the
	fundamental principle that "Mathematics is Open" (i.e. it is a theorem of

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.35

  Message passing has fundamentally transformed the foundations and practice of computation since the initial conceptions of Turing and Church. Although 1 st Com 39 be the type for a communication, and Behavior 40 be the type for a procedure that maps a communication received to an outcome that has a finite set of created Actors, a finite set of sent communications, and a behavior for the next communication received. The mathematical theory Act categorically axiomatises Actors using the following axioms where ↷ 41 is transitive and irreflexive:  Primitive Actors

		Initial
		State
	Next	Next	Next	Next
	State	State	State	State
	Nondeterministic Choice

the Actor machine always outputs an integer) but every finite subset S of NoOutput is consistent meaning ⊬S (because by finiteness of S, there is an upper bound b:N such that S is a subset of {Output[i] | i<b} but ⊬{Output[i] | i<b} and therefore S is consistent because ⊬S, i.e., the Actor machine output might be larger than b). order sentences can be useful (e.g. in SAT solvers), message passing illustrates why 1 st order logic cannot be the foundation for theories in Computer Science.

Categorical Axiomatization of Actors

Let x[e] be the behavior of Actor x at local event e, o ∀[i:N] i:Actor // natural numbers are Actors o ∀[x1,x2:Actor ] [x1, x2]:Actor // a 2-tuple of Actors is an Actor

  1 st 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. fixed point operator in the categorical theory of the lambda calculus. Michael Beeson suggested a clarification in the argument of Church's Paradox. Hendrik Boom provided an excellent critique, which resulted in a fundamental reorganization. Wilfried Sieg provided information about provability in 1 st order logic. John Woods, John Perry, and two anonymous referees provided excellent comments and suggestions that materially improved this article. Michael Beeson pointed out that I needed to use the terminology "proof checker."

	Appendix 1. Historical Background

  Gödel's alleged Mathematical proposition I'mUnprovable comes from a nonexistent fixed point (sometimes called the Diagonal Lemma) that doesn't exist because of types. 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.

	presented the following analysis:
	Gödel's proof of inferential undecidability [incompleteness] was too
	superficial. It didn't get at the real heart of what was going on. It was more
	tantalizing than anything else. It was not a good reason for something so
	devastating and fundamental. It was too clever by half. It was too superficial.
	[It was based on the clever construction] I'm unprovable. So what? This doesn't
	give any insight how serious the problem is.

Church/Turing correctly proved inferential incompleteness (sometimes called the "First Incompleteness Theorem") without using a nonexistent "self-referential" proposition as follows:

First they proved the computation undecidability of Halt

[p,x]

where Halt[p,x] means that the procedure p halts on input x. By formalizing computation, it follows that Halt[p,x]⇔⊢Halt

[p,x]

. Consequently it is computational undecidable whether a proposition is a theorem.

  By contrast with the nondeterministic lambda calculus and pure Logic Programs, there is an always-halting Actor Unbounded that when sent a start[ ] message can compute an integer of unbounded size. This is accomplished by creating a counter with the following variables: count initially 0  continue initially True and concurrently sending it both a stop[ ] message and a go[ ] message such that:  When a go[ ] message is received: 1. if continue is True, increment count by 1 and return the result of sending this counter a go[ ] message. 2. if continue is False, return Void  When a stop[ ] message is received, return count and set continue to False for the next message received.

  a homomorphism  I is the unique isomorphism: If g:X Λ t  is an isomorphism, then g=ITheorem (Model Soundness ofLam t ): (⊢ Lam  t ) ⇨ ⊨Λ t   Proof: Suppose ⊢ Lam  t .The theorem immediately follows because the axioms for the theory Lam t  hold in the type Λt. Λt ] f=g ⇔ ∀[P:Lam t  Λ t  ] P[f]⇔P[g] Lam t ] (⊨Λ t  ) ⇒ ⊢ Lam  t  Corollary. Equivalence of satisfiability and provability in Lam t  , i.e., ∀[:Lam t ] (⊨Λ t  ) ⇔ ⊢ Lam  t 

	Theorem (Indiscernibility for Lam t ): 103 ∀[f,g:Theorem: Inferential completeness of Lam t  A theory of the ordinals can be axiomatized 108 using a 2 nd order ordinal induction axiom as follows: For each order:N + and P:Ord O , ∀[:Theory of Ordinals (Ord ) (∀[α:O] ∀[β<α:O] P[β]⇨P[α]) ⇨ ∀[α:O] P[α]

  The Berry Paradox is to construct a string BString for the string for the proposition that holds for integer n if and only if every string with length less than 100 does not characterize n using the following definition: 121 Term t 1 , x2:Term t 2 , t 1 ,t 2 :: Expressions, i.e., an Expression t  is a discrimination of the following: o x:Expression t  where x:Constantt  and t :: o x:Expression t  where x:Identifier t  and t :: o (e1⦶e2):Expression t 1 ⦶t 2 , ([e1, e2]):Expression [t 1 , t 2 ], ([e1]→e2):Expression [t 1 ]→t 2 , where e1:Expression t 1 , e2:Expression t 2 , and t 1 ,t 2 :: o (e1 if True then e2 , False then e3):Expression t  148 where e1:Expression Boolean , e2,e3:Expression t  and t :: o (Fixt 1 ,t 2 ∎[F]) 149 where F:Expression Functional t 1 , t 2  and t 1 ,t

	Propositions, i.e., a Proposition is a discrimination of the following: Grammar (syntax) trees (i.e. terms, expressions and sentences) are defined below.
	o (1), 12,12,1⇨2,(1⇔2):t where 1,2:t and t :: Terms, i.e., a Term t  is a discrimination of the following: o (x1=x2):Proposition 1 where x1,x2:t and t :: o (Boolean ):ConstantType Boolean , o (t 1 ⊑t 1 ):Proposition 1 142 where t 1 ,t 2 :: (N):ConstantType N , (O):ConstantType O and o (x:t ):Proposition 1 where t :: (Actor ):ConstantType Actor  o P[x]:Proposition anOrder+1 where x:t, P:Proposition anOrder t o x:Term t  where x:Constantt  and t ::
	o (x1⦶x2):Term x1⦶x2, ([x1, x2]):Term [x1, x2], and anOrder:N + ([x1]→x2):Term [x1]→x2, ([x1]→1 x2):Term [x1]→1 x2 and o P∎[x]:Proposition anOrder+1 where P:[t ]→Proposition anOrder, (x2 x1 ):Term t 2 t1  where x1:
	StringSmallerThan100DoesNotCharacterize:Proposition anOrder+1	N
	StringSmallerThan100DoesNotCharacterize ≡
	λ[n:N] ∀[s:String Proposition anOrder]
	Length[s]<100 ⇨ Characterize[s, n]
	BString:String Proposition anOrder+1 N 
	BString ≡ "StringForStringSmallerThan100DoesNotCharacterize"
	Note that
	o Length[BString]<100.
	Length[s]<100  Characterize[s, i]}
	BSet≠{ } because is {i:N | i≧1} is infinite.
	BNumber:N ≡ Least[BSet]
	BString [BNumber]
	= ∀[s:String Proposition anOrder N ]
	Length[s]<100 ⇨ Characterize[s, BNumber] 122
	However BString:String Proposition anOrder+1 N  cannot be
	substituted for s:String Proposition anOrder N 

o {s:String Proposition anOrder | Length[s]<100} is finite. o Therefore, the following set is finite: BSet:SetN ≡ {i:N + | ∃[s:String Proposition anOrder N ] x:t , t :: and anOrder:N + o (1⊦ T 2):t where T:Theory 143 , 1,2:Proposition anOrder and t ⊑Proposition anOrder and anOrder:N + o (1├ 𝐩 𝑇 2):t where p:ProofCheckerT, T:Theory, 1,2:Proposition anOrder, and t ⊑Proposition anOrder and anOrder:N + o (∀t P) 144 ,(∃t P) 145 :Proposition anOrder+1 where P:Proposition anOrder t , t ⊑Proposition and anOrder:N + o (λt P) 146 :Proposition anOrder+1 where P:Proposition anOrder t , t ⊑Proposition and anOrder:N + o (⊨ ):t where :t, t ⊑Proposition anOrder and anOrder:N + o s T :Proposition anOrder where s:Sentence anOrder with no free variables T:Theory, and anOrder:N + o (x∋P):: where x:Term Type t  , P:Term Proposition t  and t :: o (λt 1 x):Term t 2 t1  where x:Term t 2 t1 , and t 1 ,t 2 :: o (Fixert 1 ,t 2 [F]) 147 where F:Term Mapping t 1 , t 2  and t 1 ,t 2 :: o (f[x]):Term t 2  where f:Term t 2 t1 , x:Term t 1 , t 1 ,t 2 :: o x:t where x:Term t  with no free variables and t :: 2 :: o (e1 either e2):Expression t  where e1,e2:Expression t  and t :: o (t 1 ↦ E):Expression [t 1 ]→t 2  150 where E:[Expression t 1 ]→Expression t 2 , and t 1 ,t 2 :: o (e∎[x]):Expression t 2  where e:Expression [t 1 ]→t 2 , x:Expression t 1 , and t 1 ,t 2 :: o e :t where e:Expression t  with no free identifiers and t ::

  Sentence 1 where e1,e2:Expression t 1 , t 1 :t 2 and t 2 :: o (e1:e2):Sentence 1 where e1:Expression t 1 , e2:Expression t 2  and t 1 ,t 1 :: Expression Theory , s1,s2:Expression Sentence anOrder and t ⊑Proposition anOrder and anOrder:N + o (⊨ s):t where s:t and t :: o s T :Proposition anOrder where s:Sentence anOrder, anOrder:N + , T:Expression Theory , and there are no free variables in s. 154

	Sentences, i.e., a Sentence is a discrimination of the following:
	o (s1),(s1s2),(s1s2),(s1⇨s2),(s1⇔s2):t where s1,s2:t and t ::
	o (e1=e2):Sentence 1 where e1,e2:Expression t  and t ::
	o (e1⊑e2):o (e::):Sentence 1 where e:Expression t  and t ::
	o (∀t P),(∃t P):Expression Sentence anOrder+1 where,
	P:Expression Sentence anOrder	Expression t  ,
	t ⊑Expression Sentence , and t ::
	o (λt P):Expression Sentence anOrder+1 where
	P:Expression Sentence anOrder	Expression t ,
	t ⊑Expression Sentence , and t ::
	o (t ↦P):Expression Sentence anOrder+1 151 where,
	P:Expression Sentence anOrder	Expression t  ,
	anOrder:N +
	o (s1├ 𝑇 𝐩	s2):t where p:Expression ProofChecker T,
	T:

t ⊑Expression Sentence , and t :: o (P[x]):Sentence anOrder+1 152 where x:Expression t , P:Expression Sentence anOrder Expression t  , t :: and anOrder:N + o (P∎[x]):Sentence anOrder+1 153 where x:Expression t , P:[Expression t ]→Expression Sentence anOrder, t :: and anOrder:N + o (s1⊦ T s2):t where T:Expression Theory , s1,s2:t ⊑Sentence and

  ]. ,t 2 :Type Nat ] P[t 1 ]P[t 1 ]⇒P[t 2 t1 ]) // all functions from t 1 into t 2 (∀[t 1 ,t 2 :Type Nat ] P[t 1 ]P[t 2 ]⇒P[t 1 ⦶t 2 ]) // discriminated union of t 1 and t 2 (∀[t :Type Nat  Q:Nat P[t]⇒P[t ∋ | Q]) // restriction of t by Q (∀[t :Type Nat ] P[t]⇒P[Type t ]) // type of t (∀[t 1 ,t 2 :Type Nat ] P[t 1 ]P[t 1 ]⇒P[[t 1 ]→t 2 ])) // computable proceduresfrom t 1 into t 2 ⇒ (∀[t :Type Nat ] P[t ])

	∀[P:Nat	Type Nat  ]
	((∀[t 1 Type Nat 

]

strong parameterized types, it is impossible

  based incompleteness results on the thesis that Mathematics necessarily has the proposition I'mUnprovable using what was later called the "Diagonal Lemma" [Carnap 1934], which is equivalent to the Y untyped fixed point operator on propositions. Using In this way, formal consistency of Mathematics is preserved without giving up power because there do not seem to be any practical uses for I'mUnprovable in Computer Science.A definition of NotProvable could be attempted as follows:

	NotProvable ≡ λ[p] ⊬p

to construct I'mUnprovable because the Y untyped fixed point operator does not exist for strongly typed propositions. With strong types, the attempted definition becomes: NotProvablen:N + [Proposition n]→1 Proposition n+1

Type Nat :: and

Acknowledgements

Tom Costello, Eric Martin, Per Stenstrom, and Johan van Benthem made very helpful comments and suggestions. Interactions with John Woods were very helpful in developing a resolution to Church's Paradox. Conversations with Gordon Plotkin were helpful and his suggestions led to the introduction of the Haskell Curry. "Some Aspects of the Problem of Mathematical Rigor" Bulletin of the American Mathematical Society Vol. 4. 1941. Alonzo Church. The Richard Paradox. Proceedings of American Mathematical Society. Vol. 41. No. 6. 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. Introduction to Mathematical Logic Princeton University Press. 1956. Will Clinger. Foundations of Actor Semantics MIT Mathematics Doctoral Dissertation. June 1981. 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 John Corcoran. Second-order Logic. Logic, Meaning and Computation. Kluwer. 2001. John Dawson. Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer Science FLOC'06. Richard Dedekind (1888) "What are and what should the numbers be?" (Translation in From Kant to Hilbert: A Source Book in the Foundations of Mathematics. Oxford University Press. 1996) Braunschweig. Freeman Dyson. Heretical Thoughts about Science and Society Boston University. November 1, 2005. Heinz-Dieter Ebbinghaus. Ernst Zermelo: An Approach to His Life and Work Springer. 2007. Patrik Eklund, M. Angeles Galan, Robert Helgesson, and Jari Kortelainenc. Fuzzy Terms Fuzzy Sets and Systems. 256. 2014. Erwin Engeler. Algebras and Combinators Algebra Universalis. 1981. Solomon Feferman. "Axioms for determinateness and truth" Review of Symbolic Logic. 2008. Mike Genesereth and Eric Kao. The Herbrand Manifesto Thinking Inside the Box. Rule ML. August 2-5, 2015. Jean-Yves Girard. Interprétation fonctionnelle et Élimination des coupure de l'arithmétique d'ordre supérieur 1972

Theorem: The 1 st order theory Nat1 is inconsistent 77 1. Nat 1 R [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] :Nat 1 Enumerable 2. Nat 1 R [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] :Nat 1 Enumerable

Proof:

Suppose to obtain a contradiction that Nat 1 R [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] :Nat 1 Enumerable

Define the following procedure:

Consequently:

 ⊦ Nat 1 Diagonal:Nat 1 R [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] because Diagonal is the deterministic composition of Nat1 provably total deterministic procedures.

 ⊦ Nat 1 Diagonal:Nat 1 R [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] because Diagonal differs from every Nat 1 R [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] enumerated by Nat1ProvablyComputableR [START_REF]The range of I is all of X: ∀[y:X] ∃[:O] is a homomorphism:  I[END_REF][START_REF]X:Sets 0t  X:Boolean t[END_REF] Enumerator. The above contradiction completes the proof. The following hold:

• ∀[t:N] ⊬ Act ResponseBefore[t] // unbounded response time

• ∀[t1,t2:N] t1<t2⋀ResponseBefore[t1] ⇨ ResponseBefore[t2]

• ⊨ Actor ∃[t:N] ResponseBefore [t] Theorem: There is no 1 st order theory that axiomatises Actor.

Proof: Every 1 st order theory is compact meaning that every inconsistent set of sentences has a finite inconsistent subset.

Lambda Induction for Lam t  is as follows: 98

Theorem. Inferential Decidability of :Lam t , i.e., ∀[P:

Theorem Weakest Preconditions are monotonic in both arguments, i.e., 104

Theory of Reals (Reals )

Reals is strictly more powerful than the 1 st order theory of

RealClosedFields. 105

Theorem (Categoricity of Reals ): 106 If X is a type satisfying the axioms 107 for the real numbers Reals, then there is a unique isomorphism of X with R.

Proof Checkers in

Proof checking in Ord is computationally decidable.

Theorem (Indiscernibility for

Corollary. Equivalence of satisfiability and provability in Ord , i.e.,

Theorem follows from Equivalence of satisfiability and provability in Ord.

Type Choice

Theory SetTheoryt  defined using strong parameterized types

The type Sett  can be characterized as follows:

Of course set membership is defined as follows:

A set theory SetTheoryt  for sets with base type t can be axiomatized using a 2 nd order set induction axiom as follows:

For each P:

Inductive definition:

The properties below mean that Sets t  is a "universe" of mathematical discourse. 111  Foundation: There are no downward infinite membership chains. 155  Excluded Middle Non-contradiction infers excluded middle.

(⋀)⊢⋁

 By Contradiction Contrapositives infer By Contradiction A computable procedure can be partial and can be indeterminate in its outcome.  Type of a type is Type t :: where t :: and Type is a parametrized type with parameter t . Parametrized types have become popular in programming languages where in Java they are called "generics."

Theorem (Formal Consistency

There is no unparameterized type Type in order to block Girard's paradox. 2 Blocking all the known paradoxes is necessary to defeat hackers. 3 Inference rules for Direct Logic are presented in an appendix. 4 [Verbrugge 2010] 5 Axioms and rules of Direct Logic are presented in appendices of this article. 6 Performance of computer information systems is measured in consumption of processing cycles and storage space as well as latency for response. Pervasive inconsistency for information systems means that there are numerous inconsistencies that cannot be readily found and that many of the ones that are found cannot be easily removed. 23 Proof. Induction on propositions of Nat  Inductively suppose that

∀[t :Type Nat , P:Nat t ] ∃[s:Sentence Nat] s = ∀t P 77 24 For example,  cannot be cut from the following proof:

(⊢ Nat ), (⊢ Nat False) ⊢ Nat (⊢ Nat False) ContinuumForNat is defined as follows:

where X⋖Y is defined to mean that there is no 1-to-1

which is a contradiction.

79 33 Note that the results in [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]] do not apply because propositions in Mathematics are strongly typed and consequently the fixed point used construct Gödel's proposition I'mUnprovable does not exist in Mathematics. See the critique of Gödel's results in this article. 34 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 firstorder 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 [of Dedekind, etc.]." 35 for discussion see [Hewitt 2015d] 36 in an unlawful way (Einstein, a member of the editorial board, refused to support Hilbert's action) 37 Hilbert letter to Brouwer, October 1928 38 43 The reception order of an Actor is total. 44 A Com is not received until the previous one has been processed. 45 Behavior of an Actor on first Com received is the same as its initial behavior. 46 Behavior of an Actor after a Com is received is the behavior that results from processing the Com .

47 Information in an Actor while processing a Com is contained in the following:  information in the Actor before the Com is received  information received in the Com  information for Actors created in processing the Com . 48 Information in an Actor after a Com has been processed is contained in information while processing the Com .

49 Information sent by an Actor while processing a received Com is contained in information while processing the Com .

There are only finitely many events in ↷ ordering between two events. 52 An actor behavior always has property P if it initially has the property and whenever it has the property before a Com is received then it has the property afterward. 53 Again, Mathematics here means the common foundation of all classical mathematical theories from Euclid to the mathematics used to prove Fermat's Last [START_REF] Mclarty | What Does it Take to Prove Fermat's Last Theorem? Grothendieck and the Logic of Number Theory Journal of Symbolic Logic[END_REF]]. 54 Note that the results in [START_REF] Löb | Solution of a problem of Leon Henkin[END_REF]] do not apply because propositions in Mathematics are strongly typed and consequently the fixed point used to establish his result does not exist. See discussion of Löb's Paradox in this article. 55 Note that the results in [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]] do not apply because propositions in Mathematics are strongly typed and consequently the fixed point used construct Gödel's proposition I'mUnprovable does not exist in Mathematics. See the critique of Gödel's results in this article. 56 As shown above, there is a simple proof in Classical Direct Logic that Mathematics (├) is formally consistent. If the stated axioms and rules of inference of Classical Direct Logic have a bug, then there might also be a proof that Mathematics is operationally inconsistent. Of course, if a such a bug is found, then it must be repaired. The Classical Direct Logic proof that Mathematics (├) is formally consistent is very robust. One explanation is that formal consistency is built in to the very architecture of 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. The usefulness of Classical Direct Logic depends crucially on the much stronger proposition that Mathematics is operationally consistent, i.e., that there is no proof of contradiction from the stated axioms and inference rules of Direct Logic. Good evidence for the operational consistency of Classical Direct Logic comes from the way that it avoids the known paradoxes. Humans have spent millennia devising paradoxes.

Consequently, there is no fixed point I'mUnprovableString for the procedure NotProvablen:N +  such that the following holds (where s  is the proposition for well-formed string s): NotProvablen:N+[I'mUnprovableString] ⇔ I'mUnprovableString Thus Gödel's I'mUnprovableString does not exist in Strongly Typed Mathematics.

Furthermore, Strong Types thwart the known paradoxes while at the same time facilitating proof of new theorems, as categoricity of the set theory. 58 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." 59 Consequently, there can cannot be any escape hatch into an unformalized "meta-theory." 60 sometimes called logical "incompleteness" 61 The claim also relied on Gödel's proposition I'mUnprovable. 62 Fixed points exist for types other than propositions. 63 emphasis in original 64 [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]] was accepted doctrine by mainstream logicians for over eight decades. 65 Of course, Direct Logic must preserve as much previous learning as possible. 66 According to Solomon Feferman, Gödel was "the most important logician of the 20 th century" and according to John Von Neumann he was "the greatest logician since Aristotle." [Feferman 1986, pg. 1 and 8] 67 [Feferman 1986, pg. 1 and 8] 68 Wittgenstein in 1937published in Wittgenstein 1956, p. 50e and p. 51e] 69 Wittgenstein was granting the supposition that [START_REF] Gödel | On formally undecidable propositions of Principia Mathematica[END_REF]] had proved inferential undecidability (sometimes called "incompleteness") of Russell's system, that is., ⊢ Russell ⊬ Russell P. However, inferential undecidability is easy to prove using the proposition P where P⇔⊬P: Proof. Suppose to obtain a contradiction that ⊢ Russell P. Both of the following can be inferred: 1) ⊢ Russell ⊬ Russell P from the hypothesis because P⇔⊬P 2) ⊢ Russell ⊢ Russell P from the hypothesis by Adequacy. But 1) and 2) are a contradiction. Consequently, ⊢ Russell ⊬ Russell P follows from By Contradiction. 70 [Wittgenstein in 1937 published in Wittgenstein 1956, p. 50e andp. 51e] 83 71 [Wang 1972] The theory 1stOrderDedekindPeano to which Gödel refers is not strictly speaking a subtheory of Nat even though ∀[:1stOrderDedekindPeano ] (⊢ 1stOrderDedekindPeano )⇨⊢ Nat  because 1stOrderDedekindPeano is compact and inferentially undecidable. 72 The Liar Paradox [Eubulides of Miletus] is an example of using untyped propositions to derive an inconsistency. See appendix on paradoxes. 73 According to [Church 1956 page 329]: "completeness [as to inferential provability] is unattainable, as is shown in the incompleteness theorems of Gödel." 74 [Church 1935] correctly proved computational undecidability without using Gödel's I'mUnprovable. The Church theorem and its proof are very robust. 75 The following axioms hold for the primitives

77 This inconsistency is mentioned in [START_REF] Hilbert | λ-calculus and Combinators: An Introduction[END_REF] page 123-125. 78 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! 79 Which is not the same as proving the much stronger proposition that Mathematics is operationally consistent, i.e., that there is no proof of contradiction from the stated axioms and inference rules of Direct Logic.