A set S of natural numbers is called recursively enumerable if there is a general recursive function F(x, y) such that

In other words, S is the projection of a two-dimensional general recursive set. Actually, it is no restriction on S to assume that F(x, y) is primitive recursive. If S is not empty, it is the range of the primitive recursive function

where a is a fixed element of S. Using pairing functions, we see that any non-empty recursively enumerable set is also the range of a primitive recursive function of one variable.

We use throughout the logical symbols ⋀ (and), ⋁ (or), → (if…then…), ↔ (if and only if), ∧ (for every), and ∨(there exists); negation does not occur explicitly. The variables range over the natural numbers, except as otherwise noted.

Martin Davis has shown that every recursively enumerable set S of natural numbers can be represented in the form

where P(y, b, w, x1 …, xλ) is a polynomial with integer coefficients. (Notice that this would not be correct if we replaced ≤ by <, since the right side of the equivalence would always be satisfied by b = 0.) Conversely, every set S represented by a formula of the above form is recursively enumerable. A basic unsolved problem is whether S can be defined using only existential quantifiers.

Since 1934 various different techniques for natural deduction have been developed by Gentzen, Jaśkowski, Rosser, Quine, and others (see [1], pp. 147–167; [2], especially footnotes 1, 3, and 4; and [3], pp. 75-83, 96-107, and 289-294). It has been pointed out to me by Professor Donald Kalish of U.C.L.A. that the restrictions placed upon Universal Generalization (UG) and Existential Instantiation (EI) in [3] force one to construct a less natural proof than seems desirable for such arguments as

(cf. [3], p. 139, and [1], pp. 175f.) It is my purpose in this note to formulate an alternative restriction on UG which will permit a more natural proof for such arguments, and to prove the consistency of the altered rule.

In the notation of [3], “The expression ‘Φμ’ will denote any propositional function in which there is at least one free occurrence of the variable denoted by ‘μ’. The expression ‘Φν’ will denote the result of replacing all free occurrences of μ in Φμ by ν, with the added proviso that when ν is a variable it must occur free in Φν at all places at which μ occurs free in Φμ.” ([3], p. 100.) The statement of EI is relatively unrestricted; being

provided that ν is a variable which occurs free in no earlier step.” ([3], p. 104.)

In [1] Myhill gave a system K in which much of the classical theory of rational and real numbers could be carried out but which was nevertheless complete; this was achieved by sacrificing the notions of negation and universal quantification and introducing instead the ancestral as a primitive idea. He mentioned two ways of dealing with real numbers in K; the first was to use the half-section corresponding to x, i.e. the class of rationals r satisfying r ≤, x; the second was to use the whole-section corresponding to x, i.e. the relation between rationals r, s which holds when r ≤ x and x ≤ s. In [2] he proved various theorems about the relation between these two forms of definition. In particular he proved that every bounded class of half-sections definable in K has a least bound definable in K. In a footnote he said, ‘This theorem risks triviality because it is doubtful whether there exists such a bounded class.’ We show in this note that this is the case; in fact there are not even any definable classes consisting entirely of classes of rationals. It is not difficult to see how this happens; since K has no negation, any statement matrix A (α) defining a class of classes of sequences is satisfied by α = V, where V is the class of all sequences. Thus there are no classes which consist entirely of half-sections. The same is true for whole-sections, showing that Conjecture I of [1], viz. ‘Not every bounded class of whole-sections definable in K has a least bound definable in K’, is trivially false. Since it may be of some intrinsic interest, we give below a more complete description of the classes of classes of sequences which are definable in K (or rather in K1 see below) than is necessary merely in order to prove the above assertion.

It has been shown by Quine that an interpreted theory Θ, formulated in the notation of quantification theory, is translatable into a theory Θ′ in which the only primitive predicate is a dyadic F. In establishing this result Quine takes for the universe of Θ′ a set which comprehends the universe of Θ and has the property that if x and y are members then so is {x, y}. For this fragmentary set theory the distinctness of x from {x, y} and {{x}} is assumed. It will be shown here that, if a pair of somewhat more stringent restrictions are assumed for the set theory, then there is a symmetric dyadic predicate G definable within Θ′, i.e., in terms of F alone, in terms of which F is in turn definable. It follows from this extended result that the theory Θ is translatable into a theory in which the only primitive predicate is symmetric and dyadic.

For some of the well-known set-theoretic operations a natural definition of transfinite iterations (powers) seems impossible. If, however, an operator D has the property that, for every X, D(X) ⊃ X, we may write the formula Dn(X) = D(Dn−1(X)) (which defines as usual the finite powers of D) in the form . Assuming this formula to be valid when n is any ordinal, we obtain a natural definition of transfinite powers of those operators. Obviously the dual definition would work in the case D(X) ⊂ X.

