Douglas S. Bridges
Douglas S. Bridges

Techniques of Constructive Analysis, pages vi-vii

You will find here the Preface sections, sometimes with other extracts, from most of my books. Note that, although I refer to 'my' books, only three were authored solely by me.

Apartness and Uniformity

Preface

The problem of finding a suitable constructive framework for general topology is important and elusive.                    

Errett Bishop in a letter, dated 14 April 1975, to Douglas Bridges            

                                                                                                      

In the mid-1970s, Douglas Bridges came across the article [CHN], advocating the use of nearness in the teaching of first courses in analysis. This led him to consider a constructive theory based on proximity---or, rather, the constructively more appropriate opposite notion of apartness---as a possible alternative approach to topology. Not, at that stage, being sufficiently mathematically experienced to make significant progress with this idea, he put it on one side until February 2000, when he and Luminiţa Vîţă began the project on apartness spaces that is discussed in the present monograph. Clearly, two heads were better than one, as we were able to initiate a project that, in the intervening years, has grown substantially, with contributions from mathematicians in several countries and continents.


What do we mean by constructive in this context, and why might a constructive approach to topology be interesting or significant? The answer to the first question is simple: by constructive mathematics we mean, roughly, mathematics with intuitionistic logic and a set- or type-theoretic foundation that precludes the derivation of the law of excluded middle; in other words, we mean mathematics carried out in the style of the late Errett Bishop in Foundations of Constructive Analysis (FCA). Every proof that is constructive in this sense embodies an algorithm that can be, and in several cases has been, extracted and then implemented; further, the original proof shows that the implementable algorithm (if correctly extracted) meets its specifications. One other important feature of Bishop's constructive mathematics is that it is completely consistent with classical mathematics---mathematics using classical logic.


In regard to the second question, we recall Bishop's deflationary remark (FCA, page 63):

 

Very little is left of general topology after that vehicle of classical mathematics has been

taken apart and reassembled constructively. With some regret, plus a large measure of 

relief, we see this flamboyant engine collapse to constructive size. 

 

At the time he wrote FCA, Bishop firmly believed that computation in analysis required uniform continuity---normally on compact sets---rather than the weaker notion of pointwise (let alone sequential) continuity:


The concept of a pointwise continuous function is not relevant. A continuous function

[on the real line] is one that is uniformly continuous on compact intervals. 

FCA,pages ix-x  


Since the theorem asserting the uniform continuity of every pointwise continuous, real-valued mapping on the closed interval cannot be proved within Bishop-style constructive mathematics, general topology, essentially a pointwise matter, would therefore have little constructive relevance; what was needed was a framework (such as metric-space theory) in which uniform notions could be expressed.


Bishop's remark, taken with his suggestion, in Appendix A to FCA, that constructive theories like that of distributions might rely on ad hoc topological notions, may have served to deflect attention away from the problem of finding a suitable constructive framework for general topology. The advantage of solving this problem would presumably be that we would have a general, and hence almost certainly clarifying, framework for topological matters. Moreover, work of Ishihara and others, 20 years after the publication of FCA, has shown that even sequential continuity has an important role in Bishop-style mathematics; so there is definitely a place for a constructive theory of abstract spatial relationships that covers such highly non-uniform types of continuity.


One can certainly tackle topology by simply constructivising the classical development of the subject from the usual three axioms about open sets. However, the theory of apartness that we present in this book does much more, by encompassing both point-set topology and the theory of uniform spaces. This, we believe, enables us to see those subjects in a clearer light.


We now outline the contents of the three chapters in our book, which begins with one that introduces informal constructive (intuitionistic) logic and set theory, as well as---very briefly---the basic notions and notations for metric and topological spaces.


In Chapter 2 we introduce axioms for a point-set apartness, a more computationally informative notion than nearness. We then explore some of the elementary consequences of our axioms, and examine the associated topology and various types of continuity of mappings. One interesting feature of our constructive approach is that intuitionistic logic reveals distinctions that are invisible to the classical eye. For example, we present three natural notions of continuity for maps between point-set apartness spaces, notions that coalesce classically but are quite distinct constructively.


After dealing with continuity, the chapter continues with a discussion of convergence for nets in an apartness space, followed by a study of the apartness structure on the product of two apartness spaces. It ends with some remarks about impredicativity and how that phenomenon might be avoided.

The theory really gets interesting---and a lot harder---when, in Chapter 3, we consider apartness between subsets. The five axioms on which this part of the theory is based enable us to bring most of the work on point-set apartness across to the set-set environment. Every set-set apartness gives rise to a point-set apartness in the obvious way: a point is apart from a set if the singleton of x is apart from S.


