§1. Introduction. In this survey of the history of constructivism. more space has been devoted to early developments (up till ca. 1965) than to the work of the later decades. Not only because most of the concepts and general insights have emerged before 1965, but also for practical reasons: much of the work since 1965 is of a too technical and complicated nature to be described adequately within the limits of this article.

Constructivism is a point of view (or an attitude) concerning the methods and objects of mathematics which is normative: not only does it interpret existing mathematics according to certain principles, but it also rejects methods and results not conforming to such principles as unfounded or speculative (the rejection is not always absolute, but sometimes only a matter of degree: a decided preference for constructive concepts and methods). In this sense the various forms of constructivism are all ‘ideological’ in character.

Constructivism as a specific viewpoint emerges in the final quarter of the 19th century, and may be regarded as a reaction to the rapidly increasing use of highly abstract concepts and methods of proof in mathematics, a trend exemplified by the works of R.Dedekind and G. Cantor.

The mathematics before the last quarter of the 19th century is, from the viewpoint of today, in the main constructive, with the notable exception of geometry, where proof by contradiction was commonly accepted and widely employed.

The proof of the irrationality of √2 involves proving that there cannot be positive integers n and m such that n2 = 2m2. This can be proved with a simple number-theoretic argument: First we note that n must be even, whence m must also be even, and hence both are divisible by 2. Then we observe that this is a contradiction if we assume that n is chosen minimally. There is also a geometric proof known already to Euclid, but the proof given by Tennenbaum seems to be entirely new. It is as follows: In Picture 1 we have on the left hand side two squares superimposed, one solid and one dashed. Let us assume that the area of the solid square is twice the area of the dashed square. Let us also assume that the side of each square is an integer and moreover the side of the solid square is as small an integer as possible. In the right hand side of Picture 1 we have added another copy of the dashed square to the lower left corner of the solid square, thereby giving rise to a new square in the middle and two small squares in the corners. The combined area of the two copies of the original dashed square is the same as the area of the original big solid square. In the superimposed picture the middle square gets covered by a dashed square twice while the small corner squares are not covered by the dashed squares at all. Hence the area of the middle square must equal the combined area of the two corner squares.

The work of Stanley Tennenbaum in set theory was centered on the investigation of Suslin's Hypothesis (SH), to which he made crucial contributions. In 1963 Tennenbaum established the relative consistency of ¬SH, and in 1965, together with Robert Solovay, the relative consistency of SH. In the formative period after Cohen's 1963 discovery of forcing when set theory was transmuting into a modern, sophisticated field of mathematics, this work on SH exhibited the power of forcing for elucidating a classical problem of mathematics and stimulated the development of new methods and areas of investigation.

§ 1 discusses the historical underpinnings of SH. § 2 then describes Tennenbaum's consistency result for ¬SH and related subsequent work. § 3 then turns to Tennenbaum's work with Solovay on SH and the succeeding work on iterated forcing and Martin's Axiom. To cast an amusing sidelight on the life and the times, I relate the following reminiscence of Gerald Sacks from this period, no doubt apocryphal: Tennenbaum let it be known that he had come into a great deal of money, $30,000,000 it was said, and started to borrow money against it. Gerald convinced himself that Tennenbaum seriously believed this, but nonetheless asked Simon Kochen about it. Kochen replied “Well, with Stan he might be one per-cent right. But then, that's still $300,000.”

§1. Suslin's problem. At the end of the first volume of Fundamenta Mathematicae there appeared a list of problems with one attributed to Mikhail Suslin [1920], a problem that would come to be known as Suslin's Problem.

In this first of a series of papers on ultrafinitistic themes, we offer a short history and a conceptual pre-history of ultrafinistism. While the ancient Greeks did not have a theory of the ultrafinite, they did have two words, murios and apeiron, that express an awareness of crucial and often underemphasized features of the ultrafinite, viz. feasibility, and transcendence of limits within a context. We trace the flowering of these insights in the work of Van Dantzig, Parikh, Nelson and others, concluding with a summary of requirements which we think a satisfactory general theory of the ultrafinite should satisfy.

First papers often tend to take on the character of manifestos, road maps, or both, and this one is no exception. It is the revised version of an invited conference talk, and was aimed at a general audience of philosophers, logicians, computer scientists, and mathematicians. It is therefore not meant to be a detailed investigation. Rather, some proposals are advanced, and questions raised, which will be explored in subsequent works of the series.

Our chief hope is that readers will find the overall flavor somewhat “Tennenbaumian”.

§1. Introduction: The radical Wing of constructivism. In their Constructivism in Mathematics, A. Troelstra and D. Van Dalen dedicate only a small section to Ultrafinitism (UF in the following). This is no accident: as they themselves explain therein, there is no consistent model theory for ultrafinitistic mathematics.

