We define a first-order theory FIN which has a recursive axiomatization and has the following two properties. Each finite part of FIN has finite models. FIN is strong enough to develop that part of mathematics which is used or has potential applications in natural science. This work can also be regarded as a consistency proof of this hitherto informal part of mathematics. In FIN one can count every set; this permits one to prove some new probabilistic theorems.

This paper provides an explicit description of a model for intuitionistic non-standard arithmetic, which can be formalized in a constructive metatheory without the axiom of choice.

The purpose of this paper is to investigate some problems of using finite (or *finite) computational arguments and of the nonstandard notion of an infinitesimal. We will begin by looking at the canonical example illustrating the distinction between classical and constructive analysis, the Intermediate Value Theorem.