The canonical example of a set-set apartness arises from a quasi-uniform structure (which, if a certain symmetry condition holds, becomes a uniform structure). Having introduced both apartness and quasi-uniform spaces, we are well placed to examine the connection between, on the one hand, the uniform continuity of a mapping between quasi-uniform spaces and, on the other, strong continuity, in which if the two subsets of the codomain are apart, then their pre-images under he mapping are apart in the domain. It is straightforward to show that uniform continuity entails strong continuity; but the converse direction of entailment is much harder to deal with. Similar difficulties are found in our discussion of the relation between Cauchy nets in the usual uniform-space sense, and nets that have the property of total Cauchyness relative to the apartness structure associated with a given uniform structure. (The corresponding property of total completeness of an apartness space X, whereby every totally Cauchy sequence in has a limit in X, is classically equivalent to the compactness of the underlying apartness topology on X.)


The difficulties, alluded to above, in the proofs of certain results are unified by our introduction of a general proof technique which has several applications in the theory and which resembles---but is considerably more complex than---a well-known technique introduced into constructive analysis by Ishihara. Not only does our technique apply to the study of strong and uniform continuity, but also it leads to a neat proof that, under certain conditions, the uniform convergence of a sequence of mappings between uniform spaces is equivalent to their being convergent in an apartness-space sense. (In order to provide a sound framework for the study of convergence of functions, we introduce structures, constructively weaker than apartness and quasi-uniform ones, on the space of mappings from a set into an apartness spaceY.)


After a discussion of totally Cauchy nets, the chapter continues by introducing notions of locatedness that lift that fundamental property of subsets of a metric space into the wider context of a uniform space. In particular, we connect locatedness and another important property, total boundedness (one that lifts more easily from the metric to the uniform context). We then deal with product apartness spaces, paying, as in the case of point-set apartness, particular attention to the flow of properties, such as total completeness, between a product apartness space and its two "factors".


In the next section of the chapter we discuss a form of connectedness for apartness spaces. Then we introduce a special structure, denoted by B_w, on an apartness space . We use this to discuss uniform structures that are compatible with a given apartness structure on a set. Although we cannot generally prove that there is such a uniform structure, we can show that there is at most one totally bounded uniform structure of this sort, which is then the smallest compatible uniform structure. In addition, the properties of lead us to a notion of nearness between subsets of an apartness space. If the apartness space has a strong separation property, then the point-set restriction of this nearness coincides with the notion of nearness associated, in Chapter 2, with the point-set apartness on B_w. Finally, we discuss Diener's alternative approach to compactness in apartness spaces, based on his notions of neat locatedness and neat compactness.


There are other, successful and important, constructive approaches to topology that we should mention: the ones based on the notions of frame, locale, and formal topology. Some work clarifying the relation between these "point-free" approaches and our theory of apartness spaces is the subject of the Postlude at the end of the book. We believe that constructive mathematics has room for both the theory of apartness and the point-free approaches to topology, and that these should be regarded as equally valid and viable.


Douglas Bridges and Luminiţa Simona Vîţă
24 January 2011

Extract from Chapter 3

Apartness between sets:  https://docs.zoho.com/file/2e8ypa75c6e5ad02e43789e97a123917761d1 

_______________________________________________________________________________________________________________________________________________________


Techniques of Constructive Analysis

Preface
Rosencrantz:  Shouldn't we be doing something... constructive?
Guildenstern:  What did you have in mind?
                                                                                               Tom Stoppard

We have written this book in order to provide an introduction to constructive analysis, emphasising techniques and results that have been obtained in the last twenty years. The intended readership comprises postgraduate or senior undergraduate students, and professional researchers, in mathematics or theoretical computer science. We hope that our work will help spread the message that doing mathematics constructively is interesting (it can even be fun!) and challenging, and produces new, deep computational information.


 An appreciation of the distinction between constructive and nonconstructive has become more widespread in this era of desk- and lap-top computers. Nevertheless, there are few books devoted to the development of mathematics in a rigorously constructive/computable fashion, although there are some, primarily concentrating on logic and foundations, in which the odd chapter deals with constructive mathematics proper as distinct from its underlying logic or set theory. It is now almost forty years since the publication of Errett Bishop's seminal monograph Foundations of Constructive Analysis (FCA), which in our view is one of the most remarkable intellectual documents of the twentieth century, and more than twenty since the appearance of its outgrowth Constructive Analysis (B&B). In the intervening years there has been considerable activity in constructive analysis, algebra, and topology; in related foundational areas such as type theory; and in the relation between constructive mathematics and computer science (for example, program extraction from proof. Believing that a new introduction to the mathematical, as distinct from the foundational, side of the subject is overdue, we embarked upon this monograph.


Our book is intended not to replace, but to supplement, FCA and the later volume B&B. Both of those two monographs cover aspects of analysis, such as Haar measure and commutative Banach algebras, that we do not mention. We cover some topics that are found in FCA and B&B (it would be almost inconceivable to produce a book like ours, dealing with constructive mathematics for non-experts, without proving, for example, basic results about locatedness and total boundedness); but we have tried to provide improved proofs whenever possible. However, much of the material we present was simply not around at the time of writing of either FCA or B&B.


