§1. Introduction. Natural sets that can be enumerated by a computable function (the recursively enumerable or r.e. sets) always seem to be either actually computable (recursive) or of the same complexity (with respect to Turing computability) as the Halting Problem, the complete r.e. set K. The obvious question, first posed in Post [1944] and since then called Post's Problem is then just whether there are r.e. sets which are neither computable nor complete, i.e., neither recursive nor of the same Turing degree as K?

Let be the r.e. degrees, i.e., the r.e. sets modulo the equivalence relation of equicomputable with the partial order induced by Turing computability. This structure is a partial order (indeed, an uppersemilattice or usl)with least element 0, the degree (equivalence class) of the computable sets, and greatest element 1 or 0′, the degree of K. Post's problem then asks if there are any other elements of .

The (positive) solution of Post's problem by Friedberg [1957] and Muchnik [1956] was followed by various algebraic or order theoretic results that were interpreted as saying that the structure was in some way well behaved:

Theorem 1.1 (Embedding theorem; Muchnik [1958], Sacks [1963]). Every countable partial ordering or even uppersemilattice can be embedded into .

Theorem 1.2 (Sacks Splitting Theorem [1963b]). For every nonrecursive r.e. degreeathere are r.e. degreesb, c < asuch thatb ∨ c = a.

Theorem 1.3 (Sacks Density Theorem [1964]). For every pair of nonrecursive r.e. degreesa < bthere is an r.e. degreecsuch thata < c < b.

There has been increasing interest over the last few decades in the study of the effective content of Mathematics. One field whose effective content has been the subject of a large body of work, dating back at least to the early 1960s, is model theory. (A valuable reference is the handbook [7]. In particular, the introduction and the articles by Ershov and Goncharov and by Harizanov give useful overviews, while the articles by Ash and by Goncharov cover material related to the topic of this communication.)

Several different notions of effectiveness of model-theoretic structures have been investigated. This communication is concerned with computable structures, that is, structures with computable domains whose constants, functions, and relations are uniformly computable.

In model theory, we identify isomorphic structures. From the point of view of computable model theory, however, two isomorphic structures might be very different. For example, under the standard ordering of ω the success or relation is computable, but it is not hard to construct a computable linear ordering of type ω in which the successor relation is not computable. In fact, for every computably enumerable (c. e.) degree a, we can construct a computable linear ordering of type ω in which the successor relation has degree a. It is also possible to build two isomorphic computable groups, only one of which has a computable center, or two isomorphic Boolean algebras, only one of which has a computable set of atoms. Thus, for the purposes of computable model theory, studying structures up to isomorphism is not enough.

Euclidean geometry, as presented by Euclid, consists of straightedge-and-compass constructions and rigorous reasoning about the results of those constructions. We show that Euclidean geometry can be developed using only intuitionistic logic. This involves finding “uniform” constructions where normally a case distinction is used. For example, in finding a perpendicular to line L through point p, one usually uses two different constructions, “erecting” a perpendicular when p is on L, and “dropping” a perpendicular when p is not on L, but in constructive geometry, it must be done without a case distinction. Classically, the models of Euclidean (straightedge-and-compass) geometry are planes over Euclidean fields. We prove a similar theorem for constructive Euclidean geometry, by showing how to define addition and multiplication without a case distinction about the sign of the arguments. With intuitionistic logic, there are two possible definitions of Euclidean fields, which turn out to correspond to different versions of the parallel postulate.

We consider three versions of Euclid’s parallel postulate. The two most important are Euclid’s own formulation in his Postulate 5, which says that under certain conditions two lines meet, and Playfair’s axiom (dating from 1795), which says there cannot be two distinct parallels to line L through the same point p. These differ in that Euclid 5 makes an existence assertion, while Playfair’s axiom does not. The third variant, which we call the strong parallel postulate, isolates the existence assertion from the geometry: it amounts to Playfair’s axiom plus the principle that two distinct lines that are not parallel do intersect. The first main result of this paper is that Euclid 5 suffices to define coordinates, addition, multiplication, and square roots geometrically.

We completely settle the questions about implications between the three versions of the parallel postulate. The strong parallel postulate easily implies Euclid 5, and Euclid 5 also implies the strong parallel postulate, as a corollary of coordinatization and definability of arithmetic. We show that Playfair does not imply Euclid 5, and we also give some other independence results. Our independence proofs are given without discussing the exact choice of the other axioms of geometry; all we need is that one can interpret the geometric axioms in Euclidean field theory. The independence proofs use Kripke models of Euclidean field theories based on carefully constructed rings of real-valued functions. “Field elements” in these models are real-valued functions.

For most of the 1980s, Jon Barwise focused much of his research in the area of natural language semantics. This article surveys his research publications in that area.

