We characterize, in terms of determinacy, the existence of 0## as well as the existence of each of the following: 0###, 0####, 0#####,…. For κ Є ω, we define two classes of sets, and , which lie strictly between and . We also define 01# as# and in general, 0(k+1)# as (0k#)#. We then show that the existence of 0(k + 1)# is equivalent to the determinacy of as well as the determinacy of .

A notion of reducibility ≤r between sets is specified by giving a set of procedures for computing one set from another. We say that a set A is r-reducible to a set B, A ≤rB, if one of the procedures applied to B gives A. Associated with any such reducibility notion is the structure of r-degrees, the equivalence classes of sets with respect to this reducibility, with the induced ordering. The most general notion of a computable reducibility is that of Turing, ≤T. Here we say that A ≤TB if there is a Turing machine φe which, when equipped with an oracle for B, computes A: φeB = A. Such Turing degree computations are characterized by the phenomenon that only during the computation itself do we discover which questions about B need to be answered to compute A(x). In contrast, for nearly all other computable reducibilities the set of questions needed is given in advance by a recursive procedure. Perhaps the most common example of such a procedure is many-one reducibility, ≤m: A ≤mB if there is a recursive function f such that x ∈ A ⇔ f(x) ∈ B.

Reducibilities with the property that the output, A(x), is determined by the answers that B gives to a set of questions calculated recursively from x are said to be of tabular type. The most general tabular reducibility is called truth-table reducibility, ≤tt. The procedures [e] associated with this reducibility are specified by a recursive function f (= {e}) which, for each x, gives a set of n questions about the oracle and, for each of the possible 2n sets of answers, gives the corresponding output. As usual this defines A ≤ttB as “there is an e such that [e]B = A”. It is with this notion of reducibility and the associated tt-degrees that we shall be concerned in this paper. Basic information on several such strong reducibilities can be found in Rogers [28]. For more information we recommend the survey articles by Odifreddi [25] and Degtev [2] as well as Odifreddi's book [26].

The two statements “Two different objects cannot occupy the same place at the same time” and “An object cannot be in two different places at the same time” are axioms of our everyday understanding of objects, space and time. We develop a first-order theory OST (Objects, Space and Time) in which formal equivalents of these two statements are taken as axioms. Using the theory OST, we uncover other fundamental principles of objects, space and time. We attempt to understand the logical nature of these principles, to investigate their formal consequences, and to identify logical alternatives to them. For easy reference, all of the nonlogical axioms of OST are listed together at the end of §2. In §3, we introduce two possible extensions of OST.

We say φ is an ∀∃ sentence if and only if φ is logically equivalent to a sentence of the form ∀x∃yψ(x, y), where ψ(x, y) is a quantifier-free formula containing no variables except x and y. In this paper we show that there are algorithms to decide whether or not a given ∀∃ sentence is true in (1) an algebraic number field K, (2) a purely transcendental extension of an algebraic number field K, (3) every field with characteristic 0, (4) every algebraic number field, (5) every cyclic (abelian, radical) extension field over Q, and (6) every field.

Higher Suslin trees have become a tool in some forcing constructions in set theory (see, for example, [D1] and [D2]). Most of the constructions using ω1 Suslin trees can be extended to κ+ Suslin trees for any regular cardinal κ. Some of these are given in §1.

In many such constructions, sequences of Suslin trees are used. In §II we show, in various ways, that the generalization to sequences, even ω-sequences, of κ+ Suslin trees cannot be done.

In these constructions the Suslin trees are used as forcing poset (the forcing adds a branch in the tree). There is another way to kill a Suslin tree, namely by adding a big antichain. Some results on this forcing are given in §III.

Our notation is standard. If T is a tree and x ∈ T, then ∣x∣ is the height of x in T. We define Tα (or T(α)) = {x ∈ T: ∣x∣ = α} and T∣α = {x ∈ T: ∣x∣ < α}.

If p and q are forcing conditions, p ≤ q means that p has more information than q.

If (Tα: α ∈ I) is a sequence of trees, Π Tα will always mean the set of (xα: α ∈ I) such that xα ∈ Tα and ∣xα∣ = ∣xβ∣ for α, β ∈ I.