Instead of systematically developing analysis, beginning with the real line and continuing through metric, normed, and Hilbert spaces to its higher reaches, we have chosen to write the chapters around certain themes or techniques (hence our title). For example, Chapter 3 is devoted to the λ-technique, which, since its first use in the proof of Lemma 7 on page 177 of FCA, has become a surprisingly powerful tool with applications in many areas of constructive analysis. A major influence in the application of the λ-technique was a remarkable paper by Ishihara, showing that a subtle use of the technique could enable us to prove disjunctions whose proof, although trivial with classical logic, appears at first sight to be constructively out of the question. That paper opened up many new pathways in constructive analysis.


Chapter 1 introduces constructive mathematics and lays the foundations for the later chapters. In Chapter 2 we first present a new construction of the real numbers, motivated by ideas of Aberth. After deriving standard properties such as the completeness of R, we introduce metric spaces, with the major theme of locatedness, and normed linear spaces. When we discuss metric, normed, and Hilbert spaces, we assume some familiarity with the standard classical definitions of those concepts and with those elementary classical properties that pass over unchanged to the constructive setting.


Chapter 3 we have already referred to. The main theme of Chapter 4 is finite-dimensionality, but the chapter concludes with an introduction to Hilbert spaces.


Chapter 5 deals with convexity in normed spaces. Starting with some elementary convex geometry in Rⁿ, the chapter goes on to handle separation and Hahn-Banach theorems, locally convex spaces, and duality. Following Bishop, we describe those linear functionals that are weak ∗-uniformly continuous on the unit ball of the dual space. We then give a new application of the technique used to prove that result, thereby characterising certain continuous linear functionals on the space of bounded operators on a Hilbert space.
In Chapter 6 we derive a range of results associated with the theme of locatedness and with the λ-technique introduced in Chapter 3. We pay particular attention to necessary and sufficient conditions for convex subsets of a normed space to be located, and to connections between properties of an operator on a Hilbert space and those of its adjoint (when that adjoint exists: it may not always do so constructively). The final section of the book deals with a relatively recent version of Baire's theorem and its applications, and culminates in constructive versions of three of the big guns in functional analysis: the open mapping, inverse mapping, and closed graph theorems.


Which parts of the book deal with new material, compared with what appeared in FCA or B&B? We have already mentioned the new construction of the real numbers, in Chapter 2. Notable novelties in the later chapters include all but one result in Chapter 3 on the λ-technique; the section on convexity, Ishihara's results on exact Hahn-Banach extensions, and our characterisation theorem for certain continuous linear functionals, all in Chapter 5; and virtually all of Chapter 6. Throughout the book there are what we hope will be seen as improvements and simplifications of proofs of many results that were given in FCA  or B&B.


What do we mean by "constructive analysis" in the title of this book? We do not mean analysis carried out with the usual "classical" logic within a framework, such as recursive function theory, designed to capture the concept of computability. In our view, such a notion of constructive has at least two drawbacks. First, by working within, say, the recursive setting, it can make the mathematics look less like normal mathematics and much harder to read. Secondly, the recursive constraint removes the possibility of other interpretations of the mathematics, such as Brouwer's intuitionistic one. Our approach, on the other hand, has neither of these features: the mathematics looks and reads just like the mathematics one is used to from undergraduate days, and all our proofs and results are valid in several models. They are valid in the recursive model, in intuitionistic mathematics, and, we believe, in any of the models for "computable mathematics" (including Weihrauch's Type Two Effectivity Theory, within which Andrej Bauer has found a realisability interpretation of constructive mathematics. They are also valid proofs in standard mathematics with classical logic. For example, our proof of the Hahn-Banach theorem is, as it stands, a valid algorithmic proof of the classical Hahn-Banach theorem for separable spaces. Moreover---and this is one advantage of a constructive proof in general---our proof embodies an algorithm for the construction of the functional whose existence is stated in the theorem. This algorithm can be extracted from the proof, and, as an undeserved bonus, the proof itself demonstrates that the algorithm is correct or, in computer science parlance, meets its specifications.


So how do we achieve all this? Simply by changing the logic with which we do our mathematics! Instead of using classical logic, we systematically use intuitionistic logic, which was abstracted by Heyting from the practice of Brouwer's intuitionistic mathematics. The remarkable fact is that every proof carried out with intuitionistic logic is fully constructive/algorithmic. (Is this the "secret on the point of being blabbed" that appears in the epigraph to Bishop's book?) Unfortunately, too few mathematicians outside the mathematical logic community are aware of this serendipity, and dismiss both intuitionistic logic and constructive mathematics as at best a marginal curiosity. This contrasts sharply with the theoretical computer science community, in which there is considerable knowledge of, and interest in, the computational power of intuitionistic logic.


