One of the more significant achievements of twentieth century mathematics, especially from the viewpoints of logic and computer science, was the work of Church, Gödel and Turing in the 1930's which provided a precise and robust definition of what it means for a problem to be computationally solvable, or decidable, and which showed that there are undecidable problems which arise naturally in logic and computer science. Indeed, when one is faced with a new computational problem, one of the first questions to be answered is whether the problem is decidable or undecidable. A problem is usually defined to be decidable if and only if it can be solved by some Turing machine, and the class of decidable problems defined in this way remains unchanged if “Turing machine” is replaced by any of a variety of other formal models of computation. The division of all problems into two classes, decidable or undecidable, is very coarse, and refinements have been made on both sides of the boundary. On the undecidable side, work in recursive function theory, using tools such as effective reducibility, has exposed much additional structure such as degrees of unsolvability. The main purpose of this survey article is to describe a branch of computational complexity theory which attempts to expose more structure within the decidable side of the boundary.

Motivated in part by practical considerations, the additional structure is obtained by placing upper bounds on the amounts of computational resources which are needed to solve the problem. Two common measures of the computational resources used by an algorithm are time, the number of steps executed by the algorithm, and space, the amount of memory used by the algorithm.

If U is a normal measure on κ then we can add indiscernibles for U either by Prikry forcing [P] or by taking an iterated ultrapower which will add a sequence of indiscernibles for over M. These constructions are equivalent: the set C of indiscernibles for added by the iterated ultrapower is Prikry generic for [Mat]. Prikry forcing has been extended for sequences of measures of length by Magidor [Mag], and his method readily extends to . In this case the measure U is replaced by a sequence of measures and the set C of indiscernibles is replaced by a system of indiscernibles for : is a function such that (κ, β) is a set of indiscernibles for (κ, β) for each . The equivalence between forcing and iterated ultra-powers still holds true for such sequences: there is an interated ultrapower j: V → M (which is defined in detail later in this paper) such that the system of indiscernibles for j() constructed by j is Magidor generic over M.

