The foundation of analysis does not require the full generality of set theory but can be accomplished within a more restricted frame. Just as for number theory we need not introduce a set of all finite ordinals but only a class of all finite ordinals, all sets which occur being finite, so likewise for analysis we need not have a set of all real numbers but only a class of them, and the sets with which we have to deal are either finite or enumerable.

We begin with the definitions of infinity and enumerability and with some consideration of these concepts on the basis of the axioms I—III, IV, V a, V b, which, as we shall see later, are sufficient for general set theory. Let us recall that the axioms I—III and V a suffice for establishing number theory, in particular for the iteration theorem, and for the theorems on finiteness.

We discuss the problem of finding forcing posets which introduce closed unbounded subsets to a given stationary set.

PA is Peano Arithmetic. Pr(x) is the usual Σ1,-formula representing provability in PA. A strong provability predicate is a formula which has the same properties as Pr(·) but is not Σ1. An example: Q is ω-provable if PA + ¬Q is ω-inconsistent (Boolos [4]). In [5] Dzhaparidze introduced a joint provability logic for iterated ω-provability and obtained its arithmetical completeness.

In this paper we prove some further modal properties of Dzhaparidze's logic, e.g., the fixed point property and the Craig interpolation lemma. We also consider other examples of the strong provability predicates and their applications.

In this note we shall be interested in the following problems.

Problem 1. Can IΔ0 ⊢ ∀x∃y > x(y is prime)?

Here I Δ0 is Peano arithmetic with the induction axiom restricted to bounded (i.e. Δ0) formulae.

Problem 2. Can IΔ0 ⊢ Δ0 PHP?

Here Δ0 PHP (Δ0 pigeonhole principle) is the schema

for θ ∈ Δ0, or equivalently in IΔ0, for a Δ0 formula F(x,y)

written .

By obtaining partial solutions to Problem 2 we shall show that Problem 1 has a positive solution if IΔ0 is replaced by IΔ0 + ∀xx log(x) exists.

Our notation will be entirely standard (see for example [3] and [4]). In particular all logarithms will be to the base 2 and in expressions like log(x), (1 + ε)x, etc. we shall always mean the integer part of these quantities.

Concerning Problem 2 we remark that it is shown in [5] that for k ∈ N and F ∈ Δ0,

As far as we know this is the best result of this form, in that we do not know how to replace log(z) k by anything larger. However, as we shall show in Theorem 1, we can do much better if we increase the difference between the sizes of the domain and range of F.

In what follows let M be a countable nonstandard model of IΔ0, and let be those subsets of M defined by Δ0 formulae with parameters from M.

Theorem 1. For k ∈ N and F ∈ Δ0,

Here log0(x) = x, log k + 1(x) = log(log k (x)).

Proof. To simplify matters, consider first the case k = 1. So assume M ⊨ a log(a) exists and with and a > 1. The idea of the proof is the following.

We consider two formal systems for the theory of (natural) numbers, both of which are applied second-order functional calculi with equality and the description operator. The two systems have the same primitive symbols, rules of formation, and axioms, differing only in the rules of inference.

The primitive logical symbols of the systems are the improper symbols (,), the prepositional connectives ∨, &, ⊃, ≡, ~, the quantifiers ( ), (E), the equality symbol =, the description operator ι,-infinitely many distinct individual (or number) variables, and for each positive integer k infinitely many distinct k-place function variables. Our systems have in addition the following four primitive nonlogical (or arithmetical) constants:0, 1, +, ×.

The classes of “number formulas” (nfs) and “propositional formulas” (pfs) are defined inductively as the least classes of formal expressions (i.e. of concatenations of primitive symbols) satisfying the following conditions:

(1) 0, 1, and the number variables are nfs.