Reading constructive mathematics demands careful interpretation. A theorem in this book might look like a familiar one from classical analysis, but with more complicated hypotheses and proof. However, the statement of the theorem will be phrased so that the explicit algorithmic interpretation is left to the reader; and the additional hypotheses will be necessary for a constructive proof, which will contain algorithmic information that is excluded from the classical proof by the latter's use of principles outside intuitionistic logic. Consider, for example, the following statement:


     (*)  Let C be an open convex subset of a normed space X, let ξ ∈ C, and let z ∈ X be bounded away from C.             Then the boundary of C intersects the segment [ξ,z] joining ξ and z.


This is trivial to prove classically; but to find/construct the (necessarily unique) point in which the boundary of C intersects [ξ,z] is a totally different matter. The constructive theorem (Proposition 5.1.5 below) requires us to postulate that the union of C and its metric complement -C (the set of points bounded away from C) be dense in X, and that X itself be a complete normed space. The constructive proof, though elementary, requires some careful geometrical estimation that would be supererogatory in the natural classical proof-by-contradiction. The benefit of that estimation and of the use of intuitionistic logic is that we could extract from the constructive proof an implementable algorithm for finding the point where the segment crosses the boundary. In turn, this would enable us to produce an algorithm for constructing separating hyperplanes and Hahn-Banach extensions of linear functionals, under appropriate hypotheses.


We could have made the algorithmic interpretation of the constructive version of (*) explicit by stating the proposition in this way:

       There is a "boundary crossing algorithm" which, applied to the data consisting of (i) an open convex set          C in a Banach space X such that C ∪ -C is dense in X, (ii) a point ξ of C, and (iii) a point z of -C, constructs            the point where the boundary of C intersects the segment [ξ,z].


Even this is not really explicit enough. A full description of the data to which the boundary crossing algorithm applies would require explicit information about the algorithms for such things as: membership of C; the convergence of Cauchy sequences in X; the computation, for given x in X and ε > 0, of a point y of
C -C such that ‖x - y‖ < ε (and even the decision between the cases "y C" and "y ∈ -C"); and so on. Such explicit description of algorithmic hypotheses would become an ever greater burden on writer and reader alike as the book probed deeper and deeper into abstract analysis. It is a matter of sound sense, even sanity, to unburden ourselves from the outset, relying on the reader's native wit in the interpretation of the statements of our constructive lemmas, propositions, and theorems.


We should make it clear that we are not advocating the exclusive use of intuitionistic logic in mathematics. That logic is, we believe, the natural and right one to use when dealing with the constructive content of mathematics. To abandon classical logic in those fields (such as the higher reaches of set theory) where constructivity is of little or no significance makes no sense whatsoever. Nevertheless, it is remarkable how much mathematics actually has what Bishop called "a deep underpinning of constructive truth".

                                                                                                                                                                  Douglas Bridges and Luminiţa Simona Vîţă

                                                                                                                                                                                          Christchurch, New Zealand                                                                                                                                                                                                                 January 2006   

                                                    

Extract from Chapter 2

Constructing the real numbers:   https://docs.zoho.com/file/2e8ypd6b781880be847dd822245f281fd41b1 

_______________________________________________________________________________________________________________________________________________________                                           

Foundations of Real and Abstract Analysis


Sweet Analytics, 'tis thou hast ravished me.      Marlowe, Faustus
The stone which the builders refused is become the head stone of the corner.            Psalm cxviii, 22
...from so simple a beginning endless forms most beautiful and most wonderful have been, and are being, evolved.     Darwin, The origin of species (Darwin)

Preface

The core of this book, Chapters 3 through 5, presents a course on metric, normed, and Hilbert spaces at the senior/graduate level. The motivation for each of these chapters is the generalisation of a particular attribute of the Euclidean space Rⁿ: in Chapter 3, that attribute is distance; in Chapter 4, length; and in Chapter 5, inner product. In addition to the standard topics that, arguably, should form part of the armoury of any graduate student in mathematics, physics, mathematical economics, theoretical statistics, ... , this part of the book contains many results and exercises that are seldom found in texts on analysis at this level. Examples of the latter are Wong's Theorem (3.3.12) showing that the Lebesgue covering property is equivalent to the uniform continuity property, and Motzkin's result (5.2.2) that a nonempty closed subset of Euclidean space has the unique closest point property if and only if it is convex.


The sad reality today is that, perceiving them as one of the harder parts of their mathematical studies, students contrive to avoid analysis courses at almost any cost, in particular that of their own educational and technical deprivation. Many universities have at times capitulated to the negative demand of students for analysis courses and have seriously watered down their expectations of students in that area. As a result, mathematics majors are graduating, sometimes with high honours, with little exposure to anything but a rudimentary course or two on real and complex analysis, often without even an introduction to the Lebesgue integral.


