It is shown that the boolean prime ideal theorem BPIT: every boolean algebra has a prime ideal, does not follow from the order-extension principle OE: every partial ordering can be extended to a linear ordering. The proof uses a Fraenkel–Mostowski model, where the family of atoms is indexed by a countable universal-homogeneous boolean algebra whose boolean partial ordering has a ‘generic’ extension to a linear ordering. To illustrate the technique for proving that the order-extension principle holds in the model we also study Mostowski's ordered model, and give a direct verification of OE there. The key technical point needed to verify OE in each case is the existence of a support structure.

The notion of o-minimality was formulated by Pillay and Steinhorn [PS] building on work of van den Dries [D]. Roughly speaking, a theory T is o-minimal if whenever M is a model of T then M is linearly ordered and every definable subset of the universe of M consists of finitely many intervals and points. The theory of real closed fields is an example of an o-minimal theory.

We examine the structure of the countable models for T, T an arbitrary o-minimal theory (in a countable language). We completely characterize these models, provided that T does not have 2 ω countable models. This proviso (viz. that T has fewer than 2 ω countable models) is in the tradition of classification theory: given a cardinal α, if T has the maximum possible number of models of size α, i.e. 2 α , then no structure theorem is expected (cf. [Sh1]).

O-minimality is introduced in §1. §1 also contains conventions and definitions, including the definitions of cut and noncut. Cuts and noncuts constitute the nonisolated types over a set.

In §2 we study a notion of independence for sets of nonisolated types and the corresponding notion of dimension.

In §3 we define what it means for a nonisolated type to be simple. Such types generalize the so-called “components” in Pillay and Steinhorn's analysis of ω-categorical o-minimal theories [PS]. We show that if there is a nonisolated type which is not simple then T has 2 ω countable models.

The purpose of the following is to give an ordinal analysis of bar recursion of type 0 for the cases in which the bar recursion operator has type level 3 or 4. We show that the associated ordinals are the ε0th epsilon number and the first ε0-critical number, respectively. Also we analyze a restricted bar recursion operator of level 3 which provides the Gödel functional interpretation of an intuitionistic form of König's lemma. The ordinal in this case is ε0.

Let + BR0 be Gödel's theory of primitive recursive functional of finite type extended by functors Φ for bar recursion of type zero. To make bar recursion resemble transfinite recursion more closely, and thereby facilitate the ordinal analysis, we extend + BR0 to a system of terms . By Theorem 1.1a term of + BR0 which is computable by the rules of is already computable by the rules of + BR0, so it is sufficient to give an ordinal analysis of the terms of .

A term H of is said to be semi-closed if its free variables have level not exceeding 1. If, in addition, H has level not exceeding 2, then an ordinal measure for H is given by a length for one of its computation trees. We call this a computation size for H. Let F(X) be a term whose free variables have level not exceeding 2, and suppose the variable X of type 2 is the only free variable of level 2.

This paper deals with: (i) the theory which results from by restricting induction on the natural numbers to formulas which are positive in the fixed point constants, (ii) the theory BON(μ) plus various forms of positive induction, and (iii) a subtheory of Peano arithmetic with ordinals in which induction on the natural numbers is restricted to formulas which are Σ in the ordinals. We show that these systems have proof-theoretic strength φω0.

Le rêve secret de tout logicien, c’est de prouver un résultat mathématique significatif avec des moyens de fortune; ce rêve se réalise parfois de manière quelque peu biaisée, le théorème obtenu n’étant qu’une version trop simplifiée, ou bien trop adaptée aux besoins de la logique, pour convaincre un mathématicien normal. C’est pour cela que j’annonce d’emblée la couleur, et que je précise les règles du jeu: la version du théorème de Borel-Tits que je vais montrer, concernant les groupes algébriques simples sur un corps de base algébriquement clos, sera considérée comme pratiquement évidente par un géomètre; mais c’est, à mon avis, la seule qui ait un intérêt pour un théoricien des modèles.

Quand on entreprend ainsi de redémontrer une version simple d’un résultat par ailleurs bien connu, le seul intérêt est dans la méthode: ce que je veux, ici, c’est présenter une preuve qui n’utilise aucune information, ou presque, sur la structure algébrique de ces groupes; il est même souhaitable d’oublier qu’il s’agit de groupes linéaires! Elle repose sur des résultats généraux concernant les groupes de rang de Morley fini, dus à divers auteurs, dont le principal, Boris Iosifovič Zil′ber, a déjà fait une tentative similaire [Zil′ber 1984]; je poursuis ici cette tentative, mais en me limitant à des arguments encore moins spécifiques au contexte de la géométrie.

