The historical researches of Louis Couturat saved the logical work of Leibniz from the oblivion of neglect and forgetfulness. They revealed that Leibniz developed in succession several versions of a “logical calculus” (calculus ratiocinator or calculus universalis). In consequence of Couturat's investigations it has become well known that Leibniz's development of these logical calculi adumbrated the notion of a logistic system; and for these foreshadowings of the logistic treatment of formal logic Leibniz is rightly regarded as the father of symbolic logic.

It is clear from what has been said that it is scarcely possible to overestimate the debt which the contemporary student of Leibniz's logic owes to Couturat. This gratitude must, however, be accompanied by the realization that Couturat's own theory of logic is gravely defective. Couturat was persuaded that the extensional point of view in logic is the only one which is correct, an opinion now quite antiquated, and shared by no one. This prejudice of Couturat's marred his exposition of Leibniz's logic. It led him to battle with windmills: he viewed the logic of Leibniz as rife with shortcomings stemming from an intensional approach.

The task of this paper is a re-examination of Leibniz's logic. It will consider without prejudgment how Leibniz conceived of the major formal systems he developed as logical calculi – that is, these systems will be studied with a view to the interpretation or interpretations which Leibniz himself intends for them. The aim is to undo some of the damage which Couturat's preconception has done to the just understanding of Leibniz's logic and to the proper evaluation of his contribution.

Hilbert and Ackermann ([1], p. 107) define a first order axiom system as one in which the axioms contain one or more predicate constants, but no predicate variables. Here “axiom” refers to the specific subject-matter axioms and not to the rules of the restricted predicate calculus (quantification theory), which rules are presupposed for each first-order system. It is pointed out by them that an exception could be made for the predicate of identity; for the axiom scheme for this predicate, namely

which has in (b) the variable predicate F, could nevertheless be replaced, in any given first-order system, by a finite set of axioms without predicate variables. Thus, for example, if Φ[x, y) is the one constant predicate of such a system then PId(b) could be replaced by

Thus one postulates, in addition to the reflexivity, symmetry, and transitivity of identity, the substitutivity of identical entities in each of the possible “atomic” contexts of a variable (occurrences in the primitive predicates). In this method of introducing identity it has to be taken as an additional primitive predicate and further axioms are consequently needed. In such a system having PId(a), (b1)−(b3) as axioms, the scheme PId(b) can be derived as a meta-theorem of the system, F(x) then being any formula of the system.

Let C be an axiom system formalized within the first order functional calculus, and let C′ be related to C as the Bernays-Gödel set theory is related to the Zermelo-Fraenkel set theory. (An exact definition of C′ will be given later.) Ilse Novak [5] and Mostowski [8] have shown that, if C is consistent, then C′ is consistent. (The converse is obvious.) Mostowski has also proved the stronger result that any theorem of C′ which can be formalized in C is a theorem of C.

The proofs of Novak and Mostowski do not provide a direct method for obtaining a contradiction in C from a contradiction in C′. We could, of course, obtain such a contradiction by proving the theorems of C one 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 in C from its proof in C′. 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 of C and C′.

In a previous paper it was shown that the system K of basic logic could be formulated in a simpler way owing to the fact that the proper ancestral could be defined in terms of the other concepts of that system. In the present paper analogous but more far-reaching results will be obtained for the system K′ of extended basic logic. In particular we will show that negation and the dual of the proper ancestral, as well as the proper ancestral itself, are definable in terms of the other concepts of K′. Hence, in order to define K′, we need to add only a single non-finitary rule to the rules used to define K. This rule was already among the rules originally used to define K′. It asserts that ‘Aa’ is in K′ if (and only if) every ‘b’ is such that ‘ab’ is in K′.

We will also show that a large class of non-finitary classes and relations are represented in K′, among which is K′ itself, just as all finitary syntactical classes and all finitary two- and three-place syntactical relations are represented in K, one of which is the finitary syntactical class K itself. The point is that K′ is adequate to handle the sort of transfinite induction that is essential in formulating K′, just as K is adequate to handle the ordinary finitary mathematical induction required in defining K′.

