In A note on the Entscheidungsproblem the author gave a proof of the unsolvability of the general case of the Entscheidungsproblem of the engere Funktionenkalkül. This proof, however, contains an error, in order to correct which it is necessary to modify the “additional axioms” of the system L so that they contain no free variables (either free individual variables or free propositional function variables).

The additional axioms of L other than x=y→[F(x)→F(y)] contain no free propositional function variables, and hence it is sufficient to replace each one by an expression obtained from it by quantifying all the individual variables by means of universal quantifiers initially placed—thus, in particular, x = x is replaced by (x)[x=x]. Moreover the axiom x=y→[F(x)→F(y)] may be replaced by the following set of axioms:

and similar axioms for each of the functions b1, b2, …, bk.

The purpose of this paper is to present and justify a simple proof procedure for quantification theory. The procedure will take the form of a method for proving a quantificational schema to be inconsistent, i.e., satisfiable in no non-empty universe. But it serves equally for proving validity, since we can show a schema valid by showing its negation inconsistent.

Method A, as I shall call it, will appear first, followed by a more practical adaptation which I shall call B. The soundness and completeness of A will be established, and the equivalence of A and B. Method A, as will appear, is not new.

The reader need be conversant with little more than the fairly conventional use (as in [8]) of such terms as ‘quantificational schema’, ‘interpretation’, ‘valid’, ‘consistent’, ‘prenex’, and my notation (as in [7]) of quasi-quotation.

Feiner [F] showed that a Boolean algebra need not have a computable copy (see also [T2]). Downey and Jockusch [D-J] showed that every low Boolean algebra does have a computable copy. Thurber [T3], showed that every low2 Boolean algebra has a computable copy. Here we show that every Boolean algebra which is low3, or even low4, has a computable copy.

The results of [D-J] and [T3] were obtained by passing to linear orderings. In [D-J], there is an embedding theorem saying that any linear ordering which is with the successor relation as an added predicate can be embedded in a slightly larger linear ordering which is computable. An isomorphism theorem of Remmel [R] is used to show that the interval algebras of the two linear orderings are isomorphic (except in a trivial case). In [T3], there is an embedding theorem saying that any linear ordering which is with certain added predicates can be embedded in one which is with successor. Again the isomorphism theorem of Remmel is used to show that the interval algebras are isomorphic (except in a trivial case).

Here, instead of passing to linear orderings, we work directly with Boolean algebras. We begin with a review of the known results. We re-formulate the embedding theorems of Downey-Jockusch and Thurber in terms of Boolean algebras. We extract from Remmel's isomorphism theorem some information on complexity. In this way, we show that a low Boolean algebra is isomorphic to a computable one by an isomorphism which is , at worst, and the same is true for a low2 Boolean algebra.

In 1986, Beigel [Be87] (see also [Od89, III.5.9]) proved the nonspeedup theorem: if A, B ⊆ ω, and as a function of 2n variables can be computed by an algorithm which makes at most n queries to B, then A is recursive (informally, 2n parallel queries to a nonrecursive oracle A cannot be answered by making n sequential (or “adaptive”) queries to an arbitrary oracle B). Here, 2n cannot be replaced by 2n − 1. In subsequent papers of Beigel, Gasarch, Gill, Hay, and Owings the theory of “bounded query classes” has been further developed (see, for example, [BGGOta], [BGH89], and [Ow89]). The topic has also been studied in the context of structural complexity theory (see, for example, [AG88], [Be90], and [JY90]).

If A ⊆ ω and n ≥ 1, let . Beigel [Be87] stated the powerful “cardinality conjecture” (CC): if A, B ⊆ ω, and can be computed by an algorithm which makes at most n queries to B, then A is recursive. Owings [Ow89] verified CC for n = 1, and, for n 1, he proved that A is recursive in the halting problem. We prove that CC is true for all n.

Le paradigme de théorie stable est la théorie T d'un corps algébriquement clos; une autre théorie stable T′ est celle de la structure formée d'un corps algébriquement clos, avec en outre un symbole relationnel unaire interprétant un de ses sous-corps propres algébriquement clos. C'est à l'éclaircissement des rapports de T et de T′ qu'est consacré cet article.

J'y considère une théorie complète T stable, et les structures formées d'un modèle N de T, avec en outre un symbole relationnel unaire (x) interprétant une restriction élémentaire M de N; j'appelle ces structures paires de modèles de T.

Et je dis que la paire (N, M) est belle si d'une part M est ∣T∣+-saturé, et d'autre part pour tout n-uplet ā d'éléments de N, tout type, au sens de T, sur M ⋃ {α} est réalisé dans N.