Enumeration reducibility is a reducibility between sets of natural numbers defined as follows: A is enumeration reducible to B if there is some effective operation on enumerations which when given any enumeration of B will produce an enumeration of A. One reason for interest in this reducibility is that it presents us with a natural reducibility between partial functions whose degree structure can be seen to extend the structure of the Turing degrees of unsolvability. In [7] Friedberg and Rogers gave a precise definition of enumeration reducibility, and in [12] Rogers presented a theorem of Medvedev [10] on the existence of what Case [1] was to call quasi-minimal degrees. Myhill [11] also defined this reducibility and proved that the class of quasi-minimal degrees is of second category in the usual topology. As Gutteridge [8] has shown that there are no minimal enumeration degrees (see Cooper [3]), the quasi-minimal degrees are very much of interest in the study of the structure of the enumeration degrees. In this paper we define a jump operator on the enumeration degrees which was introduced by Cooper [4], and show that every complete enumeration degree is the jump of a quasi-minimal degree. We also extend the notion of a high Turing degree to the enumeration degrees and construct a “high” quasi-minimal enumeration degree—a result which contrasts with Cooper's result in [2] that a high Turing degree cannot be minimal. Finally, we use the Sacks' Jump Theorem to characterise the jumps of the co-r.e. enumeration degrees.

There are human beings whose intellectual power exceeds that of ordinary men. In my life, in my personal experience, there were three such men, and one of them was Andrei Nikolaevich Kolmogorov. I was lucky enough to be his immediate pupil. He invited me to be his pupil at the third year of my being student at the Moscow University. This talk is my tribute, my homage to my great teacher.

Andrei Nikolaevich Kolmogorov was born on April 25, 1903. He graduated from Moscow University in 1925, finished his post-graduate education at the same University in 1929, and since then without any interruption worked at Moscow University till his death on October 20, 1987, at the age 84½.

Kolmogorov was not only one of the greatest mathematicians of the twentieth century. By the width of his scientific interests and results he reminds one of the titans of the Renaissance. Indeed, he made prominent contributions to various fields from the theory of shooting to the theory of versification, from hydrodynamics to set theory. In this talk I should like to expound his contributions to mathematical logic.

Here the term “mathematical logic” is understood in a broad sense. In this sense it, like Gallia in Caesarian times, is divided into three parts:

(1) mathematical logic in the strict sense, i.e. the theory of formalized languages including deduction theory,

(2) the foundations of mathematics, and

(3) the theory of algorithms.

Those who object to the identification of strict implication and entail-ment speak in such a way that for A to entail B, A must be relevant to B. This view of entailment agrees not only with that of the naive student of logic (who tends to think the phrase paradoxes of “implication” more accurate than “paradoxes” of implication), but also with that expressed in the initial chapters of many textbooks in logic under the heading “Fallacies of Relevance.”2

In regard to formal theories proposed as explications of the notion of entailment, it becomes important to have at our disposal some formal account of the demand for relevance as between antecedent and consequent of an entailment.

In [5] and [21] we studied countable algebra in the context of “reverse mathematics”. We considered set existence axioms formulated in the language of second order arithmetic. We showed that many well-known theorems about countable fields, countable rings, countable abelian groups, etc. are equivalent to the respective set existence axioms which are needed to prove them.

One classical algebraic theorem which we did not consider in [5] and [21] is the Hilbert basis theorem. Let K be a field. For any natural number m, let K[x1,…,xm] be the ring of polynomials over K in m commuting indeterminates x1,…,xm. The Hilbert basis theorem asserts that for all K and m, every ideal in the ring K[x1,…,xm] is finitely generated. This theorem is of fundamental importance for invariant theory and for algebraic geometry. There is also a generalization, the Robson basis theorem [11], which makes a similar but more restrictive assertion about the ring K〈x1,…,xm〉 of polynomials over K in mnoncommuting indeterminates.

In this paper we study a certain formal version of the Hilbert basis theorem within the language of second order arithmetic. Our main result is that, for any or all countable fields K, our version of the Hilbert basis theorem is equivalent to the assertion that the ordinal number ωω is well ordered. (The equivalence is provable in the weak base theory RCA0.) Thus the ordinal number ωω is a measure of the “intrinsic logical strength” of the Hilbert basis theorem. Such a measure is of interest in reference to the historic controversy surrounding the Hilbert basis theorem's apparent lack of constructive or computational content.

