In [1] and [2] D. Lewis formulates his counterfactual logic VC as follows. The language contains the connectives ∧, ∨, ⊃, ¬ and the binary connective ≤. A ≤ B is read as “A is at least as possible as B”. The following connectives are defined in terms of ≤.

A < B: = ¬(B ≤ A) (it is more possible that A than that B).

◊ A ≔ ¬(⊥ ≤ A) (⊥ is the false formula; A is possible).

□ A ≔ ⊥ ≤ ¬A (A is necessary).

(if A were the case, then B would be the case).

(if A were the case, then B might be the case).

and are two counterfactual conditional operators. (AB) iff ¬(A ¬B).

The following axiom system VC is presented by D. Lewis in [1] and [2]: V: (1) Truthfunctional classical propositional calculus.

Ehrenfeucht and Mostowski [3] introduced the notion of indiscernibles and proved that every first order theory has a model with an infinite set of order indiscernibles. Since their work, techniques involving indiscernibles have proved to be extremely useful for constructing models with various specialized properties. In this paper and in a sequel [5], we investigate the effective content of Ehrenfeucht's and Mostowski's result. In this paper we consider the question of which decidable theories have decidable models with infinite recursive sets of indiscernibles. In §1, using some basic facts from stability theory, we show that certain large classes of decidable theories have decidable models with infinite recursive sets of indiscernibles. For example, we show that every ω-stable decidable theory and every stable theory which possesses a certain strong decidability property called ∃Q-decidability have such models. In §2 we construct several examples of decidable theories which have no decidable models with infinite recursive sets of indiscernibles. These examples show that our hypothesis for our positive results in §1 are necessary. Finally in §3 we give two applications of our results. First as an easy application of our results in §1, we show that every ω-stable decidable theory has uncountable models which realize only recursive types. Also our counterexamples in §2 allow us to answer negatively two questions of Baldwin and Kueker [1] concerning the effectiveness of their elimination of Ramsey quantifiers for certain theories.

In [5], we show that in general the problem of finding an infinite set of indiscernibles in a decidable model is recursively equivalent to finding a path through a recursive infinite branching tree. Similarly, we show that the problem of finding an co-type of a set of indiscernibles in a decidable ω-categorical theory is recursively equivalent to finding a path through a highly recursive finitely branching tree.

We characterize the ordinals α of uncountable cofinality such that α is the standard part of a nonstandard model of ZFC (or equivalently KP).

Let ZF denote Zermelo-Fraenkel set theory (without the axiom of choice), and let M be a countable transitive model of ZF. The method of forcing extends M to another model M[G] of ZF (a “generic extension”). If the axiom of choice holds in M it also holds in M[G], that is, the axiom of choice is preserved by generic extensions. We show that this is not true for many weak forms of the axiom of choice, and we derive an application to Boolean toposes.

