In the twenties Brouwer established the well-known continuity theorem “every real function is locally uniformly continuous,” [3, 2, 5]. From this theorem one immediately concludes that the continuum is indecomposable (unzerlegbar), i.e., if ℝ = A ∪ B and A ∩ B = ∅ (denoted by ℝ = A + B), then ℝ = A or ℝ = B.

Brouwer deduced the indecomposability directly from the fan theorem (cf. the 1927 Berline Lectures, [7, p. 49]).

The theorem was published for the first time in [6], it was used to refute the principle of the excluded middle: ¬∀x ∈ ℝ (x ∈ ℚ ∨ ¬x ∈ ℚ).

The indecomposability of ℝ is a peculiar feature of constructive universa, it shows that ℝ is much more closely knit in constructive mathematics, than in classically mathematics. The classically comparable fact is the topological connectedness of ℝ. In a way this characterizes the position of ℝ: the only (classically) connected subsets of ℝ are the various kinds of segments. In intuitionistic mathematics the situation is different; the continuum has, as it were, a syrupy nature, one cannot simply take away one point. In the classical continuum one can, thanks to the principle of the excluded third, do so. To put it picturesquely, the classical continuum is the frozen intuitionistic continuum. If one removes one point from the intuitionistic continuum, there still are all those points for which it is unknown whether or not they belong to the remaining part.

This paper resolves 3 problems left open by R. M. Robinson in [3].

We recall that the set of primitive recursive functions is the closure under (i) substitution (or “composition”), and (ii) recursion, of the set P consisting of the zero, successor and projection functions (see any textbook, for instance p. 120 of [2]).

In [5] Gödel interpreted Peano arithmetic in Heyting arithmetic. In [8, p. 153], and [7, p. 344, (iii)], Kreisel observed that Gödel's interpretation extended to second order arithmetic. In [11] (see [4, p. 92] for a correction) and [10] Myhill extended the interpretation to type theory. We will show that Gödel's negative interpretation can be extended to Zermelo-Fraenkel set theory. We consider a set theory T formulated in the minimal predicate calculus, which in the presence of the full law of excluded middle is the same as the classical theory of Zermelo and Fraenkel. Then, following Myhill, we define an inner model S in which the axioms of Zermelo-Fraenkel set theory are true.

More generally we show that any class X that is (i) transitive in the negative sense, ∀x ∈ X∀y ∈ x ¬ ¬ x ∈ X, (ii) contained in the class St = {x: ∀u(¬ ¬ u ∈ x→ u ∈ x)} of stable sets, and (iii) closed in the sense that ∀x(x ⊆ X ∼ ∼ x ∈ X), is a standard model of Zermelo-Fraenkel set theory. The class S is simply the ⊆-least such class, and, hence, could be defined by S = ⋂{X: ∀x(x ⊆ ∼ ∼ X→ ∼ ∼ x ∈ X)}. However, since we can only conservatively extend T to a class theory with Δ01-comprehension, but not with Δ11-comprehension, we will give a Δ01-definition of S within T.

We study the minimal complexity of tilings of a plane with a given tile set. We note that every tile set admits either no tiling or some tiling with Kolmogorov complexity of its (n × n)-squares. We construct tile sets for which this bound is tight: all (n × n)-squares in all tilings have complexity Ω(n). This adds a quantitative angle to classical results on non-recursivity of tilings—that we also develop in terms of Turing degrees of unsolvability.

We construct a weak second-order theory of arithmetic which includes Weak König's Lemma (WKL) for trees defined by bounded formulae. The provably total functions (with -graphs) of this theory are the polynomial time computable functions. It is shown that the first-order strength of this version of WKL is exactly that of the scheme of collection for bounded formulae.

A reader coming anew to the recent work on languages which contain their own truth predicates may be perplexed by the simple question of where to begin. A first approach to the literature suggests a field which is alive and busy with investigations heading in many different directions, but there is much less indication of how various pieces fit together. There are at least two sources of this confusion. First, the literature is large and diffuse (as befits a subject which goes back over 2000 years); Visser's survey [33] aptly describes the literature as “vast but scattered, repetitive, and disconnected.” Moreover, recent interest in the field has led to a proliferation of research and publication; it seems that almost any issue of any philosophical logic journal from the mid-1980s contains some article on the topic. The second reason, in part a consequence of the first, is that while a typical article in print usually presents a good internal motivation, with clear reference to its immediate intellectual antecedents, its place in the broader picture may not be so easily discerned. The problem can be especially acute in presentations of axiomatic approaches, because decisions on certain basic questions can lie hidden in the formal and notational details which abound in any axiomatization.

