One of the basic results in the theory of λ-conversion is the Church-Rosser Theorem, which says that, using certain rules for conversion and reduction of λ-formulae, any two interconvertible formulae can both be reduced to one formula. (I will not explain this in detail, as λ-conversion is described fully in Church's [2], where the Church-Rosser Theorem is Theorem 7 XXVII; see also Chapter 4 of Curry and Feys' [3].) The first part of the present paper contains an abstract form of this theorem.

Indescribability is closely related to the reflection principles of Zermelo-Fränkel set theory. In this axiomatic setting the universe of all sets stratifies into a natural cumulative hierarchy (Vα: α ϵ On) such that any formula of the language for set theory that holds in the universe already holds in the restricted universe of all sets obtained by some stage.

The axioms of ZF prove the existence of many ordinals α such that this reflection scheme holds in the world Vα. Hanf and Scott noticed that one arrives at a large cardinal notion if the reflecting formulas are allowed to contain second order free variables to which one assigns subsets of Vα. For a given collection Ω of formulas in the ϵ language of set theory with higher type variables and a unary predicate symbol they define an ordinal α to be Ω indescribable if for all sentences Φ in Ω and A ⊆ Vα

Since a sufficient coding apparatus is available, this definition is (for the classes of formulas that we are going to consider) equivalent to the one that one obtains by allowing finite sequences of relations over Vα, some of which are possibly k-ary. We will be interested mainly in certain standardized classes of formulas: Let (, respectively) denote the class of all formulas in the language introduced above whose prenex normal form has n alternating blocks of quantifiers of type m (i.e. (m + 1)th order) starting with ∃ (∀, respectively) and no quantifiers of type greater than m. In Hanf and Scott [1961] it is shown that in ZFC, indescribability is equivalent to inaccessibility and indescribability coincides with weak compactness.

Of the several methods for proving the completeness of sets of axioms for the prepositional calculus perhaps the simplest is due to Kalmár, although it does not appear to be widely known. In this paper we generalize Kalmár's method to indicate how to obtain a complete axiomatization of any fragment of the propositional calculus which includes material implication. We shall carry through the description and proofs for the case where, in addition to a symbol for implication, there is just one other primitive truth-function symbol. For systems in which there are no other function symbols, or more than one other such symbol, notational changes but not conceptual changes will be required.

A hyperimaginary is an equivalence class of a type-definable equivalence relation on tuples of possibly infinite length. The notion was recently introduced in [1], mainly with reference to simple theories. It was pointed out there how hyperimaginaries still remain in a sense within the domain of first order logic. In this paper we are concerned with several issues: on the one hand, various levels of complexity of hyperimaginaries, and when hyperimaginaries can be reduced to simpler hyperimaginaries. On the other hand the issue of what information about hyperimaginaries in a saturated structure M can be obtained from the abstract group Aut(M).

In Section 2 we show that if T is simple and canonical bases of Lascar strong types exist in Meq then hyperimaginaries can be eliminated in favour of sequences of ordinary imaginaries. In Section 3, given a type-definable equivalence relation with a bounded number of classes, we show how the quotient space can be equipped with a certain compact topology. In Section 4 we study a certain group introduced in [5], which we call the Galois group of T, develop a Galois theory and make the connection with the ideas in Section 3. We also give some applications, making use of the structure of compact groups. One of these applications states roughly that bounded hyperimaginaries can be eliminated in favour of sequences of finitary hyperimaginaries. In Sections 3 and 4 there is some overlap with parts of Hrushovski's paper [2].

In this paper we prove infinitary analogues of model-theoretic results known for finitary logic. The infinitary language we deal with is Lω1ω which is roughly described by saying that, in addition to the usual formation rules of the lower predicate calculus with identity, also the formation of the conjunction and disjunction of countably many formulas is allowed.

We prove that any tame abstract elementary class categorical in a suitable cardinal has an eventually global good frame: a forking-like notion defined on all types of single elements. This gives the first known general construction of a good frame in ZFC. We show that we already obtain a well-behaved independence relation assuming only a superstability-like hypothesis instead of categoricity. These methods are applied to obtain an upward stability transfer theorem from categoricity and tameness, as well as new conditions for uniqueness of limit models.

We prove that there exists a noncomputable c.e. real which is low for weak 2-randomness, a definition of randomness due to Kurtz, and that all reals which are low for weak 2-randomness are low for Martin-Löf randomness.

We give combinatorial and computational characterizations of the NP search problems definable in the bounded arithmetic theories and .