For that reason, and also in order to provide a reference for material that is used in later chapters, I chose to begin this book with a long chapter providing a fast-paced course of real analysis, covering convergence of sequences and series, continuity, differentiability, and (Riemann and Riemann-Stieltjes) integration. The inclusion of that chapter means that the prerequisite for the book is reduced to the usual undergraduate sequence of courses on calculus. (One-variable calculus would suffice, in theory, but a lack of exposure to more advanced calculus courses would indicate a lack of the mathematical maturity that is the hidden prerequisite for most senior/graduate courses.)


Chapter 2 is designed to show that the subject of differentiation does not end with the material taught in calculus courses, and to introduce the Lebesgue integral. Starting with the Vitali Covering Theorem, the chapter develops a theory of differentiation almost everywhere that underpins a beautiful approach to the Lebesgue integral due to F. Riesz. One minor disadvantage of Riesz's approach is that, in order to handle multivariate integrals, it requires the theory of set-valued derivatives, a topic sufficiently involved and far from my intended route through elementary analysis that I chose to omit it altogether. The only place where this might be regarded as a serious omission is at the end of the chapter on Hilbert space, where I require classical vector integration to investigate the existence of weak solutions to the Dirichlet Problem in three-dimensional Euclidean space; since that investigation is only outlined, it seemed justifiable to rely only on the reader's presumed acquaintance with elementary vector calculus. Certainly, one-dimensional integration is all that is needed for a sound introduction to the Lp spaces of functional analysis, which appear in Chapter 4.


Chapters 1 and 2 form Part I (Real Analysis) of the book; Part II (Abstract Analysis) comprises the remaining chapters and the appendices. I have already summarised the material covered in Chapters 3 through 5. Chapter 6, the final one, introduces functional analysis, starting with the Hahn-Banach Theorem and the consequent separation theorems. As well as the common elementary applications of the Hahn-Banach Theorem, I have included some deeper ones in duality theory. The chapter ends with the Baire Category Theorem, the Open Mapping Theorem, and their consequences. Here most of the applications are standard, although one or two unusual ones are included as exercises.


The book has a preliminary section dealing with background material needed in the main text, and three appendices. The first appendix describes Bishop's construction of the real number line and the subsequent development of its basic algebraic and order properties; the second deals briefly with axioms of choice and Zorn's Lemma; and the third shows how some of the material in the chapters---in particular, Minkowski's Separation Theorem---can be used in the theory of Pareto optimality and competitive equilibria in mathematical economics. Part of my motivation in writing Appendix C was to indicate that mathematical economics is a far deeper subject than is suggested by the undergraduate texts on calculus and linear algebra that are published under that title.


I have tried, wherever possible, to present proofs so that they translate mutatis mutandis into their counterparts in a more abstract setting, such as that of a metric space (for results in Chapter 1) or a topological space (for results in Chapter 3). On the other hand, some results first appear as exercises in one context before reappearing as theorems in another: one example of this is the Uniform Continuity Theorem, which first appears as Exercise (1.4.8: 8) in the context of a compact interval of R, and which is proved later, as Corollary (3.3.13), in the more general setting of a compact metric space. I hope that this procedure of double exposure will enable students to grasp the material more firmly.


The text covers just over 300 pages, but the book is, in a sense, much larger, since it contains nearly 750 exercises, which can be classified into at least the following, not necessarily exclusive, types:

  •   applications and extensions of the main propositions and theorems;
  •   results that fill in gaps in proofs or that prepare for proofs later in the book;
  •   pointers towards new branches of the subject;
  •   deep and difficult challenges for the very best students.

The instructor will have a wide choice of exercises to set the students as assignments or test questions. Whichever ones are set, as with the learning of any branch of mathematics it is essential that the student attempt as many exercises as the constraints of time, energy, and ability permit.


It is important for the instructor/student to realise that many of the exercises (especially in Chapters 1 and 2) deal with results, sometimes major ones, that are needed later in the book. Such an exercise may not clearly identify itself when it first appears; if it is not attempted then, it will provide revision and reinforcement of that material when the student needs to tackle it later. It would have been unreasonable of me to have included major results as exercises without some guidelines for the solution of the non-routine ones; in fact, a significant proportion of the exercises of all types come with some such guideline, even if only a hint.


Although Chapters 3 through 6 make numerous references to Chapters 1 and 2, I have tried to make it easy for the reader to tackle the later chapters without ploughing through the first two. In this way the book can be used as a text for a semester course on metric, normed, and Hilbert spaces. (If Chapter 2 is not covered, the instructor may need to omit material that depends on familiarity with the Lebesgue integral---in particular Section 4 of Chapter 4.) Chapter 6 could be included to round off an introductory course on functional analysis.


