Foundations of Constructive Mathematics

Before studying the foundations of any subject, it is desirable (and perhaps necessary) to have a thorough grasp of the subject itself. In the case of constructive mathematics, this grasp can best be attained by the actual practice of constructive mathematics, combined with a comparison of constructive and classical (not-necessarily-constructive) mathematics. With this in mind, we shall give a series of illustrative examples. This chapter is more nearly a review of the subject than an introduction to it; the reader who is truly without experience of constructive mathematics should first turn to Bishop [1967] or Bridges [1979] for an introduction.

It is possible to distinguish at least five different philosophies of constructive mathematics, plus at least one “semi-constructive” philosophy. By a philosophy of constructive mathematics, we mean a philosophy that subscribes to the two fundamental principles: On the basis of these two principles alone, a considerable amount of agreement concerning mathematical practice can be reached. That is to say, any constructive mathematician can read Bishop or Bridges and find the proofs correct. That is not say that every constructive mathematician would agree with Bishop on all philosophical points! In fact, there are some significant differences between the various schools. In this chapter, we shall examine these different views in detail.

The doctrine stated above (in 1927) became, in the late forties and the fifties, the foundation of a fairly extensive body of mathematics, in which one replaces the vague intuitive concept of “law” or “rule” by the precisely-defined concept of “recursive function”. This chapter presents the main results. Of course, every positive result of constructive mathematics translates into a corresponding theorem of recursive mathematics. A large number of such translations of positive results has been spelled out explicitly in Aberth [1980]. There also exists a variety of strange and delightful, sometimes counter-intuitive, negative results in recursive mathematics. Negative, that is, in the sense that they show that some classical theorem fails in recursive mathematics; although many of these results are positive in the sense that they actually exhibit a counterexample to the recursive version of the theorem. One value of such results is the following: if we show that a theorem fails in recursive mathematics, we can stop wasting our time trying to prove it in constructive mathematics — at least unless we are willing to use some axiom which contradicts Church’s thesis. Just to give one example: a number of mathematicians tried to prove that if ƒ: [0,1]→R is uniformly continuous and everywhere positive, then inf ƒ(x) is positive too — a problem which was mentioned in Bishop [1967] and Bridges [1979]. But this fails in recursive mathematics, as we shall see below.

It may be somewhat surprising to some that after four chapters of a book with the subtitle, “Metamathematical Studies”, not a single formal system has yet appeared. The first four chapters of this book are metamathematical, in the sense that no mathematics is done for its own sake. Even the extensive presentation of recursive analysis is of interest here mainly because it shows us what not to try to prove constructively. Nevertheless, formal systems have been and are an important tool in studying the foundations of mathematics, and the rest of the book will be full of formal systems. We take the viewpoint, however, that our main purpose is to study the foundations of mathematics, by means of metamathematics, and formal systems are a tool to that end. Since formal systems are often quite beautiful and enticing objects of study, it is worthwhile to analyze clearly how we intend to use them; otherwise there is a danger of forgetting our original purpose while under the spell of our formal systems.

The debate over the truth or falsity of Kant’s statement is still going on, and is far beyond the scope of this book. However, if “nature” is replaced by “mathematics” in the first sentence of the quotation, the issue specializes to the controversy over constructive versus classical mathematics: does everything in mathematics proceed according to rules? Evidently the subject of “rules” plays a central role. In the spirit of this book, we will examine some formal theories of rules, to see if they can shed any light on the issues. At this point the reader may reasonably wish to inquire, “What exactly are the issues?” I should tentatively reply,

In 1945 Kleene forged a link between the two previously unconnected areas of intuitionism and recursive function theory, by finding a way to interpret the intuitionistic logic using recursive functions for the “we can find” of the intuitionistic “there exists”. He defined the notion of “recursive realizability”, which is a precisely-defined concept designed to interpret the “rules” which are inherent in the constructive meaning of the logical operations, especially the quantifier combination ∀x∃y and implication. For example, a statement ∀n∃mR (n m) will be “recursively realized” by an index e such that for every n, R(n,{e}(n)), at least in case R is recursive. In general, one should think of realizability as a sort of “constructive model”: the intuition is that, when defining a model of a constructive theory, one ought not only to give an interpretation to the constants and variables (as in classical model theory) but also to the logical operations. Some notion of “rule” is implicit in the intuitionistic logic — that notion ought to be modeled.

