Comparison of subtheories

Let ZF denote the Zermelo-Fraenkel set theory and ZFI the theory obtained from it by the addition of an axiom which asserts the existence of at least one inaccessible number. If ZF is consistent then ZFI contains number-theoretic theorems which are not theorems of ZF, e.g. the arithmetical sentence which asserts the consistency of ZF-Con(ZF). Mostowski [4] introduced a sentence of the theory of real numbers which can be proved in ZFI but cannot be proved in ZF. Let S1 and S2 be two theories such that the relation of Si to S2 is like that of ZFI to ZF. The present paper will show to what extent the subtheories of S1 contain more theorems than the corresponding subtheories of S2. We shall use the terminology of Tarski-Mostowski-Robinson [8].2 A set of symbols of the first order predicate calculus with the usual formation rules for terms and formulae, as laid out in [8, pp. 6-7], will be called a standard formal language. Each theory with standard formalization is formalized in a standard formal language. If R is a standard formal language and P an unary predicate (P need not be a symbol of R) we construct a new formal language R(P) by the relativization of quantifiers in R to P (see [8, p. 24]). If A is a sentence of R we denote by A (P) the sentence obtained from A by relativizing the quantifiers in it to P. Let Q be a theory with standard formalization. We define the notion of an interpretation of R in Q as in [8, pp. 20-21, 29]. This interpretation is obtained by a new theory with standard formalization Q(R) which is formalized in the language which consists of the symbols of both Q and R(P). The valid sentences of Q(R) are exactly those which are derivable from the set which consists of the valid sentences of Q and possible definitions of the nonlogical constants of R(P) in Q. Given a particular interpretation of R in Q we can define in the language R a theory with standard formalization Q/R (which may be called the theory induced by Q in R) by the following stipulation: A sentence A of R is valid in Q/R