If T is an isol let D(T) be the least set of isols which contains T and is closed under predecessors and the application of almost recursive combinatorial functions. We find an infinite regressive isol T such that the universal theory (with respect to recursive relations and almost recursive combinatorial functions) of D(T) is the same as that of the nonnegative integers.

Les synthèses nouvelles par le rapprochement de disciplines mathématiques différentes constituent des événements remarquables dans l'histoire des mathématiques. Une telle synthèse semble émerger actuellement du rapprochement de:

(1) La géométrie algébrique sous la forme élaborée par Grothendieck.

(2) La logique formelle.

Le point de contact s'est effectué aux environs de 1970 par W. Lawvere et M. Tierney et l'instrument de rapprochement a été la théorie des catégories, plus particulièrement la théorie des faisceaux. Depuis ce moment, une dialectique incessante imprime un mouvement dynamique à toute une série de recherches qui visent à rapprocher les méthodes suivantes:

(1) Mathématique intuitionniste.

(2) Forcing de Cohen et Robinson.

(3) Logique algébrique.

(4) Géométrie algébrique.

(5) Géométrie différentielle et analytique.

(6) Topologie algébrique: cohomologie, homotopie.

(7) Théorie de Galois.

Certains rapprochements sont dans un stade avancé, d'autres encore embryonnaires: (6) ↔ (3).

La structure centrale qui joue le rôle d'élément provocateur et unificateur est celle de topos. Avant d'être axiomatisée par Lawvere, celle-ci a été étudiée systématiquement par l'école de Grothendieck (voir [1]) et c'est dans le contexte de la géométrie algébrique qu'elle fit son apparition. Dans cet article nous utiliserons cependant la définition de Lawvere telle qu'améliorée par Mikkelsen [12] et Kock [8].

Le but de ce travail est de présenter une version (au sens de la logique formelle) du concept de topos et d'examiner brièvement les rapports entre la théorie des topos, la logique et les mathématiques. Cette version a déjà été exposée par l'un des auteurs lors du Séminaire de Mathématiques Supérieures de l'Université de Montréal, à l'été 1974. Depuis elle a fait l'objet d'une thèse où elle a été améliorée et sa cohérence vérifiée [2]. Des systèmes différents ont été proposés simultanément par Fourman [4] et Coste [3].

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.

The consistency of the Axiom of Determinateness (AD) poses a somewhat problematic question for set theorists. On the one hand, many mathematicians have studied AD, and none has yet derived a contradiction. Moreover, the consequences of AD which have been proven form an extensive and beautiful theory. (See [5] and [6], for example.) On the other hand, many extremely weird propositions follow from AD; these results indicate that AD is not an axiom which we can justify as intuitively true, a priori or by reason of its consequences, and we thus cannot add it to our set theory (as an accepted axiom, evidently true in the cumulative hierarchy of sets). Moreover, these results place doubt on the very consistency of AD. The failure of set theorists to show AD inconsistent over as short a time period as fifteen years can only be regarded as inconclusive, although encouraging, evidence.

On the contrary, there is a great deal of rather convincing evidence that the existence of various large cardinals is not only consistent but actually true in the universe of all sets. Thus it becomes of interest to see which consequences of AD can be proven consistent relative to the consistency of ZFC + the existence of some large cardinal. Earlier theorems with this motivation are those of Bull and Kleinberg [2] and Spector ([14]; see also [12], [13]).

A pointclass is a class of subsets of the Baire space (ωω) closed under inverse images by continuous functions. The dual of a pointclass Γ, denoted is {~A∣ A ∈ Γ}. (Complements are relative to ωω.) If Γ is nonselfdual, i.e. , then let . We say a nonselfdual pointclass Γ has the first separation property, and write Sep(Γ), iff (∀A, B ∈ Γ)(A ⋂ B = ∅ ⇒ (∃C ∈ Δ)(A ⊆ C ∧ B ⋂ = ∅)). The set C is said to separate A and B.

Descriptive set theory abounds in nonselfdual pointclasses Γ, and for the more natural examples of such Γ one can always show by assuming enough determinateness that exactly one of Sep(Γ) and Sep() holds. Van Wesep [2] provides a partial explanation of this fact by showing that, assuming the full axiom of determinateness, one of Sep(Γ) and Sep() must fail for all nonselfdual pointclasses Γ. We shall complete the explanation by showing that one of Sep(Γ) and Sep() must hold.

The axiom of determinateness has other interesting consequences in the general theory of pointclasses. See e.g. [3].

The double nature, both logical and geometrical, of topos theory is one of the most fascinating aspects of this discipline. Consequently, it might be of some interest that an essentially “geometric” fact such as the associated sheaf theorem admits a proof entirely based on methods of categorical logic.

The idea of this proof comes from a previous paper [V], where the same technique was used in the context of Grothendieck topoi. That paper used a generalized notion of forcing which leads directly from classical Tarski semantics in sets to Kripke-Joyal semantics in an arbitrary Grothendieck topos and gives a precise description of the links between the two. On account of this very close relationship, we thus could establish various basic facts on Grothendieck topoi without an extensive use of categorical methods, simply by viewing given subobjects as interpretations of appropriate formulas written in the formal language that had been used all along.