Chapter 1 could be used on its own as a second course on real analysis (following the typical advanced calculus course that introduces formal notions of convergence and continuity); it could also be used as a first course for senior students who have not previously encountered rigorous analysis. Chapters 1 and 2 together would make a good course on real variables, in preparation for either the material in Chapters 3 through 5 or a course on measure theory. The whole book could be used for a sequence of courses starting with real analysis and culminating in an introduction to functional analysis.


I have drawn on the resource provided by many excellent existing texts cited in the bibliography, as well as some original papers. My first drafts were prepared using the T³ Scientific Word Processing System; the final version was produced by converting the drafts to LaTeX and then using Scientific Word. Both T³ and Scientific Word are products of TCI Software Research, Inc.


It is right and proper for me here to acknowledge my unspoken debt of gratitude to my parents. This book really began 35 years ago, when, with their somewhat mystified support and encouragement, I was beginning my love affair with mathematics and in particular with analysis. It is sad that they did not live to see its completion.

Douglas Bridges
28 January 1997
Extract from Chapter 2

The Lebesgue integral as an antiderivative: https://docs.zoho.com/file/2e8ypeed2f404c12c4721af193ac1ee84d3f8 

_______________________________________________________________________________________________________________________________________________________



Representations of Preference Orderings


Preface

A basic assumption made by pioneers of classical microeconomics such as Edgeworth and Pareto was that the ranking of a consumer's preferences could always be measured numerically, by associating to each possible consumption bundle a real number that measured its utility: the greater the utility, the more preferred was the bundle, and conversely. It took several decades before the naivety of this assumption was seriously challenged by economists, such as Wold, attempting to find conditions under which it could be justified mathematically. Wold's work was the first in a long chain of results of that type, leading to the definitive theorems of Debreu and others in the 1960s, and subsequently to the refinements and generalisations that have appeared in the last twenty-five years.


Out of this historical background there has appeared a general mathematical problem which, as well as having applications in economics, psychology, and measurement theory, arises naturally in the study of sets bearing order relations:

Given some kind of ordering ≽ on a set S, find a real-valued mapping u on S such that for any elements x,y of S, x ≽ y if and only if u(x) ≥ u(y). If also S has a topology (respectively, differential structure), find conditions that ensure the continuity (respectively, differentiability) of the mapping u.

A mapping u of this kind is called a representation of the ordering ≽.


In this book we have tried to gather together, using a uniform, consistent terminology and notation, a number of the most important representation theorems which are scattered widely, with a corresponding variety of nomenclature, throughout the literature of several branches of mathematics. Our objective was to make those results accessible, in a more-or-less self-contained presentation, to readers with a basic knowledge of set theory, topology, measure theory, functional analysis, and differentiable manifolds. A rudimentary knowledge of economics will provide motivation for some of the concepts in the book, but is not essential for the understanding of our results.


Our choice of topics was determined partly by our own preferences, partly by our lack of expertise in certain fields, and partly by our desire to make the book of readable length. Whatever the omissions, we believe that we have included the most significant theorems and methods in the field.


We have assigned credit for results to the best of our knowledge. However, there are some ideas that are part of the folklore of the subject and have been included without attribution of credit. We acknowledge our indebtedness to books of Fishburn, Roberts, and Davey and Priestley in the preparation of Chapter 1.

Douglas Bridges and Ghanshyam Mehta
Hamilton, N.Z., and Brisbane, Australia
22 October 1994

_______________________________________________________________________________________________________________________________________________________



Computability: A Mathematical Sketchbook

'I can't believe that!' said Alice. `Can't you?' the Queen said in a pitying tone. 'Try again: draw a long breath and shut your eyes.' Alice laughed. 'There's no use trying,' she said: 'One can't believe impossible things.' 'I daresay you haven't had much practice,' said the Queen.             
Lewis Carroll, Through the Looking Glass
Preface

My intention in writing this book is to provide mathematicians and mathematically literate computer scientists with a brief but rigorous introduction to a number of topics in the abstract theory of computation, otherwise known as computability theory or recursion theory. It develops major themes in computability, such as Rice's Theorem and the Recursion Theorem, and provides a systematic account of Blum's abstract complexity theory up to his famous speed-up theorem.


A relatively unusual aspect of the book is the material on computable real numbers and functions, in Chapter 4. Parts of this material are found in a number of books, but I know of no other at the senior/beginning graduate level that introduces elementary recursive analysis as a natural development of computability theory for functions from natural numbers to natural numbers. (Some of the work in this book---notably, Proposition (4.28) and the application of the Recursion Theorem preceding Exercises (5.14)---appears to be original.) This part of the book is definitely for mathematicians rather than computer scientists and has a prerequisite of a first course in elementary real analysis; it can be omitted, without rendering the subsequent chapters unintelligible, in a course including the more standard topics in computability theory found in Chapters 4-6.