Le premier résultat (Théorème 4) est que deux belles paires sont élémentairement équivalentes. Plus précisément, si (N1, M1) et (N2, M2) sont deux belles paires, et si ā est dans la première, b¯ dans la seconde, le fait que le type de ā sur M1 et celui de b¯ sur M2 soient équivalents dans l'ordre fondamental au sens de T suffit (et est bien sûr nécessaire) pour que ā at b¯ aient même type (sur ⊘) au sens de la théorie T′ des belles paires.

The theory of trees with additional unary predicates and quantification over nodes and branches embraces a rich branching time logic. This theory was reduced in the companion paper to the first-order theory of binary, bounded, well-founded trees with additional unary predicates. Here we prove the decidability of the latter theory.

The main result of this paper is Theorem 3.1 which is a criterion for weak o-minimality of a linearly ordered structure in terms of realizations of 1-types. Here we also prove some other properties of weakly o-minimal structures. In particular, we characterize all weakly o-minimal linear orderings in the signature {<, =} . Moreover, we present a criterion for density of isolated types of a weakly o-minimal theory. Lastly, at the end of the paper we present some remarks on the Exchange Principle for algebraic closure in a weakly o-minimal structure.

The properties of small cardinals such as ℵ1 tend to be much more complex than those of large cardinals, so that properties of ℵ1 may often be better understood by viewing them as large cardinal properties. In this paper we show that the existence of a precipitous ideal on ℵ1 is essentially the same as measurability.

If I is an ideal on P(κ) then R(I) is the notion of forcing whose conditions are sets x ∈ P(κ)/I, with x ≤ x′ if x ⊆ x′. Thus a set D R(I)-generic over the ground model V is an ultrafilter on P(κ) ⋂ V extending the filter dual to I. The ideal I is said to be precipitous if κ ⊨R(I)(Vκ/D is wellfounded).

One example of a precipitous ideal is the ideal dual to a κ-complete ultrafilter U on κ. This example is trivial since the generic ultrafilter D is equal to U and is already in the ground model. A generic set may be viewed as one that can be worked with in the ground model even though it is not actually in the ground model, so we might expect that cardinals such as ℵ1 that cannot be measurable still might have precipitous ideals, and such ideals might correspond closely to measures.

In this paper we shall outline a purely model theoretic method for obtaining independence results for Peano's first order axioms (P). The method is of interest in that it provides for the first time elementary combinatorial statements about the natural numbers which are not provable in P. We give several examples of such statements.

Central to this exposition will be the notion of an indicator. Indicators were introduced by L. Kirby and the author in [3] although they had occurred implicitly in earlier papers, for example Friedman [1]. The main result on indicators which we shall need (Lemma 1) was proved by Laurie Kirby and the author in the summer of 1976 but it was not until early in the following year that the author realised that this lemma could be used to give independence results.

The first combinatorial independence results obtained were essentially statements about certain finite games and consequently were not immediately meaningful (see Example 2). This shortcoming was remedied by Leo Harrington who, upon hearing an incorrect version of our results, noticed a beautifully simply independent combinatorial statement. We outline this result in Example 3. An alternative, more detailed, proof may be found in [5].

Clearly Laurie Kirby and Leo Harrington have made a very significant contribution to this paper and we wish to express our sincere thanks to them.

Tarski made a fundamental contribution to our understanding of R, perhaps mathematics’ most basic structure. His theorem is the following.

To any formula ϕ(X1, …, Xm) in the vocabulary {0, 1, +, ·, <} one can effectively associate two objects: (i) a quantifier free formula (X 1, …, Xm ) in

(1) the same vocabulary, and (ii) a proof of the equivalence ϕ ↔ that uses only the axioms for real closed fields. (Reminder: real closed fields are ordered fields with the intermediate value property for polynomials.)

Everything in (1) has turned out to be crucial: that arbitrary formulas are considered rather than just sentences, that the equivalence ϕ ↔ holds in all real closed fields rather than only in R; even the effectiveness of the passage from ϕ to has found good theoretical uses besides firing the imagination.

We begin this survey with some history in §1. In §2 we discuss three other influential proofs of Tarski's theorem, and in §3 we consider some of the remarkable and totally unforeseen ways in which Tarski's theorem functions nowadays in mathematics, logic and computer science.

I thank Ward Henson, and in particular Wilfrid Hodges without whose constant prodding and logistic support this article would not have been written.