The aim of this paper is to provide an addendum to a paper by Rose with the same title which has appeared in an earlier issue of this Journal [2]. Our new result is:

Theorem. A ring of characteristic zero which admits elimination of quantifiers in the language (0, 1, +, ·) is an algebraically closed field.

This paper continues the study of κ-ultrafilters over a measurable cardinal κ, following the sequence of papers Ketonen [2], Kanamori [1] and Menas [4]. Much of the concern will be with p-point κ-ultrafilters, which have become a focus of attention because they epitomize situations of further complexity beyond the better understood cases, normal and product κ-ultrafilters.

For any κ-ultrafilter D, let iD: V → MD ≃ Vκ/D be the elementary embedding of the universe into the transitization of the ultrapower by D. Situations of U < RKD will be exhibited when iU(κ) < iD(κ), and when iU(κ) = iD(κ). The main result will then be that if the latter case obtains, then there is an inner model with two measurable cardinals. (As will be pointed out, this formulation is due to Kunen, and improves on an earlier version of the author.) Incidentally, a similar conclusion will also follow from the assertion that there is an ascending Rudin-Keisler chain of κ-ultrafilters of length ω + 1. The interest in these results lies in the derivability of a substantial large cardinal assertion from plausible hypotheses on κ-ultrafilters.

It will be shown that system Q of [1], with minor corrections, is free from contradiction and can be strengthened in various ways without destroying its consistency.

By the system C*A will be meant the system that results in place of CA if rule 3.4.10 is omitted in [2] from the rules 3.4 defining PA and RA for an arbitrary class A of equations. We let P*A be the theorems of C*A and R*A be the antitheorems of C*A, just as PA and RA are respectively the theorems and antitheorems of CA in [2]. Similarly Γ* is the class that is defined exactly like the class Γ in 4.18 of [2] except that systems of the form C*A replace those of the form CA. The terminology and conventions of [2] will be assumed in what follows.

Using the methods that were used to show in 5.9 of [2] that CΓ is free from contradiction, it is easy to show that C*A is free from contradiction for every class A of equations. (The fact that rule 3.4.10 is omitted causes the proof of consistency to work even for cases where A is not systematically closed in the sense of 4.11 of [2].)

Just as it was shown in 4.19 of [2] that Γ is systematically closed (in the sense of 4.11 of [2]), so also it clearly can be shown that Γ* is systematically closed. This means, in effect, that the rule of substitution of equals for equals holds in the system C*Γ*.

In this paper I will develop a semantic account for modal logic by considering only the values of sentences (and formulas). This account makes no use of possible worlds. To develop such an account, we must recognize four values. These are obtained by subdividing (plain) truth into necessary truth (T) and contingent truth (t); and by subdividing falsity into contingent falsity (f) and necessary falsity (impossibility: F). The semantic account results from reflecting on these concepts and on the meanings of the logical operators.

To begin with, we shall consider the propositional language L0. The language L0 has (1) infinitely many atomic sentences, (2) the two truth-functional connectives ∼, ∨, and the modal operator □. (Square brackets are used for punctuation.) The other logical expressions are defined as follows:

D1 [A & B] = (def)∼[∼A ∨ ∼ B],

D2 [A ⊃ B] = (def)[∼A ∨ B],

D3 ◊ A =(def)∼□∼A.

I shall use matrices to give partial characterizations of the significance of logical expressions in L0. For negation, this matrix is wholly adequate:

Upon reflection, it should be clear that this matrix is the obviously correct matrix for negation.

In Gabbay [1] it is stated as an open problem whether or not Craig's Theorem holds for the logic of constant domains CD, i.e. for the extension of the intuitionistic predicate calculus, IPC, obtained by adding the schema; . Then in the later article, [2], Gabbay gives a proof of it. The proof given in [2] is via Robinson's (weak) consistency theorem and depends on relatively complicated (Kripke-) model-theoretical constructions developed in [1] (see p. 392 of [1] for a brief sketch of the method). The aim of this note is to show that the interpolation theorem for CD can also be obtained, by simple proof-theoretic methods, from §80 of Kleene's Introduction to Metamathematics [3].

GI is the classical formal system whose postulates are given on p. 442 of [3]. Let GD be the system obtained from GI by the following modifications: (1) the sequents of GD are to have at most two formulas in their succedents and (2) the intuitionistic restriction that Θ be empty is required for the succedent rules (→ ¬) and (→ ⊃). It is a simple matter to show that: , x not free in . It then follows that, using Theorem 46 of [3], if then .

Ever since Cohen invented forcing in 1963, people have studied the properties that cardinals can have in generic extensions of the ground model. A very early result of Lévy shows that if κ is a regular cardinal and λ > κ is strongly inaccessible, then there is a notion of forcing which collapses every cardinal strictly between κ and λ yet preserves every other cardinal. This, of course, answers one question of the genre “What properties can a cardinal have in a generic extension?”

