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.

is a fragment of first-order aritlimetic so weak that it cannot prove the totality of an iterated exponential fimction. Surprisingly, however, the theory is remarkably robust. I will discuss formal results that show that many theorems of number theory and combinatorics are derivable in elementary arithmetic, and try to place these results in a broader philosophical context.

Stephen George Simpson. with definition 1.2.3 and the discussion following it. For example, taking 90(n) to be the formula n §E Y, we have an instance of comprehension, VYEIXVn(n€X<—>n¢Y), asserting that for any given set Y there exists a ...

Elementary Recursive Nonstandard Analysis, in short ERNA, is a constructive system of nonstandard analysis proposed around 1995 by Patrick Suppes and Richard Sommer, who also proved its consistency inside PRA. It is based on an earlier system developed by Rolando Chuaqui and Patrick Suppes, of which Michal Rössler and Emil Jeřábek have recently proposed a weakened version. We add a Π₁-transfer principle to ERNA and prove the consistency of the extended theory inside PRA. In this extension of ERNA a σ₁-supremum (...) principle 'up-to-infinitesimals', and some well-known calculus results for sequences are deduced. Finally, we prove that transfer is 'too strong' for finitism by reconsidering Rössler and Jeřábek's conclusions. (shrink)

We introduce a nonstandard arithmetic $NQA^-$ based on the theory developed by R. Chuaqui and P. Suppes in [2] (we will denote it by $NQA^+$ ), with a weakened external open minimization schema. A finitary consistency proof for $NQA^-$ formalizable in PRA is presented. We also show interesting facts about the strength of the theories $NQA^-$ and $NQA^+$ ; $NQA^-$ is mutually interpretable with $I\Delta_0 + EXP$ , and on the other hand, $NQA^+$ interprets the theories IΣ1 and $WKL_0$.

In treatises or advanced textbooks on theoretical physics, it is apparent that the way mathematics is used is very different from what is to be found in books of mathematics. There is, for example, no close connection between books on analysis, on the one hand, and any classical textbook in quantum mechanics, for example, Schiff, [11], or quite recent books, for example Ryder, [10], on quantum field theory. The differences run a good deal deeper than the fact that the books (...) on theoretical physics are not written in the definition-theorem-proof style characteristic of pure mathematics. Although a good many propositions are proved in the books on physics, there are almost with exception no existential proofs, and consequently there is no really serious systematic use of quantifiers. Another important characteristic is the free use of infinitesimals. In fact, most results would not lose anything, from a physicist's point of view, by leaving them in approximate form, i.e., instead of strict equalities or inequalities, using equalities or inequalities only up to an infinitesimal.The discrepancy between the way mathematics is ordinarily done in theoretical physics and the way it is built up from a foundational standpoint in any of the standard modern views raises the question of whether it might be possible to construct quite directly a rigorous foundation that reflects a significant part of this standard practice in theoretical physics. Other parts of standard practice in physics, for example, the use of physically intuitive but nonrigorous arguments, are not present in our system. (shrink)

Many arguments found in the physics literature involve concepts that are not well-defined by the usual standards of mathematics. I argue that physicists are entitled to employ such concepts without rigorously defining them so long as they restrict the sorts of mathematical arguments in which these concepts are involved. Restrictions of this sort allow the physicist to ignore calculations involving these concepts that might lead to contradictory results. I argue that such restrictions need not be ad hoc, but can sometimes (...) be justified by considering some of the metaphysical issues surrounding the question of the applicability of mathematics to physical reality. 1 Introduction 2 Rejecting inferential permissiveness 3 The agreement problem 4 Independent objections to the liberal view. (shrink)

Elementary Recursive Nonstandard Analysis, in short ERNA, is a constructive system of nonstandard analysis with a PRA consistency proof, proposed around 1995 by Patrick Suppes and Richard Sommer. It is built on a previous system by Rolando Chuaqui and Patrick Suppes, which was recently reconsidered by Michal Rössler and Emil Jeřábek. A $\Pi _1 $ -transfer principle has already been added to ERNA and the consistency of the resulting theory proved in PRA. Here, we equip ERNA with Σ₂-transfer and a (...) saturation principle, while keeping the consistency proof inside PRA. We show that the extended theory allows for generalized transfer, a basic tool of nonstandard analysis, and interprets several strong theories, like BΣ₂ and IΣ₂. (shrink)