In a previous number of this Journal, Dr. Arnold F. Emch argues that the mathematical properties of the system of strict implication preclude the interpretation of p⊰q as synonymous with “q is deducible from p” and of ◊(pq), or p o q, as “p and q are consistent.” He proposes a new calculus of propositions in which the primitive ideas of the system of strict implication are retained but an additional idea, “logical consistency,” Op, is introduced, and two new relations, “logical implication,” p∾q, and “logical equivalence,” p = q, are denned. He believes that the properties of this new system are in accord with the facts about deducibility, consistency, and independence of propositions where those of p⊰q and ◊(pq) fail of such accord.

Not all of the objections which Dr. Emch advances against strict implication are given due consideration in what follows. Concerning one especially important point, something will be said at the end of this paper. For the rest, discussion will here be limited to certain formal properties of the two systems, and certain consequences for the interpretation of them.

For brevity, the system of strict implication will be referred to, in what follows, as the “system S,” or merely as S; and Dr. Emch's calculus as the “system L,” or as L.

1. Introduction. In his set theory Zermelo uses the variables “x”, “y”, etc. for the representation of “things” generally. Among these things he includes sets, or, as I shall say henceforth, classes. He adopts the connective “ϵ” of membership as his sole special primitive; thus the elementary formulae of his system are describable simply as expressions of the form “xϵy”, with any thing-variables ”x”, “y”, “z”, etc. supplanting “x” and “y”. The postulates of his system are so fashioned as to avoid the logical paradoxes without use of the theory of types. One of the postulates, the so-called Aussonderungsaxiom, may be stated in familiar logical notation as

where is understood as any statement about y which is definite in a certain sense which Zermelo introduces informally for the purpose. Skolem has pointed out that it is adequate here to construe “definite” statements as embracing just the elementary formulae and all formulae thence constructible by the truth functions and by quantification with respect to thing-variables. A second of Zermelo's postulates is the principle of extensionality; this asserts that mutually inclusive classes are identical, i.e. are members of just the same classes. There are further postulates which provide for the existence of the null class, the class of all subclasses of any given class, the class of all members of members of any given class, the unit class of any given thing, and the class whose sole members are any two given things. Finally the multiplicative axiom (Auswahlprinzip) and the axiom of infinity are adopted.

We shall say that a logic is “simply consistent” if there is no formula A such that both A and ∼ A are provable. “ω-consistent” will be used in the sense of Gödel. “General recursive” and “primitive recursive” will be used in the sense of Kleene, so that what Gödel calls “rekursiv” will be called “primitive recursive.” By an “Entscheidungsverfahren” will be meant a general recursive function ϕ(n) such that, if n is the Gödel number of a provable formula, ϕ(n) = 0 and, if n is not the Gödel number of a provable formula, ϕ(n) = 1. In specifying that ϕ must be general recursive we are following Church in identifying “general recursiveness” and “effective calculability.”

First, a modification is made in Gödel's proofs of his theorems, Satz VI (Gödel, p. 187—this is the theorem which states that ω-consistency implies the existence of undecidable propositions) and Satz XI (Gödel, p. 196—this is the theorem which states that simple consistency implies that the formula which states simple consistency is not provable). The modifications of the proofs make these theorems hold for a much more general class of logics. Then, by sacrificing some generality, it is proved that simple consistency implies the existence of undecidable propositions (a strengthening of Gödel's Satz VI and Kleene's Theorem XIII) and that simple consistency implies the non-existence of an Entscheidungsverfahren (a strengthening of the result in the last paragraph of Church).

By concepts will be meant propositions (or truth-values), attributes (or classes), and relations of all degrees. The degree of a concept will be said to be 0, 1, or n (> 1), and the concept will be said to be medadic, monadic, or n-adic, according as the concept is a proposition, an attribute, or an n-adic relation. The common procedure in systematizing logistic is to treat these successive degrees as ultimately separate categories. The partition is not rested upon properties of the thus classified elements within the formal system, but is imposed rather at the metamathematical level, through stipulations as to what combinations of signs are to be accorded or denied meaning. Each function of the formal system is restricted, thus metamathematically, to one degree for its values and to one for each of its arguments. The theory of types imports a further scheme of infinite partition, imposed by metamathematical stipulations as to the relative types of admissible arguments of the several functions and stipulations as to the types of the values of the functions relative to the types of the arguments.