Let G be a separated (Hausdorff) topological group and let *G be an enlargement of G (see [8]). Thus, *G (i) possesses the same formal properties as G in the sense explained in [8], and (ii) every set of subsets {Aν } of G with the finite intersection property—i.e. such that every nonempty finite subset of {Aν } has a nonempty intersection—satisfies ∩*Aν ≠ ø, where the *Aν are the extensions of the Aν in *G, respectively.

Consider the predicate of natural numbers defined by:

where R is recursive. If, as usual, the variable ƒ ranges over ωω (the set of functions from natural numbers to natural numbers) then this is just the usual normal form for Π11 sets. If, however, ƒ ranges over 2ω (the set of functions from ω into {0, 1}) then every such predicate is recursively enumerable.3 Thus the second type of formula is generally ignored. However, the reduction just mentioned requires proof, and the proof uses some form of the Brower-König Infinity Lemma.

“Apart from merits or defects of PA1, however, its existence demonstrates the feasibility of a new approach to the logic of propositions involving the principle of subjunctive contrariety. We thus have good reason to investigate the effect this principle, and a concept of conditionality compatible with it, might exert if introduced into standard quantification theory, into set theory, into modal logic and into epistemology and the philosophy of science.”

A Boolean algebra (henceforth abbreviated B.A.) is said to be recursive if B is a recursive subset of the natural numbers N and the operations ∧ (meet), ∨ (join), and ¬ (complement) are partial recursive. Let denote the set of atoms of and denote the ideal generated by the atoms of . Given recursive B.A.s and , we write ≈ if is isomorphic to and ≈r if is recursively isomorphic to , i.e., if there is a partial recursive isomorphism from onto .

Recursive B.A.s have been studied by several authors including Ershov [2], Fiener [3], [4], Goncharov [5], [6], [7], LaRoche [8], Nurtazin [7], and the author [10], [11]. This paper continues a study of the recursion theoretic relationships among , , and the recursive isomorphism type of a recursive B.A. we started in [11]. We refer the reader to [11] for any unexplained notation and definitions. In [11], we were mainly concerned with the possible recursion theoretic properties of the set of atoms in recursive B.A.s. We found that even if we insist that be recursive, there is considerable freedom for the properties of . For example, we showed that if is a recursive B.A. such that is recursive and is infinite, then (i) there exists a recursive B.A. such that and both and are recursive and (ii) for any nonzero r.e. degree δ, there exist recursive B.A.s , , … such that for each i, is of degree δ, is recursive, is immune if i is even and is not immune if i is odd, and no two B.A.s in the sequence are recursively isomorphic.

We prove the following Main Theorem: ZF + AD + V ⇒ L(R) ⇒ DC. As a corollary we have that Con(ZF + AD) ⇒ Con(ZF + AD + DC). Combined with the result of Woodin that Con(ZF + AD) ⇒ Con(ZF + AD + ¬ ACω) it follows that DC (as well as ACω) is independent relative to ZF + AD. It is finally shown (jointly with H. Woodin) that ZF + AD + ¬DCR, where DCR is DC restricted to reals, implies the consistency of ZF + AD + DC, in fact implies R# (i.e. the sharp of L(R)) exists.

We investigate extensions of Heyting's predicate calculus (HPC). We relate geometric properties of the trees of Kripke models (see [2]) with schemas of HPC and thus obtain completeness theorems for several intermediate logics defined by schemas. Our main results are:

(a) ∼(∀x ∼ ∼ϕ(x) Λ ∼∀xϕ(x)) is characterized by all Kripke models with trees T with the property that every point is below an endpoint. (From this we shall deduce Glivenko type theorems for this extension.)

(b) The fragment of HPC without ∨ and ∃ is complete for all Kripke models with constant domains.

We assume familiarity with Kripke [2]. Our notation is different from his since we want to stress properties of the trees. A Kripke model will be denoted by (Aα, ≤ 0), α ∈ T where (T, ≤, 0) is the tree with the least member 0 ∈ T and Aα, α ∈ T, is the model standing at the node α. The truth value at α of a formula ϕ(a1 … an) under the indicated assignment at α is denoted by [ϕ(a1 … an)]α.

A Kripke model is said to be of constant domains if all the models Aα, α ∈ T, have the same domain.

Cet article ne contient rien de révolutionnaire, et son auteur a conscience du risque qu'il court de le voir dépassé, lors de sa parution, par des travaux plus profonds. Il a pensé qu'il n'était pas inutile de publier, faute de mieux, les résultats simples auxquels il est parvenu (le lecteur lui saura gré de ce caractère reposant), en espérant qu'il passeront à la postérité sous forme d'exercices dans les manuels futurs où les petits enfants apprendront la théorie des modèles.

