For an ultrafilter , consider the ultrapower NN/. 〈an〉/ is in the top sky of NN/ if there exists a sequence 〈bn〉 ∈ NN such that

and

In [M2] we showed, assuming the Continuum Hypothesis, that there are exactly 10 c/p's (where c is the ring of real convergent sequences and p is a prime ideal of c). To get the lower bound we showed that there will be at least 10 c/p's in any model of ZFC where there exist both of the following kinds of ultrafilter:

(i) nonprincipal P-points,

(ii) non-P-points such that when the top sky is removed from NN/, the remaining model has countable cofinality.

In [M2] we showed that the Continuum Hypothesis implies the existence of the ultrafilter in (ii). In this paper we show that its existence is implied by an axiom weaker than the Continuum Hypothesis, in fact weaker than Martin's Axiom, namely,

(*) If is a subset of NN such that for any f: N → N there exists g ∈ such that g(n) > f(n) for all n, then ∣∣ = .

We generalise various properties of quasiendomorphisms from groups with regular generic to small abelian groups. In particular, for a small stable abelian group such that no infinite definable quotient is connected-by-finite, the ring of quasi-endomorphisms is locally finite. Under some additional assumptions, it decomposes modulo some nil ideal into a sum of finitely many matrix rings.

Galois theory states that if L is a certain algebraic extension (called a Galois extension) of a field K, then there is a one-to-one correspondence (called a Galois correspondence) between subfields M, K ⊂ M ⊂ L and subgroups of the automorphism groups of L fixing the elements in K.

A subfield of a field L can be considered as a substructure of L in general model theory. However, a substructure is a subset closed under functions which are interpretations of function symbols in a given language, so the notion of substructure may change if we expand the language by adding definable notions. On the other hand a definably closed substructure is a subset which is closed under all definable functions, and it does not change by such expansions. If we are interested in subfields of an algebraically closed field of characteristic 0, these two notions are the same. But in a field of prime characteristic they are not equal. Speaking roughly, a Galois extension of a field K is an extension whose subfields are relatively definably closed. Poizat [4] showed that if a structure M has elimination of imaginaries there is a kind of Galois correspondence between definably closed substructures and subgroups of bijective elementary mappings of M.

In this paper, using Poizat's result we study algebraic types. As is well known, one motivation for developing the Galois theory was to show the unsolvability of equations with degree ≥ 5. We want to take this unsolvability as a special case of general phenomena. For this purpose, we introduce several notions which are stronger than mere algebraicity and study relations between these notions and groups of bijective elementary mappings. (See Theorems 3.7 and 3.9.)

Let Ω ≔ ℵ1. For any α< εΩ + 1 ≔ min {ξ > Ω: ξ = ωξ} let EΩ(α) be the finite set of ε-numbers below Ω which are needed for the unique representation of α in Cantor-normal form using 0, Ω, +, and ω. Let α* ≔ max(EΩ(α) ∪ {0}). A function f: εΩ + 1 → Ω is called essentially increasing, if for any α < εΩ + 1; f(α) ≥ α*: f is called essentially monotonic, if for any α, β<εΩ + 1;

Let be the least set of ordinals which contains 0 as an element and which satisfies the following two conditions:

(a)

(b)

Let be the Howard-Bachmann ordinal, which is, for example, defined in [3]. The following theorem is shown: If f: εΩ + 1 → Ω is essentially monotonic and essentially increasing, then the order type of is less than or equal to .

We study descriptive set theory in the space by letting trees with no uncountable branches play a similar role as countable ordinals in traditional descriptive set theory. By using such trees, we get, for example, a covering property for the class of -sets of .

We call a family of trees universal for a class of trees if ⊆ and every tree in can be order-preservingly mapped into a tree in . It is well known that the class of countable trees with no infinite branches has a universal family of size ℵ1. We shall study the smallest cardinality of a universal family for the class of trees of cardinality ≤ ℵ1 with no uncountable branches. We prove that this cardinality can be 1 (under ¬CH) and any regular cardinal κ which satisfies (under CH). This bears immediately on the covering property of the -subsets of the space .

We also study the possible cardinalities of definable subsets of . We show that the statement that every definable subset of has cardinality <ωn or cardinality is equiconsistent with ZFC (if n ≥ 3) and with ZFC plus an inaccessible (if n = 2).

Finally, we define an analogue of the notion of a Borel set for the space and prove a Souslin-Kleene type theorem for this notion.

It is shown, assuming the linear case of Schinzel's Hypothesis, that the first-order theory of the structure 〈ω; +, P〉, where P is the set of primes, is undecidable and, in fact, that multiplication of natural numbers is first-order definable in this structure. In the other direction, it is shown, from the same hypothesis, that the monadic second-order theory of 〈ω S, P〉 is decidable, where S is the successor function. The latter result is proved using a general result of A. L. Semënov on decidability of monadic theories, and a proof of Semënov's result is presented.

In his paper [7] Steel asked whether there can exist a normal measure U on a cardinal κ such that

We use Reverse Easton forcing to show that this is consistent from a P2κ hypermeasure; we also show that the result is sharp, using the core model for nonoverlapping coherent extender sequences.

The proof uses forcing technology due to Woodin.

In this section we collect some facts that are useful in the forcing constructions of the next section. None of them are due to us, and we are unsure to whom they should be attributed for the most part. We give sketchy proofs; the reader who wants to see more details is referred to [2].

