Locally finite theories

Abstract

We say that a first order theory T is locally finite if every finite part of T has a finite model. It is the purpose of this paper to construct in a uniform way for any consistent theory T a locally finite theory FIN( T ) which is syntactically (in a sense) isomorphic to T . Our construction draws upon the main idea of Paris and Harrington [6] (I have been influenced by some unpublished notes of Silver [7] on this subject) and generalizes the syntactic aspect of their result from arithmetic to arbitrary theories. (Our proof is syntactic, and it is simpler than the proofs of [5], [6] and [7]. This reminds me of the simple syntactic proofs of several variants of the Craig-Lyndon interpolation theorem, which seem more natural than the semantic proofs.) The first mathematically strong locally finite theory, called FIN, was defined in [1] (see also [2]). Now we get much stronger ones, e.g. FIN(ZF). From a physicalistic point of view the theorems of ZF and their FIN(ZF)-counterparts may have the same meaning. Therefore FIN(ZF) is a solution of Hilbert's second problem. It eliminates ideal (infinite) objects from the proofs of properties of concrete (finite) objects. In [4] we will demonstrate that one can develop a direct finitistic intuition that FIN(ZF) 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].