Si je fais ainsi, ce n’est pas pour donner l’impression que l’unique ambition de la théorie des modèles est de montrer des résultats triviaux par des méthodes triviales.

Krull [4] extended Galois theory to arbitrary normal extensions, in which the Galois groups are precisely the profinite groups (i.e. totally disconnected, compact, Hausdorff groups). Metakides and Nerode [7] produced two recursively presented algebraic extensions K ⊂ F of the rationals such that F is abelian, F is of infinite degree over K, and the Galois group of F over K, although of cardinality c, has only one recursive element (viz. the identity). This indicated the limits of effectiveness for Krull's theory. (The Galois theory of finite extensions is completely effective.) Nerode suggested developing a natural effective version of Krull's theory (done here in §1).

It is evident from the classical literature that the free profinite group on denumerably many generators can be obtained effectively as the Galois group of a recursive extension of the rationals over a subfield. Nerode conjectured that it could be obtained effectively as the Galois group of the algebraic numbers over a suitable subfield (done here in §2). The case of finitely many generators was done non-effectively by Jarden [3]. The author believes that the denumerable case, as presented in §2, is also new classically. Using this result and the effective Krull theory, every “co-recursively enumerable” profinite group is effectively the Galois group of a recursively enumerable field of algebraic numbers over a recursive subfield.

We prove several independence results relevant to an old question in the folklore of set theory. These results complement those in [Sh, Chapter XIII, §4]. The question is the following. Suppose V ⊨ “ZFC + CH” and r is a real not in V. Must V[r] ⊨ CH? To avoid trivialities assume = .

We answer this question negatively. Specifically we find pairs of models (W, V) such that W ⊨ ZFC + CH, V = W[r], r a real, = and V ⊨ ¬CH. Actually we find a spectrum of such pairs using ZFC up to “ZFC + there exist measurable cardinals”. Basically the nicer the pair is as a solution, the more we need to assume in order to construct it.

The relevant results in [Sh, Chapter XIII] state that if a pair (of inner models) (W, V) satisfies (1) and (2) then there is an inaccessible cardinal in L; if in addition V ⊨ 2ℵ0 > ℵ2 then 0# exists; and finally if (W, V) satisfies (1), (2) and (3) with V ⊨ 2ℵ0 > ℵω, then there is an inner model with a measurable cardinal.

Definition 1. For a pair (W, V) we shall consider the following conditions:

(1) V = W[r], r a real, = , W ⊨ ZFC + CH but CH fails in V.

(2) W ⊨ GCH.

(3) W and V have the same cardinals.

We show that given ω many supercompact cardinals, there is a generic extension in which there are no Aronszajn trees at ℵω+1· This is an improvement of the large cardinal assumptions. The previous hypothesis was a huge cardinal and ω many supercompact cardinals above it, in Magidor–Shelah [7].

The aim of this note is to determine whether certain non-o-minimal expansions of o-minimal theories which are known to be NIP, are also distal. We observe that while tame pairs of o-minimal structures and the real field with a discrete multiplicative subgroup have distal theories, dense pairs of o-minimal structures and related examples do not.

We show that metric abstract elementary classes (mAECs) are, in the sense of [15], coherent accessible categories with directed colimits, with concrete ℵ1-directed colimits and concrete monomorphisms. More broadly, we define a notion of κ-concrete AEC—an AEC-like category in which only the κ-directed colimits need be concrete—and develop the theory of such categories, beginning with a category-theoretic analogue of Shelah’s Presentation Theorem and a proof of the existence of an Ehrenfeucht–Mostowski functor in case the category is large. For mAECs in particular, arguments refining those in [15] yield a proof that any categorical mAEC is μ-d-stable in many cardinals below the categoricity cardinal.

We see far away, Newton said, if we stand on giants' shoulders. We take him seriously here and moreover (as appropriate to recursion-theorists) we will jump from one giant to another, since this paper is mostly an exegesis of two fundamental works: Feferman's Some applications of the notions of forcing and generic sets [4] and Sacks' Forcing with perfect closed sets [19]. We hope the reader is not afraid of heights: our exercises are risky ones, since the two giants are in turn on the shoulders of others! Feferman [4] rests on the basic works of Cohen [2], who introduced forcing with finite conditions in the context of set theory; Sacks [19] relies on Spector [24], who realized—in recursion theory—the necessity of more powerful approximations than the finite ones.

