LetCbe an axiom system formalized within the first order functional calculus, and letC′ be related toCas the Bernays-Gödel set theory is related to the Zermelo-Fraenkel set theory. Ilse Novak [5] and Mostowski [8] have shown that, ifCis consistent, thenC′ is consistent. Mostowski has also proved the stronger result that any theorem ofC′ which can be formalized inCis a theorem ofC.The proofs of Novak and Mostowski do not provide a direct method for obtaining a contradiction inCfrom a contradiction inC′. We could, (...) of course, obtain such a contradiction by proving the theorems ofCone by one; the above result assures us that we must eventually obtain a contradiction. A similar process is necessary to obtain the proof of a theorem inCfrom its proof inC′. The purpose of this paper is to give a new proof of these theorems which provides a direct method of obtaining the desired contradiction or proof.The advantage of the proof may be stated more specifically by arithmetizing the syntax ofCandC′. (shrink)

Introduction. The system of axioms for set theory to be exhibited in this paper is a modification of the axiom system due to von Neumann. In particular it adopts the principal idea of von Neumann, that the elimination of the undefined notion of a property (“definite Eigenschaft”), which occurs in the original axiom system of Zermelo, can be accomplished in such a way as to make the resulting axiom system elementary, in the sense of being formalizable in the logical calculus (...) of first order, which contains no other bound variables than individual variables and no accessory rule of inference (as, for instance, a scheme of complete induction).The purpose of modifying the von Neumann system is to remain nearer to the structure of the original Zermelo system and to utilize at the same time some of the set-theoretic concepts of the Schröder logic and of Principia mathematica which have become familiar to logicians. As will be seen, a considerable simplification results from this arrangement.The theory is not set up as a pure formalism, but rather in the usual manner of elementary axiom theory, where we have to deal with propositions which are understood to have a meaning, and where the reference to the domain of facts to be axiomatized is suggested by the names for the kinds of individuals and for the fundamental predicates.On the other hand, from the formulation of the axioms and the methods used in making inferences from them, it will be obvious that the theory can be formalized by means of the logical calculus of first order (“Prädikatenkalkul” or “engere Funktionenkalkül”) with the addition of the formalism of equality and the ι-symbol for “descriptions” (in the sense of Whitehead and Russell). (shrink)

1. The theory of classes presented in this paper is a simplification of that presented by J. von Neumann in his paper Die Axiomatisierung der Mengenlehre. However, this paper is written so that it can be read independently of von Neumann's. The principal modifications of his system are the following.(1) The idea of ordered pair is defined in terms of the other primitive concepts of the system. (See Axiom 4.3 below.)(2) A much simpler proof of the well-ordering theorem, based on (...) von Neumann's equivalence axiom (Axiom 2.2 below) is given. (More exactly, the theory of ordinal numbers, on which the proof of the well-ordering theorem is based, is simplified—see §8.)(3) Functions are not assumed to be defined for all arguments. In place of “ = A” we have “is undefined.” This makes possible a constructive interpretation of the system. (See §2.)2. We wish first to give a rough picture of the system which we are trying to construct. Suppose that we have the idea “class,” but no material from which to construct classes. Nevertheless, we can construct the class 0 having no elements. And then the class 1 having 0 as its only element. And then the classes {1}, and {0, 1}, etc., using always the previously constructed classes as elements. To extend this method to infinite classes, we must give rules telling what elements are to be included. Since the nature of the rules which we can use is not altogether clear, we try to formalize the whole system; that is, to set up a system of axioms which seems to characterize this system of classes. Now in this set of axioms we find it necessary to use the idea of function (in the “Axiom of Replacement”). (shrink)

The reader of Part VI will have noticed that among the set-theoretic models considered there some models were missing which were announced in Part II for certain proofs of independence. These models will be supplied now.Mainly two models have to be constructed: one with the property that there exists a set which is its own only element, and another in which the axioms I–III and VII, but not Va, are satisfied. In either case we need not satisfy the axiom of (...) infinity. Thereby it becomes possible to set up the models on the basis of only I–III, and either VII or Va, a basis from which number theory can be obtained as we saw in Part II.On both these bases the Π0-system of Part VI, which satisfies the axioms I–V and VII, but not VI, can be constructed, as we stated there. An isomorphic model can also be obtained on that basis, by first setting up number theory as in Part II, and then proceeding as Ackermann did.Let us recall the main points of this procedure.For the sake of clarity in the discussion of this and the subsequent models, it will be necessary to distinguish precisely between the concepts which are relative to the basic set-theoretic system, and those which are relative to the model to be defined. (shrink)