I believe, against the trend towards weighty, all-embracing treatises (vide the typical modern calculus text), that many mathematicians would like to be able to purchase books that give them insight into unfamiliar branches of the subject in a relatively short compass and without requiring a major investment of time, effort, or money. Following that belief, I have had to exclude from this book many topics---such as detailed proofs of the equivalence of various mathematical models of computation, the theory of degrees of unsolvability, and polynomial and nonpolynomial complexity---whose absence will be deplored by at least some of the experts in the field. I hope that my readers will be inspired to pursue their study of recursion theory elsewhere.


A number of excellent texts on computability theory are primarily aimed at computer scientists rather than mathematicians, and so do not always maintain the level of rigour that would be expected in a modern text on, say, abstract algebra. I have tried to maintain that higher level of rigour throughout, even at the risk of deflecting the interest of mathematically insecure computer scientists.


Ideally, all mathematics and computer science majors should be exposed to at least some of the material found in this book. It horrifies me that in some universities such majors can still graduate ignorant of the theoretical limitations of the computer, as expressed, for example, by the undecidability of the halting problem (Theorem (4.2)). A short course on computability, accessible even to students below junior level, would comprise Chapters 1-3 and the material in Chapter 4 up to Exercises (4.7). A longer course for more advanced undergraduates would also include Rice's theorem and the Recursion Theorem, from Chapter 5, and at least parts of Chapter 6. The entire book, including the difficult material on recursive analysis from Chapter 4, would be suitable for a course for bright seniors or beginning graduate students.


I have tried to make the book suitable for self-study. To this end, it includes solutions for most of the exercises. Those exercises for which no solutions are given have been marked with the asterisk {*}; of varying levels of difficulty, they provide the instructor with material for homework and tests. The exercises form an integral part of the book and are not just there for the students' practice; many of them develop material that is used in later proofs, which is another reason for my inclusion of solutions.


My interest in constructive mathematics leads me to comment here on the logic of computability theory. This is classical logic, the logic used by almost all mathematicians in their daily work. However, the use of classical logic has some perhaps undesirable consequences. Consider the following definition of a function f on the set N of natural numbers: for all n, f(n) equals 1 if the Continuum Hypothesis is true, and equals 0 if the Continuum Hypothesis is false. (The Continuum Hypothesis (CH) says that the smallest cardinal number greater than ℵ₀, the cardinality of N, is the cardinality of the set of all subsets of N. The work of Cohen and Gödel shows that neither CH nor its negation can be proved within ZFC: Zermelo-Fraenkel set theory plus the axiom of choice.)  Since most mathematicians are formalists on weekdays and Platonists on Sundays, at least on Sundays most of us would accept this as a good definition of a function f. According to classical logic, f is computable because there exists an algorithm that computes it; that algorithm is either the one which, applied to any natural number n, outputs 1, or else the one which, applied to any natural number n, outputs 0. Since the Continuum Hypothesis is independent of the axioms of ZFC, the standard framework of mathematics, we will never be able to tell, using ZFC alone, which of the two algorithms actually is the one that computes f.


It appears from this example, eccentric though it may be, that the standard theory of computation does not exactly match computational practice, in which we would expect to pin down the algorithms that we use. A facetious question may reinforce my point: what would happen to an employee who, in response to a request that he write software to perform a certain computation, presented his boss with two programs and the information that, although one of those programs performed the required computation, nobody could ever tell which one?


With classical logic there seems to be no way to distinguish between functions that are computed by programs which we can pin down and those that are computable but for which there is no hope of our telling which of a range of programs actually performs the desired computation. To handle this problem successfully, we need a different logic, one capable of distinguishing between existence in principle and existence in practice. For example, with constructive (intuitionistic) logic the problem disappears, since f is then not properly defined: it is only properly defined if we can decide the truth or falsehood of the Continuum Hypothesis (which we cannot) and therefore which of the two possible algorithms computes f.
Having said this, let me stress that, despite the inability of classical logic to make certain distinctions of the type I have just dealt with, I have followed standard practice and used classical logic throughout this book. For a development of computability theory using intuitionistic logic see Chapter 3 of Varieties of Constructive Mathematics (D.S. Bridges and F. Richman, London. Math. Soc. Lecture Notes 97, CUP, 1987).

Not only the logic but also most of the material that I have chosen is standard, although some of the exercises and examples are new.


The origins of my book lie in courses I gave at the University of Buckingham (England), New Mexico State University (USA), and the University of Waikato (New Zealand). I am grateful to the students in those classes for the patience with which they received various slowly improving draft versions.


Special thanks are due to Fred Richman for many illuminating conversations about recursion theory; to Paul Halmos for his advice and encouragement; and to Cris Calude, Nick Dudley Ward, Graham French, Hazel Locke, and Steve Merrin, all of whom have read versions of the text and made many helpful corrections and suggestions. As always, it is my wife and children who suffered most as the prolonged birth of this work took so much of my care and attention; I present the book to them with love and gratitude.

 Douglas S. Bridges
  Hamilton, N.Z.,May 1993

