In a recent series of papers Kanamori ([4], [5], and [6]) defines generalizations of several combinatorial principles known to follow from the existence of morasses. Kanamori proves the consistency of his generalizations by forcing arguments which come close to satisfying the hypotheses of the Martin's Axiom-type characterizations of morasses developed independently by Shelah and Stanley [9] and the author [12]. A similar “almost application” of morasses appears in [11], in which Todorčević uses forcing to prove the consistency of the existence of Kurepa trees with no Aronszajn or Cantor subtrees. In all cases the attempted proofs using morasses fail for the same reason: the partial orders involved do not have strong enough closure properties.

In an attempt to solve this problem Shelah and Stanley strengthened their characterization of morasses to allow applications to what they called “good canonical limit” partial orders. However, for rather subtle reasons even this strengthened forcing axiom is not good enough for the proposed applications. The problem this time is that Shelah and Stanley's “weak commutativity of Lim and restriction” requirement (see [9, 3.9(iv)]) is not satisfied. Furthermore, there is reason to believe that an ordinary morass is just not good enough for these applications, since in L morasses exist at all regular uncountable cardinals, but even a weak form of Todorčević's conclusion cannot hold at ineffable cardinals (see the end of §4).

A possible solution to this problem is suggested by the fact that □κ is equivalent to a forcing axiom which applies to partial orders satisfying precisely the kind of weak closure conditions involved in the examples described above (see [13]). What is needed to make the proposed morass applications work is something which will do for morass constructions what □κ does for ordinary transfinite recursion constructions. In this paper we show how extra structure can be built into a morass to accomplish this goal.

Assume G.C.H. We prove that for singular λ, □λ implies the diamonds hold for many S ⊆ λ+ (including S ⊆ {δ:δ ∈ λ+, cf δ = cf λ}.) We also have complementary consistency results.

§1. A counterexample and preservation of “proper + X”.

Theorem. Suppose V satisfies, , and for some A ⊆ ω1, every B ⊆ ω1, belongs to L[A].

Then we can define a countable support iterationsuch that the following conditions hold:

a) EachQiis proper and ⊩Pi “Qi, has power ℵ1”.

b) Each Qi is -complete for some simple ℵ1-completeness system.

c) Forcing with Pα = Lim adds reals.

Proof. We shall define Qi by induction on i so that conditions a) and b) are satisfied, and Ci, is a Qi-name of a closed unbounded subset of ω1. Let : ξ < ω1› ∈ L[A] be a list of all functions f which are from δ to δ for some δ < ω1 and let h: ω1 → ω1, h ∈ L[A], be defined by h(α) = Min{β: β > α and Lβ[A]⊨ “∣α∣ = ℵ0”}.

Suppose we have defined Qj for every j < i; then Pi is defined, is proper (as each Qj, j < i, is proper, and by III 3.2) and has a dense subset of power ℵ (by III 4.1). Let Gi ⊆ Pi be generic so clearly there is B ⊆ ω1, such that in V[Gi] every subset of ω1 belongs to L[A, B], The following now follows:

Fact. In V[Gi], every countableN ⥽(H(ℵ2), ∈, A, B) is isomorphic toLβ[A ∩ δ, B ∩ δ] for some β < h(δ), where δ = δ(N) = ω1, ∩ N.

We consider extensions of Peano arithmetic suitable for doing some of nonstandard analysis, in which there is a predicate N(x) for an elementary initial segment, along with axiom schemes approximating ω1-saturation. We prove that such systems have the same proof-theoretic strength as their natural analogues in second order arithmetic. We close by presenting an even stronger extension of Peano arithmetic, which is equivalent to ZF for arithmetic statements.

In this paper we show that the propositional logics E of entailment, R of relevant implication and T of ticket entailment are undecidable. The decision problem is also shown to be unsolvable in an extensive class of related logics. The main tool used in establishing these results is an adaptation of the von Neumann coordinatization theorem for modular lattices.