§1. Introduction. It is a unique feature of the field of mathematical logic, that almost any technical result from its various subfields: set theory, models of arithmetic, intuitionism and ultrafinitism, to name just a few of these, touches upon deep foundational and philosophical issues. What is the nature of the infinite? What is the significance of set-theoretic independence, and can it ever be eliminated? Is the continuum hypothesis a meaningful question? What is the real reason behind the existence of non-standard models of arithmetic, and do these models reflect our numerical intuitions? Do our numerical intuitions extend beyond the finite at all? Is classical logic the right foundation for contemporary mathematics, or should our mathematics be built on constructive systems? Proofs must be correct, but they must also be explanatory. How does the aesthetic of simplicity play a role in these two ideals of proof, and is there ever a “simplest” proof of a given theorem?

The papers collected here engage each of these questions through the veil of particular technical results. For example, the new proof of the irrationality of the square root of two, given by Stanley Tennenbaum in the 1960s and included here, brings into relief questions about the role simplicity plays in our grasp of mathematical proofs. In 1900 Hilbert asked a question which was not given at the Paris conference but which has been recently found in his notes for the list: find a criterion of simplicity in mathematics. The Tennenbaum proof is a particularly striking example of the phenomenon Hilbert contemplated in his 24th Problem.

§1. A tale of two problems. The formal independence of Cantor' Continuum Hypothesis from the axioms of Set Theory (ZFC) is an immediate corollary of the following two theorems where the statement of the Cohen's theorem is recast in the more modern formulation of the Boolean valued universe.

Theorem 1 (Gödel, [3]). Assume V = L. Then the Continuum Hypothesis holds.

Theorem 2 (Cohen, [1]). There exists a complete Boolean algebra, B, such that

VB ⊨ “The Continuum Hypothesis is false”.

Is this really evidence (as is often cited) that the Continuum Hypothesis has no answer?

Another prominent problem from the early 20th century concerns the projective sets, [8]; these are the subsets of ℝn which are generated from the closed sets in finitely many steps taking images by continuous functions, f : ℝn → ℝn, and complements. A function, f : ℝ → ℝ, is projective if the graph of f is a projective subset of ℝ × ℝ. Let Projective Uniformization be the assertion:

For each projective set A ⊂ ℝ × ℝ there exists a projective function, f : ℝ → ℝ, such that for all x ∈ ℝ if there exists y ∈ ℝ such that (x, y) ∈ A then (x, f(x)) ∈ A.

The two theorems above concerning the Continuum Hypothesis have versions for Projective Uniformization. Curiously the Boolean algebra for Cohen's theorem is the same in both cases, but in case of the problem of Projective Uniformization an additional hypothesis on V is necessary. While Cohen did not explicitly note the failure of Projective Uniformization, it is arguably implicit in his results.

Stanley Tennenbaum's influential 1959 theorem asserts that there are no recursive nonstandard models of Peano Arithmetic (PA). This theorem first appeared in his abstract [42]; he never published a complete proof. Tennenbaum's Theorem has been a source of inspiration for much additional work on nonrecursive models. Most of this effort has gone into generalizing and strengthening this theorem by trying to find the extent to which PA can be weakened to a subtheory and still have no recursive nonstandard models. Kaye's contribution [12] to this volume has more to say about this direction.

This paper is concerned with another line of investigation motivated by two refinements of Tennenbaum's theorem in which not just the model is nonrecursive, but its additive and multiplicative reducts are each nonrecursive. For the following stronger form of Tennenbaum's Theorem credit should also be given to Kreisel [5] for the additive reduct and to McAloon [26] for the multiplicative reduct.

Tennenbaum's Theorem. If M = (M, +, ·, 0, 1, ≤) is a nonstandard model of PA, then neither its additive reduct (M, +) nor its multiplicative reduct (M, ·) is recursive.

What happens with other reducts? The behavior of the order reduct, as is well known, is quite different from that of the additive and multiplicative reducts. The order type of every countable nonstandard model is ω + (ω* + ω) · η, where ω and η are the order types of the nonnegative integers ℕ and the rationals ℚ, respectively.

§1. Introduction. In 1964 Shepherdson [6] introduced a weak system of arithmetic, Open Induction (OI), in which the Tennenbaum phenomenon does not hold. More precisely, if we restrict induction just to open formulas (with parameters), then we have a recursive nonstandard model. Since then several authors have studied Open Induction and its related fragments of arithmetic. For instance, since Open Induction is too weak to prove many true statements of number theory (It cannot even prove the irrationality of √2), a number of algebraic first order properties have been suggested to be added to OI in order to obtain closer systems to number theory. These properties include: Normality [9] (abbreviated by N), having the GCD property [8], being a Bezout domain [3, 8] (abbreviated by Bez), and so on. We mention that GCD is stronger than N, Bez is stronger than GCD and Bez is weaker than IE1 (IE1 is the fragment of arithmetic based on the induction scheme for bounded existential formulas and by a result of Wilmers [11], does not have a recursive nonstandard model). Boughattas in [1, 2] studied the non-finite axiomatizability problem and established several new results, including: (1) OI is not finitely axiomatizable, (2) OI + N is not finitely axiomatizable.

