Online research in philosophy

In a short, technical note, the system of arithmetic, F, introduced in Systems for a Foundation of Arithmetic and "True" Arithmetic Can Prove Its Own Consistency and Proving Quadratic Reciprocity, is demonstrated to be equivalent to a sub-theory of Peano Arithmetic; the sub-theory is missing, most notably, the Successor Axiom.

Kirby and Paris have exhibited combinatorial algorithms whose computations always terminate, but for which termination is not provable in elementary arithmetic. However, termination of these computations can be proved by adding an axiom first introduced by Goodstein in 1944. Our purpose is to investigate this axiom of Goodstein, and some of its variants, and to show that these are potentially adequate to prove termination of computations of a wide class of algorithms. We prove that many variations of Goodstein's axiom are equivalent, over elementary arithmetic, and contrast these results with those recently obtained for Kruskal's theorem.

Using a slight generalization, due to Palmgren, of sheaf semantics, we present a term-model construction that assigns a model to any first-order intuitionistic theory. A modification of this construction then assigns a nonstandard model to any theory of arithmetic, enabling us to reproduce conservation results of Moerdijk and Palmgren for nonstandard Heyting arithmetic. Internalizing the construction allows us to strengthen these results with additional transfer rules; we then show that even trivial transfer axioms or minor strengthenings of these rules destroy conservativity over HA. The analysis also shows that nonstandard HA has neither the disjunction property nor the explicit definability property. Finally, careful attention to the complexity of our definitions allows us to show that a certain weak fragment of intuitionistic nonstandard arithmetic is conservative over primitive recursive arithmetic.

Let $\mathscr{L} = \{0, 1, +, \cdot, <\}$ be the usual first-order language of arithmetic. We show that Peano arithmetic is the least first-order L-theory containing IΔ0 + exp such that every complete extension T of it has a countable model K satisfying. (i) K has no proper elementary substructures, and (ii) whenever $L \prec K$ is a countable elementary extension there is $\bar{L} \prec L$ and $\bar{K} \subseteq_\mathrm{e} \bar{L}$ such that $K \prec_{\mathrm{cf}}\bar{K}$ . Other model-theoretic conditions similar to (i) and (ii) are also discussed and shown to characterize Peano arithmetic.

We give a consistency proof within a weak fragment of arithmetic of elementary algebra and geometry. For this purpose, we use EFA (exponential function arithmetic), and various first order theories of algebraically closed fields and real closed fields.

A realizability notion that employs only Kalmar elementary functions is defined, and, relative to it, the soundness of EA-(10-IR), a fragment of Heyting Arithmetic (HA) with names and axioms for all elementary functions and induction rule restricted to 10 formulae, is proved. As a corollary, it is proved that the provably recursive functions of EA-(10-IR) are precisely the elementary functions. Elementary realizability is proposed as a model of strict arithmetic constructivism, which allows only those constructive procedures for which the amount of computational resources required can be bounded in advance.

The system called F is essentially a sub-theory of Frege Arithmetic without the ad infinitum assumption that there is always a next number. In a series of papers (Systems for a Foundation of Arithmetic, True” Arithmetic Can Prove Its Own Consistency and Proving Quadratic Reciprocity) it was shown that F proves a large number of basic arithmetic truths, such as the Euclidean Algorithm, Unique Prime Factorization (i.e. the Fundamental Law of Arithmetic), and Quadratic Reciprocity, indeed a sizable amount of arithmetic. In particular, F proves some (but not all) of the Peano Axioms; that is, F proves the axioms of a sub-theory - call it FPA - of second-order Peano-Arithmetic. This short technical note will demonstrate that the converse also holds, in the following sense. F has the same language as second-order Peano Arithmetic except that, in addition, it has a two-place predicate symbol “Μ”. Then it is possible to provide a definition, indeed a reasonable definition, for “Μ” such that FPA proves all the axioms of F. So F and FPA effectively have the same proof-theoretic strength. In particular FPA, which lacks the Successor Axiom stating that every natural number has a successor, is able to prove the Euclidean Algorithm, Unique Prime Factorization, and Quadratic Reciprocity, indeed (again) a sizable amount of arithmetic.

This paper develops the very basic notions of analysis in a weak second-order theory of arithmetic BTFA whose provably total functions are the polynomial time computable functions. We formalize within BTFA the real number system and the notion of a continuous real function of a real variable. The theory BTFA is able to prove the intermediate value theorem, wherefore it follows that the system of real numbers is a real closed ordered field. In the last section of the paper, we show how to interpret the theory BTFA in Robinson's theory of arithmetic Q. This fact entails that the elementary theory of the real closed ordered fields is interpretable in Q.

A general method of interpreting weak higher-type theories of nonstandard arithmetic in their standard counterparts is presented. In particular, this provides natural nonstandard conservative extensions of primitive recursive arithmetic, elementary recursive arithmetic, and polynomial-time computable arithmetic. A means of formalizing basic real analysis in such theories is sketched.