We say that a first order theoryTislocally finiteif every finite part ofThas a finite model. It is the purpose of this paper to construct in a uniform way for any consistent theoryTa locally finite theory FIN which is syntactically isomorphic toT.Our construction draws upon the main idea of Paris and Harrington [6] and generalizes the syntactic aspect of their result from arithmetic to arbitrary theories. The first mathematically strong locally finite theory, called FIN, was defined in [1]. Now we get (...) much stronger ones, e.g. FIN.From a physicalistic point of view the theorems of ZF and their FIN-counterparts may have the same meaning. Therefore FIN is a solution of Hilbert's second problem. It eliminates ideal objects from the proofs of properties of concrete objects.In [4] we will demonstrate that one can develop a direct finitistic intuition that FIN is locally finite. We will also prove a variant of Gödel's second incompleteness theorem for the theory FIN and for all its primitively recursively axiomatizable consistent extensions.The results of this paper were announced in [3]. (shrink)

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.

On June 4, 1925, Hilbert delivered an address to the Westphalian Mathematical Society in Miinster; that was, as a quick calculation will convince you, almost exactly sixty years ago. The address was published in 1926 under the title Über dasUnendlicheand is perhaps Hilbert's most comprehensive presentation of his ideas concerning the finitist justification of classical mathematics and the role his proof theory was to play in it. But what has become of the ambitious program for securing all of mathematics, once (...) and for all? What of proof theory, the very subject Hilbert invented to carry out his program? The Hilbertian ambition reached out too far: in its original form, the program was refuted by Gödel's Incompleteness Theorems. And even allowing more than finitist means in metamathematics, the Hilbertian expectations for proof theory have not been realized: a constructive consistency proof for second-order arithmetic is still out of reach. Nevertheless, remarkable progress has been made. Two separate, but complementary directions of research have led to surprising insights: classical analysis can be formally developed in conservative extensions of elementary number theory; relative consistency proofs can be given by constructive means for impredicative parts of second order arithmetic. The mathematical and metamathematical developments have been accompanied by sustained philosophical reflections on the foundations of mathematics. This indicates briefly the main themes of the contributions to the symposium; in my introductory remarks I want to give a very schematic perspective, that is partly historical and partly systematic. (shrink)