It is an immediate consequence of results of Church and Gödel that there exist arithmetical recursively unsolvable problems, that is, recursively unsolvable problems of the form [M](P = Q) where P and Q are polynomials and [M] is some finite sequence of existential and universal quantifiers. A question which is immediately raised by this result is whether there exist unsolvable problems of this form where [M] is some finite sequence of existential quantifiers only. As a matter of fact this question is easily seen to be closely related to the tenth problem in the famous list proposed by Hilbert in 1900.

In this paper, we prove the existence of recursively unsolvable problems of the form

where P and Q are polynomials with non-negative integral coefficients. As a matter of fact we show that every recursively enumerable predicate is of the form (1), and conversely that every predicate of the form (1) is recursively enumerable. While our result does not yield the recursive unsolvability of Hilbert's tenth problem, it is easily seen that any considerable improvement of our result would yield this unsolvability.

The author wishes to take this opportunity to express his gratitude to Professors Alonzo Church and E. L. Post with whom he has had the privilege of discussing some of the questions involved in this paper. He also wishes to thank his friends Melvin Hausner and Jacob Schwartz who have made valuable suggestions.

The purpose of the present paper is to dispel such mystery as may be traceable to use of the ill-chosen term ‘ω-inconsistency’ and to a certain application of the term ‘axiom of infinity’. The application of ‘axiom of infinity’ which I have in mind is made by Rosser in his penetrating studies of the system of my New foundations. Let me begin with a synopsis of that system, which I shall call NF.

NF assumes as primitive just the membership connective ‘ϵ’, the truth functions, and quantification over a single style of variables ‘x’, ‘y’, etc. without type distinctions. The axioms, superimposed on standard quantification theory, comprise the axiom of extensionality ‘(x)(x ϵ y · = · x ϵ z) · y ϵ w · ⊃· z ϵ w’ and the axioms of abstraction, these latter being all sentences of the form ‘(∃y)(x)(x ϵ y · = Fx)’ in which the sentence supplanting ‘Fx’ is stratified (i.e., adaptable to type theory by some assignment of types to variables).

The usual logical paradoxes, which stem from Russell's class R0 (i.e., and its relatives R1, R2, and so on (i.e., , , and so on, correspondingly), are contradictions (Ri ϵ Ri) ≡ ~(Ri ϵ Ri), derivable under unrestricted rules of inference. No contradiction appears to obtain.

Lewis and Langford state, “… it appears that the relation of strict implication expresses precisely that relation which holds when valid deduction is possible. It fails to hold when valid deduction is not possible. In that sense, the system of strict implication may be said to provide that canon and critique of deductive inference which is the desideratum of logical investigation.” Neglecting for the present other possible criticisms of this assertion, it is plausible to maintain that if strict implication is intended to systematize the familiar concept of deducibility or entailment, then some form of the deduction theorem should hold for it. The purpose of this paper is to analyze and extend some results previously established which bear on the problem.

We will begin with a rough statement of some relevent considerations. Let the system S contain among its connectives an implication connective ‘I’ and a conjunction connective ‘&’. Let A1, A2, …, An ⊦ B abbreviate that B is provable on the hypotheses A1, A2, …, An for a suitable definition of “proof on hypotheses”, where A1, A2, …, An, B are well-formed expressions of S.

It is a well known fact that Zermelo's Axiom of Choice and Zorn's Lemma are equivalent logical assumptions. However, an investigation from the viewpoint of the hierarchy of types reveals a complication in the nature of this equivalence. In a type-theoretical formalism both postulates enter as spectra (ZAα) and (ZLα) of formulas, where ZAα is Zermelo's Axiom and ZLα is Zorn's Lemma stated for variables of a fixed type α. The complication has its origin in the fact that, although the formula ZAα implies ZLα, in order to deduce ZAα it seems to be necessary to assert Zorn's Lemma ZLβ for a type β which is higher than α. In other words, we don't know a proof assuring the equivalence of the two formulas ZAα and ZLα. Therefore the equivalence of Zermelo's Axiom and Zorn's Lemma has to be understood in the sense that the assertion of the formulas ZAα for all types α implies every one of the formulas ZLβ and conversely the assertion of the spectrum of formulas (ZLα) implies every one of the formulas ZAβ.

In § 3 we shall indicate a type β which makes the deduction of ZAα from ZLβ possible. For this purpose a proof by G. Birkhoff [3] is translated into type-theoretical language.

In § 2 it is shown that ZAα implies ZLα. In this proof no use is made of the notion of well-ordering. Specifically, we do not first deduce the Well-Ordering Theorem as it is usually done in proving Zorn's Lemma from Zermelo's Axiom. However, the method is suggested by Zermelo's second proof of the Well-Ordering Theorem [2].

Im Folgenden wird eine Vereinfachung der Beweisanordnung für Henkin's Theorem [2] p. 162 angegeben (Abschnitt I). – Die Vereinfachung zeigt sich u.a. darin, daß für den abgeänderten Beweis eine Abschätzung der “projektiven Klasse” (im Sinne der Kleene-Mostowski'schen Theorie der projektiven Mengen von natürlichen Zahlen) für das zu konstruierende Modell gelingt (Abschnitte II–IV). Die Kenntnis der Henkin'schen Arbeit wird vorausgesetzt.