Il s'agit d'un problème combinatoire de logique formelle, formulé par Jevons; il sera expliqué en détails dans ce qui suit (voir no. 1). Jevona luimême n'a traité le problème que dans les cas les plus simples (n = 1, 2, 3); un cas plus difficile (n = 4) a été traité par Clifford; le cas général (n quelconque) a été à peine abordé.

Le but de ce travail est de faire remarquer que ce problème de Jevons et de Clifford est contenu comme cas particutier dans un problème combinatoire général que j'ai traité ailleurs. La méthode générale ramène le problème présent à l'étude d'un certain groupe de permutations d'ordre n!2n, étroitement lié au groupe symétrique d'ordre n!. J'ai fait les calculs nécessaires pour n = 1, 2, 3, 4. Mes résultats numèriques sont complètement en accord avec les résultats de Jevons, mais ils ne s'accordent qu'en partie avec les résultats de Clifford.

Une proposition peut être vraie ou fausse. On peut exprimer la même chose en disant que nous pouvons attribuer à une proposition l'une ou l'autre des deux “valeurs logiques” qui s'excluent mutuellement: la “vérité” et la “fausseté.”

This paper shows that non-normal modal logics can be simulated by certain polymodal normal logics and that polymodal normal logics can be simulated by monomodal (normal) logics. Many properties of logics are shown to be reflected and preserved by such simulations. As a consequence many old and new results in modal logic can be derived in a straightforward way, sheding new light on the power of normal monomodal logic.

This paper was suggested by some work of Alan Ross Anderson on deontic logic. Anderson proposed in [1] that the various deontic modalities (‘it is obligatory that’, ‘it is forbidden that’, ‘it is permitted that’, etc.) should be defined in terms of the ordinary alethic modalities (‘it is necessary that’, ‘it is possible that’, etc.). The definition I shall consider is not in fact Anderson's own, though it is closely related to it. His definition, as set out in [1], involves the idea of an (unspecified) penalty or sanction. A forbidden action is defined as one whose commission entails the application of the sanction; an obligatory action is one whose omission entails the application of the sanction.

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.

An algorithm has been described by S. Burris [3] which decides if a finite set of identities, whose function symbols are of rank at most 1, has a finite, nontrivial model. (By “nontrivial” it is meant that the universe of the model has at least two elements.) As a consequence of some results announced in the abstracts [2] and [8], it is clear that if the restriction on the ranks of function symbols is relaxed somewhat, then this finite model problem is no longer solvable by an algorithm, or at least not by a “recursive algorithm” as the term is used today.

In this paper we prove a sharp form of this negative result; showing, by the way, that Burris' result is in a sense the best possible result in the positive direction. Our main result is that in a first order language whose only function or relation symbol is a 2-place function symbol (the language of groupoids), the set of identities that have no nontrivial model, is recursively inseparable from the set of identities such that the sentence has a finite model. As a corollary, we have that each of the following problems, restricted to sentences defined in the language of groupoids, is algorithmically unsolvable: (1) to decide if an identity has a finite nontrivial model; (2) to decide if an identity has a nontrivial model; (3) to decide if a universal sentence has a finite model; (4) to decide if a universal sentence has a model. We note that the undecidability of (2) was proved earlier by McNulty [13, Theorem 3.6(i)], improving results obtained by Murskiǐ [14] and by Perkins [17]. The other parts of the corollary seem to be new.

It is shown that many different problems have the same degree of unsolvability. Among these problems are:

The Inductive Inference Problem. Infer in the limit an index for a recursive function f presented as f(0), f(1),f(2),….

The Recursive Index Problem. Decide in the limit if i is the index of a total recursive function.

The Zero Nonvariant Problem. Decide in the limit if a recursive function f presented as f(0), f(1), f(2),… has value unequal to zero for infinitely many arguments.

Finally, it is shown that these unsolvable problems are strictly easier than the halting problem.