A proof is given that the set of maximal intermediate propositional logics with the disjunction property and the set of maximal intermediate predicate logics with the disjunction property and the explicit definability property have the power of continuum. To prove our results, we introduce various notions which might be interesting by themselves. In particular, we illustrate a method to generate wide sets of pairwise “constructively incompatible constructive logics”. We use a notion of “semiconstructive” logic and define wide sets of “constructive” logics by representing the “constructive” logics as “limits” of decreasing sequences of “semiconstructive” logics. Also, we introduce some generalizations of the usual filtration techniques for propositional logics. For instance, “fitrations over rank formulas” are used to show that any two different logics belonging to a suitable uncountable set of “constructive” logics are “constructively incompatible”.

We introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number of lines (or formulas) in the proof.

A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by “nearly linear” is meant the ratio of proof lengths is O(α(n)) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O(n . α(n)). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O(n log n) lines and of height O(log n). As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O(n log n).

PA is Peano Arithmetic. Pr(x) is the usual Σ1,-formula representing provability in PA. A strong provability predicate is a formula which has the same properties as Pr(·) but is not Σ1. An example: Q is ω-provable if PA + ¬Q is ω-inconsistent (Boolos [4]). In [5] Dzhaparidze introduced a joint provability logic for iterated ω-provability and obtained its arithmetical completeness.

In this paper we prove some further modal properties of Dzhaparidze's logic, e.g., the fixed point property and the Craig interpolation lemma. We also consider other examples of the strong provability predicates and their applications.

Let σ() denote the number of automorphisms of a model of power ω1. We derive a necessary and sufficient condition in terms of trees for the existence of an with . We study the sufficiency of some conditions for . These conditions are analogous to conditions studied by D. Kueker in connection with countable models.

Inductive definability has been studied for some time already. Nonetheless, there are some simple questions that seem to have been overlooked. In particular, there is the problem of the expressibility of the μ-calculus.

The μ-calculus originated with Scott and DeBakker [SD] and was developed by Hitchcock and Park [HP], Park [Pa], Kozen [K], and others. It is a language for including inductive definitions with first-order logic. One can think of a formula in first-order logic (with one free variable) as defining a subset of the universe, the set of elements that make it true. Then “and” corresponds to intersection, “or” to union, and “not” to complementation. Viewing the standard connectives as operations on sets, there is no reason not to include one more: least fixed point.

There are certain features of the μ-calculus coming from its being a language that make it interesting. A natural class of inductive definitions are those that are monotone: if X ⊃ Y then Γ (X) ⊃ Γ (Y) (where Γ (X) is the result of one application of the operator Γ to the set X). When studying monotonic operations in the context of a language, one would need a syntactic guarantor of monotonicity. This is provided by the notion of positivity. An occurrence of a set variable S is positive if that occurrence is in the scopes of exactly an even number of negations (the antecedent of a conditional counting as a negation). S is positive in a formula ϕ if each occurrence of S is positive. Intuitively, the formula can ask whether x ∊ S, but not whether x ∉ S. Such a ϕ can be considered an inductive definition: Γ (X) = {x ∣ ϕ(x), where the variable S is interpreted as X}. Moreover, this induction is monotone: as X gets bigger, ϕ can become only more true, by the positivity of S in ϕ. So in the μ-calculus, a formula is well formed by definition only if all of its inductive definitions are positive, in order to guarantee that all inductive definitions are monotone.

By a variety we mean a class of algebras in a language , containing only function symbols, which is closed under homomorphisms, submodels, and products. A variety is said to be strongly abelian if for any term in , the quasi-identity

holds in .

In [1] it was proved that if a strongly abelian variety has less than the maximal possible uncountable spectrum, then it is equivalent to a multisorted unary variety. Using Shelah's Main Gap theorem one can conclude that if is a classifiable (superstable without DOP or OTOP and shallow) strongly abelian variety then is a multisorted unary variety. In fact, it was known that this conclusion followed from the assumption of superstable without DOP alone.

This paper is devoted to the proof that the superstability assumption is enough to obtain the same structure result. This fulfills a promise made in [2]. Namely, we will prove the following

Theorem 0.1. If is a superstable strongly abelian variety, then it is multisorted unary.

This paper reorganizes and further develops the theory of partial meet contraction which was introduced in a classic paper by Alchourrón, Gärdenfors, and Makinson. Our purpose is threefold. First, we put the theory in a broader perspective by decomposing it into two layers which can respectively be treated by the general theory of choice and preference and elementary model theory. Second, we reprove the two main representation theorems of AGM and present two more representation results for the finite case that “lie between” the former, thereby partially answering an open question of AGM. Our method of proof is uniform insofar as it uses only one form of “revealed preference”, and it explains where and why the finiteness assumption is needed. Third, as an application, we explore the logic characterizing theory contractions in the finite case which are governed by the structure of simple and prioritized belief bases.

Recent work in natural language semantics leads to some new observations on generalized quantifiers. In §1 we show that English quantifiers of type 〈1, 1〉 are booleanly generated by their generalized universal and generalized existential members. These two classes also constitute the sortally reducible members of this type.

Section 2 presents our main result — the Generalized Prefix Theorem (GPT). This theorem characterizes the conditions under which formulas of the form (Q1x1…QnxnRx1…xn and q1x1…qnxnRx1…xn are logically equivalent for arbitrary generalized quantifiers Qi, qi. GPT generalizes, perhaps in an unexpectedly strong form, the Linear Prefix Theorem (appropriately modified) of Keisler & Walkoe (1973).