Interest in the decision problem for these systems dates from the late 1950s. The earliest result was obtained by Anderson and Belnap who proved that the first degree fragment of all these logics is decidable. Kripke [11] proved that the pure implicational fragments R→ and E→ of R and E are decidable. His methods were extended by Belnap and Wallace to the implication-negation fragments of these systems [3]; Kripke's methods also extend easily to include the implication-conjunction fragments of R and E. Meyer in his thesis [14] extended the result for R to include a primitive necessity operator. He also proved decidable the system R-mingle, an extension of R, and ortho-R (OR), the logic obtained from R by omitting the distribution axiom. Various weak relevant logics are also known to be decidable by model-theoretic proofs of the finite model property (see Fine [5]). Finally, S. Giambrone [7] has solved the decision problem for various logics obtained by the omission of the contraction axiom (A → ⦁ A → B) → ⦁ A → B, including R+ − W (R+ minus contraction). It is worth noting that even where positive results were obtained, the decision methods were usually of a complexity considerably greater than in the case of other nonclassical logics such as intuitionistic logic or modal logic, a fact which already indicates the difficulty of the decision problem.

E. Specker has proved that the axiom of choice (AC) is false in NF [6]. Since AC is stratified, one can, according to another famous result of Specker [7], prove directly ¬AC in type theory (TT) plus some finite set of ambiguity axioms, i.e. sentences of the form φ ↔ φ+, where φ+ results from φ by adding one to its type indices.

We shall in §2 of this paper give a disproof of AC directly in TT plus some axioms of ambiguity. The argument will be split into two parts. The first one (contained in Proposition 2) concerns cardinal arithmetic and has nothing to do with typical ambiguity. Though carried out in TT, it could have been done in other set theories such as Zermelo's Z or ZF. The second part is an application of this to the cardinals of the universes at different types. This is made possible through the introduction of an appropriate definition of 2α in §1 enabling one to express shifting sentences as “typed properties” of the universe, in Boffa's sense. The disproof of AC is then completed in TT plus two extra ambiguity axioms. In §3, we show that this is in a sense the best possible result: that means that every single ambiguity axiom is consistent with TT plus AC, thus giving a positive solution to a conjecture of Specker [7, p. 119].

This paper is the sequel of “a functorial construction of the Veblen hierarchy” [GV]: it was announced in it.

