More on Logic, Computation and Arithmetic

 The following note should be considered an addendum to "Analyticity, Computability and the A Priori".  We presented therein numerous arguments for the circularity, co-implication, co-presupposition, between logic, computation and arithmetic (for simplicity we do not mention combinatorics and graph theory) and made the case that this circle is itself a priori. But there are major themes and perspectives that were not touched upon or given adequate development.

 One question regards the relationship between computability and countability. A computable universe would seem to be an essentially countable one.  But what is interesting in this thesis is the embodiments of countability under consideration and the necessary connection of countability not only with computation but with arithmetic, more specifically, with the induction axiom. The term countability itself suggests a conscious or computational process of going through and enumerating elements starting at the beginning.  We could say that the most general concept of countability is that of a well-ordering, of a countable ordinal (even if in classical set theory the set of all countable ordinals, equated to $\omega_1$, is not itself countable). Now in the standard axiomatizations of $\mathbb{N}$ (let us say PA) we have the remarkable situation that we can codify certain sets of countable ordinals (for instance those less that $\epsilon_0$). The induction axiom-scheme can be generalized to the natural ordinal order and interpreted as a kind of computation over countable ordinals (this is precisely $\epsilon_0$-recursion). Gentzen's remarkable version of the incompleteness of PA expresses that PA does not capture the full strength of ordinal-countability, ordinal-recursion, ordinal-induction, but does so only up to $\epsilon_0$. Thus PA is limited at once in its expression of countability, the recursive nature of its provably total functions and its ordinal-induction - thus showing again the essential circularity and co-determination between arithmetic, computation and the logical expression of ordinal iteration in the induction axiom-scheme (countability).

 Can we interpret Gentzen's incompleteness theorem as expressing that the tree of computational and well-ordering is always larger than the tree of logic and axiomatic arithmetic?  In a countable framework, logical systems adequate for arithmetic (and its associated computation) are always computationally incomplete, their computability is always bounded (cf. also Howard's majorizability result for Gödel's system T).

  We have  considered the human mind as a natural universal Turing machine (one might use Leibniz's expression: a spiritual automaton) expressed in a mutually transparent logical and computational form (the Curry-Howard philosophy).  The above discussion suggests that it is reasonable to characterize the a priori logico-arithmetic-computational structure of the human mind in a way that involves natural bounds and feasibility. There is a notable argument put forward by Edward Nelson in his book Predicative Arithmetic based on the perceived impredicativity and indeed circularity of the induction axiom-scheme: for indeed the formula over which we do induction can involve bounded variables quantified over the whole set of natural numbers, something which can be perceived as circular or contradicting a constructive interpretation of the axiom-scheme. The are also arguments based on the concept of feasibility and the dubious ontological status of numbers or processes which are not possible for humans to calculate or perform - or more generally such that they are not even physically possible.  This led Nelson to develop his theory of feasible arithmetic over Robinson's Q equipped with bounded principle of induction over bounded formulas. Nelson can derive the usual algebraic properties of addition and multiplication restricted to cuts $I(x)$. Nelson mostly considers first-order arithmetic. A serious problem with second-order arithmetic is, besides the problem with induction, that the comprehension axiom guarantees the existence of non-recursive sets - something which does not fit into a computationalist framework.  Thus the restriction (for instance to $\Sigma_1$-formulas) of the class of formulas appearing in induction and restriction of comprehension to formulas of recursive logical form  appears to be a natural move (this is the foundation of the work of Buss and Simpson. Simpson showed that much of ordinary applied analysis can be derived by adding a few more intuitive axioms such as the Weak König Lemma). A result of Buss regarding the computational bounds of this and similar systems  features the Polynomial Time Hierarchy. Buss' work shows a profound connection between alternating bounded quantifiers and computational complexity classes (both a kind of computable projection of their classical hyper-computational counterparts). We have again here a deep co-implication between logic, arithmetic and computation - in an explicitly bounded context, again suggesting the philosophical interest of boundedness.

 We end with the following additional consideration on Nelson's notion of feasibility. Scientific and engineering problems are usually reduced to the framework of basic applied mathematics (analysis).  Models in this frameworks in turn, to be meaningful and useful,  must be transformed into algorithms which are humanly feasible to carry out (or at least computationally feasible on standard hardware).  This suggests a research program in which from results in Simpson's weak analysis we can derive feasible algorithms and eliminate the non-feasible axioms used in the process, according to Leibniz's philosophy of "convenient fictions" (this can also be compared to certain aspects of proof-mining).