The construction of the system of indiscernibles works equally well for o(κ) ≧ κ +. Radin has defined a variant of Prikry forcing which also works for o(κ) > κ + ([R]; see also [Mi82] where Radin forcing is applied specifically to sequences of measures, rather than to hypermeasures as in Radin's paper), but Radin's forcing is weaker than Magidor's extension of Prikry forcing in the sense that the system of indiscernibles generated by the interated ultrapower is not Radin generic for j(), but only the set . That is, an indiscernible does not belong to a specific measure, but only to the whole sequence of measures on the cardinal κ.

Answering a question of A. Kanamori, we prove that there is no Jónsson filter over the least Jónsson cardinal. We also notice that, assuming □κ, the successor κ+ cannot be Jónsson.

The underlying modules of existentially closed ⊿-algebras are studied. Among other things, it is proved that they are all elementarily equivalent, and that all of them are existentially closed as modules if and only if ⊿ is regular. It is also proved that every saturated module in the appropriate elementary equivalence class underlies an ex. ⊿-algebra. Applications to some problems in module theory are given. A number of open questions are mentioned.

We set = ‹, ≤L , # ›, where is the set of degrees of nonconstructibility for countable sets of countable ordinals. We show how to define inductively over this structure the degrees of such sets of ordinals in Κ, the core model, and the next few core models thereafter, i.e. without reference to mice, premice or measurable cardinals

This paper introduces, as an alternative to the (absolutely) lawless sequences of Kreisel and Troelstra, a notion of choice sequence lawless with respect to a given class of lawlike sequences. For countable , the class of -lawless sequences is comeager in the sense of Baire. If a particular well-ordered class of sequences, generated by iterating definability over the continuum, is countable then the -lawless sequences satisfy the axiom of open data and the continuity principle for functions from lawless to lawlike sequences, but fail to satisfy Troelstra's extension principle. Classical reasoning is used.

It is well known that combinatory logic with unrestricted introduction and elimination rules for implication is inconsistent in the strong sense that an arbitrary term Y is provable. The simplest proof of this, now usually called Curry's paradox, involves for an arbitrary term Y, a term X defined by X = Y(CPy).

The fact that X = P XY = X ⊃ Y is an essential part of the proof.

The paradox can be avoided by placing restrictions on the implication introduction rule or on the axioms from which it can be proved.

In this paper we determine the forms that must be taken by inconsistency proofs of systems of propositional calculus based on combinatory logic, with arbitrary restrictions on both the introduction and elimination rules for the connectives. Generally such a proof will involve terms without normal form and cut formulas, i.e. formulas formed by an introduction rule that are immediately removed by an elimination with at most some equality steps intervening. (Such a sequence of steps we call a “cut”.)

The above applies not only to the strong form of inconsistency defined above, but also to the weak form of inconsistency defined by: all propositions are provable, if this can be represented in the system.

Any inconsistency proof of this kind of system can be reduced to one where the major premise of the elimination rule involved in the cut and its deduction must also appear in the deduction of the minor premise involved in the cut.

We can, using this characterization of inconsistency proofs, put appropriate restrictions on certain introduction rules so that the systems, including a full classical propositional one, become provably consistent.

For several old problems in combinatorial set theory A. Hajnal and the present author [2] showed that on collapsing a sufficiently Mahlo cardinal to ω 1 by the Lévy-collapse one gets a model where these problems are solved in the “counter-example” direction. The authors of [2] have speculated that the theorems of that paper should hold in L, and this, in fact, was shown for some of the results by Todorčević and Velleman [7,8]. The observation that collapsing a large cardinal to ω 1 may give rise to L-like constructions is not new. As it was shown long ago by Silver and Rowbottom, there is a Kurepa-tree if a strongly inaccessible cardinal is Lévy-collapsed to ω 1. In [5] it is proved that even Silver's W holds in that model. Here we show that even a quagmire exists there, but not necessarily a morass. To be more exact, we show that if κ < λ are the first two strongly inaccessible cardinals, first λ is Lévy-collapsed to κ +, and then κ is Lévy-collapsed to then there is no ω 1-morass with built-in diamond in the resulting model (GCH is assumed). If λ is Mahlo, there is not even a morass.

Our notations are standard. For excellent survey papers on morass-like principles and their uses in combinatorial set theory see [4,5,6].

Cherlin and Dickmann [2] proved that the theory RCVR of real closed (valuation) rings admits quantifier-elimination (q.e.) in the language ℒ = {+, −, ·, 0, 1, <, ∣} for ordered rings augmented by the divisibility relation “∣”. The purpose of this paper is to prove a form of converse of this result:

Theorem. Let T be a theory of ordered commutative domains (which are not fields), formulated in the language ℒ. In addition we assume that:

• (1) The symbol “∣” is interpreted as the honest divisibility relation:

• (2) The following divisibility property holds in T:

• 

If T admits q.e. in ℒ, then T = RCVR.

We do not know at present whether the restriction imposed by condition (2) can be weakened.

The divisibility property (DP) has been considered in the context of ordered valued fields; see [4] for example. It also appears in [2], and has been further studied in Becker [1] from the point of view of model theory. Ordered domains in which (DP) holds are called in [1] convexly ordered valuation rings, for reasons which the proposition below makes clear. The following summarizes the basic properties of these rings:

Proposition I [2, Lemma 4]. (1) Let A be a linearly ordered commutative domain. The following are equivalent:

• (a) A is a convexly ordered valuation ring.

• (b) Every ideal (or, equivalently, principal ideal) is convex in A.

• (c) A is a valuation ring convex in its field of fractions quot(A).

• (d) A is a valuation ring and its maximal ideal MA is convex (in A or, equivalently, in quot (A)).

• (e) A is a valuation ring and its maximal ideal is bounded by ± 1.

This paper is a sequel to our earlier paper [2] entitled Saturation and simple extensions of models of Peano arithmetic. Among other things, we will answer some of the questions that were left open there. In §1 we consider the question of whether there are lofty models of PA which have no recursively saturated, simple extensions. We are still unable to answer this question; but we do show in that section that these models are precisely the lofty models which are not recursively saturated and which are κ-like for some regular κ. In §2 we use diagonal methods to produce minimal models of PA in which the standard cut is recursively definable, and other minimal models in which the standard cut is not recursively definable. In §3 we answer two questions from [2] by exhibiting countable models of PA which, in the terminology of this paper, are uniformly ω-lofty but not continuously ω-lofty and others which are continuously ω-lofty but not recursively saturated. We also construct a model (assuming ◇) which is not recursively saturated but every proper, simple cofinal extension of which is ℵ1-saturated. Finally, in §4 we answer another question from [2] by proving that for regular κ ≥ ℵ1; every κ-saturated model of PA has a κ-saturated proper, simple extension which is not κ +-saturated.

Our notation and terminology are quite standard. Anything unfamiliar to the reader and not adequately denned here is probably defined in §1 of [2]. All models considered are models of Peano arithmetic.

This paper concerns ultrafilters on a cardinal γ extending the filter of λ-closed, unbounded sets, λ < γ. The history of these ultrafilters is closely connected with that of the axiom of determinacy (AD). Solovay noticed first that, under AD, there was such an ultrafilter for γ = ℵ1; λ = ω. Later, Kleinberg found that the existence of such ultrafilters followed from the partition relation γ → (γ)λ+λ . Specific instances of this and more powerful relations on cardinals were then proved from AD by Martin, Kunen, Paris, and others. The axiom of determinacy was recently shown consistent with ZF relative to something less than a supercompact cardinal by Martin and Steel. Solovay's and Kleinberg's results were actually stronger, and we discuss this at the end of the paper. Good references for these results include [K2] and [KM].

We are interested here in the case where γ is the ultrapower of a strong partition cardinal κ (a cardinal satisfying for all α < κ). Such cardinals exist in great abundance assuming AD, and in fact, if sufficiently many cardinals are strong, then AD holds in L[R] [KKMW].

We study the sets definable in an algebraic number field by first order formulas of various simple types, showing in particular that N and Z do not have very simple definitions.

For a countable complete o-minimal theory T, we introduce the notion of a sequentially complete model of T. We show that a model of T is sequentially complete if and only if ≺ for some Dedekind complete model . We also prove that if T has a Dedekind complete model of power greater than , then T has Dedekind complete models of arbitrarily large powers. Lastly, we show that a dyadic theory—namely, a theory relative to which every formula is equivalent to a Boolean combination of formulas in two variables—that has some Dedekind complete model has Dedekind complete models in arbitrarily large powers.

The formalism of P(redicate) P(rovability) L(ogic) is the result of adjoining the unary operator □ to first-order logic without identity, constants, or function symbols. The term “provability” indicates that □ is to be “read” as “it is provable in P(eano) A(rithmetic) that…” and that the formulae of predicate provability logic are to be interpreted via formulae of PA as follows.

Pr(x), alias Bew(x), is the standard provability predicate of PA. For any formula F of PA, Pr[F] is the formula of PA that expresses the PA-provability of F “of” the values of the variables free in F, i.e., it is the formula of PA with the same free variables as F that expresses the PA-provability of the result of substituting for each variable free in F the numeral for the value of that variable. For the details of the construction of Pr[F], the reader may consult [B2, p. 42]. If F is a sentence of PA, then Pr[F] = Pr(‘F’), the sentence that expresses the PA-provability of F.

Let υ 1, υ 2,… be an enumeration of the variables of PA. An interpretation * of a formula ϕ of PPL is a function which assigns to each predicate symbol P of ϕ a formula P* of the language of arithmetic whose free variables are the first n variables of PA, where n is the degree of P.

The interpretation of the ZF set theory reported in this paper is, actually, part of a wider effort, namely, a new approach to the foundation of mathematics, which is referred to as The Cybernetic Foundation. A detailed exposition of the Cybernetic Foundation will be published elsewhere. Our approach leads to a full acceptance of the formalism of the classical set theory, but interprets it using only the idea of potential, but not actual (completed) infinity, and dealing only with finite objects that can actually be constructed. Thus we have a finitist proof of the consistency of ZF. This becomes possible because we set forth a metatheory of mathematics which goes beyond the classical logic and set theory and, of course, cannot be formalized in ZF, yet yields proofs which are as convincing—at least, from the author's viewpoint—as any mathematical proof can be.

Our metatheory is based on the following two ideas. Firstly, we define the semantics of the mathematical language using the cybernetical concept of knowledge. According to this concept, to say that a cybernetic system (a human being, in particular) has some knowledge is to say that it has some models of reality. In the Cybernetic Foundation we consider mathematics as the art of constructing linguistic models of reality.

Two elementary extensions of the topos axioms are given, each implying the topos has a local geometric morphism to a category of sets. The stronger one realizes sets as precisely the decidables of the topos, so there is a simple internal description of the range of validity of the law of excluded middle in the topos. It also has a natural geometric meaning. Models of the extensions in Grothendieck toposes are described.

We will show that there is a nontrivial strongly minimal expansion of (ω, s), the natural numbers with successor. Pillay and Steinhorn [1] proved that there is no -minimal expansion of (ω, ≤). This result provides an interesting contrast.

The strongly minimal expansion of (ω, s) is very easy to describe. Consider the order-two permutation of ω, π recursively defined by

Let T be Th(ω, s, π, 0).

Much of recursion theory centers on the structures of different kinds of degrees. Classically there are the Turing degrees and r. e. Turing degrees. More recently, people have studied α-degrees for α an ordinal, and degrees over E-closed sets and admissible sets. In most contexts, deg(0) is the bottom degree and there is a jump operator' such that d' is the largest degree r. e. in d and d' > d. Both the degrees and the r. e. degrees usually have a rich structure, including a relativization to the cone above a given degree.

A natural exception to this pattern was discovered by S. Friedman [F], who showed that for certain admissible ordinals β the β-degrees ≥ 0′ are well-ordered, with successor provided by the jump.

For r. e. degrees, natural counterexamples are harder to come by. This is because the constructions are priority arguments, which require only mild restrictions on the ground model. For instance, if an admissible set has a well-behaved pair of recursive well-orderings then the priority construction of an intermediate r. e. degree (i.e., 0 < d < 0′) goes through [S]. It is of interest to see just what priority proofs need by building (necessarily pathological) admissible sets with few r. e. degrees.

Harrington [C] provides an admissible set with two r. e. degrees, via forcing. A limitation of his example is that it needs ω 1 (more accurately, a local version thereof) as a parameter. In this paper, we find locally countable admissible sets, some with three r. e. degrees and some with four.

The aim of this short note is to correct an error in the proof in [1], more precisely in Remark 1 on page 395, where it is stated that any improper word has rank ≥2. This claim is false; and, consequently, Remark 2, asserting that any 1,0-deduction does not contain improper Q-terms, also fails immediately. In fact, let us consider the word

It is easily seen that the rank of W is 1, but W is obviously improper. We remark that it is possible, in the same way, to give examples of improper words of rank 1 containing (without subordination) ε-subterms of arbitrarily high rank. In the following section we sketch a corrected version of the proof in order to eliminate all improper ε-terms.

We refer to the notation and definitions of [1]. A more extended description of the theories involved can be found in [2].

We show that either PFA+ or Martin's maximum implies Fleissner's Axiom R, a reflection principle for stationary subsets of P ℵ(λ). In fact, the “plus version” (for one term denoting a stationary set) of Martin's axiom for countably closed partial orders implies Axiom R.