To minimize the risk we will try to keep technicalities to a minimum, choosing to give priority to the methodology of forcing. We do not suppose any previous knowledge of forcing in the reader, but we do require some acquaintance with recursion theory. After all, our interest lies in the applications of the forcing method to the study of various recursion-theoretic notions of degrees. The farther we go, the deeper we plunge into recursion theory.

In Part I only very basic notions and results are used, like the definitions of the arithmetical hierarchy and of the jump operator and their relationships.

We investigate extensions of S. Solecki's theorem on closing off finite partial isometries of metric spaces [11] and obtain the following exact equivalence: any action of a discrete group Γ by isometries of a metric space is finitely approximable if and only if any product of finitely generated subgroups of Γ is closed in the profinite topology on Γ.

In this paper we give relational semantics and an accompanying relational proof theory for full Lambek calculus (a sequent calculus which we denote by FL). We start with the Kripke semantics for FL as discussed in [11] and develop a second Kripke-style semantics, RelKripke semantics, as a bridge to relational semantics. The RelKripke semantics consists of a set with two distinguished elements, two ternary relations and a list of conditions on the relations. It is accompanied by a Kripke-style valuation system analogous to that in [11]. Soundness and completeness theorems with respect to FL hold for RelKripke models. Then, in the spirit of the work of Orlowska [14], [15], and Buszkowski and Orlowska [3], we develop relational logic RFL. The adjective relational is used to emphasize the fact that RFL has a semantics wherein formulas are interpreted as relations. We prove that a sequent Γ → α in FL is provable if and only if a translation, t(γ1 ● … ● γn ⊃ α)ευu, has a cut-complete fundamental proof tree. This result is constructive: that is, if a cut-complete proof tree for t(γ1 ● … ● γn ⊃ α)ευu is not fundamental, we can use the failed proof search to build a relational countermodel for t(γ1 ● … ● γn ⊃ α)ευu and from this, build a RelKripke countermodel for γ1 ● … ● γn ⊃ α. These results allow us to add FL, the basic substructural logic, to the list of those logics of importance in computer science with a relational proof theory.

Although Peano's arithmetic can be developed in set theories, it can also be developed independently. This is also true for the theory of ordinal numbers. The author formalized the theory of ordinal numbers in logical systems GLC (in [2]) and FLC (in [3]). These logical systems which contain the concept of ‘arbitrary predicates’ or ‘arbitrary functions’ are of higher order than the first order predicate calculus with equality. In this paper we shall develop the theory of ordinal numbers in the first order predicate calculus with equality as an extension of Peano's arithmetic. This theory will prove to be easy to manage and fairly powerful in the following sense: If A is a sentence of the theory of ordinal numbers, then A is a theorem of our system if and only if the natural translation of A in set theory is a theorem of Zermelo-Fraenkel set theory. It will be treated as a natural extension of Peano's arithmetic. The latter consists of axiom schemata of primitive recursive functions and mathematical induction, while the theory of ordinal numbers consists of axiom schemata of primitive recursive functions of ordinal numbers (cf. [5]), of transfinite induction, of replacement and of cardinals. The latter three axiom schemata can be considered as extensions of mathematical induction.

In the theory of ordinal numbers thus developed, we shall construct a model of Zermelo-Fraenkel's set theory by following Gödel's construction in [1]. Our intention is as follows: We shall define a relation α ∈ β as a primitive recursive predicate, which corresponds to F′ α ε F′ β in [1]; Gödel defined the constructible model Δ using the primitive notion ε in the universe or, in other words, using the whole set theory.

We show that every infinite computable partial ordering has either an infinite chain or an infinite antichain. Our main result is that this cannot be improved: We construct an infinite computable partial ordering that has neither an infinite chain nor an infinite antichain.

Introduction. This paper contains a new proof of the Church-Rosser theorem for the typed λ-calculus, which also applies to systems with infinitely long terms.

The ordinary proof of the Church-Rosser theorem for the general untyped calculus goes as follows (see [1]). If is the binary reduction relation between the terms we define the one-step reduction 1 in such a way that the following lemma is valid.

Lemma. For all terms a and b we have: ab if and only if there is a sequence a = a0, …, an = b, n ≥ 0, such that aiiai + 1for 0 ≤ i < n.

We then prove the Church-Rosser property for the relation 1 by induction on the length of the reductions. And by combining this result with the above lemma we obtain the Church-Rosser theorem for the relation .