In fact, though, the recent research on methods for handling self-referential truth can be seen as a body of work which is very well structured, one in which a few fundamental decisions suffice to locate any particular approach in its appropriate place on the landscape. My goal is to describe this structure and in particular to stress a few critical forks in the road, which will be the recurring metaphor throughout this paper. I will also pay particular attention to pointing out where the interesting technical and mathematical questions lie.

§1. A complete atomic modal algebra (CAMA) is a complete atomic Boolean algebra with an additional completely additive unary operator. A (Kripke) frame is just a binary relation on a nonempty set. If is a frame, then is a CAMA, where mX = {y ∣ (∃x)(y < x Є X)}; and if is a CAMA then is a frame, where is the set of atoms of and b1 < b2 ⇔ b1 ∩ mb2 ≠∅.

Now , and the validity of a modal formula on is equivalent to the satisfaction of a modal algebra polynomial identity by and conversely, so the validity-preserving constructions on frames ought to be in some sense equivalent to the identity-preserving constructions on CAMA's. The former are important for modal logic, and many of the results of universal algebra apply to the latter, so it is worthwhile to fix precisely the sense of the equivalence.

The most important identity-preserving constructions on CAMA's can be described in terms of homomorphisms and complete homomorphisms. Let and be the categories of CAMA's with homomorphisms and complete homomorphisms, respectively. We shall define categories and of frames with appropriate morphisms, and show them to be dual respectively to and . Then we shall consider certain identity-preserving constructions on CAMA's and attempt to describe the corresponding validity-preserving constructions on frames.

The proofs of duality involve some rather detailed calculations, which have been omitted. All the category theory a reader needs to know is in the first twenty pages of [7].

We examine several conditions, either the existence of a rank or a particular property of þ-forking that suggest the existence of a well-behaved independence relation, and determine the consequences of each of these conditions towards the rosiness of the theory. In particular we show that the existence of an ordinal valued equivalence relation rank is a (necessary and) sufficient condition for rosiness.

This is the first of a sequence of papers in which we will develop a foundation for the theory of computation based on a precise, mathematical notion of abstract algorithm. To understand the aim of this program, one should keep in mind clearly the distinction between an algorithm and the object (typically a function) computed by that algorithm. The theory of computable functions (on the integers and on abstract structures) is obviously relevant to this work, but we will focus on making rigorous and identifying the mathematical properties of the finer (intensional) notion of algorithm.

It is characteristic of this approach that we take recursion to be a fundamental (primitive) process for constructing algorithms, not a derived notion which must be reduced to others—e.g. iteration or application and abstraction, as in the classical λ-calculus. We will model algorithms by recursors, the set-theoretic objects one would naturally choose to represent (syntactically described) recursive definitions. Explicit and iterative algorithms are modelled by (appropriately degenerate) recursors.

The main technical tool we will use is the formal language of recursion, FLR, a language of terms with two kinds of semantics: on each suitable structure, the denotation of a term t of FLR is a function, while the intension of t is a recursor (i.e. an algorithm) which computes the denotation of t. FLR is meant to be intensionally complete, in the sense that every (intuitively understood) “algorithm” should “be” (faithfully modelled, in all its essential properties by) the intension of some term of FLR on a suitably chosen structure.

c.c.c. posets are characterised in terms of -generic conditions. This characterisation can be applied to get simple proofs of many facts about c.c.c. forcing including Con(MA + ┐CH).

The notion of a recursive function with type-2 arguments was introduced by Kleene [4]. Soon E, the type-2 object that introduces numerical quantification, began to play a central role in the development of the theory. First, Kleene [4, XLVIII] proved that the hyperarithmetical functions are exactly the functions recursive in E. Later, Gandy [1, p. 14] proved the existence of a selection operator recursive in E (that is, some ψ(х, ), partial recursive in E, having the property that, if {х}(y, ) converges for some y, then ψ(х, ) converges and is such a y).

We develop canonical rules capable of axiomatizing all systems of multiple-conclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [37]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumption-free rule. Other applications of canonical rules include a generalization of the Blok–Esakia theorem and the theory of modal companions to systems of multiple-conclusion rules or (unitary structural global) consequence relations, and a characterization of splittings in the lattices of consequence relations over monomodal or superintuitionistic logics with the finite model property.

Posner [6] has shown, by a nonuniform proof, that every degree has a complement below 0′. We show that a 1-generic complement for each set of degree between 0 and 0′ can be found uniformly. Moreover, the methods just as easily can be used to produce a complement whose jump has the degree of any real recursively enumerable in and above ∅′. In the second half of the paper, we show that the complementation of the degrees below 0′ does not extend to all recursively enumerable degrees. Namely, there is a pair of recursively enumerable degrees a above b such that no degree strictly below a joins b above a. (This result is independently due to S. B. Cooper.) We end with some open problems.

