A theory of natural numbers will be outlined in what follows. This theory will also be extended to give an account of positive and negative integers and positive and negative rational numbers. The system of logic used will be that of Whitehead and Russell's Principia mathematica with the simple theory of types. It will be assumed that the reader is familiar with the more elementary properties of relations and with such notions as the relative product of two relations, the square of a relation, the cube of a relation, and the various other whole-number powers of relations.

The guiding principle of this theory is that the natural number zero is to be regarded as the relation of the zevoth power of a relation А to А itself, and the natural number 1 is to be regarded as the relation of the first power of a relation А to А itself, and the natural number 2 is to be regarded as the relation of the square of a relation А to А itself, and so on.

Nach allgemeiner Ueberzeugung können gewisse Sätze der Analysis nicht konstruktiv bewiesen werden. Man denke etwa an den folgenden Satz: Eine monotone und beschränkte Folge a(n) von rationalen Zahlen konvergiert, d.h. es gibt eine solche ganzzahlige Funktion k(m), daß

Unter einem konstruktiven Beweis dieses Satzes hätte man etwa die Angabe eines Verfahrens zu verstehen, das gestattet, die Funktion k(m) auf Grand der Folge a(n) rekursiv zu definieren. Wenn ein solcher Beweis vorläge, wäre insbesondere gezeigt, daß es zu einer rekursiv definierten Folge a(n) mit den verlangten Eigenschaften stets eine rekursiv definierbare Konvergenzfunktion k(m) gibt.

Es soil nun im folgenden von einigen grundlegenden Sätzen der reellen Analysis gezeigt werden, daß sie nicht konstruktiv bewiesen werden können—konstruktiv in dem Sinn, der eben angedeutet wurde. Wir stützen uns dabei auf die Begriffe der rekursiven und der berechenbaren Funktion; rekursive und berechenbare Funktionen sind zahlentheoretische Funktionen. Unter einer rekursiven Funktion möge vorläufig eine primitiv rekursive Funktion verstanden werden (vgl. etwa D. Hilbert und P. Bernays [3], S.286); berechenbar meint berechenbar im Sinne von A. Church [1], S. C. Kleene [4], A. M. Turing [6]. Der Begriff der “konstruktiv definierten Funktion” wird durch die Bestimmung als “rekursive Funktion” eher eng, durch die Bestimmung als “berechenbare Funktion” eher weit gefaßt.

Definition I. Eine Folge rationaler Zahlen Φ(n) heißt rekursiv,(berechenbar), wenn es solche rekursiven (berechenbaren) Funktionen ϕ{n), ψ(n) und χ(n) gibt, daß χ(n) ≧1 und

.

Definition II. Eine Folge Φ(n) von rationalen Zahlen heißt rekursiv (berechenbar) konvergent, wenn es eine solche rekursive (berechenbare) Funktion v(m) gibt, daß

Wir werden zeigen (Satz I): Es gibt eine rekursive, monotone und beschränkte Folge rationaler Zahlen, die nicht berechenbar konvergiert. Bei unserer Auffassungsweise ist darin enthalten, daß der zu Beginn erwähnte Satz nicht konstruktiv bewiesen werden kann.

I am very grateful to the Association for Symbolic Logic for inviting me to give this address—an honor which I am conscious of having done very little to deserve. My efforts during the last fifteen years (seconded by those of a number of younger collaborators, whose devoted help has meant more to me than I can adequately express) have been directed wholly towards a unified exposition of all the basic branches of mathematics, resting on as solid foundations as I could hope to provide. I have been working on this as a practical mathematician; in matters pertaining to pure logic, I must confess to being self-taught, and laboring under all the handicaps that this implies; and if, after no little self-questioning, I am speaking here today, I am doing so chiefly in order to enjoy the benefit of your professional advice and criticism, by which I hope to correct my views before I venture into print with them.

1.1. In two previous papers a consistent theory of real numbers has been outlined by the author, using a system K′. This latter system is an extension of a system K, which is “basic” in the sense that every finitary (recursively enumerable) subclass of its well-formed expressions is in a certain sense represented in it. The system L described below is a further extension of K. The system K′ lacks two important features possessed by L: a symbol for a special kind of implication (or “conditionality”) and a symbol for the modal concept “necessity.” The presence of the implication symbol, and the additional assumptions that go with it, make available in L various kinds of restricted universal quantification not available in K′, for example, universal quantification restricted to the real numbers of the author's theory of real numbers.

1.2. If ‘~[a & ~a]’ is a theorem of L, then the proposition expressed by ‘a’ may be said to L-satisfy the principle of excluded middle. I t is always the case that ‘a’ L-satisfies the principle of excluded middle (or rather that the proposition expressed by ‘a’ does so) if and only if ‘a’ or ‘~a’ is a theorem of L. An example of a proposition that does not L-satisfy the principle of excluded middle is that expressed by ‘’, namely the proposition that asserts that the class of classes that are not members of themselves is a member of itself.