We start with the framework upon which this paper is based. The most useful reference for these notions is [2]. For any nonempty index set I and any proper filter D on S(I) (the power set of I), we denote by I/D the reduced power of modulo D as defined in [2, pp. 167–169]. The first-order language associated with I/D will always be the same language as associated with . We denote the 2-element Boolean algebra 〈{0, 1}, ⋂, ⋃, c, 0, 1〉 by 2 and 2I/D denotes the reduced power of it modulo D. We point out the intimate connection between the structures I/D and 2I/D given in [2, pp. 341–345]. Moreover, we assume as known the definition of Horn formula and Horn sentence as given in [2, p. 328] along with the fundamental theorem that φ is a reduced product sentence iff φ is provably equivalent to a Horn sentence [2, Theorem 6.2.5/ (iff φ is a 2-direct product sentence and a reduced power sentence [2, Proposition 6.2.6(ii)]). For a theory T(any set of sentences), ⊨ T denotes that is a model of T.

In addition to the above we assume as known the elementary characteristics (due to Tarski) associated with a complete theory of a Boolean algebra, and we adopt the notation 〈n, p, q〉 of [3], [10], or [6] to denote such an elementary characteristic or the corresponding complete theory. We frequently will use Ershov's theorem which asserts that for each 〈n, p, q〉 there exist an index set I and filter D such that 2I/D ⊨ 〈n, p, q〉 [3] or [2, Lemma 6.3.21].

Cette note est une suite à mon article Théories instables, this Journal, vol. 46 (1981), pp. 513–522. Quand il en a eu pris connaissance, Saharon Shelah–et c'est remplir un devoir agréable que de lui témoigner ici ma reconnaissance pour l'intérêt qu'il porte à mes travaux–m'a fait savoir qu'il pouvait en simplifier les résultats, et a publié le Théorème 1 de ce post-scriptum, pour le cas des cohéritiers, dans les “added in proof” de son Simple unstable théories, Annals of Mathematical Logic, vol. 19 (1980), pp. 177–203, plusieurs mois avant que ne paraisse l'article qu'il améliore. On verra ici que ce théorème se généralise sans problème aux fils spéciaux, et que son corollaire, le Théorème 2, représente un net progrès sur mon résultat original, puisqu'il est à la fois plus général, plus précis, et obtenu à moindre frais, le lemme sur les ultrafiltres devenant inutile.

Quelques rappels pour commencer: je considère une théorie complète T, sans propriété d'indépendance; cela signifie que toute suite … ai … indicernable dans l'ordre est insécable, c'est-à-dire qu'il ne peut exister de formule f(x, ȳ) et de paramètres tels que f(ai, ) soit vraie cofinalement, et fausse cofinalement, dans la suite; cela signifie encore que cette suite s est découpée par la formule f(x, ) en un nombre fini de segments S1, …, Sk, la formule prenant la même valeur de vérité dans chaque segment, et des valeurs opposées dans des segments consécutifs; ce nombre k de segments sera appelé nombre d'alternance de la formule f(x, ) sur la suite s. On remarquera que, par compacité, ce nombre d'alternance est majoré en fonction seulement de f(x, ȳ).

In [10] Friedman showed that (-AC) is a conservative extension of (-CA)<ε0 for -sentences where i = min(n + 2, 4), i.e., i = 2, 3, 4 for n = 0, 1, 2 + m. Feferman [5], [7] and Tait [11], [12] reobtained this result for n = 0, 1 and even with (-DC) instead of (-AC). Feferman and Sieg established in [9] the conservativeness of (-DC) over (-CA)<ε0 for -sentences (i as above) for all n. In each paper, different methods of proof have been used. In particular, Feferman and Sieg showed how to apply familiar proof-theoretical techniques by passing through languages with Skolem functionals.

In this paper we study the same choice principles in the presence of the Bar Rule (BR), which permits one to infer the scheme of transfinite induction on a primitive recursive relation ≺ when it has been proved that ≺ is wellfounded. The main result (Theorem 1 below) characterizes (-DC) + (BR) as a conservative extension of a system of the autonomously iterated -comprehension axiom for -sentences (i depending on n as above). For n = 0 this has been proved by Feferman in the form that (-DC) + (BR) is a conservative extension of (-CA)<Γ0; this was first done in [8] by use of the Gödel functional interpretation for the stronger system Zω + μ + (QF-AC) + (BR) and then more recently by the simpler methods of [9]. Jäger showed how the latter methods could also be used to obtain the general result of Theorem 1 below.

This paper has three parts. In this first part, we formulate and prove from V = L a new combinatorial principle, ⋄++. In the second part, we discuss the topological problem which led to the formulation of ⋄++. Finally, we use ⋄++ to construct a space solving the topological problem.

The following rough summary is intended to give the non-specialist in fine-structure an idea of what core models are and what they are used for. References are usually given to proofs but very few proofs are given. Also attribution of results is rather careless: I hope to give full historical notes in a forthcoming more detailed exposition.

Jensen is certainly responsible for the bulk of these results. This paper is based in part on a lecture he gave in Oxford in 1979, and my warmest thanks are due to him for his patient explanations of these results. (I should add that he has not seen this paper in proof and should not be held responsible for any false claims which it contains.) Mitchell has been the main driving force behind the generalisations of K, and his influence on the results in §5 is perhaps not adequately reflected there. The language of “hypermeasures” has been replaced here by “extenders”, but the reader of [14] will find translation easy.

Graeme Forbes, Robin Gandy, Wilfrid Hodges and the referee read the paper in proof and I am most grateful for their many suggested improvements.

Definition 1 (Kurepa [3, p. 99]). Let E be a partially ordered set. Then σE denotes the set of all bounded well-ordered subsets of E. We consider σE as a partially ordered set with ordering defined as follows: st if and only if s is an initial segment of t.

Then σE is a tree, i.e., {s ∈ σ E∣ st} is well-ordered for every t ∈ σE. The trees of the form αE were extensively studied by Kurepa in [3]–[10]. For example, in [4], he used σQ and σR to construct various sorts of Aronszajn trees. (Here Q and R denote the rationals and reals, respectively.) While considering monotone mapping between some kind of ordered sets, he came to the following two questions several times:

P.1. Does there exist a strictly increasing rational function on σQ? (See [4, Problème 2], [5, p. 1033], [6, p. 841], [7, Problem 23.3.3].)

P.2. Let T be a tree in which every chain is countable and every level has cardinality <2ℵ0. Does there exist a strictly increasing real function on T? (See [6, p. 246] and [7].)

It is known today that Problem 2 is independent of the usual axioms of set theory (see [1]). Concerning Problem 1 we have the following.

There are several ways for a formula to be “the contrary” of a thesis. When there is a negation we could call a formula an “antithesis” if it is the negation of a thesis—or its negation is a thesis—both properties being equivalent when the negation is classical.

When there is no negation or when the connective called “negation” is very different from classical negation, we are forced to look for a different notion.

Whence:

Definition 1. In a propositional calculus, a substitution antithesis—or, for short, an s-antithesis—is a formula no instance of which is a thesis.

There is another kindred notion, but only for calculi for which a deducibility has been defined:

Definition 2. A deduction antithesis—for short, a d-antithesis—is a formula from which every formula is deducible.

Both notions have been used in the study of the deducibility of certain systems (see below, §4).

In the classical propositional calculus, the s-antitheses are simply the formulas which are negations of theses (and whose negations are theses).

In S5 and in all the weaker modal propositional calculi, there are s-antitheses which are not negations of theses (and whose negations are not theses); typical examples are ¬(Mp ⊃ Lp) and ¬(p ⊃ Lp) where p is a propositional variable, and ⊃, ¬, M and L are respectively material implication, negation, possibility and necessity (see [8]).

In this paper we continue the study of the structure of the lattice of recursively enumerable (r.e.) open subsets of a topological space. Work in this approach to effective topology began in Kalantari and Retzlaff [5] and continued in Kalantari [2], Kalantari and Leggett [3] and Kalantari and Remmel [4]. Studies in effectiveness of results in structures other than integers began with the work of Specker [17] and Lacombe [8] on effective analysis.

The renewed activity in the study of the effective content of mathematical structures owes much to Nerode's program and Metakides' and Nerode's [11], [12] work on vector spaces and fields. These studies have been extended by Kalantari, Remmel, Retzlaff, Shore and Smith. Similar studies on the effective content of other mathematical structures have been conducted. These include work on topological vector spaces, boolean algebras, linear orderings etc.

Kalantari and Retzlaff [5] began a study of effective topological spaces by considering a topological space with a countable basis ⊿ for the topology. The space X is to be fully effective; that is, the basis elements are coded into ω and the operations of intersection of basis elements and the relation of inclusion among them are both computable. An r.e. open subset of X is then represented as the union of basic open sets whose codes lie in an r.e. subset of ω.

The modern problem of infinity was first raised by Aristotle who held (at least on the popular interpretation) that infinite sets exist potentially (i.e. one more number can always be counted, one more division can always be made in a line segment) but not actually (i.e. the numbers or divisions cannot all exist at one time). In fact, Aristotle not only held that completed infinities never actually exist, but also that they are impossible, that is, that the assumption that they do exist leads to contradictions. To see this, consider Aristotle's view that mathematical entities depend for their existence on the existence of primary substance in which they inhere, coupled with his view that there can be no infinite body. From these it follows that if there were actual completed infinities, infinite bodies would both exist and not exist. The details here are not so important as the idea that if a completed infinite is assumed to exist a contradiction follows.

This negative attitude towards completed infinities flourished for centuries. By the mid-1500's, the German mathematician Stifel (who apparently also invented Pascal's triangle) was moved to condemn irrational numbers simply by their association with the completed infinite:

