This paper is a sequel to [1]. Our purpose is to exhibit certain basic relationships between (ordered dyadic) trees and regular nest structures. We introduce the notion of a tree being isomorphic to a nest structure, and we study some necessary and sufficient conditions for the existence of such isomorphisms. By virtue of some of our results, Kónig's lemma on infinite trees, and our fundamental lemma of [1] concerning infinite regular nest structures become intimately related — either yields an alternative proof of the other.

In [1] Anderson gave what he claimed was a decision procedure for Lewis's calculus S4. One of the proofs of [1] was faulty, however, and he sought to remedy the situation in [2] by modifying slightly one of the conditions of the decision procedure of [1]. Poliferno subsequently reported in [5] that, according to Anderson, the procedure of [2] was not adequate either, but tha t a correct decision procedure for S4 could be obtained by combining the procedures of [1] and [2]. The purpose of the present note is to show tha t none of the three procedures referred to above are correct decision procedures for S4.

In Jaśkowski [1], some properties of the consequences of formulas of the sentential calculus with no more than two occurrences of any variable have been settled. Analogous problems may be raised concerning the consequences of equalities in which the same restriction relates to individual variables. In the present paper, problems of this kind are solved and more general theorems are proved about the logical consequences of some formulas, called here multiconditionals.

I. (Bull's system OIC, defined in [1] as positive implication plus ССССpqqrСССpqrr, can be axiomatised by adding this to a weaker base.)

1. СpСqp

2. ССpqССqrСpr

3. ССССpqqrСССpqrr

4. ССССqrСprsССpqs = D22

5. ССrСpqСССpqСrqСrq = D43

6. СССССpqССrqСrqsССrСpqs = D25

7. ССpСqrССpqСpr = D64

Our terminology and notation is the same as that of [1], of which this note is a sequel.

We wish to show that if we take the natural deduction system (N) described in [1], and delete the rules for the quantifiers, we obtain a complete system for propositional logic. [Of course we now construe “X”, “Y”, “Z” as syntactic variables ranging over formulas of propositional logic, rather than sentences of quantification theory.] Moreover the system serves as a neat decision procedure.

Our principal result is that there exist two incomparable recursively enumerable degrees whose greatest lower bound in the upper semilattice of degrees is 0. This was conjectured by Sacks [5]. As a secondary result, we prove that on the other hand there exists a recursively enumerable degree a < 0(1) such that for no non-zero recursively enumerable degree b is 0 the greatest lower bound of a and b.

The proof of the main theorem involves a method that we have developed elsewhere [8] to deal with situations in which a partial recursive functional may interfere infinitely often with an opposed requirement of lower priority.

We study certain first and second order theories which are semantically defined as the sets of all sentences true in certain given structures. Let be a structure where A is a non-empty set, λ is an ordinal, and Pα is an n(α)-ary relation or function4 on A. With we associate a language L appropriate for which may be a first or higher order calculus. L has an n(α)-place predicate or function constant P for each α < λ. We shall study three types of languages: (1) first-order calculi with equality; (2) second-order monadic calculi which contain monadic predicate (set) variables ranging over subsets of A; (3) restricted (weak) second-order calculi which contain monadic predicate variables ranging over finite subsets of A.

The following is a self-contained proof theoretic treatment of two of the principal axiom schemata of current intuitionistic analysis: the axiom of bar induction (Brouwer's bar theorem) and the axiom of continuity. The results are formulated in terms of formal derivability in elementary intuitionistic analysis H(§ 1), so the positive (i.e., derivability) results also apply to elementary classical analysis Z1 (Appendix 1). Both schemata contain the combination of quantifiers νfΛn, where f, g, … are intended to range over free choice sequences of suitable kinds of objects x, y, …; for example, natural numbers or sequences of natural numbers, and n, m, p, r, … over natural numbers (non-negative integers).

In this paper we follow up our work in [2] on standard classes of recursively enumerable sets, and it will be supposed that the reader is familiar with [2]. One of the main problems left open in [2], that of determining whether or not every standard class has a least member is resolved by the construction of a standard class all of whose members are non-empty, and two of whose members are disjoint. This shows that there is a standard class which is not p.r. in the sense of [2] and we now prefer the adjective sequential for those standard classes which were called p.r. in [2]. Otherwise our terminology will be the same as in [2]. We shall also prove the theorem only stated in [2] that any standard class all of whose members have cardinality < 3 is sequential. Further, we give an example of a standard class which is not sequential and all of whose members have cardinality < 4.

Let Nk denote the set of words over the alphabet Σk = {1, …, k}. Nk contains the null word which is denoted λ. We consider decision problems for various first-order interpreted predicate languages in which the variables range over Nk (k ≧ 2). Our main result is that there is no decision procedure for truth in the interpreted language which has the subword relation as its only non-logical primitive. This, together with known results summarized in Section 4, settles the decision problem for any language constructed on the basis of the relations and functions listed below.

By ΡL we shall mean the first order predicate logic based on S4. More explicitly: Let Ρ0 stand for the first order predicate calculus. The formalisation of Ρ0 used in the present paper will be given later. ΡL is obtained from Ρ0 by adding the rules the propositional constant □ and

In this paper we continue the investigations begun in [2] of equivalence classes of (denumerable) well-orderings under one-one partial recursive, order-preserving maps (recursive isotonisms). The numbering and notation are continued from [2] except that we now use lower case Greek letters for classical ordinals and upper case Roman letters for sets and we slightly modify the definition of (see §IX.3).

In section IX, after proving some lemmata which we use repeatedly in this paper, we establish the existence of Cantor Normal Forms for all co-ordinals less than a co-ordinal of the form WA (a fortiori for all co-ordinals less than a principal number for exponentiation).

Following [1] we write {n} for the nth recursively enumerable (re) set; that is, {n} = {x|VyT(n, x, y)}. By a “pair (T, α)” we mean a consistent re extension T of Peano arithmetic P and an RE-formula α which numerates the non-logical axioms of T in P [4]. Given a pair (T, α) and a particular formula which binumerates the Kleene T predicate in P, there can be defined a primitive recursive function Nα such that and which has the additional property that {Nα(Nα(n))} = ø for all n.

Let Ω be an infinite cardinal larger than ω. By Lω we mean a language with infinitely long expressions having no individual constants, and such that the only predicates are < and =, and the length of ν or ∃ in a formula in Lω is smaller than Ω (cf. §2).

In their original paper on degrees [3], Kleene and Post showed that there is a degree between 0 and 0′. Later, Friedberg [1] and Muchnik [4] showed that there is a recursively enumerable degree between 0 and 0′. Since then, this phenomenon has been repeated several times: a result has been proved for degrees, and then, after considerable additional effort, it has been proved for recursively enumerable degrees.

There are some obvious respects in which that set of all degrees differs from the set of recursively enumerable degrees; e.g., the former is uncountable and has no largest member.

This paper is a sequel to [7], and the terminology of [7] is largely presupposed here. In [7], the algebraic methods of McKinsey-Tarski were employed and extended to yield semantic results of a Kripke kind for a class of relatively weak modal logics, the strongest of which was the Feysvon Wright system T. Deontic versions of both T and E2, called T(D) and D2, and even weaker systems, were handled. The main aim of the present paper is to extend these results to stronger systems of modal logic. Thus the Lewis systems S2–S5, the Brouwersche system B of Kripke [4], the systems E3–E5 of [5], and Łukasiewicz's modal logic, as well as certain new systems, are considered.

Certain modifications of the method of [7] have proved convenient. Thus in Section I, some further results concerning model structures are proved in order that the relationship between S2 and E2, S3 and E3, can be properly stated; in particular, the notions of a refined and connected model structure play a pervasive role throughout.

Modal logic received its modern impetus from the work of Lewis and Langford [10]. In recent years, however, their axiomatic approach, aided by somewhat ad hoc matrices for distinguishing different modal systems, has been supplemented by other techniques. Two of the most profound of these were, first, the algebraic methods employed by McKinsey and Tarski (see [11] and [12]) and, second, the semantic method of Kripke (see [5] and [6]); and there have been others. The aim of the present series of papers is to afford a synthesis of these methods. Thus, though new results are given, the interest lies rather in revealing interconnexions between familiar results and in providing a general framework for future research. In general, we show that semantic completeness results of the Kripke kind can be deduced from the algebraic results by means of one central theorem (Theorem 21).