Comparability of classes. Till now we tried to get along without the axioms Vc and Vd. We found that this is possible in number theory and analysis as well as in general set theory, even keeping in the main to the usual way of procedure.

For the considerations of the present section application of the axioms Vc, Vd is essential. Our axiomatic basis here consists of the axioms I—III, V*, Vc, and Vd. From V*, as we know, Va and Vb are derivable. We here take axiom V* in order to separate the arguments requiring the axiom of choice from the others. Instead of the two axioms V* and Vc, as was observed in Part II, V** may be taken as well.

In this paper we shall prove theorems about some systems of sentential calculus, by making use of results we have established elsewhere regarding closure algebras and Brouwerian albegras. We shall be concerned mostly with the Lewis system and the Heyting system. Some of the results here are new (in particular, Theorems 2.4, 3.1, 3.9, 3.10, 4.5, and 4.6); others have been stated without proof in the literature (in particular, Theorems 2.1, 2.2, 4.4, 5.2, and 5.3).

The proofs to be given here will be found to be mostly very simple; generally speaking, they amount to drawing conclusions from the theorems established in McKinsey and Tarski [10] and [11]. We have thought it might be worth while, however, to publish these rather elementary consequences of our previous work—so as to make them readily available to those whose main interest lies in sentential calculus rather than in topology or algebra.

Quine remarked that the system of his book exclusive of *200 is a completely safe basal logic. Axioms of this basal logic are given by *100-*105 and *201-*202 in the book. For relation theory and number theory, we need some further axioms to guarantee elementhood of certain entities. In the article, Quine proposed to adopt as axioms f610 and the following two statements:

The purpose of this paper is to show that some of the difficulties confronting logicians are caused by too narrow an interpretation of the function of mathematical logic. I hope to show that very fruitful results can be obtained by considering a much wider range of problems than usually found in the literature.

I believe that the function of mathematical logic is to study all logical systems. The problems now considered usually concern some particular system or set of systems. Of course we would have to agree first on what a logical system is. I shall suggest a tentative definition. The rest of my paper will proceed on the assumption that we have agreed on this question. However, it is only necessary for this paper that some definition should be accepted, it is not necessary that it should be the one I suasest.

A calculus, or its formalization, is m-valued when its truth-functions are allowed to take truth-values ranging from 1 through m. It is customary to divide the m truth-values that are possible into those that are “designated” and those that are “undesignated.” Furthermore, it is usually desired of a formalization that provable formulas and only provable formulas take designated truth-values exclusively. For our present purposes, we shall suppose that the truth-values 1, …, 8 are designated and the truth-values 8+1, …, m are undesignated. When calculi differ in respect to the number of their designated truth-values, we shall consider them different calculi, even if they are otherwise similar.

Russell's theory of types, though probably not providing the soundest possible foundation for mathematics, follows closely the outlook of most mathematicians. The present paper is an attempt to present the theory of types in forms in which the types themselves only play a rather small part, as they do in ordinary mathematical argument. Two logical systems are described (called the “nested-type” and “concealed-type” systems). It is hoped that the ideas involved in these systems may help mathematicians to observe type theory in proofs as well as in doctrine. It will not be necessary to adopt a formal logical notation to do so.

It has been shown by Lewis and Langford that the postulate B8,

is not deducible in SI. From this it follows that neither are the paradoxes of strict implication deducible in that system. However, the following weaker—but perhaps philosophically equally important—analogues are deducible:

The purpose of this note is to contribute to the discussion of nonextensional languages that is now in progress. A formal language, L, that contains, besides the lower functional calculus, predicates and predicate variables of higher type will here be called nonextensional if the sentence

In his very interesting address On the calculus of refations, Professor Tarski discussed alternative bases for that calculus. He was there interested in “…different methods of setting up the foundations of this elementary calculus in a rigorously deductive way…” and so did not discuss the method of developing the calculus of relations with which this paper is concerned. Our purpose here is to show how the use of matrix notation for relations permits an algorithmic rather than a postulational-deductive development of the calculus of relations. One limitation of the present approach is to be admitted at the very outset: to enjoy the full benefits of the matrix approach, we are obliged to confine our investigations to Universes of Discourse which are finite. The reason for this restriction will become apparent presently.

A logical calculus Κ was defined in a previous paper and then shown in a subsequent paper to contain within itself a representation of every constructively definable subclass of expressions of a certain infinite class U of expressions, where Κ itself is one such subclass. (The former paper will be referred to as BL and the latter paper as RC.) The calculus Κ was called a “basic calculus” and its theorems were thought of as expressing the asserted propositions of a “basic logic,” that is, of a logic within which is definable every constructively definable system of logic and indeed every constructively definable class or relation. The notion of constructive definability was essentially equated with the notion of recursive enumerability.

There are logicians who maintain that modal logic violates Leibniz's principle that if x and y are identical, then y has every property of x. The alleged difficulty is illustrated in the following example due to Quine.1

A. It is logically necessary that 9 is less than 10.

B. 9 = the number of the planets.

C. Therefore, it is logically necessary that the number of the planets is less than 10.

We are inclined to believe that, by means of an argument entirely analogous to that which leads to the Richard antinomy, the notion of definability as applied to entities discussed in a formal system can easily be shown not to be itself definable in this system. It will be seen from this discussion that actually the situation is not quite so simple as it would appear at first glance. Our discussion will have a rather sketchy and informal character.

It has been proved by S. C. Kleene and David Nelson that the formula

is intuitionistically non-deducible, i.e., non-deducible within the intuitionistic functional calculus.

The aim of this note is to outline a general method which permits us to establish the intuitionistic non-deducibility of many formulas and in particular of the formula (1).

The two following papers are in need of certain corrections: Modal functions in two-valued logic and Note on modal functions. I became aware of the need for these corrections while comparing these earlier papers of mine with J. C. C. McKinsey's paper, On the syntactical construction of systems of modal logic.

The first of the two papers should be corrected in such a way that the system of two-valued logic there employed becomes “complete” in the sense that either p or ∼ p is in Τ for every Κ-symbol Τ. This could be achieved by use of an additional axiom that postulates the required completeness. (I mistakenly supposed that the original set of axioms guaranteed this completeness.)