Let T be superstable. We say a type p is weakly minimal if R(p, L, ∞) = 1. Let M ⊨ T be uncountable and saturated, H = p(M). We say D ⊂ H is locally modular if for all X, Y ⊂ D with X = acl(X) ∩ D, Y = acl(Y) ∩ D and X ∩ Y ≠ ∅,

Theorem 1. Let p ∈ S(A) be weakly minimal and D the realizations of stp(a/A) for some a realizing p. Then D is locally modular or p has Morley rank 1.

Theorem 2. Let H, G be definable over some finite A, weakly minimal, locally modular and nonorthogonal. Then for all a ∈ H∖acl(A), b ∈ G∖acl(A) there area′ ∈ H, b′ ∈ G such that a′ ∈ acl(abb′A)∖acl(aA). Similarly when H and G are the realizations of complete types or strong types over A.

We reduce to a standard circuit-size complexity problem a relativisation of the P=NP question that we believe to be connected with the same question in the model for computation over the reals defined by L. Blum. M. Shub, and S. Smale. On this occasion, we set the foundations of a general theory for computation over an arbitrary structure, extending what these three authors did in the case of rings.

A paradigm of scientific discovery is defined within a first-order logical framework. It is shown that within this paradigm there exists a formal scientist that is Turing computable and universal in the sense that it solves every problem that any scientist can solve. It is also shown that universal scientists exist for no regular logics that extend first-order logic and satisfy the Löwenheim-Skolem condition.

Minimal predicates P satisfying a given first-order description ϕ(P) occur widely in mathematical logic and computer science. We give an explicit first-order syntax for special first-order ‘PIA conditions’ ϕ(P) which guarantees unique existence of such minimal predicates. Our main technical result is a preservation theorem showing PIA-conditions to be expressively complete for all those first-order formulas that are preserved under a natural model-theoretic operation of ‘predicate intersection’. Next, we show how iterated predicate minimization on PIA-conditions yields a language MIN(FO) equal in expressive power to LFP(FO), first-order logic closed under smallest fixed-points for monotone operations. As a concrete illustration of these notions, we show how our sort of predicate minimization extends the usual frame correspondence theory of modal logic, leading to a proper hierarchy of modal axioms: first-order-definable, first-order fixed-point definable, and beyond.

I intend to show that for S1, S2, and S3 the class of true formulas cannot coincide with the class of theorems. This is to hold irrespective of the meaning assigned to “◊”. when only “∼”, “▪”, and the variables are interpreted in the customary manner.

The idea of the proof is extremely simple and can be illustrated by the following argument concerning S3. The formula ~(◊(p▪~p)⥽▪p▪~p) ∨ (◊(q▪~q)⥽▪q▪~q) is a theorem of S3. Suppose now that all S3-theorems are true. Then either ~(◊(p▪~p)⥽▪p▪~p) is true (for every p) or (◊(q▪~q)⥽▪q▪~q) is true (for every q). But none of these formulas is an S3-theorem. Then some true S3-formula is not an S3-theorem. Hence, if all S3-theorems are true, some true S3-formula is not an S3-theorem. Then the class of S3-theorems cannot be identical with the class of true S3-formulas.

If K is a field of finite Morley rank, then for any parameter set A ⊆ Keq the prime model over A is equal to the model-theoretic algebraic closure of A. A field of finite Morley rank eliminates imaginaries. Simlar results hold for minimal groups of finite Morley rank with infinite acl(∅).

In this paper we continue the study of inner models of the type studied in Inner models for set theory—Part I. The present paper is concerned exclusively with a particular kind of model, the ‘super-complete models’ defined in section 2.4 of I (page 186). The condition (c) of 2.4 and the completeness condition 1.42 imply that such a model is uniquely determined when its universal class Vm is given. Writing condition (c) and the completeness conditions 1.41, 1.42 in terms of Vm , we may state the definition in the form:

3.1. Dfn. A class Vm is said to determine a super-complete model if the model whose basic notions are defined by, satisfies axioms A, B, C.

N. B. This definition is not necessarily metamathematical in nature. If desired, it could be written out quite formally as the definition of a notion ‘SCM(U)’ (‘U determines a super-complete model’) thus:

where ψ(U) is the propositional function expressing in terms of U the fact that the model determined by U according to 3.1 satisfies the relativization of axioms A, B, C. E.g. corresponding to axiom A1m , i.e., , ψ(U) contains the equivalent term . All the relativized axioms can be similarly expressed in this way by first writing out the relativized form (after having replaced all defined symbols which occur by the corresponding formulae in primitive notation) and then replacing ‘(A m )ϕ(A m ) by which is in turn replaced by , and similarly replacing ‘(xm )ϕ(xm )’ by ‘(x m )ϕ(x m )’ by ‘(X)(X ϵ U ▪ ⊃ ▪ ϕ (X)), and Thus ψ(U) is obtained in primitive notation.