About a hundred years later, Galileo further discredited the completed infinite by pointing out that line segments of different lengths can be brought into one-to-one correspondence by projection, as can the natural numbers and the perfect squares by assigning each number to its square.

We show that all QE rings of prime power characteristic are constructed in a straightforward way out of three components: a filtered Boolean power of a finite field, a nilpotent Jacobson radical, and the ring Zp. or the Witt ring W2(F4) (which is the characteristic four analogue of the Galois field with four elements).

A model M (of a countable first order language) is said to be finitely generated if it is prime over a finite set, namely if there is a finite tuple ā in M such that (M, ā) is a prime model of its own theory. Similarly, if A ⊂ M, then M is said to be finitely generated overA if there is finite ā in M such that M is prime over A ⋃ ā. (Note that if Th(M) has Skolem functions, then M being prime over A is equivalent to M being generated by A in the usual sense, that is, M is the closure of A under functions of the language.) We show here that if N is ā model of an ω-stable theory, M ≺ N, M is finitely generated, and N is finitely generated over M, then N is finitely generated. A corollary is that any countable model of an ω-stable theory is the union of an elementary chain of finitely generated models. Note again that all this is trivial if the theory has Skolem functions.

The result here strengthens the results in [3], where we show the same thing but assuming in addition that the theory is either nonmultidimensional or with finite αT. However the proof in [3] for the case αT finite actually shows the following which does not assume ω-stability): Let A be atomic over a finite set, tp(ā / A) have finite Cantor-Bendixson rank, and B be atomic over A ⋃ ā. Then B is atomic over a finite set.