Um eine maximale widerspruchsfreie Menge Γω von geschlossenen Formeln, in der zu jeder Existenzaussage (∃x)A(x) eine Beispielaussage A(uij) vorhanden ist, zu erhalten, führt Henkin einen Turm von Kalkülen S0, S1, …, Si, … und dessen Vereinigung Sω ein. Abwechselnd wird dann die gegebene Menge von Formeln in Si zu einer maximalen widerspruchsfreien Menge Γi erweitert und in Si+1 durch Hinzunahme von Beispielaussagen für alle Existenzaussagen aus Γi ergänzt, für die das nicht schon in einem früheren Schritt geschehen ist. Γω ist dann die Vereinigung aller Γi.

Die Vereinfachung besteht nun darin, daß – nach Erweiterung von S0 zu einem Kalkül S* durch Hinzunahme einer einfachen Folge u1, u2, … von “neuen” Konstanten – in S* zu jeder Existenzaussage eine bedingte Beispielaussage gebildet wird. K sei die Klasse dieser Aussagen, Λ die gegebene widerspruchsfreie Menge; dann wird Λ* = K ◡ Λ in S* einmal zu einer maximalen widerspruchsfreien Menge ergänzt.

Unter Verwendung der Standard-Anordnung aller geschlossenen Formeln von S* erhalten wir für diejenigen von der Form (∃x)A(x) eine Aufzählung (∃x)Ai(x), dazu eine Indexfolge ji (i =1, 2, …), definiert durch:

It is known that we can introduce in number theory (for example, the system Z of Hilbert-Bernays) by induction schemata certain predicates of natural numbers which cannot be expressed explicitly within the framework of number theory. The question arises how we can define these predicates in some richer system, without employing induction schemata. In this paper a general notion of definability by induction (relative to number theory), which seems to apply to all the known predicates of this kind, is introduced; and it is proved that in a system L1 which forms an extension of number theory all predicates which are definable by induction (hereafter to be abbreviated d.i.) according to the definition are explicitly expressible.

In order to define such predicates and prove theorems answering to their induction schemata, we have to allow certain impredicative classes in L1. However, if we want merely to prove that for each constant number the special case of the induction schema for a predicate d.i. is provable, we do not have to assume the existence of impredicative classes. A certain weaker system L2, in which only predicative classes of natural numbers are allowed, is sufficient for the purpose. It is noted that a truth definition for number theory can be obtained in L2. Consistency proofs for number theory do not seem to be formalizable in L2, although they can, it is observed, be formalized in L1.

In general, given any ordinary formal system (say Zermelo set theory), it is possible to define by induction schemata, in the same manner as in number theory, certain predicates which are not explicitly definable in the system. Here again, by extending the system in an analogous fashion, these predicates become expressible in the resulting system. The crucial predicate instrumental to obtaining a truth definition for a given system is taken as an example.

The 2-valued calculus of non-contradiction of Dexter has been extended to 3-valued logic. The methods used were, however, too complicated to be capable of generalisation to m-valued logics. The object of the present paper is to give an alternative method of generalising Dexter's work to m-valued logics with one designated truth-value. The rule of procedure is generalised in the same way as before, but the deductive completeness of the system is proved by applying results of Rosser and Turquette. The system has an infinite set of primitive functions, written n(P1, P2, …, Pr) (r = 1,2, …). With the notation of Post, n(P1, P2, …, Pr) has the same truth-value as ~(P1 & P2 & … & Pr). Thus n(P) is Post's primitive ~P, and we can define & by

We use n2(P1, P2, …, Pr) as an abbreviation for n(n(P1, P2, …, Pr)); similarly for higher powers of n. But if we set up the 1-1 correspondence of truth-values i ↔ m−i+1, then & corresponds to ∨ and ~m−1 corresponds to ~. Hence the functional completeness of our system follows from a theorem of Post.

We define the functions N(P), N(P, Q) by

Thus the truth-value of N(P) is undesignated if and only if the truth-value of P is designated, and the truth-value of N(P, Q) is undesignated if and only if the truth-values of P and Q are both designated.

These systems are roughly natural number theory in, respectively, nth order function calculus, for all positive integers n. Each of these systems is expressed in the notation of the theory of types, having variables with type subscripts from 1 to n. Variables of type 1 stand for natural numbers, variables of type 2 stand for classes of natural numbers, etc. Primitive atomic wff's (well-formed formulas) of Tn are those of number theory in variables of type 1, and of the following kind for n > 1: xi ϵ yi+1. Other wff's are formed by truth functions and quantifiers in the usual manner. Quantification theory holds for all the variables of Tn. Tn has the axioms Z1 to Z9, which are, respectively, the nine axioms and axiom schemata for the system Z (natural number theory) on p. 371 of [1]. These axioms and axiom schemata contain only variables of type 1, except for the schemata Z2 and Z9, which are as follows:

where ‘F(x1)’ can be any wff of Tn. Identity is primitive for variables of type 1; for variables of other types it is defined as follows:

During the past several decades, linguists have developed and applied widely techniques which enable them, to a considerable extent, to determine and state the structure of natural languages without semantic reference. It is of interest to inquire seriously into the formality of linguistic method and the adequacy of whatever part of it can be made purely formal, and to examine the possibilities of applying it, as has occasionally been suggested, to a wider range of problems. In order to pursue these aims it is first necessary to reconstruct carefully the set of procedures by which the linguist derives the statements of a linguistic grammar from the behaviour of language users, distinguishing clearly between formal and experimental in such a way that grammatical notions, appearing as definienda in a constructional system, will be formally derivable for any language from a fixed sample of linguistic material upon which the primitives of the system are experimentally defined. The present paper will be an attempt to formalize a certain part of the linguist's generalized syntax language.

From another point of view, this paper is an attempt to develop an adequate notion of syntactic category within an inscriptional nominalistic framework. The inscriptional approach seems natural for linguistics, particularly in view of the fact that an adequate extension of the results of this paper will have to deal with the problem of homonymity, i.e., with a statement of the conditions under which tokens of the same type must be assigned to different syntactic classes.

In this third and last paper on inner models we consider some of the inherent limitations of the method of using inner models of the type defined in 1.2 for the proof of consistency results for the particular system of set theory under consideration. Roughly speaking this limitation may be described by saying that practically no further consistency results can be obtained by the construction of models satisfying the conditions of theorem 1.5, i.e., conditions 1.31, 1.32, 1.33, 1.51, viz.:

This applies in particular to the ‘complete models’ defined in 1.4. Before going on to a precise statement of these limitations we shall consider now the theorem on which they depend. This is concerned with a particular type of complete model examples of which we call “proper complete models”; they are those complete models which are essentially interior to the universe, those whose classes are sets of the universe constituting a class thereof, i.e., those for which the following proposition is true:

The main theorem of this paper is that the statement that there are no models of this kind can be expressed formally in the same way as the axioms A, B, C and furthermore it can be proved that if the axiom system A, B, C is consistent then so is the system consisting of axioms A, B, C, plus this new hypothesis that there exist no proper complete models. When combined with the axiom ‘V = L’ introduced by Gödel in (1) this new hypothesis yields a system in which any normal complete model which exists has for its universal class V, the universal class of the original system.

The sign ‘⊃’ (or ‘→’ or ‘C’) functions in many logical systems in a way which precludes its interpretation as either strict or material implication. For example, in the systems of Heyting, Johansson, Fitch and Bernays (positive logic), the following are theorems:

Now if ‘⊃’ were interpreted as strict implication, ⊃2 would mean ‘if p is true, then p is strictly implied by every proposition’, i.e. ‘if p is true, it is necessarily true’, which is false for contingently true p. If on the other hand ‘⊃’ were interpreted as material implication, ⊃1 would reduce to ‘~p ∨ p’, i.e. to the law of excluded middle, which is conspicuously lacking in the systems mentioned. The reader is likely in practice to veer between these two interpretations. Thus in Fitch or Heyting on realizing that ‘~p⊃▪ p⊃q’ is a theorem, one thinks of it as meaning ‘a false proposition implies everything’ and regards the implication as material; but the presence of ‘p⊃p’ as a theorem, even for choices of p which do not satisfy excluded middle, inclines one again to the strict interpretation. This vacillation, while it need not lead to the commission of any formal fallacies, tends to hamstring one's intuition and thus waste time. The purpose of this paper is to suggest an interpretation of ‘⊃’ which will prevent such havering.

Let two formulae A and B be called interdeducible if A ⊢ B and B ⊢ A.

It has been shown that the conditioned disjunction function [X, Y, Z] with the same truth-table as (X & Y) ∨ (Z & ) together with the logical constants t and f, form a complete set of independent connectives for the 2-valued propositional calculus and that these connectives are self-dual. This has since been generalised to the theorem which states that the conditioned disjunction function [Y, X1, X2, …, Xm, Y] with the same truth-table as (X1 & J1(Y)) ∨ (X2 & J2(Y)) ∨ … ∨ (Xm & Jm(Y)) together with the logical constants 1, 2, …, m form a complete set of independent connectives for the m-valued propositional calculus and that these connectives are self-dual. It has been conjectured by Church that conditioned disjunction together with the universal and existential quantifiers form a complete set of independent connectives for the 2-valued erweiterter Aussagenkalkül. The object of the present paper is to prove a theorem for the m-valued erweiterter Aussagenkalkül which reduces, in the case m = 2, to the conjecture of Church. In the m-valued propositional calculus if the propositional variable X occurs as a free variable in the formula then (∃X) and (X) are read “there exists X such that ” and “for all X, ”, respectively. If for a given assignment of truth-values to the remaining free propositional variables occurring in , takes the truth-value f(x), where x is the truth-value of X, then (∃X) and (X) take the truth-values min (f(1), f(2), …, f(m)), max(f(1), f(2), …, f(m)), respectively. We shall prove:

Theorem. The conditioned disjunction function, together with the universal and existential quantifiers, form a complete set of independent connectives for the m-valued erweiterter Aussagenkalkül.