Recent discussion serves to bring out, amply and convincingly, the utility of observing the ordinary correct use of words and phrases for the purpose of clearing up philosophical problems. In this paper, I shall endeavour to show, by means of an example, that the reverse method may have its interest, too. An attempt will be made to cultivate a minor deviation from the accepted ways of using certain words and phrases in idiomatic English as well as in the formalized “languages” of the logicians. The words and phrases in question are those for the formalization of which a logician employs (free or bound) variables. Cases in point are the words customarily called quantifiers. The deviation I have in mind affects the relation of these words to the notion of identity. The deviation is illustrated by the following sentences:

(1a) Any two points of a straight line completely determine that line;

(2a) He is John's brother if he has the same parents as John;

(3a) Mazzini did more for the emancipation of his country than any living man of his time.

These examples may be contrasted with the following closely related sentences:

(1b) Any two distinct points of a straight line completely determine that line;

(2b) He is John's brother if he has the same parents as John and if he is not John himself;

(3b) Mazzini did more for the emancipation of his country than any other living man of his time.

1. This paper grew out of an attempt to answer a question raised in [4]. Let a logic L containing “numerals” z1, z2, … and a certain statement N(x) (intended to express the proposition that x is a natural number) be called ω-inconsistent if there is a statement such that ⊦ F(zk) for k = 1, 2, …, and ⊦ ∼(x)·N(x) ⊃ F(x); then it is evident that L cannot have a model in which N(x) is satisfied by the images of the numerals and nothing else if L is ω-inconsistent.

Question: If L is ω-consistent, i.e. not ω-inconsistent, must there be such a model? Calling a model of the kind just described a special model, we ask for necessary and sufficient conditions on L to insure the existence of a special model. We give several sets of such conditions, applicable to a certain very inclusive class of logics, in Theorem 1 and Theorems 3 and 4. Theorem 2 shows that a logic may be ω-consistent but still not have a special model.

This paper was close to completion when [3] appeared. For systems with only denumerably many symbols our results include Henkin's, for, by adjoining a new predicate N(x) to each of the systems considered in [3] which have only a denumerable number of constant symbols and then adding as an axiom (x)N(x), these systems become special cases of the systems we consider. It is easily seen that Henkin's Theorem 7 essentially proves the equivalence of conditions (2) and (3) in our Theorem 1, and Theorem 3 of [3] corresponds to our Theorem 2. Incidentally, our argument of Theorem 2 could also serve to prove Henkin's Theorem 6.

The following are some consequences of a recent result concerning the prime implicants of disjunctive normal formulas.

I. Introduce the void fundamental formula λ, and define the consensus of αϕ and as in [5], but allowing ϕ or ψ or both to be λ. Then a normal formula Φ is valid if and only if the operations of dropping subsuming clauses and adjoining consensus formulas end by transforming Φ into the single formula λ. (For under the notions of fundamental formula and consensus as now extended, λ is a (unique) prime implicant of all valid formulas and of no others; and the argument of [5] now shows that the operations mentioned transform every normal formula, whether valid or not, into the disjunction of its prime implicants.)

II. A normal formula ψ implies a normal formula Φ if and only if every clause of ψ subsumes one of the prime implicants of Φ, which are found as in I above. (The condition is clearly sufficient. It is necessary, for if ψ implies Φ, then every clause of ψ implies Φ and subsumes a shortest fundamental formula implying Φ.) In this condition, the prime implicants of Φ may be replaced by the clauses of the result of merely adjoining, as long as possible, consensus formulas to Φ.

Leo Simons has shown that H1—H6 below constitute a set of independent axiom schemata for S3, with detachment for material implication “→” as the only primitive rule. He also showed that addition of the scheme (◇ ◇ α ⥽ ◇ α) yields S4, and that these schemata for S4 are independent. The question for S5 was left open. We shall show (presupposing familiarity with Simons' paper) that H1—H6 and S, below, constitute a set of independent axiom schemata for S5, with detachment for material implication as the only primitive rule.

Let S5′ be the system generated from H1—H6 and S with the help of the primitive rule. It is easy to see that Simons' derivations of the rules (a) adjunction, (b) detachment for strict implication, and (c) intersubstitutability of strict equivalents, may be carried out for S5′. We know that (1) (∼ ◇ ∼ α ⥽ ◇ α) is provable in S2, hence also in S3 and S5′; and (1) and S yield (2) (α ⥽ ∼ ◇ ∼ ◇ α). Perry has shown that addition of (2) to S3 yields S5, so S5 is a subsystem of S5′. And it is easy to prove S in S5; hence the systems are equivalent.

According to McKinsey and Tarski [3], who introduced the notion, a closure algebra Γ = (K, ∪, ∩, –, C) is a Boolean algebra (K, ∪, ∩, –) with an additional unary operator C, closed in K, such that, for every x, y ϵ K, x ⊆ Cx, CCx = Cx, C(x∪y) = Cx∪Cy, CΛ = Λ. McKinsey [2] has proved that a matrix Γ = (K, D, ∪, ∩, –, C) is a representation (normal matrix) of S4, if and only if (1) (K, ∪, ∩, –, C) is a closure algebra, (2) D is an additive ideal of K, (3) if – Cx ϵ D then x = Λ, D being the distinguished proper subset of K and ∪, ∩, –, C having been made to correspond to ∨, ·, ∼, ◊, respectively. Following McKinsey, one proves immediately

Theorem 1. A matrix Γ is a representation of S5, if and only if it is a closure algebra and

(α) for every x ϵ K, –C–Cx = Cx, and

(β) D is an additive ideal of K such that, for every x ϵ D, Cx = V.

This raises the question of alternative characterizations of S5. Because of (β), one may without substantial loss of generality put D = {V}. The question then becomes one for conditions that are in closure algebras equivalent to (α). One such characterization has been given by McKinsey and Tarski [4]. Defining x∸y = C(x∩–y) and ¬x = V∸x, these authors have shown that the closed elements K* of a closure algebra Γ form a Brouwerian algebra Γ* = (K*, ∪, ∩, ∸), and furthermore that Γ* is a Boolean algebra under ∪, ∩, ¬, if and only if, for every x ϵ K*,

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.

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).

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.

The two results of this paper (a theorem and an example) are applications of a device described in section 1. Our notation is that of [4], with which we assume familiarity. It may be worth while to mention in particular the function Φ(n, x) which recursively enumerates the partial recursive functions of one variable, the Cantor enumerating functions J(x, y), K(x), L(x), and the classes F and Q of r.e. (recursively enumerable) and finite sets respectively.

It is possible to “give” a finite set in a way which conveys the maximum amount of information; this may be called “giving explicitly”, and it requires that in addition to an effective enumeration or decision procedure for the set we give its cardinal number. It is sometimes desired to enumerate effectively an infinite class of finite sets, each given explicitly (e.g., [4] p. 360, or Dekker [1] p. 497), and we suggest here a device for doing this.

We set up an effective one-to-one correspondence between the finite sets of non-negative integers and these integers themselves: the integer , corresponds to the set αi, = {a1, a2, …, an} and inversely. α0 is the empty set. Clearly i can be effectively computed from the elements of αi and its cardinal number.