Frege's attempts to formulate a theory of properties to serve as a foundation for logic, mathematics and semantics all dissolved under the weight of the logicial paradoxes. The language of Frege's theory permitted the representation of the property which holds of everything which does not hold of itself. Minimal logic, plus Frege's principle of abstraction, leads immediately to a contradiction. The subsequent history of foundational studies was dominated by attempts to formulate theories of properties and sets which would not succumb to the Russell argument. Among such are Russell's simple theory of types and the development of various iterative conceptions of set. All of these theories ban, in one way or another, the self-reference responsible for the paradoxes; in this sense they are all “typed” theories. The semantical paradoxes, involving the concept of truth, induced similar nightmares among philosophers and logicians involved in semantic theory. The early work of Tarski demonstrated that no language that contained enough formal machinery to respresent the various versions of the Liar could contain a truth-predicate satisfying all the Tarski biconditionals. However, recent work in both disciplines has led to a re-evaluation of the limitations imposed by the paradoxes.

In the foundations of set theory, the work of Gilmore [1974], Feferman [1975], [1979], [1984], and Aczel [1980] has clearly demonstrated that elegant and useful type-free theories of classes are feasible. Work on the semantic paradoxes was given new life by Kripke's contribution (Kripke [1975]). This inspired the recent work of Gupta [1982] and Herzberger [1982]. These papers demonstrate that much room is available for the development of theories of truth which meet almost all of Tarski's desiderata.

We define a generic notion of cut that applies to many first-order theories. We prove a generic cut elimination theorem showing that the cut elimination property holds for all theories having a so-called pre-model. As a corollary, we retrieve cut elimination for several axiomatic theories, including Church's simple type theory.

In the axiomatic development of the logic of nonrelativistic quantum mechanics it is not difficult to set down certain plausible axioms which ensure that the quantum logic of propositions has the structure of an orthomodular poset. This can be done in a number of ways, for example, as in Gunson [2], Mackey [4], Piron [5], Varadarajan [7] and Zierler [8], and we summarise one of these ways in §2 below.

Die Verbandstheorie ist bekanntlich von Dedekind an Hand seiner idealtheoretischen Untersuchungen begründet worden. Es hat sich in letzter Zeit herausgestellt, daß die wesentliche Eigenschaft des Dedekind'schen Idealsystems darin liegt, daß die Ideale einen Halbverband (§1) bilden. Die Idealtheorie führt so auf die Frage nach alien Halbverbänden über einer beliebigen halbgeordneten Menge M. Die einfache Antwort enthält §2. Ebenso einfach ist die Frage nach alien distributiven Verbänden uber M zu beantworten. In beiden Fällen ist unter den Halbverbänden bzw. distributiven Verbänden über M einer dadurch ausgezeichnet, daß alle anderen homomorph zu ihm sind. Diesen ausgezeichneten Halbverband bzw. distributiven Verband nennen wir den freien Halbverband bzw. freien distributiven Verband über M.

Zu neuen Fragen kommt man bei der Untersuchung speziellerer Halbverbände über M. Es ist z.B. bekannt, daß M stets zu einem vollständigen Boole'schen Verband erweitert werden kann. Gibt es unter diesen Erweiterungen stets den freien vollständigen Boole'schen Verband über M, der dadurch ausgezeichnet ist, daß alle anderen zu ihm homomorph sind ?

In §3 wird zunächst die Existenz des freien orthokomplementären Halbverbandes über M bewiesen. Mit Hilfe der hier benutzten Methode läßt sich auch der Existenzbeweis für den freien abzählbar-vollständigen Boole'schen Verband über M führen.

S. A. Kripke has given [6] a very simple notion of model for intuitionistic predicate logic. Kripke's models consist of a quasi-ordering (C, ≤) and a function ψ which assigns to every c ∈ C a model of classical logic such that, if c ≤ c′, ψ(c′) is greater or equal to ψ(c). Grzegorczyk [3] described a class of models which is still simpler: he takes, for every ψ(c), the same universe. Grzegorczyk's semantics is not adequate for intuitionistic logic, since the formula

where х is not free in α. holds in his models but is not intuitionistically provable. It is a conjecture of D. Klemke that intuitionistic predicate calculus, strengthened by the axiom scheme (D), is correct and complete with respect to Grzegorczyk's semantics. This has been proved independently by D. Klemke [5] by a Henkinlike method and me; another proof has been given by D. Gabbay [1]. Our proof uses lattice-theoretical methods.