Extract from Chapter 4

Computable numbers and functions:  https://docs.zoho.com/file/2e8yp55fe0534f4c24849ad1dd3ccc8de6fc2 

_________________________________________________________________________________________________________________________________________________________________________________________________________________


Varieties of Constructive Mathematics

Preface

In Hilary Term, 1981, Douglas Bridges gave a course of lectures on intuitionism and constructive mathematics in the Mathematical Institute of Oxford University. Shortly afterwards, he invited Fred Richman to join in the writing of a book based (as it turns out, rather loosely) on those lectures. The book now lies in front of the reader, as an introduction to the spirit and practice of modern constructive mathematics.


There are several excellent works---such as Beeson's Foundations of Constructive Mathematics and Dummett's Elements of Intuitionism---on the logical and philosophical foundations of constructive mathematics; and there are others, such as Bishop's seminal treatise Foundations of Constructive Analysis, dealing with the detailed development of major portions of mathematics within a constructive framework. The present book is intended to land between those two positions: specifically, we hope that, with a minimum of philosophy and formal logic, and without requiring of the reader too great an investment of time and effort over technical details, it will leave him with a clear conception of the problems and methods of the three most important varieties of modern constructive mathematics.


Since classical mathematics, as practised by all but a tiny minority of mathematicians, appears to offer a much less arduous route to discovery, and a far greater catalogue of successes, than its constructive counterpart, one may well ask: Why should anyone, other than a devotee of a constructivist philosophy, be interested in learning about constructive mathematics? We believe there are several reasons why one might be so interested.


First, there is the richer structure of constructive mathematics that flows from the deepened meaning of existence. In the classical interpretation, an object exists if its non-existence is contradictory. There is a clear distinction between this meaning of existence and the constructive, algorithmic one, under which an object exists only if we can construct it, at least in principle. As Bishop has said, such 'meaningful distinctions deserve to be maintained'.


Second, there is the unexpected role played by intuitionistic logic and constructive methods in topos theory. Any theorem in constructive mathematics may be interpreted as a classical theorem about a topos; if the topos is suitably chosen, then the theorem may have classical interest outside of topos theory. For example, constructive theorems about diagonalizing matrices over the reals may be interpreted as classical theorems about diagonalizing matrices over the ring of continuous functions on a compact metric space.


Finally, there is the possibility of applications of constructive mathematics to areas such as numerical mathematics, physics, and computer science. For computer science, we refer the reader to Martin-Löf's paper 'Constructive mathematics and computer programming' (in: Logic, Methodology and the Philosophy of Science VI, North-Holland, 1982), and to the recent book Implementing Mathematics with the Nuprl Proof Development System, by Constable et al. (Prentice-Hall, 1986).


We now outline the contents of our book. In Chapter 1 we introduce the three varieties of constructive mathematics with which we shall be concerned: Bishop's constructive mathematics, Brouwer's intuitionistic mathematics, and the constructive recursive mathematics of the Russian school of Markov; we also construct the real line R and examine its basic properties.


In Chapter 2 we discuss, within Bishop's mathematics, a range of topics in analysis. These topics are chosen to illustrate distinctive features of the practice of constructive mathematics, such as the splitting of one classical theorem (for example, Baire's theorem) into several inequivalent constructive ones, and the investigation of important notions, like locatedness, with little or no classical significance. A similar approach to constructive algebra is found in Chapter 4, which culminates in a constructive treatment of the Hilbert basis theorem. Chapter 4 also offers some comparisons between constructive algebra and classical recursive algebra.


Chapter 3 contains the essentials of constructive recursive mathematics, and is based on Richman's axiomatic approach to Church's thesis. This approach greatly simplifies the presentation of mathematics within the recursive framework, and leads to particularly perspicuous proofs of Specker's theorem and the existence of a compact subset of R that is not Lebesgue measurable.


Chapter 5 deals with intuitionistic mathematics, by formulating axioms which capture the mathematical essence of Brouwer's approach. The elements of intuitionistic mathematics are developed, including Brouwer's famous theorem that every real-valued function on a compact interval is uniformly continuous.
In Chapter 6 the three varieties of constructive mathematics are compared by an examination of the status within each of the classical proposition: If f is a uniformly continuous mapping of [0,1] into the positive real line, then the infimum of f is positive.
    
The final chapter deals with intuitionistic logic and topos models, mainly through the presentation of a few examples. We treat this material somewhat superficially, not wishing to involve the reader in a detailed development of the logic and category theory necessary for a fully rigorous treatment.

Douglas S. Bridges,   Buckingham, England        
Fred Richman, Las Cruces, New Mexico, USA   
 

Extract from Chapter 4

Constructive algebra:   https://docs.zoho.com/file/2e8yp2d5c83fea00f4b498c52eb1af1203d7a