Let {Wk }k ≥ 0 be a standard enumeration of all recursively enumerable (r.e.) sets. If A is any class of r.e. sets, let θ A denote the index set of A, i.e., θA = {k ∣ Wk ∈ A}. The one-one degrees of index sets form a partial order ℐ which is a proper subordering of the partial order of all one-one degrees. Denote by ⌀ the one-one degree of the empty set, and, if b is the one-one degree of θB, denote by the one-one degree of . Let . Let {Ym }m≥0 be the sequence of index sets of nonempty finite classes of finite sets (classified in [5] and independently, in [2]) and denote by a m the one-one degree of Ym . As shown in [2], these degrees are complete at each level of the difference hierarchy generated by the r.e. sets. It was proved in [3] that, for each m ≥ 0,

(a) a m+1 and ā m+1 are incomparable immediate successors of a m and ā m, and

(b) .

For m = 0, since Y 0 = θ{⌀}, it follows from (a) that

(c) .

Hence it follows that

(d) {⌀, , a o, ā 0, a 1, ā 1 is an initial segment of ℐ.

For each n > 0, two alternative axiomatizations of the theory of strings over n alphabetic characters are presented. One class of axiomatizations derives from Tarski's system of the Wahrheitsbegriff and uses the n characters and concatenation as primitives. The other class involves using n character-prefixing operators as primitives and derives from Hermes' Semiotik. All underlying logics are second order. It is shown that, for each n, the two theories are synonymous in the sense of deBouvere. It is further shown that each member of one class is synonymous with each member of the other class; thus that all of the theories are synonymous with each other and with Peano arithmetic. Categoricity of Peano arithmetic then implies categoricity of each of the above theories.

This paper is a continuation of An abstract form of the Church-Rosser theorem. I (this Journal, vol. 35 (1969), pp. 545–560). In Part I, the Church-Rosser property was deduced from abstract premises (A1)–(A8). The original draft of Part II contained some applications of this result, and a fairly simple abstract result by which the Church-Rosser property could be extended from λβ-reduction to λβη-reduction (Curry's notation [3, Chapter 3]). But since this draft was written, these results have been obtained independently and improved by other workers, and a simple and natural new proof for λβ-reduction has been discovered by W. W. Tait and P. Martin-Löf (see §11 later, and [17, §2.4.3]).

So the main purpose of the present Part II is merely to justify the claim in Part I that the abstract theorem does cover the case of λβ-reduction (and various modifications). I shall also include a summary of the main kinds of Church-Rosser proofs. The paragraph and theorem numbers in Part II will continue from those of Part I.

In §§5 and 6 below, Theorem 1 will be specialised to reductions defined by replacements of parts of expressions by others (Theorems 2 and 2A). At the end of §6 an important subclass of such reductions will be treated (Theorem 3).

In §7, Theorem 3 will be applied to prove the Church-Rosser property for combinatory weak reduction [10, §11B], with or without type-restrictions and extra “arithmetical” reduction-rules (Theorems 4 and 5). (In the original draft Theorem 5 was deduced directly from Theorem 2A; the present intervening Theorem 3 is an independent result of B. Rosen [7].)

We prove that certain syntactic conditions similar to separation principles on a theory are equivalent to semantic properties such as amalgamation and strong amalgamation, by showing that appropriate classes of structures are definable by Lω1ω-sentences. Then we characterise the elements of core models and thus give a natural proof of Rabin's characterisation of convex theories.

The notion of a syntactic characterisation of a semantic property of a theory is by now fairly well known. The earliest such were the classical preservation theorems: For example, a theorem of Lyndon characterised the theories whose models were closed under homomorphic images as those with a set of positive axioms.

Presumably the notion of syntactic characterisation can be made precise, but it is probably better at this stage to leave it vague. The general idea is that theories are “algebras” (cylindric algebras, or logical categories, with suitable extra structure) and that a semantic property P of theories is syntactically characterisable if the class of theories with P is an “elementary” class of “algebras.”

When one codes countable theories as real numbers, a syntactically characterisable property will be arithmetical. The converse does not seem reasonable, especially as it is often fairly easy to prove a property arithmetical (using extra predicates, usually), when we may not be able to find a syntactic characterisation.

Some negative results will be proved concerning the following for certain infinitary languages ℒ1 and ℒ2.

Definition. Beth(ℒ1, ℒ2) iff, for every sentence ϕ(R) of ℒ1, and n-place relation symbols R and S such that S does not occur in ϕ(R), if

then there is an ℒ2 formula θ(x1, …, xn) such that

and θ is built up using only those constant and relation symbols of ϕ other than R.

That is, Beth(ℒ1, ℒ2) iff for every implicit ℒ1 definition ϕ(R) of relations, there is a corresponding explicit ℒ2 definition θ. Beth(ℒωω, ℒωω) was proved by Beth.

Malitz proved that not Beth(ℒω1 ω1, ℒ∞∞) (hence not Beth (ℒ∞∞, ℒ∞∞)), but Beth (ℒ∞ω, ℒ∞∞). In §1, it is shown that Beth(ℒ∞ω, ℒ∞ω) is false. In §2, we strengthen this by showing that, for every cardinal κ, not Beth(ℒ∞ω, ℒ∞κ). In fact, not Beth (ℒκ+ω, ℒ∞κ) follows from property A(κ) defined in §2, and A(κ) is known for regular κ > ω (unpublished result of Morley).

More information on infinitary Beth and Craig theorems is given in [2] and [3]. We assume that the reader is acquainted with the languages ℒκλ which allow conjunctions over ≺κ formulas and quantifiers over ≺λ variables. Thus, we assume that the reader is acquainted with the back and forth argument for showing that two structures are ≡∞κ (ℒ∞κ-elementarily equivalent). Our notation is fairly standard.

For any linear order type τ with first element let be the Boolean set algebra generated by the left-closed right-open (including [x, ∞)) intervals of some linear order of type τ. Let η and ω be the order types of the rationals and natural numbers respectively (when not used as an order type, ω will, as usual, be the set of nonnegative integers). We show that the Boolean algebra of the elementary theory of well-orders, i.e., the Boolean algebra of elementary classes of well-orders or, equivalently, the algebra of equivalence classes of sentences of the elementary theory of well-orders, is isomorphic to and that the Boolean algebra of the elementary theory of abelian groups is isomorphic to . Both results are obtained by applying Hanf's structure diagram technique to the work of Mostowski, Tarski, and Szmielew. One may formalize discussion of algebras of proper classes by assuming the classes are included in a universe which is a set in a larger universe.Given a Boolean algebra, let 0 be its zero and 1 its unit, let ≤ be its associated partial ordering, and, for any elements a, b, and c of the algebra, let “a + b = c ” be the assertion that c is the disjoint sum of a and b. A subset of the algebra disjointly generates the algebra iff each of the algebra's elements is a disjoint sum of a finite number of the subset's elements.

It has been stated by Tarski [5] and “proved” by Grzegorczyk [3] that:

Proved has been put in quotes, not because Grzegorczyk's proof is faulty but because the system he describes as mereology is in fact not Leśniewski's mereology.

Leśniewski's first attempt at describing the collective class, i.e. mereology, was done in ordinary language with no rigorous logical foundation. In describing the collective class, he needed to use the notion of distributive class. So as to clearly distinguish and expose the interplay between the two notions of class, he introduced his calculus of name (name being the distributive notion), which is also called ontology, since he used the primitive term “is.” At this stage, mereology included ontology. Then, in order to have a logically rigorous system, he developed as a basis, a propositional calculus with quantifiers and semantical categories (types), called protothetic. At this final stage, what is properly called mereology includes both protothetic and ontology.

What Grzegorczyk describes as mereology is even weaker than Leśniewski's initial version. To quote from [3]:

With the definition of effective operations as stated in the paper cited above (this Journal, vol. 35 (1970), p. 217), the last step of Lemma 1 does not appear to extend to types ≥ 3. This may be rectified by altering the second clause of the definition of effective operation (loc. cit. p. 217) to read:

ℱ is an effective operation of type i + 2 with Gödel number f∈E i+2, if for every g∈E i+1 there is an effective operation of type i + 1 (not depending on ℱ and f) with Gödel number g such that ℱ() = p(f, g).

With this definition the proofs go through without alteration.

There are two other variants for representing an effective operation by higher type objects.

I. We adopt the definition of effective as given in the text, and require the terms to satisfy the additional condition

II. Here we add to the definition of effective operations given in the text the condition:

If ℱ and ℱ1 are effective operations of type i + 2 and for all effective operations of type i + 1, then ℱ = ℱ1.

We now require terms s, t ∈ fi to satisfy the additional condition

The proof of Lemmas 1 and 2 are easily modified to establish I and II.

Perhaps II may be regarded as giving the most natural characterisation since in this case all terms represent continuous functionals.

A classical result of descriptive set theory expresses every co-analytic subset of the real line as the union of an increasing sequence of Borel sets, the length of the chain being at most the first uncountable ordinal ℵ1 (see [5], [8]). An effective analog of this theorem, obtained by replacing co-analytic (Π11) and Borel (Δ11) with their lightface analogs, would represent every Π11 subset of the real line as the union of a chain of Δ11 sets. No such analog is true, however, because some Δ11 sets are not the union of their Δ11 subsets. For example, the set W, consisting of those reals which code well-orderings (in some standard coding) is Π11, but, by the boundedness principle ([3], [9]), any Δ11 subset of W contains codes only for well-orderings shorter than ω1, the first nonrecursive ordinal. Accordingly, we define the core of a Π11 set to be the union of its Δ11 subsets; clearly this is the largest subset of the given Π11 set for which an effective version of the classical representation could exist.

In §1, we develop the elementary properties of cores of Π11 sets. For example, such a core is itself Π11 and can be represented as the union of a chain of Δ11 sets in a natural way; the chain will have length at most ω1. We show that the core of a Π11 set is “almost all” of the set, while on the other hand there are uncountable Π11 sets with empty cores.

A constructive version of Morse set theory is given, based on Heyting's predicate calculus and with countable rather than full choice. An elaboration of the method of [5] is used to show that the theory is combinator-realizable in the sense defined there. The proof depends on the assumption of the syntactic consistency of the theory.

The method is introduced by first treating a subtheory without countable choice of foundation.

It is intended that the work can be read either classically or constructively, though whether the word constructive is correctly used as a description of either the theory or the metatheory is of course a matter of opinion.

We examine the action of unary functions on the regressive isols. A manageable theory is produced and we find that such a function maps ⋀R into ⋀ if and only if it is eventually R↑ increasing and maps ⋀R into ⋀R if and only if it is eventually recursive increasing. Our paper concludes with a discussion of other methods for extending functions to ⋀R.

In [2], Prikry showed that if κ is a weakly inaccessible cardinal which carries a Rowbottom filter, then there is a Boolean extension of V (the universe), having the same cardinals as V, in which cf(κ) = ω. In this note, we obtain necessary and sufficient conditions which a filter D on κ must possess in order that this may be done.

The main purpose of this paper is to show that there exists a prime differentially closed extension over each differentially perfect field. We do this in a roundabout manner by first giving new and simple axioms for the theory of differentially closed fields (in the manner of Blum [1] for characteristic 0) and by proving that this theory is the model completion of the theory of differentially perfect fields. This paper can be read independently from [10], where we gave more complicated axioms for the same theory (in the manner of Robinson [6] for characteristic 0).

I am indebted to E. R. Kolchin for answering many questions and for making the manuscript of his forthcoming book [2] available to me.

R. Parikh has shown that in the predicate calculus without function symbols it is possible to decide whether or not a given formula A is provable in a Hilbert-style proof of k lines. He has also shown that for any formula A(x 1, …, xn ) of arithmetic in which addition and multiplication are represented by three-place predicates, {(a 1, …, an ): A(a 1, …, an ) is provable from the axioms of arithmetic in k lines} is definable in (N,′, +,0). See [2].

In §1 of this paper it is shown that if S is a definable set of n-tuples in (N,′, +, 0), then there is a formula A(x 1, …, xn ) and a number k so that (a 1 …, a n) ∈ S if and only if A(a 1 …, an ) can be proved in a proof of complexity k from the axioms of arithmetic. The result does not depend on which formalization of arithmetic is used or which (reasonable) measure of proof complexity. In particular, this gives a converse to Parikh's result.

In §II, a measure of proof complexity is given which is based on counting the quantifier steps in semantic tableaux. The idea behind this measure is that A is k provable if in the attempt to construct a counterexample one meets insurmountable difficulties in the definition of the appropriate Skolem functions over sets of cardinality ≤ k. A method is given for deciding whether or not a sentence A in the full predicate calculus is k provable. The question for the full predicate calculus and Hilbert-style systems of proof remains open.

There are two main lacunae in recent work on modal logic: a lack of general results and a lack of negative results. This or that logic is shown to have such and such a desirable property, but very little is known about the scope or bounds of the property. Thus there are numerous particular results on completeness, decidability, finite model property, compactness, etc., but very few general or negative results.

In these papers I hope to help fill these lacunae. This first part contains a very general completeness result. Let In be the axiom that says there are at most n incomparable points related to a given point. Then the result is that any logic containing K4 and In is complete.

The first three sections provide background material for the rest of the papers. The fourth section shows that certain models contain no infinite ascending chains, and the fifth section shows how certain elements can be dropped from the canonical model. The sixth section brings the previous results together to establish completeness, and the seventh and last section establishes compactness, though of a weak kind. All of the results apply to the corresponding intermediate logics.

A. H. Lachlan [2] and C. E. M. Yates [4] independently showed that minimal pairs of recursively enumerable (r.e.) degrees exist. Lachlan and Richard Ladner have shown (unpublished) that there is no uniform method for producing a minimal pair of r.e. degrees below a given nonzero r.e. degree. It is not known whether every nonzero r.e. degree bounds a r.e. minimal pair, but in the present paper it is shown (uniformly) that every high r.e. degree bounds a r.e. minimal pair. (A r.e. degree is said to be high if it contains a high set in the sense of Robert W. Robinson [3].)

Theorem. Let a be a recursively enumerable degree for which a′ = 0″. Then there are recursively enumerable degrees b0 and b1 such that0 < bi < a for each i ≤ 1, and b0 ⋂ b1 = 0.

The proof is based on the Lachlan minimal r.e. pair construction. For notation see Lachlan [2] or S. B. Cooper [1].

By Robinson [3] we can choose a r.e. representative A of the degree a, with uniformly recursive tower {As, ∣ s ≥ 0} of finite approximations to A, such that CA dominates every recursive function where

We define, stage by stage, finite sets Bi,s, i ≤ 1, s ≥ 0, in such a way that Bi, s + 1 ⊇ Bi,s for each i, s, and {Bi,s ∣ i ≤ 1, s ≥ 0} is uniformly recursive.

The cardinality problem for ultraproducts is as follows: Given an ultrafilter over a set I and cardinals αi, i ∈ I, what is the cardinality of the ultraproduct ? Although many special results are known, several problems remain open (see [5] for a survey). For example, consider a uniform ultrafilter over a set I of power κ (uniform means that all elements of have power κ). It is open whether every countably incomplete has the property that, for all infinite α, the ultra-power has power ακ. However, it is shown in [4] that certain countably incomplete , namely the κ-regular , have this property.

This paper is about another cardinality property of ultrafilters which was introduced by Eklof [1] to study ultraproducts of abelian groups. It is open whether every countably incomplete ultrafilter has the Eklof property. We shall show that certain countably incomplete ultrafilters, the κ-good ultrafilters, do have this property. The κ-good ultrafilters are important in model theory because they are exactly the ultrafilters such that every ultraproduct modulo is κ-saturated (see [5]).

Let be an ultrafilter on a set I. Let αi, n, i ∈ I, n ∈ ω, be cardinals and αi, n, ≥ αi, m if n < m. Let

.

Then ρn are nonincreasing and therefore there is some m and ρ such that ρn = ρ if n ≥ m. We call ρ the eventual value (abbreviated ev val) of ρn.

The purpose of this paper is to show that arithmetically minimal systems of notations can be constructed which provide notations for all ramified analytical ordinals (all the ordinals in the minimum β-model for analysis). This is a much larger section of the second number class than the Church-Kleene constructive ordinals (although still only an initial segment of the ordinals). Arithmetic minimality means that if H is an “H-set” associated with an ordinal α in our system and H′ is an H-set associated with the same ordinal α in an arbitrary system of notations S, then H is arithmetical in H′. Thus the arithmetical degrees associated with ordinals in our system are as low as possible.

In order to clarify the structure of degrees of unsolvability and, more generally, to gain a deeper insight into the power set of the integers, coarser but neater classifications than the structure of Turing degrees have been sought. Several hierarchies of sets of integers have been studied, each of which organizes a certain class of sets (or their degrees of unsolvability) into a well-ordering of levels with increasing complexity of nonrecursiveness appearing at each new level. The best known of these hierarchies is the Kleene hierarchy of arithmetical sets.

A common method of obtaining the classical modal logics, for example the Feys system T, the Lewis systems, the Brouwerian system etc., is to build on a basis for the propositional calculus by adjoining a new symbol L, specifying new axioms involving L and the symbols in the basis for PC, and imposing one or more additional transformation rules. In the jargon of algebraic logic, which is the point of view we shall adopt, the “necessity” symbol L may be interpreted as an operator on the Boolean algebra of propositions of PC. For example, the Lewis system S4 may be regarded as a Boolean algebra ℒ together with an operator L on ℒ having the properties: (1)Lp ≤ p for all p in ℒ, (2)L1 = 1, (3) L(p → q) ≤ Lp → Lq for all p, q in ℒ, and (4) Lp = L(Lp) for all p in ℒ. Here, of course, → denotes the material implication connective: p→q = p′ ∨ q. It is easy to verify that property (3) may be replaced by either (3′) L(p ∧ q) = Lp ∧ Lq for all p, q in ℒ, or by (3″) L(p → q) ∧ Lp ≤ Lq for all p, q in ℒ. In particular, it follows from (1) through (4) above that L is a decreasing, idempotent and isotone operator on ℒ. Such mappings are often called interior operators.

In a previous paper [5], we considered the problem of introducing an implication connective into a quantum logic. This is greatly complicated by the fact that the quantal propositions band together to form an orthocomplemented lattice which is only “locally” distributive. Such lattices are called orthomodular. For definitions and further discussion, the reader is referred to that paper. In it, we argued that the Sasaki implication connective ⊃ defined by p ⊃ q = p′ ∨ (p ∧ q) is a natural generalization of material implication when the lattice of propositions is ortho-modular. Indeed, if unrestricted distributivity were permitted, p ⊃ q would reduce to the classical material implication p → q. For this reason, we choose ⊃ to play the role of material implication in an orthomodular lattice. Further properties of ⊃ are enumerated in Example 2.2(1) and Corollary 2.4 below.

In [1] Diego showed that there are only finitely many nonequivalent formulas in n variables in the positive implicational propositional calculus P. He also gave a recursive construction of the corresponding algebra of formulas, the free Hilbert algebra In on n free generators. In the present paper we give an alternative proof of the finiteness of In, and another construction of free Hilbert algebras, yielding a normal form for implicational formulas. The main new result is that In is built up from n copies of a finite Boolean algebra. The proofs use Kripke models [2] rather than the algebraic techniques of [1].

Let V be a finite set of propositional variables, and let F(V) be the set of all formulas built up from V ⋃ {t} using → alone. The algebra defined on the equivalence classes , by setting

is a free Hilbert algebra I(V) on the free generators . A set T ⊆ F(V) is a theory if ⊦pA implies A ∈ T, and T is closed under modus ponens. For T a theory, T[A] is the theory {B ∣ A → B ∈ T}. A theory T is p-prime, where p ∈ V, if p ∉ T and, for any A ∈ F(V), A ∈ T or A → p ∈ T. A theory is prime if it is p-prime for some p. Pp(V) denotes the set of p-prime theories in F(V), P(V) the set of prime theories. T ∈ P(V) is minimal if there is no theory in P(V) strictly contained in T. Where X = {A1, …, An} is a finite set of formulas, let X → B be A1 →····→·An → B (ϕ → B is B). A formula A is a p-formula if p is the right-most variable occurring in A, i.e. if A is of the form X → p.