As an example of the use of this definition, we show how the sets used by von Neumann to represent ordinals can be constructed by means of the operator N(X) = X⋃{X}. Denoting the union of the elements of X by S(X), we have for the set E(ξ), which represents the ordinal ξ, E(ξ) = S(Nξ({ϕ})), as can easily be verified by transfinite induction. As the sets E(ξ) are different for different values of ξ, the powers of N are all different as well.

This is not always the case. The powers of certain operators start repeating themselves from a certain ordinal onward. If an operator has the property that, for every set A of sets a, , then the sequence of its powers becomes constant already from ω on. This is a special case of the following theorem.

The logic of quantification is conveniently developed in terms of the so-called quantificational schemata. The atomic quantificational schemata consist each of a schematic predicate letter (‘F’, ‘G’, etc.) attached to one or more quantifiable variables (‘x’, ‘y’, etc.). Compound quantificational schemata are built up of these atomic ones by means of truth functions and quantifiers. The business of the logic of quantification then becomes that of spotting the valid schemata: the ones that are true under all interpretations.

The logic of quantification is well understood and well behaved. Proof procedures in this domain are known, thanks to Gödel, to be complete. If decision procedures are not known for the whole of this part of logic, still we do know, thanks to Church, that they cannot exist. And we know how to streamline our proof procedure for quick success in the average case where proof is possible. Because of all this, there is a premium on adapting special theories, of special subject matters, to this general mold. This means representing the truths of the special theory as a class of quantificational schemata with interpreted predicate letters and a chosen universe of discourse. Once a theory has been thus regimented, it is a standard theory (in approximately Tarski's sense of the term).

In the first of her papers on functional calculi based on strict implication, Ruth Barcan Marcus takes as her starting point the Lewis systems S2 and S4, supplemented by one of the normal bases for quantification theory, and by one special axiom for the mixture, asserting that if possibly something φ's then something possibly φ's. In the symbolism of Łukasiewicz, which will be used here, this axiom is expressible as CMΣxφxΣxMφx. In the present note I propose to show that if S5 had been taken as a startingpoint rather than S2 or S4, this formula need not have been laid down as an axiom but could have been deduced as a theorem.

It has been shown by Gödel that a system equivalent to S5 may be obtained if we add to any complete basis for the classical propositional calculus a pair of symbols for ‘Necessarily’ and ‘Possibly,’ which here will be ‘L’ and ‘M’; the axioms

the rule

RL: If α is a thesis, so is Lα;

and the definition

Df. M: M = NLN.

In the present paper we investigate in some detail two systems closely related to those contained in [4]. The system K1 of [4] is simplified by eliminating conjunction and disjunction, giving rise to a system Σ whose primitives are two individuals, concatenation, identity, existential and limited universal quantification. Any relation expressible in Σ may be expressed in the form (Eα1)(β)α1(Eα2)…(Eαn)(γ = δ). A further reduction of primitives leads to a system Σμ, which differs from Σ by containing the operator μ (i.e. “the first string, such that” with respect to a certain ordering) in place of the quantifiers. Reasons are given for restricting Myhill's definition of constructive ideas to those expressible in Σμ.

Acquaintance with [4], [5], [6] is assumed. We deviate from [4] by dropping concatenation-signs and parentheses in chain matrices from the official notation, and, furthermore, by using Greek and German letters as metalinguistic variables standing for chain matrices and chains, respectively, while retaining small Roman letters (excluding a, b) for use as variables of the systems.

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.

1. Gödel's theorem that sufficiently strong formal systems cannot prove their own consistency and Tarski's method for constructing truth-definitions can be combined to give several independence results in axiomatic set theory. In substance, the following theorems can be obtained: (a) The existence of inaccessible ordinals is not provable from the axioms of set theory, if these axioms are consistent, (b) The axiom of infinity is independent of the other axioms, if these other axioms are consistent, (c) The axiom of replacement is independent of the other axioms, if these other axioms are consistent. In all cases, V = L will be included as an axiom.

The result (a) concerning inaccessible ordinals already has been proved in Shepherdson [10] and Mostowski [6], but their proofs are somewhat different from the one given here. According to Mostowski [6], Kuratowski essentially had a proof of (a) in 1924. Propositions (b) and (c) have been proved, for axiomatic set theory without the axiom V = L, by Bernays [1] pp. 65–69. The method of proof used in this paper is due to Firestone and Rosser [2].

An outline of a similar proof along these lines is given in Rosser [7] pp. 60–62.

As our system G of set theory, we choose Gödel's system A, B, C, as given in [4], except for the following changes.