We define the notion of garden (Definition I.1.6), that is a functorial version of a Bachmann collection: in a garden Jy, at each ordinal x ≤ y, of cofinality Ω, is associated an Ω-flower (Definition I.1.1); we define also the notion of a function compatible with a garden (Definition I.3.3). We construct a hierarchy of functors from Ω to Ω (for each x ≤ y and x ∈ Jy) and for each function (f ∈ I(x, y) compatible with Jy a natural transformation T(f) from to ; we show that, if the garden is Gε Ω + 1 (Definition I.2.1), then, for each ordinal x ≤ εΩ + 1, the hierarchy of functions coincides exactly with the usual hierarchy ψx constructed using the usual Bachmann collection of height εΩ + 1, and founded on composition (that is, ψx + 1 = ψx ˚ ψ1; then, (0) is the usual Howard ordinal. We show also, that for eac x ≤ y, φx is an Ω-flower, and so we can use this hierarchy of functors for ordinal notations: see Chapter II of -logic [G].

The construction made in this article corresponds, essentially, to Chapter V of -logic [G]: the exact connections between these two works will be the matter of a subsequent article.

In [O1], we gave algebraic characterizations of elementary equivalence for finitely generated finite-by-abelian groups, i.e. finitely generated FC-groups. We also provided several examples of finitely generated finite-by-abelian groups which are elementarily equivalent without being isomorphic.

In this paper, we shall use our previous results to describe precisely the models of the theories of finitely generated finite-by-abelian groups and the elementary embeddings between these models.

Let V∞ be a fully effective infinite dimensional vector space over a recursive field F. That is, we assume that the universe of V∞ is a recursive set, the operations of addition and scalar multiplication are recursive, and there is a uniform effective procedure to decide whether any finite set {υ0, …, υn} of vectors from V∞ is independent. The lattice of recursively enumerable subspaces has been extensively studied since its introduction by Metakides and Nerode [MN1] (see for example, [Do2], [Gu], [KR], [Re1], [Re2], and [Sh]). For those unfamiliar with the literature on , we shall give a list of basic definitions required for this paper in §0.

It is well known that complements in V∞ are not unique. For example, in [Re2] Remmel constructed r.e. spaces M1 and M2 and co-r.e. spaces Q1 and Q2 such that for all i, j ∈ {1, 2}, Mi ⊕ Qj = V∞ and M1 is supermaximal, M2 is not maximal, Q1 has a fully extendible basis, and Q2 has no extendible basis. We say a subspace Q of V∞ is fully co-r.e. if Q is generated by a co-r.e. subset of some recursive basis of V∞. Downey [Do2] has shown that every r.e. subspace of V∞ has a complement which is a fully co-r.e. subspace. Moreover suppose Q is any fully co-r.e. subspace, say Q = (C)* where C is a co-r.e. subset of a recursive basis B of V∞; if C is nonrecursive, then it is shown in [Do2] that Q has a decidable complement as well as a nondecidable nowhere simple complement.

A subspace V of an infinite dimensional fully effective vector space V∞ is called decidable if V is r.e. and there exists an r.e. W such that V ⊕ W = V∞. These subspaces of V∞ are natural analogues of recursive subsets of ω. The set of r.e. subspaces forms a lattice L(V∞) and the set of decidable subspaces forms a lower semilattice S(V∞). We analyse S(V∞) and its relationship with L(V∞). We show:

Proposition. Let U, V, W ∈ L(V∞) where U is infinite dimensional andU ⊕ V = W. Then there exists a decidable subspace D such that U ⊕ D = W.

Corollary. Any r.e. subspace can be expressed as the direct sum of two decidable subspaces.

These results allow us to show:

Proposition. The first order theory of the lower semilattice of decidable subspaces, Th(S(V∞), is undecidable.

This contrasts sharply with the result for recursive sets.

Finally we examine various generalizations of our results. In particular we analyse S*(V∞), that is, S(V∞) modulo finite dimensional subspaces. We show S*(V∞) is not a lattice.

One of the most interesting concepts arising from the study of L(V∞), the lattice of r.e. subspaces of a fully effective vector space of infinite dimension (cf. [6], [7] or [10]), was that of a supermaximal subspace. Supermaximal subspaces of V∞ were those with the fewest possible r.e. superspaces, that is, we say M ∈ L(L∞) is supermaximal if dim(V∞/M) = ∞ and for all Q ∈ L(V∞) with Q ⊇ M, either dim(Q/M) < ∞ or Q = V∞. These spaces were particularly interesting because they had no natural analogue in L(ω), the lattice of r.e. sets. Later Metakides and Nerode [8], Baldwin [1] and the author [2] found that supermaximal substructures occurred in more general settings. In particular, they were found to occur in L(F∞), the lattice of r.e. algebraically closed subfields of F∞ (a recursively presented field of infinite transcendence degree) (cf. [3]). The main tool in these later papers was the concept of a Steinitz (closure) system with recursive dependence (cf. [1], [2], [4] or [8]). We assume familiarity with the definitions and basic results of Metakides and Nerode [8], and only give a brief sketch of some nonstandard facts in §2. If the reader is not familiar with Steinitz systems he is advised to either obtain [1] or [2], or simply identify a Steinitz system (U, cl) with (V∞, *), that is, he should identify U with V∞, and cl(A) with A*, the subspace generated by A.

Certain investigations have been made concerning the nature of classes of recursively enumerable sets, and the relation of such classes to the recursively enumerable indices of their sets. For instance, a theorem of Rice [3, Theorem XIV(a), p. 324] states that if A is the complete set of indices for a class of recursively enumerable sets (that is, if there is a class of recursively enumerable sets such that and if A is recursive, then either A = ⌀ or A = ω. A relate theorem by Rice and Shapiro [3, Theorem XIV(b), p. 324] can be stated as follows:

Let be a class of recursively enumerable sets, and let A be the complete set of indices for . Then A is r.e. if and only if there is an r.e. set D of canonical indices of finite sets Du, u ∈ D, such that

A somewhat similar theorem of Yates is the following: Let be a class of recursively enumerable sets which contains all finite sets. Let A be the complete set of indices for . Then there is a uniform recursive enumeration of the sets in if and only if A is recursively enumerable in 0(2)—that is, if and only if A is Σ3. A corollary of this is that if C is any r.e. set such that C(2)≡T⌀(2), there is a uniform recursive enumeration of all sets We such that We ≤TC [9, Theorem 9, p. 265].

The Classification Theorem for ℵ0-categorical strictly minimal sets says that if H is strictly minimal and ℵ0-categorical, either H has in effect no structure at all or is essentially an affine or projective space over a finite field. Zil′ber, in [Z2], showed that if H were a counterexample to this Classification Theorem it would interpret a rank 2, degree 1 pseudoplane. Cherlin later noticed (see [CHL, Appendices 2 and 3], for the proof) that the Classification Theorem is a consequence of the Classification Theorem for finite simple groups. In [Z4] and [Z5], Zil′ber found a quite different proof of the Classification Theorem using no deep group theory.

Meanwhile in [Z3], Zil′ber introduced the notion of envelope in an attempt to prove that no complete totally categorical theory T can be finitely axiomatizable. The idea of the proof was to show that if M is a model of such a T and H ⊆ M is strongly minimal, then an envelope of any sufficiently large finite subset of H is a finite model of any fixed finite subset of T. [Z3] contains an error, which Zil′ber has since corrected (in a nontrivial way).

In [CHL], Cherlin, Harrington and Lachlan used the Classification Theorem to expand and reorganize Zil′ber's work. In particular, they generalized most of his work to ℵ0-categorical, ℵ0-stable structures, proved the Morley rank is finite in these structures, and introduced the powerful Coordinatization Theorem (Theorem 3.1 of [CHL]; Proposition 1.14 of the present paper). They also showed that ℵ0-categorical, ℵ0-stable structures are not finitely axiomatizable using a notion of envelope that is the same as Zil′ber's except in one particularly perverse case; [CHL]'s notion of envelope is used throughout the current paper. Peretyat'kin [P] has found an example of an ℵ1-categorical finitely axiomatizable structure.

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.

It will be shown that in the lattice of recursively enumerable sets one can define elementarily with parameters a structure isomorphic to (), i.e. isomorphic to the lattice of sets together with a unary predicate selecting out exactly the sets.

A subset X of a structure S is called free in S if ∀x ∈ Xx ∉ S[X − {x}]; here, S[Y] is the substructure of S generated from Y by the functions of S. For κ, λ, μ cardinals, let Frμ(κ, λ) be the assertion:

We show that Frω(ωω, ω), the free-subset property for ωω, is equiconsistent with the existence of a measurable cardinal (2.2,4.4). This answers a question of Devlin [De].

In the first section of this paper we prove some combinatorial facts about Frμ(κ, λ); in particular the first cardinal κ such that Frω(κ, ω) is weakly inaccessible or of cofinality ω (1.2). The second section shows that, under Frω(ωω, ω), ωω is measurable in an inner model. For the convenience of readers not acquainted with the core model κ, we first deduce the existence of 0# (2.1) using the inner model L. Then we adapt the proof to the core model and obtain that ωω is measurable in an inner model. For the reverse direction, we essentially apply a construction of Shelah [Sh] who forced Frω(ωω, ω) over a ground model which contains an ω-sequence of measurable cardinals. We show in §4 that indeed a coherent sequence of Ramsey cardinals suffices. In §3 we obtain such a sequence as an endsegment of a Prikry sequence.

In this paper we introduce a new hierarchy of sets and operators which we call the REA hierarchy for “recursively enumerable in and above”. The hierarchy is generated by composing (possibly) transfinite sequences of the pseudo-jump operators considered in Jockusch and Shore [1983]. We there studied pseudo-jump operators defined by analogy with the Turing jump as ones taking a set A to A ⊕ for some index e. We would now call these 1-REA operators and will extend them to α-REA operators for recursive ordinals α in analogy with the iterated Turing jump operators (A → A(α) for α < and Kleene's hyperarithmetic hierarchy. The REA sets will then, of course, be the results of applying these operators to the empty set. They will extend and generalize Kleene's H sets but will still be contained in the class of set singletons thus providing us with a new richer subclass of the set singletons which, as we shall see, is related to the work of Harrington [1975] and [1976] on the problems of Friedman [1975] about the arithmetic degrees of such singletons. Their degrees also give a natural class extending the class H of Jockusch and McLaughlin [1969] by closing it off under transfinite iterations as well as the inclusion of [d, d′] for each degree d in the class. The reason for the class being closed under this last operation is that the REA operators include all operators and so give a new hierarchy for them as well as the sets. This hierarchy also turns out to be related to the difference hierarchy of Ershov [1968], [1968a] and [1970]: every α-r.e. set is α-REA but each level of the REA hierarchy after the first extends all the way through the difference hierarchy although never entirely encompassing even the next level of the difference hierarchy.

The Gödel class with identity (GCI) is the class of closed, prenex quantificational formulas whose prefixes have the form ∀∀∃ … ∃ and whose matrices contain arbitrary predicate letters and the identity sign “ = ”, but do not contain function signs or individual constants. The ∀∀∃ … ∃ class without identity was shown solvable over fifty years ago ([4], [12], [17]); slightly later, that class was shown to possess the stronger property of finite controllability ([5], [18]). (A class of formulas is solvable iff it is decidable for satisfiability; it is finitely controllable iff every satisfiable formula in it has a finite model.) At the end of [5], Gödel claims that the finite controllability of the GCI can be shown “by the same method” as he employed to show this for the class without identity. This claim has been questioned for nearly twenty years; in §1 below we give a brief history of investigations into it. The major result of this paper shows Gödel to have been mistaken: the GCI is unsolvable. §2 contains the basic construction, which yields a satisfiable formula in the GCI that lacks finite models. This formula may easily be exploited to encode undecidable problems into the GCI.

The minimal Gödel class with identity (MGCI) is the class of closed, prenex quantificational formulas whose prefixes have the form ∀x1∀x2∃x3 and whose matrices contain arbitrary predicate letters and the identity sign “=”, but contain no function signs or individual constants. The MGCI was shown undecidable (for satisfiability) in 1983 [Go2]; this both refutes a claim of Gödel's [Gö, p. 443] and settles the decision problem for all prefix-classes of quantification theory with identity.

In this paper, we show the decidability of a natural subclass of the MGCI. The formulas in this subclass can be thought of as exploiting only half of the power of the existential quantifier. That is, since an MGCI formula has prefix ∀x1∀x2∃x3, in general its truth in a model requires for any elements a and b, the existence of both a witness for and a witness for . The formulas we consider demand less: they require, for any elements a and b, a witness for the unordered pair {a, b}, that is, a witness either for or for .

Let L be a first order predicate calculus with equality which has a fixed binary predicate symbol <. In this paper, we shall deal with quantifiers Cx, ∀x ≦ y, ∃x ≦ y defined as follows: CxA(x) is ∀y∃x(y ≦ x ∧ A(x)), ∀x ≦ yA{x) is ∀x(x ≦ y ⊃ A(x)), and ∃x ≦ yA(x) is ∃x(x ≦ y ∧ 4(x)). The expressions x̄, ȳ, … will be used to denote sequences of variables. In particular, x̄ stands for 〈x1, …, xn〉 and ȳ stands for 〈y1,…, ym〉 for some n, m. Also ∃x̄, ∀x̄ ≦ ȳ, … will be used to denote ∃x1 ∃x2 … ∃xn, ∀x1 ≦ y1 ∀x2 ≦ y2 … ∀xn ≦ yn, …, respectively. Let X be a set of formulas in L such that X contains every atomic formula and is closed under substitution of free variables and applications of propositional connectives ¬(not), ∧(and), ∨(or). Then, ∑(X) is the set of formulas of the form ∃x̄B(x̄), where B ∈ X, and Φ(X) is the set of formulas of the form

.

Since X is closed under ∧, ∨, the two sets Σ(X) and Φ(X) are closed under ∧, ∨ in the following sense: for any formulas A and B in Σ(X) [Φ(X)], there are formulas in Σ(X)[ Φ(X)] which are obtained from A ∧ B and A ∨ B by bringing some quantifiers forward in the usual manner.