For functions b, T,… we denote by b ∣α, T∣ α,… their restriction to α.

If x is a sequence of ordinals and α is an ordinal, x∧α is the sequence obtained by concatenating α at the end of x.

The condensed detachment rule, or ruleD, was first proposed by Carew Meredith in the 1950's for propositional logic based on implication. It is a combination of modus ponens with a “minimal” amount of substitution. We shall give a precise detailed statement of rule D. (Some attempts in the published literature to do this have been inaccurate.)

The D-completeness question for a given set of logical axioms is whether every formula deducible from the axioms by modus ponens and substitution can be deduced instead by rule D alone. Under the well-known formulae-as-types correspondence between propositional logic and combinator-based type-theory, rule D turns out to correspond exactly to an algorithm for computing principal type-schemes in combinatory logic. Using this fact, we shall show that D is complete for intuitionistic and classical implicational logic. We shall also show that D is incomplete for two weaker systems, BCK- and BCI-logic.

In describing the formulae-as-types correspondence it is common to say that combinators correspond to proofs in implicational logic. But if “proofs” means “proofs by the usual rules of modus ponens and substitution”, then this is not true. It only becomes true when we say “proofs by rule D”; we shall describe the precise correspondence in Corollary 6.7.1 below.

This paper is written for readers in propositional logic and in combinatory logic. Since workers in one field may not feel totally happy in the other, we include short introductions to both fields.

We wish to record thanks to Martin Bunder, Adrian Rezus and the referee for helpful comments and advice.

In [3], Todorčević showed that ω1 ⇸ [ω1]ω12. In this paper we use similar methods to prove an analogous partition theorem for Pω1(λ), for certain uncountable cardinals λ.

Recall that ω1 → [ω1]ω12, means that for every function f: [ω1]2 → ω1 there is a set A ∈ [ω1]ω1 such that f“[A]2 ≠ ω1, and of course ω1 ⇸ [ω1]ω12, is the negation of this statement. For partition relations on Pω1(→) it is customary to partition only those pairs of sets in which the first set is a subset of the second. Thus for A ⊆ Pω1(λ) we define

We will write Pω1(λ) → [unbdd]λ2 to mean that for every function f: [Pω1(λ)]⊂2 → λ there is an unbounded set A ⊆ Pω1(λ) such that f“[A]⊂2 ≠ λ, and again Pω1(λ) ⇸ [unbdd]λ2 is the negation of this statement.

A reduction algebra is defined as a set with a collection of partial unary functions (called reduction operators). Motivated by the lambda calculus, the Church-Rosser property is defined for a reduction algebra and a characterization is given for those reduction algebras satisfying CRP and having a measure respecting the reductions. The characterization is used to give (with 20/20 hindsight) a more direct proof of the strong normalization theorem for the impredicative second order intuitionistic propositional calculus.

We provide partial answers to the following problem: Is the class of Borel linear orders well-quasi-ordered under embeddability? We show that it is indeed the case for those Borel orders which are embeddable in Rω, with the lexicographic ordering. For Borel orders embeddable in R2, our proof works in ZFC, but it uses projective determinacy for Borel orders embeddable in some Rn, n < ω, and hyperprojective determinacy for the general case.

Although it is known that reachability in undirected finite graphs can be expressed by an existential monadic second-order sentence, our main result is that this is not the case for directed finite graphs (even in the presence of certain “built-in” relations, such as the successor relation). The proof makes use of Ehrenfeucht-Fraïssé games, along with probabilistic arguments. However, we show that for directed finite graphs with degree at most k, reachability is expressible by an existential monadic second-order sentence.

The algebraic systems of combinatory spaces [3] and operative spaces [1] have been designed to provide appropriate settings for the development of abstract recursion theory. As shown in [1, Chapter 27], these systems are closely related; namely, every combinatory space has a companion operative space with a storing operation St such that Skordev recursiveness in the former equals st-recursiveness in the latter. The problem of characterization of those operative spaces which have companion combinatory spaces was solved in [2] by introducing a class of operative spaces called Skordev spaces and showing that these give an alternative axiomatics of Skordev's combinatory spaces.