Unfortunately when we come to infinite terms the above lemma is not valid anymore. The difficulty is that, assuming the hypothesis for the infinitely many premises of the infinite rule, there may not exist an upper bound for the lengths n of the sequences ai = a0, …, an = bi (i < α); cf. the infinite rule (iv) in §6.

A completely new idea in the case of the typed λ-calculus would be to exploit the type structure in the way Tait did in order to prove the normalization theorem. In this we succeed by defining a suitable predicate, the monovaluedness predicate, defined over the type structure and having some nice properties. The key notion permitting to define this predicate is the notion of I-form term (see below). This Tait-type proof has a merit, namely that it can be extended immediately to the case of infinite terms.

In this paper T will always be a countable ℵ0-stable theory, and in this introduction a model of T will mean a countable model.

One of the main notions we introduce is that of almost homogeneous model: we say that a model M of T is almost homogeneous if for all ā and finite sequences of elements in M, if the strong type of ā is the same as the strong type of (i.e. for all equivalence relations E, definable over the empty set and with a finite number of equivalence classes, ā and are in the same equivalence class), then there is an automorphism of M taking ā to . Although this is a weaker notion than homogeneity, these models have strong properties, and it can be seen easily that the Scott formula of any almost homogeneous model is in L1. In fact, Pillay [Pi.] has shown that almost homogeneous models are characterized by the set of types they realize.

The motivation of this research is to distinguish two classes of ℵ0-Stable theories:

(1) theories such that all models are almost homogeneous;

(2) theories with 2ℵ0 nonalmost homogeneous models.

The example of theories with Skolem functions [L. 1] (almost homogeneous is then equivalent to homogeneous) seems to indicate a link between these properties and the notion of multidimensionality, and that nonmultidimensional theories are in the first case.

Let us say that a geometric theory T is of presheaf type if its classifying topos is (equivalent to) a presheaf topos. (We adhere to the convention that geometric logic allows arbitrary disjunctions, while coherent logic means geometric and finitary.) Write Mod(T) for the category of Set-models and homomorphisms of T. The next proposition is well known; see, for example, MacLane–Moerdijk [13], pp. 381-386, and the textbook of Adámek–Rosický [1] for additional information:

Proposition 0.1. For a category , the following properties are equivalent:

(i) is a finitely accessible category in the sense of Makkai–Paré [14], i.e., it has filtered colimits and a small dense subcategory of finitely presentable objects

ii) is equivalent to Pts, the category of points of some presheaf topos

(iii) is equivalent to the free filtered cocompletion (also known as Ind-) of a small category .

(iv) is equivalent to Mod(T) for some geometric theory of presheaf type.

Moreover, if these are satisfied for a given , then the —in any of (i), (ii) and (iii)—can be taken to be the full subcategory of consisting of finitely presentable objects. (There may be inequivalent choices of , as it is in general only determined up to idempotent completion; this will not concern us.)

This seems to completely solve the problem of identifying when T is of presheaf type: check whether Mod(T) is finitely accessible and if so, recover the presheaf topos as Set-functors on the full subcategory of finitely presentable models. There is a subtlety here, however, as pointed out (probably for the first time) by Johnstone [10].

This paper is a continuation of our previous work in [12]. The results, and some applications, have been described in the announcement [13]; it may be useful to discuss here, a little more fully, the nature and purpose of this work.

We are concerned basically with three kinds of algorithmic problem: (1) isomorphism problems, (2) “orbit problems”, and (3) “effective generation”.

(1) Isomorphism problems. Here we have a class of algebraic objects of some kind, and ask: is there a uniform algorithm for deciding whether two arbitrary members of are isomorphic? In most cases, the answer is no: no such algorithm exists. Indeed this has been one of the most notable applications of methods of mathematical logic in algebra (see [26, Chapter IV, §4] for the case where is the class of all finitely presented groups). It turns out, however, that when consists of objects which are in a certain sense “finite-dimensional”, then the isomorphism problem is indeed algorithmically soluble. We gave such algorithms in [12] for the following cases:

= {finitely generated nilpotent groups};

= {(not necessarily associative) rings whose additive group is finitely generated};

= {finitely Z-generated modules over a fixed finitely generated ring}.

Combining the methods of [12] with his own earlier work, Sarkisian has obtained analogous results with the integers replaced by the rationals: in [20] and [21] he solves the isomorphism problem for radicable torsion-free nilpotent groups of finite rank and for finite-dimensional Q-algebras.