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.

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 recent paper the author has proposed a definition of the commonly used term “effectively calculable” and has shown on the basis of this definition that the general case of the Entscheidungsproblem is unsolvable in any system of symbolic logic which is adequate to a certain portion of arithmetic and is ω-consistent. The purpose of the present note is to outline an extension of this result to the engere Funktionenkalkul of Hilbert and Ackermann.

In the author's cited paper it is pointed out that there can be associated recursively with every well-formed formula a recursive enumeration of the formulas into which it is convertible. This means the existence of a recursively defined function a of two positive integers such that, if y is the Gödel representation of a well-formed formula Y then a(x, y) is the Gödel representation of the xth formula in the enumeration of the formulas into which Y is convertible.

Consider the system L of symbolic logic which arises from the engere Funktionenkalkül by adding to it: as additional undefined symbols, a symbol 1 for the number 1 (regarded as an individual), a symbol = for the propositional function = (equality of individuals), a symbol s for the arithmetic function x+1, a symbol a for the arithmetic function a described in the preceding paragraph, and symbols b1, b2, …, bk for the auxiliary arithmetic functions which are employed in the recursive definition of a; and as additional axioms, the recursion equations for the functions a, b1, b2, …, bk (expressed with free individual variables, the class of individuals being taken as identical with the class of positive integers), and two axioms of equality, x = x, and x = y →[F(x)→F(y)].