We generalize the Bolzano-Weierstrass theorem (that every bounded sequence of reals admits a convergent subsequence) on ideal convergence. We show examples of ideals with and without the Bolzano-Weierstrass property, and give characterizations of BW property in terms of submeasures and extendability to a maximal P-ideal. We show applications to Rudin-Keisler and Rudin-Blass orderings of ideals and quotient Boolean algebras. In particular we show that an ideal does not have BW property if and only if its quotient Boolean algebra has a countably splitting family.

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.

We show how to extract effective bounds Φ for ⋀u1⋀v ≤ytu⋁wηG0-sentences which depend on u only (i.e. ⋀u⋀v ≤y, tu⋁w ≤η ΦuG0) from arithmetical proofs which use analytical assumptions of the form

(ϒ, δ, ρ, and τ are arbitrary finite types, η ≤ 2, G0 and F0 are quantifier-free, and s and t are closed terms). If τ ≤ 2, (*) can be weakened to

This is used to establish new conservation results about weak Konig's lemma. Applications to proofs in classical analysis, especially uniqueness proofs in approximation theory, will be given in subsequent papers.

Let p be an odd prime. A method is described which given a structure M of finite similarity type produces a nilpotent group of class 2 and exponent p which is in the same stability class as M.

Theorem. There are nilpotent groups of class 2 and exponent p in all stability classes.

Theorem. The problem of characterizing a stability class is equivalent to characterizing the (nilpotent, class 2, exponent p) groups in that class.

In [2] Prior puts forward a tense logic, GH1, which is intended to axiomatise tense logic with time linear and rational; he also contemplates the tense logic with time linear and real. The purpose of this paper is to give completeness proofs for three axiom systems, GH1, GHlr, GHli, with respect to tense logic with time linear and rational, real, and integral, respectively.1 In a fourth section I show that GH1 and GHlr have the finite model property, but that GHli lacks it.

GH1 has the operators of the classical propositional calculus, together with operators P, H, F, G for ‘It has been the case that’, ‘It has always been the case that’, ‘It will be the case that’, ‘It will always be the case that’, respectively.

Anderson and Belnap asked in §8.11 of their treatise Entailment [1] whether a certain pure implicational calculus, which we will call P − W, is minimal in the sense that no two distinct formulas coentail each other in this calculus. We provide a positive solution to this question, variously known as The P − W problem, or Belnap's conjecture.

We will be concerned with two systems of pure implication, formulated in a language constructed in the usual way from a set of propositional variables, with a single binary connective →. We use A, B,…, A1, B1, …, as variables ranging over formulas. Formulas are written using the bracketing conventions of Church [3].

The first system, which we call S (in honour of its evident incorporation of syllogistic principles of reasoning), has as axioms all instances of

The second system, P − W, has in addition to the axioms and rules of S the axiom scheme

We write ⊢SA (⊣SA) to mean that A is (resp. is not) a theorem of S, and similarly for P − W.

We use the Low Basis Theorem of Jockusch and Soare to show that all computable algebraic fields are d-computably categorical for a particular Turing degree d with d′ = 0″, but that not all such fields are 0′-computably categorical. We also prove related results about algebraic fields with splitting algorithms, and fields of finite transcendence degree over ℚ.

We study computably enumerable equivalence relations (ceers), under the reducibility $R \le S$ if there exists a computable function f such that $x\,R\,y$ if and only if $f\left( x \right)\,\,S\,f\left( y \right)$, for every $x,y$. We show that the degrees of ceers under the equivalence relation generated by $\le$ form a bounded poset that is neither a lower semilattice, nor an upper semilattice, and its first-order theory is undecidable. We then study the universal ceers. We show that 1) the uniformly effectively inseparable ceers are universal, but there are effectively inseparable ceers that are not universal; 2) a ceer R is universal if and only if $R\prime \le R$, where $R\prime$ denotes the halting jump operator introduced by Gao and Gerdes (answering an open question of Gao and Gerdes); and 3) both the index set of the universal ceers and the index set of the uniformly effectively inseparable ceers are ${\rm{\Sigma }}_3^0$-complete (the former answering an open question of Gao and Gerdes).

The splitting theorem says that any set of formulae has a finest representation as a family of letter-disjoint sets. Parikh formulated this for classical propositional logic, proved it in the finite case, used it to formulate a criterion for relevance in belief change, and showed that AGM partial meet revision can fail the criterion. In this paper we make three further contributions. We begin by establishing a new version of the well-known interpolation theorem, which we call parallel interpolation, use it to prove the splitting theorem in the infinite case, and show how AGM belief change operations may be modified, if desired, so as to ensure satisfaction of Parikh's relevance criterion.