Substitution for predicate letters is a syntactically intricate inference procedure that is derivable in standard systems of non-modal quantificational logic. It allows a new theorem to be deduced from a given theorem ϕ by replacing an atomic formula Pτ1 ··· τn within ϕ by another formula ψ, of arbitrary complexity, involving the terms τ1, …, τn. The intricacy comes in stating the restrictions that must be placed on free variables of ϕ and ψ for the substitution to be allowed.

Church [1956, p. 289] gives some historical notes on this rule, pointing out that it was inadequately stated in early works of Hilbert and Ackerman, Carnap, and Quine; and first correctly stated, but not in full generality, in Hilbert and Bernays's Grundlagen der Mathematik in 1934. Church himself calls the predicate letter P a functional variable, viewing it as a variable whose values are propositional functions of individuals. In non-modal logic, this means that P is interpreted as an n-ary function Un → {truth, falsehood} from individuals to truth-values.

Intuitively, a logic that is closed under substitution for predicate letters is one whose theorems represent “universal laws”, expressing properties that hold of all predicates, i.e. hold no matter what interpretation is given to the predicate letters, hence hold no matter what formulas are (correctly) substituted for them.

This book is about the possible-worlds semantic analysis of systems of logic that have quantifiers binding individual variables. Our approach is based on a notion of “admissible” model that places a restriction on which sets of worlds can serve as propositions. We show that admissible models provide semantic characterisations of a wide range of logical systems, including many for which the well-known model theory of Kripke [1963b] is incomplete. The key to this is an interpretation of quantification that takes into account the admissibility of propositions.

This is a subject that bristles with choices and challenges. Should terms be treated as rigid designators, or should their denotations vary from world to world? Should individual constants and variables be treated the same in this respect, or differently? Should each world have its own domain of existing individuals over which the quantifiable variables range, or should there be just a single domain of individuals? If there are varying domains, how should they relate to each other? Can any function from worlds to individuals be regarded as the “meaning” of some individual concept? Should an arbitrary mapping from individuals to propositions be admissible as a propositional function? Can we deductively axiomatise the class of valid formulas determined by each answer to these questions?

We now extend our language for quantified modal logic by adding a predicate symbol ≈ for an identity relation, allowing us to express assertions about the identity of individuals. A two-sorted language is developed, with one sort of term standing for individual concepts, represented as partial functions from worlds to individuals, and the other sort specialising to concepts that are rigid, i.e. have the same value in accessible worlds. The identity predicate allows the existence predicate ε to be defined, taking ετ to be the self-identity formula τ ≈ τ, whose corresponding proposition/truth set is the domain of the partial function interpreting τ. The use of admissibility is extended from propositions to individuals by requiring each model to have a designated set of admissible individual concepts, within which there is a designated set of admissible rigid ones.

We axiomatise the set of formulas that are valid in these models, using a new inference rule that allows deduction of assertions of non-existence (¬ετ). The logic characterised by Kripkean models is then treated separately. The final section of the chapter gives a semantic analysis of Russelian definite description terms ιx.ϕ in this context, and shows how to construct canonical models and axiomatisations for logics in languages that have these description terms as well as the identity predicate.

The main aim of this chapter is to set out a new kind of admissible model theory for the propositional relevant logic R and its quantified extension RQ. First we review the relational semantics for R of Routley and Meyer [1973], and its adaptation by Mares and Goldblatt [2006] to an admissible semantics for RQ. Then we introduce an alternative kind of structure, called a cover system, motivated by topological ideas about “local truth” from the Kripke-Joyal semantics for intuitionistic logic in topos theory. These are combined with a modelling of negation by a binary world-relation of orthogonality, or incompatibility, as in [Goldblatt 1974], and an operation of combination, or “fusion”, of worlds to interpret relevant implication. Characteristic model systems for R have an algebra Prop of admissible propositions, while those for RQ have a set PropFun of admissible propositional functions as well.

We then show that by conservatively adding an intuitionistic implication connective to R it is possible to characterise that logic by models in which all possible propositions are admissible. The prospects for a similar analysis of RQ are considered at the end.

Routley-Meyer Models for R

The subject of relevant logic (also known as relevance logic) is based on the view that an implication A → B can only be true if the meaning of A is relevant to the meaning of B.