We present a method for demonstrating the consistency of von Neuman-Gödel set theory Σ (or Zermelo set theory Σ′) relative to various other formal set theories. When a model for a logic L1 is constructed, there are two other logics involved: L2, the system which contains the model, and L3, the metalogic in which the argument that L2 contains a model for L1 is carried out. These three systems need not of course all be distinct. In [2] L1 is Σ strengthened by the axiom ∨ = L, L2 is Σ, and L3 is unformalized. In the present paper L1 will be either Σ or Σ′. The basic idea for proving the relative consistency of L1 with respect to some other system L2 is to construct in L2 a model for L1 similar to the model constructed in [2]. Since L2 may be some kind of type theory, the function corresponding to Gödel's function F must be modified in a suitable manner. In verifying the relativized versions of axioms of L1 in L2, we shall have to overcome certain special problems depending on the system L2 and not met with in [2]. Except for the remarks at the end of Section 2, we shall not consider the question of formalizing L3, i.e. we use intuitive logic as our metalogic.

In Section 1 we illustrate the method by demonstrating the consistency of Σ relative to the system ML″ obtained by adding E of [4] as an axiom to ML′ of [4]. We use the notation and results of [4] and [7].

Section 2 discusses the use of certain other systems for L2. It will be noted that the systems used for L2 are always slightly strengthened versions of well known systems ([5], [6], and the simple theory of types); it is of course to be hoped that modifications may be discovered which would make the method work in the original, unstrengthened systems, or that the relative consistency of the strengthened systems with respect to the original systems can be established.