We consider first-order logic only. A theory S will be called locally interpretable in a theory T if every theorem of S is interpretable in T. If S is locally interpretable in T and T is consistent then S is consistent. Most known relative consistency proofs can be viewed as local interpretations. The classic examples are the cartesian interpretation of the elementary theorems of Euclidean n-dimensional geometry into the first-order theory of real closed fields, the interpretation of the arithmetic of integers (rational numbers) into the arithmetic of positive integers, the interpretation of ZF + (V = L) into ZF, the interpretation of analysis into ZFC, relative consistency proofs by forcing, etc. Those interpretations are global. Under fairly general conditions local interpretability implies global interpretability; see Remarks (7), (8), and (9) below.We define the type (interpretability type) of a theory S to be the class of all theories T such that S is locally interpretable in T and vice versa. There happen to be such types and they are partially ordered by the relation of local interpretability. This partial ordering is of lattice type and has the following form:The lattice is distributive and complete and satisfies the infinite distributivity law of Brouwerian lattices:We do not know if the dual lawis true. We will show that the lattice is algebraic and that its compact elements form a sublattice and are precisely the types of finitely axiomatizable theories, and several other facts.