Il s'agit de groupes stables; on sait depuis longtemps que la stabilité de la théorie d'un groupe impose des “conditions de chaîne” sur ses sous-groupes définissables : l'exploitation de ce phénomène, de nature bien algébrique, qui est brièvement exposé dans la première section de cet article, a fait le bonheur d'une génération de théoriciens des modèles. Un autre phénomène, plus subtil, semble ne pas avoir épuisé sa substance : c'est celui, dont l'apparition remonte aux travaux de B. Zilber, qui est décrit dans [7] sous le nom de “types de strate maximum”, et dans [2] sous le nom de “large sets”; la deuxième section lui est consacrée: elle a été écrite dans le désir de montrer l'équivalence de ces deux approches, et aussi par repentir de n'avoir pas suffisament éclairé ses motivations dans [7]. Ce souci d'unification a eu une influence, que j'espère salutaire, sur le vocabulaire: je parle ici de “types génériques” et d'“ensembles (ou de formules) génériques”. Ces termes, ainsi que celui de “composante connexe”, sont empruntés au langage de la géométrie: un groupe algébrique, étant définissable dans la théorie d'un corps algébriquement clos, est stable, et ses “types génériques” sont les “points génériques” des géomètres.

The present paper concerns the relation of relative interpretability introduced in [8], and arises from a question posed by Tarski: are there two finitely axiomatizable subtheories of the arithmetic of natural numbers neither of which is relatively interpretable in the other? The question was answered affirmatively (without proof) in [3], and the answer was generalized in [4]: for any positive integer n, there exist n finitely axiomatizable subtheories of arithmetic such that no one of them is relatively interpretable in the union of the remainder. A further generalization was announced in [5] and is proved here: there is an infinite set of finitely axiomatizable subtheories of arithmetic such that no one of them is relatively interpretable in the union of the remainder. Several lemmas concerning the existence of self-referential and mutually referential formulas are given in Section 1, and will perhaps be of interest on their own account.

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.

Attention was directed to modal systems in which ‘necessarily α’ is interpreted as ‘α. is and always will be the case’ by Prior in his John Locke Lectures of 1956. The present paper shows that S4.3, the extension of S4 with

ALCLpLqLCLqLp,

is complete with respect to this interpretation when time is taken to be continuous, and that D, the extension of S4.3 with

ALNLpLCLCLCpLpLpLp,

is complete with respect to this interpretation when time is taken to be discrete. The method employed depends upon the application of an algebraic result of Garrett Birkhoff's to the models for these systems, in the sense of Tarski.

A considerable amount of work on S4.3 and D precedes this paper. The original model with discrete time is given in Prior's [7] (p. 23, but note the correction in [8]); that taking time to be continuous yields a weaker system is pointed out by him in [9]. S4.3 and D are studied in [3] of Dummett and Lemmon, where it is shown that D includes S4.3 and

CLCLCpLpLpCMLpLp.

While in Oxford in 1963, Kripke proved that these were in fact sufficient for D, using semantic tableaux. A decision procedure for S4.3, using Birkhoff's result, is given in my [2]. Dummett conjectured, in a conversation, that taking time to be continuous yielded S4.3. Thus the originality of this paper lies in giving a suitable completeness proof for S4.3, and in the unified algebraic treatment of the systems. It should be emphasised that the credit for first axiomatising D belongs to Kripke.

In [3], Martin computed the degrees of certain classes of RE sets. To state the results succinctly, some notation is useful.

If A is a set (of natural numbers), dg(A) is the (Turing) degree of A. If A is a class of sets, dg ( A ) = {dg(A): A ∈ A ). Let M be the class of maximal sets, HHS the class of hyperhypersimple sets, and DS the class of dense simple sets. Martin showed that dg ( M ), dg ( HHS ), and dg ( DS ) are all equal to the set H of RE degrees a such that a ′ = 0″.

Let M * be the class of coinfinite RE sets having no superset in M ; and define HHS * and DS * similarly. Martin showed that dg ( DS *) = H. In [2], Lachlan showed (among other things) that dg ( M *)⊆K, where K is the set of RE degrees a such that a ″ > 0″. We will show that K ⊆ dg ( HHS *). Since maximal sets are hyperhypersimple, this gives dg ( M *) = dg ( HHS *) = K.

These results suggest a problem. In each case in which dg(A) has been calculated, the set of nonzero degrees in dg(A) is either H or K or the empty set or the set of all nonzero RE degrees. Is this always the case for natural classes A? Natural here might mean that A is invariant under all automorphisms of the lattice of RE sets; or that A is definable in the first-order theory of that lattice; or anything else which seems reasonable.