A demonstrably consistent theory of real numbers has been outlined by the writer in An extension of basic logic1 (hereafter referred to as EBL). This theory deals with non-negative real numbers, but it could be easily modified to deal with negative real numbers also. It was shown that the theory was adequate for proving a form of the fundamental theorem on least upper bounds and greatest lower bounds. More precisely, the following results were obtained in the terminology of EBL: If С is a class of U-reals and is completely represented in Κ′ and if some U-real is an upper bound of С, then there is a U-real which is a least upper bound of С. If D is a class of (U-reals and is completely represented in Κ′, then there is a U-real which is a greatest lower bound of D.

In this note we present a simplification of the axiom schemes which were given in our earlier paper Axiom schemes for m-valued propositional calculi. Except for new concepts that are needed for our present purposes, the terminology used will be the same as that introduced in the earlier paper. Hence, we can say that in addition to listing our simplified specifications for axiom schemes, we shall indicate how our new axiom schemes may be used to establish deductive completeness.

The simplification of our axiom schemes is achieved by using only the operators ⊃ and Jk( ) with the resulting elimination of ∨ and ·. This does not constitute an actual reduction in functional complexity since the latter operators can be denned in terms of the former. For example,

However, by dispensing with ∨ and · one can greatly reduce the number of axioms without an appreciable increase in the difficulties of proving deductive completeness.

Our simplified specifications for axiom schemes will retain conditions (1) and (3) of our earlier set but (2) and (4) will be changed to (2*) and (4*) which we will now state.

(2*) Assume that an implication function (P ⊃ Q) can be defined exclusively in terms of the basic functions Fi(P1, …:, Pαi).

The statement of what follows is simplified by introducing a chain symbol defined recursively as follows:

The variable i of a chain symbol which takes values from u to v will be called the chain variable. When it is clear that i is the chain variable we will use the notation in place of . Hence, denotes (P5 ⊃ (P4 ⊃ (P3 ⊃ Q))).

In this paper we give the complete list of the functions of one variable with some of their properties, and lists of functions corresponding to various properties of sum, product, implication, and equivalence. The range of the variables as well as that of functional values will be о (false), ½, 1 (true). As an application we consider Frege's, Russell's and Heyting's systems in ternary logic. The proofs are mostly omitted as obvious if sometimes laborious.

Functions will be denned by matrices: e.g. F(p, q)

Although several proofs have been published showing the completeness of the propositional calculus (cf. Quine (1)), for the first-order functional calculus only the original completeness proof of Gödel (2) and a variant due to Hilbert and Bernays have appeared. Aside from novelty and the fact that it requires less formal development of the system from the axioms, the new method of proof which is the subject of this paper possesses two advantages. In the first place an important property of formal systems which is associated with completeness can now be generalized to systems containing a non-denumerable infinity of primitive symbols. While this is not of especial interest when formal systems are considered as logics—i.e., as means for analyzing the structure of languages—it leads to interesting applications in the field of abstract algebra. In the second place the proof suggests a new approach to the problem of completeness for functional calculi of higher order. Both of these matters will be taken up in future papers.

The system with which we shall deal here will contain as primitive symbols

and certain sets of symbols as follows:

(i) propositional symbols (some of which may be classed as variables, others as constants), and among which the symbol “f” above is to be included as a constant;

(ii) for each number n = 1, 2, … a set of functional symbols of degree n (which again may be separated into variables and constants); and

(iii) individual symbols among which variables must be distinguished from constants. The set of variables must be infinite.

The present note introduces a constructible interpretation for the logical connectives of number theory which is divergent from that of the intuitionists. Under the intuitionistic interpretation, the principle of excluded middle and certain other classically acceptable principles of logic must be rejected. Under the present interpretation, while some classical principles may be reinstated, other principles, acceptable both classically and intuitionistically, may be shown to be invalid. Among these is the principle of contradiction.

We make certain notational conventions. These are referred to as CL (Computational Logic). The relation of interchangeability is introduced as the basic connection between logical formulas. This approach lends perspicuity to the results of sentential calculus. With its technical devices CL is able to rephrase logical theorems in rather succinct manner. Our exposition tries to steer a middle course between informality and strict rigor.

It is felt that the method of CL offers advantages for the teaching of logic. Proofs are algorithmic and resemble those of elementary algebra. All inferences are reversible and practically non-tentative.

Sign is a primitive term of CL. Its denning property is a capacity for entering into binary combination with other signs, or with itself, according to this convention:

x and y are signs if, and only if, (x y) is a sign. Bracketing is looked upon as an operation on signs in terms of which other operations are definable. The practice of some authors in classifying brackets under the heading of symbols, seems to us questionable; for unlike symbols or signs brackets are never used to denote anything. Brackets enter into the composition of signs, not to denote a grouping, but rather to exhibit it, in the manner of a diagram.

An unending list of letters, with or without subscripts,

serve to denote arbitrary signs. An arbitrary sign may or may not have other signs as parts. The numeral “2” is used as a constant. Bracketing abbreviation is as follows:

and so on. Outermost brackets will ordinarily be omitted. This kind of bracketing may be termed left-associative. For convenience, these bracketing conventions are crystallized into a rule.

In this note two independent comments are offered concerning nominalistic syntax.

If one has a nominalistic theory of natural numbers (or positive integers) at one's disposal, one can of course readily formulate a nominalistic syntax by the familiar method of arithmetization. A nominalistic theory of natural numbers is formulated in a previous paper by the author, and thus a basis for a nominalistic syntax is already provided. (The objection that this theory is infinitistic would appear without force, because it provides the only known nominalistic basis for the theory of general recursive functions. On a finitistic basis one merely throws out this vital domain of mathematical theory.)

The second comment is concerned with nominalistic syntax as formulated by Goodman and Quine. The nominalistic construction of natural numbers alluded to above owes much of its power to a primitive device of ancestral quantification. This device is somewhat more powerful than the notions Goodman and Quine allow themselves. Now nominalistic syntax in their somewhat narrower sense can be formulated by utilizing a relation akin to the relation L of the theory of ordered individuals developed elsewhere by the author. ‘L’ here is to designate the relation between inscriptions of being wholly to the left of.

The Goodman-Quine primitive ‘C’, designating a relation of concatenation, and their primitive ‘Part’ with its field confined to inscriptions, can be defined in terms of ‘L’. Thus:

.

(This definition is essentially that of ‘P’ in O.I.)

In a paper J. Łukasiewicz and A. Tarski study the systems arising out of the implication function C (x, y) = min(1, 1 – x + y) and the negation function Nx = 1 – x, where x, y are real numbers between 0 and 1 inclusive. Let us then writeСxy = min(1, 1 – x + y) and Nx = 1 – x. (1)

In this note we shall consider another implication function, namelyС′xy = ССNxyy, (2)

This note should be considered as an appendix to a paper by McKinsey. Familiarity with this paper is assumed; its terminology and notation will be used without explanation. McKinsey's main result (theorem 1) is that every class of sentences fulfilling P1–P5, with a set of substitutions satisfying A1–A4, is a system of modal logic in the sense that the “associated” set, T2, contains all theorems of S4. It is also proved (theorem 2) that for T2 to contain all theorems of S5, it is sufficient that the elements of S form a group. The basic idea of the construction is the formalization, by means of D5, of our intuitive notion of possibility.

In view of the great generality of S, it may be of some interest to give a condition that is both necessary and sufficient for T2 to contain S5 after some restriction suggested by our intuitive notions about modalities has first been imposed upon S. The following postulate is related to the idea that if a sentence is possible, then its negation is not necessary. Informally speaking, it requires that S be sufficiently “comprehensive” for this idea to become formalizable in terms of S.

P. If ♢α is in T1, then there exists an element sm of S such that ♢∼sm(α) is not in T1.

I shall now prove that if P is satisfied, the following condition is both necessary and sufficient for T2 to contain all theorems of S5.

C. If α is in T1, then ♢s(α) is in T1 for all elements s of S.

The purpose of this note is (i) to point out an important similarity between the nominalistic system discussed by Quine in his recent paper On universals and the system of logic (the system н) developed by the author in A homogeneous system for formal logic, (ii) to offer certain corrections to the latter, and (iii) to show that that system (н) is adequate for the general theory of ancestrale and for the definition of any general recursive function of natural numbers.

Nominalism as a thesis in the philosophy of science, according to Quine, is the view that it is possible to construct a language adequate for the purposes of science, which in no wise admits classes, properties, relations, or other abstract objects as values for variables.

In this paper, we are concerned with the arithmetical definability of certain notions of integers and rationals in terms of other notions. The results derived will be applied to obtain a negative solution of corresponding decision problems.

In Section 1, we show that addition of positive integers can be defined arithmetically in terms of multiplication and the unary operation of successor S (where Sa = a + 1). Also, it is shown that both addition and multiplication can be defined arithmetically in terms of successor and the relation of divisibility | (where x|y means x divides y).

The present note suggests how the computation of complexity-values outlined in The logical simplicity of predicates may be so modified as to satisfy a more stringent requirement than was there imposed.

By the method of computation described in that article, a basis consisting of two two-place predicates has in general the value 6. Any such basis may be replaced by one four-place predicate that is self-complete with respect to two of its places and also with respect to the remaining two. Such a predicate has but one “joint,” and therefore a value of 5. The consolidation of the two predicates into one thus results in a basis having a lower complexity-value. This does not violate the cardinal rule laid down in that article for testing proposed ways of assigning complexity-values; for, conversely, a four-place predicate that is self-complete in the way described can always be replaced by two two-place prediates. The rule requires a four-place predicate of the kind described to have a higher value than two two-place predicates only if replacement of two two-place predicates by such a four-place predicate is always possible, while replacement of such a four-place predicate by two two-place predicates is not.

However, we might reasonably strengthen our cardinal rule for complexity-valuation by adding as a second requirement:

If each basis of kind A is always replaceable by some basis of kind B, and each basis of kind B is always replaceable by some basis of kind A, then a basis of kind A and a basis of kind B must, in the absence of contrary indications, have the same complexity-value.