Most, but not all, of those publications were in the area of situation semantics, a new approach to natural language semantics Barwise developed jointly with his colleague John Perry in the first half of the 1980s. That work was both blessed, and cursed, by becoming closely identified in academic circles with the award of a $23 million gift to Stanford from the System Development Foundation for the establishment in 1983 of its Center for the Study of Language and Information (CSLI). The development of situation semantics, and in due course its underlying mathematical foundation Situation Theory, carried out for the most part within the framework of CSLI's STASS research group (Situation Theory and Situation Semantics), was actually a relatively small part of the overall research program at CSLI. But because Barwise and Perry were leading figures at CSLI, were centrally involved in securing the SDF gift, and were respectively the first and second directors of CSLI, a general impression sprung up that the two of them had been awarded millions of dollars to develop situation semantics.

A major consequence of this false impression was that from the theory's early days, a great deal of interest was shown in the project. With so many accomplished scholars pouring over the work while the ink was still wet on the manuscript pages, Barwise and Perry were able to take advantage of a broad range of helpful criticism (even if it was not always given with a view to being helpful). This meant that they were able to develop the new theory much more rapidly than would otherwise have been the case.

We survey the history of Shelah’s conjecture on strongly dependent fields, give an equivalent formulation in terms of a classification of strongly dependent fields and prove that the conjecture implies that every strongly dependent field has finite dp-rank.

This lecture was given by Per Martin-Löf at Leiden University on August 25, 2001 at the invitation by Göran Sundholm to address the topic mentioned in the title and to reflect on Dummett’s earlier effort of almost a decade before (published in this journal). The lecture was part of a three-day conference on Gottlob Frege. Sundholm arranged for the lecture to be recorded and commissioned Bjørn Jespersen to make a transcript. The information in footnote 1, which Sundholm provided, has been independently confirmed by Thomas Ricketts in an email to the author. The present version has been edited by Ansten Klev. Following the displayed text (Int-id) there is a lacuna in the original transcript corresponding to a pause in the recording when the tape was changed. The continuous text of the present version is the result of a few additions to the original transcript suggested by Klev and agreed to by the author.

In this paper, we shall discuss some recent contributions to the project [15, 14, 2, 18, 22, 23] of explaining why no satisfactory system of complete invariants has yet been found for the torsion-free abelian groups of finite rank n ≥ 2. Recall that, up to isomorphism, the torsion-free abelian groups of rank n are exactly the additive subgroups of the n-dimensional vector space ℚn which contain n linearly independent elements. Thus the collection of torsion-free abelian groups of rank at most n can be naturally identified with the set S (ℚn) of all nontrivial additive subgroups of ℚn. In 1937, Baer [4] solved the classification problem for the class S(ℚ)of rank 1 groups as follows.

Let ℙ be the set of primes. If G is a torsion-free abelian group and 0 ≠ x ϵ G, then the p-height of x is defined to be

hx(p) = sup{n ϵ ℕ ∣ There exists y ϵ G such that pny = x} ϵ ℕ ∪{∞}; and the characteristic χ (x) of x is defined to be the function

Computable model theory, also called effective or recursive model theory, studies algorithmic properties of mathematical structures, their relations, and isomorphisms. These properties can be described syntactically or semantically. One of the major tasks of computable model theory is to obtain, whenever possible, computability-theoretic versions of various classical model-theoretic notions and results. For example, in the 1950's, Fröhlich and Shepherdson realized that the concept of a computable function can make van der Waerden's intuitive notion of an explicit field precise. This led to the notion of a computable structure. In 1960, Rabin proved that every computable field has a computable algebraic closure. However, not every classical result “effectivizes”. Unlike Vaught's theorem that no complete theory has exactly two nonisomorphic countable models, Millar's and Kudaibergenov's result establishes that there is a complete decidable theory that has exactly two nonisomorphic countable models with computable elementary diagrams. In the 1970's, Metakides and Nerode [58], [59] and Remmel [71], [72], [73] used more advanced methods of computability theory to investigate algorithmic properties of fields, vector spaces, and other mathematical structures.

This article serves to present a large mathematical perspective and historical basis for the Axiom of Replacement as well as to affirm its importance as a central axiom of modern set theory.

This is an exposition of Lambek's strengthening and generalization of the deduction theorem in categories related to intuitionistic propositional logic. Essential notions of category theory are introduced so as to yield a simple reformulation of Lambek's Functional Completeness Theorem, from which its main consequences can be readily drawn. The connections of the theorem with combinatory logic, and with modal and substructural logics, are briefly considered at the end.

We investigate Turing's contributions to computability theory for real numbers and real functions presented in [22, 24, 26]. In particular, it is shown how two fundamental approaches to computable analysis, the so-called ‘Type-2 Theory of Effectivity’ (TTE) and the ‘realRAM machine’ model, have their foundations in Turing's work, in spite of the two incompatible notions of computability they involve. It is also shown, by contrast, how the modern conceptual tools provided by these two paradigms allow a systematic interpretation of Turing's pioneering work in the subject.