Our results concern the existence of a countable extension of the countable atomless Boolean algebra such that is a “nonconstructive” extension of . It is known that for any fixed admissible indexing φ of there is a countable nonconstructive extension of (relative to φ). The main theorem here shows that there exists an extension of such that for any admissible indexing φ of , is nonconstructive (relative to φ).Thus, in this sense a countable totally nonconstructive extension of .

Notations, conventions, and definitions. {μi∣i < ω} will be an effective enumeration of all partial recursive μi{ω → 2. A type of a theory T will be a set of formulas in the language of T, in finitely many free variables, which is consistent with T. A complete type is a maximal type in some fixed number of free variables. A type is recursive if, relative to some effective enumeration of the formulas of the language, the characteristic function for the type is recursive. A set ψ of recursive types has property P if some set of indices of characteristic functions for all the types in ψ has property P. So, for example, we might say that a set of recursive types is . If is an L-structure, then the type spectrum of , denoted ‘TySp()’, is the set of complete types realized in (we will assume that an n-type has formulas with free variables among {x1, …, xn}). A type spectrum for a theory T is a type spectrum of some model of T. ‘TySp0(T)’ will denote the set of principal types of T.

We will assume that the reader is familiar with Henkin constructions of models, and of passing from a maximal consistent set of sentences, with “Henkin constants”, to a model. In particular, for a theory T in L we will let {ai∣i < ω} be new distinct constant symbols, and {φi < ω} a list of all sentences in the expanded language. ‘ΔN’ will denote the elementary diagram constructed at stage N, and .

By induction for a formula φ we mean the schema

(where the terms in brackets are implicitly substituted for some fixed variable, with the usual restrictions). Let be the schema IAφ for φ in Πn (i.e. ); similarly for . Each instance of is Δn+2, and each instance of is Σn+1 Thus the universal closure of an instance α is Πn+2 in either case. Charles Parsons [72] proved that and are equivalent over Z0, where Z0 is essentially Primitive Recursive Arithmetic augmented by classical First Order Logic [Parsons 70].

Theorem. For each n > 0 there is a Πn formula π for whichis not derivable in Z0from

(i) true Πn+1sentences; nor even

(ii) Πn+1sentences consistent withZ0.

Let α be an admissible ordinal. An α-recursively enumerable set H is hyper-hypersimple (hh-simple) if its lattice of α-r.e. supersets forms a Boolean algebra. In [3], Chong and Lerman characterized the class ℋ() of hh-simple -r.e. sets as precisely those -r.e. sets whose complements are unbounded and of order type less than . Perhaps a nice example of such a set is {σ∣σ is not for any n < ω}. It follows that all hh-simple sets in are nonhyperregular and therefore of degree 0′. That ℋ() is a natural class to study can be seen from the role played by its ω-counterpart in the study of decision problems and automorphisms of ℰ*(ω), the lattice of ω-r.e. sets modulo finite sets (Soare [13] gives an extensive literature on these topics). In α-recursion theory the existence of hh-simple sets is not an all pervasive phenomenon, and there is as yet no complete characterization of the admissible ordinal α for which ℋ(α) is nonempty. While this situation is admittedly unsatisfactory, we feel that the lattice ℰ*(α) of α-r.e. sets modulo α*-finite sets for which ℋ(α) ≠ ∅ deserves a careful study. Indeed armed with some understanding over the last few years of the general theory of admissible ordinals, it is tempting to focus one's attention on some specific ordinals whose characteristics admit a more detailed analysis of the fine structure of sets and degrees. From this point of view, and ℋ() are natural objects of study since the former is a typical example of a non-Σ2-projectible, Σ2-inadmissible ordinal, while the latter is important for the investigations of automorphisms over ℰ*().

It is well known that for all recursively enumerable sets X1, X2 there are disjoint recursively enumerable sets Y1 ⊆ Y2 such that Y ⊆ X1, Y2 ⊆ X2 and Y1, ⋃ Y2 = X1 ⋃ X2. Alistair Lachlan called distributive lattices satisfying this property separated. He proved that the first-order theory of finite separated distributive lattices is decidable. We prove here that the first-order theory of all separated distributive lattices is undecidable.