There are two obvious approaches to constructive set theory: (i) Carefully add some set variables to a simpler theory, cautiously add some axioms about them, and try to explain the constructive meaning of the theory, (ii) Start with classical set theory, throw out the law of the excluded middle and any axioms which imply it, and see what is left over. We shall begin with the second approach; the first approach will be followed in Chap. X.

This chapter is primarily of technical interest, in the sense that nothing in the rest of the book depends upon it, and in the sense that the proofs are rather complicated. Nevertheless, the existence property has attracted considerable attention, since many people feel a constructive theory “ought to” have the existence property. It has turned out to be difficult to establish the existence property for constructive set theories, and new techniques have been developed for the purpose. From this perspective, the methods of this chapter are of more than “mere” technical interest, in that they represent the frontier of knowledge in the subject of constructive set theory.

In this chapter we will discuss Feferman’s theories of rules and classes, and some variants of them invented by the author. These theories are based on the theory EON described in Chap. VI. We add to EON a unary predicate S(x) to denote, as in IZF, “x is a set”. This does not mean, however, that we have the same notion of “set” in mind as when formulating IZF. Feferman deliberately used the words “classification” or “class” instead; the difference between “class” and “set” will be discussed below. Given the formal set-up just described, the question that has to be answered is

This chapter will describe the approach to formal systems for constructive mathematics initiated by Martin-Löf. Of the various systems described in this book, these systems have so far been the most used by computer scientists interested in actual implementation; this will be discussed briefly at the end of the chapter. The word “type” in the title is similar to “set”; but also similar to the “data type” of computer science. A “type” is a set which can serve as the range of a variable. The evolution of programming languages has resulted in more and more flexible and general syntax for the definition of types; Martin-Löf s systems can be viewed as another step in this direction. They can also be viewed from the logical side as a kind of restricted set theory; not just any set can be a type, but only what we have called in previous chapters a “completely presented set”.

In this chapter we will present model constructions, or otherwise expressed, “concrete” realizability interpretations, for constructive set theories (sub-theories of intuitionistic ZF), patterned after the models of EM ₀ and ML ₁ given in preceding chapters. These models are of interest for two distinct reasons:

It is not uncommon for metamathematical results to require the formalization of other metamathematical arguments. The most familiar example of this phenomenon is probably Gödel’s second incompleteness theorem, whose proof proceeds (roughly speaking) by formalizing the proof of the first incompleteness theorem. The simplest example that arises in the metamathematics of constructive theories (as opposed to classical theories) is Church’s rule, which we shall now consider. Suppose we have a theory T and an argument to show that every term t which T proves to be in N^N actually denotes a recursive function.

Forcing was introduced for classical set theory by P. Cohen in the sixties. It was soon shown to be equivalent to Scott’s Boolean models, which had their origins in earlier semantics for intuitionistic systems, namely the topological models and Beth models. In the past decade, there has been an explosion of interest in model-theoretic constructions which bear some relation to forcing, but from another direction: category theory. The Kripke and Beth models have been generalized to models in an arbitrary topos. It is not part of the plan of this book to touch upon this material. This book isresult-oriented and not method-oriented; we need forcing for only two results: (i) a clear analysis of the functionals which provably map 2^N into N, and (ii) certain conservative extension results. We shall obtain these two (kinds of) results by means of direct definitions of forcing, not requiring any category theory. The connections between the definitions given here and the more general notions of topoi (or more particularly, sheaf models) are explained in Grayson [1983], and the interested reader may consult Fourman-Scott [1979], Fourman-Hyland [1979], Lambek-P. Scott [TA], or the books Goldblatt [1979] and Johnstone [1977] for more exposition about sheaf and topos models.

Continuity and constructivity have an intimate relationship, which has been recognized for nearly a century, studied for half a century, and is still fruitful today. The connection is easy to see: If we are to be able to compute some number F(x) for a real number x, we must be able to proceed with the computation given approximations to x. Our method for computing F(x) should then yield approximations to F(x). Evidently F will then be continuous. Recognition of this idea goes back at least to Hadamard, who formulated three conditions for a problem in differential equations to be “well-posed” (see e.g. Courant-Hilbert [1953], p. 227):