Another question of the same genre that can be asked is the following: Is it possible to have a generic extension of the ground model in which all cardinals are preserved and yet the cofinalities of some cardinals are different? This question was first answered in the affirmative by Prikry, who proved the following theorem.

Theorem 1.1 (Prikry [5]). Assume that V ⊨ “ZFC + κ is measurable”. Then there is a notion of forcing, P, such that for G V-generic over P:

(1) V and V[G] have the same cardinals.

(2) V and V[G] have the same bounded subsets of κ.

(3) V[G], i.e, V[G] ⊨ “κ is Rowbottom”.

(4) V[G] ⊨ “cof(κ) = ω”.

Prikry's result naturally raises the following question: Is it possible to get a generic extension in which cardinals are preserved and yet the cofinalities of certain cardinals are different from the ground model's but are uncountable? This question was first answered in the affirmative by Magidor, who proved the following theorem.

Let α be any countable admissible ordinal greater than ω. There is a transitive set A such that A is admissible, locally countable, OnA = α, and A satisfies Σ1-separation. In fact, if B is any nonstandard model of KP + ∀x ⊆ ω (the hyperjump of x exists), the ordinal standard part of B is greater than ω, and every standard ordinal in B is countable in B, then HCB ∩ (standard part of B) satisfies Σ-separation.

Every ℵ0-categorical partially ordered set of finite width has a finitely axiomatizable theory. Every ℵ0-categorical partially ordered set of finite weak width has a decidable theory. This last statement constitutes a major portion of the complete (with three exceptions) characterization of those finite partially ordered sets for which any ℵ0-categorical partially ordered set not embedding one of them has a decidable theory.

Although Brouwer became famous for his vehement attacks upon classical logic and set theory, his work did not develop in a vacuum and strongly depended on that of Cantor.

His mind bent on shifting aside nonconstructive arguments, he tried to rebuild Cantor's edifice along new, intuitionistic lines. The continuum hypothesis, lying at the core of set theory, also confronted Brouwer, and he had to face the farthest conclusion Cantor had been able to reach in trying to solve it: every nondenumerable closed subset of the real line has the power of the continuum.

Brouwer's thinking about it seems to have been subject to some development. In 1914 we hear him saying: “Wir sahen oben dass das Cantorsche Haupttheorem für den Intuitionisten keines Beweises bedarf” (“As we saw above, for us, being intuitionists, Cantor's Main Theorem does not need a proof”) [3]. Nevertheless, five years later, he publishes an essay: Theorie der Punktmengen, which might be described as an attempt to reconstruct Cantor's reasonings in detail [4].

This attempt was not entirely successful, as Brouwer comes to admit in 1952, probably having lost, now, some of his youthful rashness [10]. So the question of what the constructive content of Cantor's Main Theorem is, still awaits an answer.

We do not think the answer we will give can be considered a conclusive one, but, in any case, it is a beginning.

On sait, depuis les travaux de Zil'ber et de Cherlin, que le degré de Morley de la théorie T d'un groupe G totalement transcendant est l'indice du plus petit sous-groupe définissable d'indice fini de G. Il est clair qu'il lui est supérieur, et l'inégalité inverse peut s'obtenir de la manière suivante: on fait agir G sur les types de S1(G) de rang de Morley maximum en associant à p, type de x au-dessus de G, le type ap de ax au-dessus de G; on montre alors que cette action est définissable, que le fait que ap = q équivaut au fait que a satisfasse une certaine formule à paramètres dans G, ce qui est bien facile si on n'oublie pas que dans une théorie stable tous les types sont définissables; on montre ensuite que cette action est transitive, que si p et q sont de rang de Morley maximum il existe a dans G tel que ap = q, et la méthode la plus rapide, mais qui est aussi la plus sophistiquée, est d'utiliser l'argument de symétrie de la déviation employé dans la preuve de la Proposition 1 de présent article; on conclut alors puisque le degré de Morley, qui est par définition le nombre de types de rang de Morley maximum, ést egal à l'indice du stabilisateur de p, qui est définissable.

Ce comportement des types de rang de Morely maximum se retrouve sans peine, si G est seulement superstable, dans celui des types de “plus petit rang continu” (encore appellé “degré de Shelah”) maximum. Pour trouver ce qui leur correspond dans le cas où G est seulement stable, il faut être un peu plus soigneux, et considérer les types p de S1(G), où G aura éventuellement été remplacé par une extension élémentaire suffisament saturée, tels que pour tout a de G ap ne dévie pas sur ∅: on montre qu'ils existent, et qu'ils sont tous conjugués par action de G; le fait que ap = q s'exprimera cette fois par une infinité de formules et non plus par une seule.

A 2-affable ultrafilter has only finitely many predecessors in the Rudin-Keisler ordering of isomorphism classes of ultrafilters over the natural numbers. If the continuum hypothesis is true, then there is an ℵ1-sequence of ultrafilters Dα such that the strict Rudin-Keisler predecessors of Dα are precisely the isomorphs of the Dβ's for β < α.