As we know, the system of material implication is led into an inconsistency by the Russellian class, defined as λx. Nϵxx. This class, however, does no harm to many other systems, for example, the three-valued system L3 given by J. Łukasiewicz. A natural question is whether or not there exist classes which affect some of these other logical systems. The main result of the present paper is to answer this question affirmatively. At the end of this paper we point out that the interpretation given by J. Łukasiewicz for the system L3 is not satisfactory, and propose a new interpretation.

B. Russell deduced the mentioned inconsistency by the aid of the notion of negation. Later on, H. B. Curry pointed out that we could get the same result without the aid of that notion. None of these results affects the system L3 and other similar systems. But these systems may be involved.

To show this, we need the following definitions.

A function of two variables Cpq will be called an implication when the following “implication rule” is valid:

Under this definition we should note that material equivalence Epq, for example, is an implication.

Let C be such an implication. Then the symbol “(Cp)iq” is defined recursively by

The class an is defined as λx. (Cϵxx)np, where p is a propositional variable. The rule of absorption of order n, denoted by (An), is:

In Chapter X of The Structure of appearance the concept of linear array is given in terms of a two-place predicate “M” for matching. Also given in terms of “M” is the two-place predicate “B” for besideness. It is unnecessary to discuss here the formal definitions, since Goodman has proved that they are adequate to describe our presystematic ideas of linear array and besideness. Thus, we shall be concerned with a finite collection of elements with an assigned order satisfying:

This order is not uniquely defined by the relation M; either of the two end points may be taken as the ‘first.’ We shall represent the order in diagrams by the convention that x is to the left of y if x < y. For x ≠ y, we shall define S(x, y), the distance between x and y, as one more than the number of elements strictly between them, in the order <; also, S(x, x) = 0. Thus S(x, y) = 1 if and only if x is beside y. The order is connected with the reflexive and symmetric matching relation M by the conditions

(2) Bx, y ⊃ Mx, y,

(3) Mx, y▪x ≤; u ≤ ν ≤ y▪ ⊃ ▪Mu, ν.

Condition (3) is what Goodman calls the weak mapping rule. All arrays considered here must satisfy (3). To avoid trivial cases, we shall assume that not all elements match. There is a strong mapping rule,

(4) Mx, y▪ ∼Mu, ν▪ ▪ ▪S(x, y) < S(u, ν),

which it is desirable, but not necessary, for arrays to satisfy. An array which does satisfy (4) is called regular.

In previous papers, Post, Webb, Götlind and the present author have described some Sheffer functions (in Swift's terminology, “independent binary generators”) in m-valued logic. Professor J. Dean Swift has recently isolated the symmetric Sheffer functions of 3-valued logic. In the present paper, we will prove some properties of Sheffer functions in m-valued logic and isolate all of the Sheffer functions of 3-valued logic.

Before we proceed we will define some terms which we will find convenient. A set of functions in m-valued logic is functionally complete, if the set of the functions which can be defined explicitly from the functions of the set is exactly the set of all functions of m-valued logic. A function is functionally complete, if its unit set is functionally complete. A Sheffer function is a two-place functionally complete function. If i and j are truth values (1 i, j ≤ m), we will say i ~ j (D), if D is a decomposition of the truth values 1, …, m into 2 or more disjoint non-empty classes and i and j are elements of the same class. A binary function f(p, q) satisfies the substitution law for a decomposition D, if for any truth values h, i, j, k, whenever h ~ j (D) and i~k(D), then f(h, i) ~ f(j, k) (D). The function f(p,q) satisfies the co-substitution law for D, if for any truth values h, i, j, k, whenever f(h, i) ~ f(j, k) (D), then h ~ j (D) or i ~ k (D). We will say f(p, q) has the proper substitution property, if there is a decomposition of the truth values into less than m classes for which it satisfies the substitution law.