The elaborateness of the metamathematical grillwork which thus underlies formal logistic accounts in part for the tendency of those interested in logistic less for the matters treated than for the structures exemplified to limit their attention to the propositional calculus and the Boolean calculus of attributes (or classes), which, taken separately, are independent of the partitioning. A second reason for the algebraic appeal of these departments is their freedom from bound (apparent) variables: for use of bound variables fuses systematic considerations with notational or metamathematical ones in a way which resists ordinary formulation in terms of fixed functions and their arguments. Freedom from bound variables may be regarded, indeed, as the feature distinguishing algebra from analysis.

The system of formal logic to be presented in this paper has the following main properties:

(1). The Mengenlehre paradoxes do not arise in it.

(2). It seems to be free from other contradictions.

(3). It does not resort to a theory of types.

(4). It uses negation and material implication and does not weaken the principle of excluded middle.

(5). It contains no analogue to the Curry W operator; consequently, given a propositional function ϕ, a propositional function Ψ cannot always be found such that, for all x, ϕ(x, x) and Ψ(x) are equivalent propositions.

(6). It employs a universal quantifier, G, such that (x)f(x), (x)f(x, x), (x)f(x, x, x), …, would be respectively expressed thus, G(f, f), G(f, f, f), G(f, f, f, f), ….

(7). It employs Schönfinkel's functional notation, so that f(x1, x2, …, xn) will be written as (( … ((fx1)x2) …)xn) and abbreviated to (fx1x2… xn) and, when no ambiguity results, to fx1x2…xn.

(8). A theory of integers and real numbers cannot, apparently, be deduced from it.

(9). A form of the axiom of choice is provable in it.

Lewis, in the presentation of his calculus of strict implication, contends that this calculus accords with the usual meaning of “implies” such that “p strictly implies q” is synonymous with “q is deducible from p” (pp. 126–127, 235–262). It is the purpose of this paper to present, in 1, certain considerations in the light of which this statement does not hold, and in 2, a new implicative relation upon which a calculus of propositions can be based such that it will accord with the relation of deducibility and from which it is possible to derive the calculi of strict and material implications.

1. Strict implication regarded as synonymous with deducibility. In the presentation of his calculus of strict implication Lewis observes that despite inclusion of both intensional and extensional propositions in this calculus, the meaning of its elements, p, q, r, etc., “remain fixed, whether it is their extensional or their intensional relations which are in question” (p. 120). But if the meaning or content of the elements of this calculus is irrelevant to the logical truth which it contains, then, as Weiss has already remarked, the propositions of this calculus “are really extensionally treated, involving multiple values,” e.g., possibility, on the analogy of truth and falsity. The importance of this fact is that, in consequence, the relation of strict implication is subject to certain paradoxes, such as (19.74) “a proposition which is impossible strictly implies any proposition” or (19.75) “a proposition which is necessarily true is strictly implied by any proposition” (p. 174) or (19.84) “any two necessarily true propositions are strictly equivalent” (p. 176).

Problems of construction have engaged the attention of mathematicians from the earliest times. The three famous unsolved problems of the Greeks were problems of construction. Apparently the attitude of the Greeks toward these problems was that, if a geometric entity exists, it must be constructible. For example they believed that given an arbitrary angle, there is another one equal to a third of the first. Hence there must be a way of constructing the second angle, that is, a way of trisecting the first angle. This attitude is very similar in formulation but vastly different in content from the attitude of the modern intuitionists, who say that a mathematical entity does not exist unless it is constructible. Had Brouwer been a Greek, he would probably have declared that, given an angle, it is non-sense to speak of another angle equal to a third of it until such a second angle has been constructed.

However, it seems scarcely necessary to remind the reader that, for the Greeks, constructibility meant a special kind of constructibility, namely, constructibility by ruler and compass. Other methods of constructing geometric entities are known, and by use of them, the problems of the Greeks can be solved. More than that, it is now known that ruler and compass constructions alone do not suffice to solve any one of the three famous problems of the Greeks. Therefore, we see that the Greeks erred in restricting themselves to ruler and compass constructions, even though they may have felt justified in making these restrictions, due to considerations of mathematical elegance, or to ignorance of other methods.

In A note on the Entscheidungsproblem the author gave a proof of the unsolvability of the general case of the Entscheidungsproblem of the engere Funktionenkalkül. This proof, however, contains an error, in order to correct which it is necessary to modify the “additional axioms” of the system L so that they contain no free variables (either free individual variables or free propositional function variables).

The additional axioms of L other than x=y→[F(x)→F(y)] contain no free propositional function variables, and hence it is sufficient to replace each one by an expression obtained from it by quantifying all the individual variables by means of universal quantifiers initially placed—thus, in particular, x = x is replaced by (x)[x=x]. Moreover the axiom x=y→[F(x)→F(y)] may be replaced by the following set of axioms:

and similar axioms for each of the functions b1, b2, …, bk.