In this paper we study operative spaces with two special constants S1 and S2 which, in computer science terms, axiomatize the availability of stacking facility. We establish that any such space has a Skordev subspace and, moreover, all Skordev spaces can be obtained in this way. The construction ensures that st-recursiveness in the Skordev space concerned is equivalent to recursiveness in S1 and S2 in the wider operative space. Therefore, it quite unexpectedly turns out that Skordev recursiveness can be expressed via relative recursiveness in operative spaces in a straightforward manner, without employing higher spaces as done in [1].

In this paper we ask the question: to what extent do basic set theoretic properties of Loeb measure depend on the nonstandard universe and on properties of the model of set theory in which it lies? We show that, assuming Martin's axiom and κ-saturation, the smallest cover by Loeb measure zero sets must have cardinality less than κ. In contrast to this we show that the additivity of Loeb measure cannot be greater than ω1. Define cof(H) as the smallest cardinality of a family of Loeb measure zero sets which cover every other Loeb measure zero set. We show that card(⌊log2(H)⌋) ≤ cof (H) ≤ card(2H), where card is the external cardinality. We answer a question of Paris and Mills concerning cuts in nonstandard models of number theory. We also present a pair of nonstandard universes M ≼ N and hyperfinite integer H ∈ M such that H is not enlarged by N, 2H contains new elements, but every new subset of H has Loeb measure zero. We show that it is consistent that there exists a Sierpiński set in the reals but no Loeb-Sierpiński set in any nonstandard universe. We also show that it is consistent with the failure of the continuum hypothesis that Loeb-Sierpiński sets can exist in some nonstandard universes and even in an ultrapower of a standard universe.

In this paper we investigate omitting types for a certain kind of stable theories which we call stable ccc theories. In Theorem 2.1 we improve Steinhorn's result from [St]. We prove also some independence results concerning omitting types. The main results presented in this paper were part of the author's Ph.D. thesis [N1].

Throughout, we use the standard set-theoretic and model-theoretic notation, such as can be found for example in [Sh] or [M]. So in particular T is always a countable complete theory in the language L. We consider all models of T and all sets of parameters subsets of the monster model ℭ, which is very saturated. Ln(A) denotes the Lindenbaum-Tarski algebra of formulas with parameters from A and n free variables. We omit n in Ln(A) when n = 1 or when it is clear from the context what n is. If φ, ψ ∈ L(A) are consistent then we say that φ is below ψ if ψ⊢ψ. For a type p and a set A ⊆ ℭ, p(A) is the set of tuples of elements of A which satisfy p. Formulas are special cases of types. We say that a type p is isolated over A if, for some φ() ∈ L(A), φ() ⊢ p(x), i.e. φ isolates p. For a formula φ, [φ] denotes the class of types which contain φ. We assume that the reader is familiar with some basic knowledge of forking, as presented in [Sh, III] or [M].

Throughout, we work in ZFC. and denote (countable) transitive models of ZFC. cov K is the minimal number of meager sets covering the real line R. In this paper we prove theorems showing connections between omitting types and the combinatorics of the real line. More results in this direction are presented in [N2] and [N3].

Let β be an arbitrary limit ordinal. A β-r.e. set is l-finite iff all its β-r.e. subsets are β-recursive. The l-finite sets correspond to the ideal of finite sets in the lattice of r.e. sets. We give a characterization of l-finite sets in terms of their ordertype: a β-r.e. set is l-finite iff it has ordertype less than β*, the Σ1, projectum of β).

We define the notion of generic for an arbitrary subgroup H of a stable group, and show that H has a definable hull with the same generic properties. We then apply this to the theory of stable fields.

The lattice of r.e. equivalence relations has not been carefully examined even though r.e. equivalence relations have proved useful in logic. A maximal r.e. equivalence relation has the expected lattice theoretic definition. It is proved that, in every pair of r.e. nonrecursive Turing degrees, there exist maximal r.e. equivalence relations which intersect trivially. This is, so far, unique among r.e. submodel lattices.