What counts as an intuitively plausible set theoretic content (notion, axiom or theorem) has been a matter of much debate in contemporary philosophy of mathematics. In this paper I develop a critical appraisal of the issue. I analyze first R. B. Jensen's positions on the epistemic status of the axiom of constructibility. I then formulate and discuss a view of intuitiveness in set theory that assumes it to hinge basically on mathematical success. At the same time, I present accounts of set theoretic axioms and theorems formulated in non-strictly mathematical terms, e.g., by appealing to the iterative concept of set and/or to overall methodological principles, like unify and maximize, and investigate the relation of the latter to success in mathematics.

A set of infinite binary sequences ${\cal C} \subseteq 2$ℕ is negligible if there is no partial probabilistic algorithm that produces an element of this set with positive probability. The study of negligibility is of particular interest in the context of ${\rm{\Pi }}_1^0 $ classes. In this paper, we introduce the notion of depth for ${\rm{\Pi }}_1^0 $ classes, which is a stronger form of negligibility. Whereas a negligible ${\rm{\Pi }}_1^0 $ class ${\cal C}$ has the property that one cannot probabilistically compute a member of ${\cal C}$ with positive probability, a deep ${\rm{\Pi }}_1^0 $ class ${\cal C}$ has the property that one cannot probabilistically compute an initial segment of a member of ${\cal C}$ with high probability. That is, the probability of computing a length n initial segment of a deep ${\rm{\Pi }}_1^0 $ class converges to 0 effectively in n.

We prove a number of basic results about depth, negligibility, and a variant of negligibility that we call tt-negligibility. We provide a number of examples of deep ${\rm{\Pi }}_1^0 $ classes that occur naturally in computability theory and algorithmic randomness. We also study deep classes in the context of mass problems, examine the relationship between deep classes and certain lowness notions in algorithmic randomness, and establish a relationship between members of deep classes and the amount of mutual information with Chaitin’s Ω.

A new games model of the language FPC, a type theory with products, sums, function spaces and recursive types, is described. A definability result is proved, showing that every finite element of the model is the interpretation of some term of the language.

The eta rule for a set A says that an arbitrary element of A is judgementally identical to an element of constructor form. Eta rules are not part of what may be called canonical Martin-Löf type theory. They are, however, justified by the meaning explanations, and a higher order eta rule is part of that type theory. The main aim of this article is to clarify this somewhat puzzling situation. It will be argued that lower order eta rules do not, whereas the higher order eta rule does, accord with the understanding of judgemental identity as definitional identity. A subsidiary aim is to clarify precisely what an eta rule is. This will involve showing how such rules relate to various other notions of type theory, proof theory, and category theory.

The purpose of this communication is to survey a theory of liftings, as developed in author's thesis ([8]). The first result in this area was Shelah's construction of a model of set theory in which every automorphism of P(ℕ)/ Fin, where Fin is the ideal of finite sets, is trivial, or inother words, it is induced by a function mapping integers into integers ([33]). (It is a classical result of W. Rudin [31] that under the Continuum Hypothesis there are automorphisms other than trivial ones.) Soon afterwards, Velickovic ([47]), was able to extract from Shelah's argument the fact that every automorphism of P(ℕ)/ Fin with a Baire-measurable lifting has to be trivial. This, for instance, implies that in Solovay's model ([36]) all automorphisms are trivial. Later on, an axiomatic approach was adopted and Shelah's conclusion was drawn first from the Proper Forcing Axiom (PFA) ([34]) and then from the milder Open Coloring Axiom (OCA) and Martin's Axiom (MA) ([48], see §5 for definitions). Both shifts from the quotient P(ℕ)/ Fin to quotients over more general ideals P(ℕ)/I and from automorphisms to arbitrary ho-momorphisms were made by Just in a series of papers ([14]-[17]), motivated by some problems in algebra ([7, pp. 38–39], [43, I.12.11], [45, Q48]) and topology ([46, p. 537]).

This paper reports recent progress in applying nonstandard analysis to additive number theory, especially to problems involving upper Banach density.

The journal of symbolic logic began publishing in 1936. From the outset, the Journal included a Reviews Section, edited by Alonzo Church. The very first issue carried three pages of reviews, written by Bernays, Church, Rosser, and Quine.

As the first issue stated, “It is intended that this section of the Journal shall serve as a complete bibliography of current literature in the field of symbolic logic, from January 1, 1936. To this end an effort will be made to include in it, at least by title, all publications in this field, both books and articles in journals, and as far as possible these will be accompanied by signed reviews.” Thus the purpose of the Reviews Section was two-fold. For one, there was its bibliographical function: to provide a complete, suitably indexed, listing of all the publications—both books and journal articles—in symbolic logic, wherever and in whatever language published. And secondly, the reviews were to provide critical, analytical commentary on these publications, whenever possible.

The Reviews Section should be viewed as a continuation and expansion of Church's A bibliography of symbolic logic. The Bibliography was a listing, with some annotations, of the publications in symbolic logic prior to 1936. It was published as volume 1, number 4 of the Journal. Church made the listing as complete as he could, of course.

We survey some results and problems arising from a classic problem of Steinhaus: Is there a subset S of ℝ2 such that each isometric copy of ℤ2 (the lattice points in the plane) meets S in exactly one point.