This is an introduction to, and survey of, the constructive approaches to pure mathematics. The authors emphasise the viewpoint of Errett Bishop's school, but intuitionism. Russian constructivism and recursive analysis are also treated, with comparisons between the various approaches included where appropriate. Constructivemathematics is now enjoying a revival, with interest from not only logicans but also category theorists, recursive function theorists and theoretical computer scientists. This account for non-specialists in these and other disciplines.
This edited collection bridges the foundations and practice of constructivemathematics and focuses on the contrast between the theoretical developments, which have been most useful for computer science (ie: constructive set and type theories), and more specific efforts on constructive analysis, algebra and topology. Aimed at academic logician, mathematicians, philosophers and computer scientists with contributions from leading researchers, it is up to date, highly topical and broad in scope.
Integration within constructive, especially intuitionistic mathematics in the sense of L. E. J. Brouwer, slightly differs from formal integration theories: Some classical results, especially Lebesgue's dominated convergence theorem, have tobe substituted by appropriate alternatives. Although there exist sophisticated, but rather laborious proposals, e.g. by E. Bishop and D. S. Bridges , the reference to partitions and the Riemann-integral, also with regard to the results obtained by R. Henstock and J. Kurzweil , seems to give a better direction. Especially, (...) convergence theorems can be proved by introducing the concept of “equi-integrability”. (shrink)
We examine, from a constructive perspective, the relation between the complements of S, T, and S ∩ T in X, where X is either a metric space or a normed linear space. The fundamental question addressed is: If x is distinct from each element of S ∩ T, if s ϵ S, and if t ϵ T, is x distinct from s or from t? Although the classical answer to this question is trivially affirmative, constructive answers involve Markov's (...) principle and the completeness of metric spaces. (shrink)
Any philosophy of science ought to have something to say about the nature of mathematics, especially an account like constructive empiricism in which mathematical concepts like model and isomorphism play a central role. This thesis is a contribution to the larger project of formulating a constructive empiricist account of mathematics. The philosophy of mathematics developed is fictionalist, with an anti-realist metaphysics. In the thesis, van Fraassen's constructive empiricism is defended and various accounts of (...) class='Hi'>mathematics are considered and rejected. Constructive empiricism cannot be realist about abstract objects; it must reject even the realism advocated by otherwise ontologically restrained and epistemologically empiricist indispensability theorists. Indispensability arguments rely on the kind of inference to the best explanation the rejection of which is definitive of constructive empiricism. On the other hand, formalist and logicist anti-realist positions are also shown to be untenable. It is argued that a constructive empiricist philosophy of mathematics must be fictionalist. Borrowing and developing elements from both Philip Kitcher's constructive naturalism and Kendall Walton's theory of fiction, the account of mathematics advanced treats mathematics as a collection of stories told about an ideal agent and mathematical objects as fictions. The account explains what true portions of mathematics are about and why mathematics is useful, even while it is a story about an ideal agent operating in an ideal world; it connects theory and practice in mathematics with human experience of the phenomenal world. At the same time, the make-believe and game-playing aspects of the theory show how we can make sense of mathematics as fiction, as stories, without either undermining that explanation or being forced to accept abstract mathematical objects into our ontology. All of this occurs within the framework that constructive empiricism itself provides the epistemological limitations it mandates, the semantic view of theories, and an emphasis on the pragmatic dimension of our theories, our explanations, and of our relation to the language we use. (shrink)
The purpose of this paper is an axiomatic study of the interrelations between certain continuity properties. We deal with principles which are equivalent to the statements "every mapping is sequentially nondiscontinuous", "every sequentially nondiscontinuous mapping is sequentially continuous", and "every sequentially continuous mapping is continuous". As corollaries, we show that every mapping of a complete separable space is continuous in constructive recursive mathematics (the Kreisel-Lacombe-Schoenfield-Tsejtin theorem) and in intuitionism.
We apply some tools developed in categorical logic to give an abstract description of constructions used to formalize constructivemathematics in foundations based on intensional type theory. The key concept we employ is that of a Lawvere hyperdoctrine for which we describe a notion of quotient completion. That notion includes the exact completion on a category with weak finite limits as an instance as well as examples from type theory that fall apart from this.
It is argued that Hellman's arguments purporting to demonstrate that constructivemathematics cannot cope with unbounded operators on a Hilbert space are seriously flawed, and that there is no evidence that his thesis is correct.
The first part of the paper introduces the varieties of modern constructivemathematics, concentrating on Bishop's constructivemathematics (BISH). it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructivemathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.
We present a two-level theory to formalize constructivemathematics as advocated in a previous paper with G. Sambin.One level is given by an intensional type theory, called Minimal type theory. This theory extends a previous version with collections.The other level is given by an extensional set theory that is interpreted in the first one by means of a quotient model.This two-level theory has two main features: it is minimal among the most relevant foundations for constructivemathematics; (...) it is constructive thanks to the way the extensional level is linked to the intensional one which fulfills the “proofs-as-programs” paradigm and acts as a programming language. (shrink)
We discuss the foundations of constructivemathematics, including recursive mathematics and intuitionism, in relation to classical mathematics. There are connections with the foundations of physics, due to the way in which the different branches of mathematics reflect reality. Many different axioms and their interrelationship are discussed. We show that there is a fundamental problem in BISH (Bishop’s school of constructivemathematics) with regard to its current definition of ‘continuous function’. This problem is closely (...) related to the definition in BISH of ‘locally compact’. Possible approaches to this problem are discussed. Topology seems to be a key to understanding many issues. We offer several new simplifying axioms, which can form bridges between the various branches of constructivemathematics and classical mathematics (‘reuniting the antipodes’). We give a simplification of basic intuitionistic theory, especially with regard to so-called ‘bar induction’. We then plead for a limited number of axiomatic systems, which differentiate between the various branches of mathematics. Finally, in the appendix we offer BISH an elegant topological definition of ‘locally compact’, which unlike the current definition is equivalent to the usual classical and/or intuitionistic definition in classical and intuitionistic mathematics, respectively. (shrink)
claims that constructivemathematics is inadequate for spacetime physics and hence that constructivemathematics cannot be considered as an alternative to classical mathematics. He also argues that the contructivist must be guilty of a form of a priorism unless she adopts a strong form of anti-realism for science. Here I want to dispute both claims. First, even if there are non-constructive results in physics this does not show that adequate constructive alternatives could not (...) be formulated. Secondly, the constructivist adopts a 'philosophy first' approach that Hellman rejects. This deep difference means that the viability of constructivemathematics cannot yet be decided by determining whether current scientific theories require classical mathematics. We need to decide which approach is most appropriate before we can even determine how we should go about deciding whether we should be constructive or classical mathematicians. (shrink)
We represent the well-known surprise exam paradox in constructive and computable mathematics and offer solutions. One solution is based on Brouwer’s continuity principle in constructivemathematics, and the other involves type 2 Turing computability in classical mathematics. We also discuss the backward induction paradox for extensive form games in constructive logic.
The first part of the paper introduces the varieties of modern constructivemathematics, concentrating on Bishop's constructivemathematics. it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructivemathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.
The situation in constructivemathematics in the nineties is so vastly different from that in the thirties, that it is worthwhile to pause a moment to survey the development in the intermediate years. In doing so, I follow the example of Heyting, who at certain intervals took stock of intuitionistic mathematics, which for a long time was the only variety of constructivemathematics. Heyting entered the foundational debate in 1930 at the occasion of the famous (...) Königsberg meeting. (shrink)
As argued in Hellman (1993), the theorem of Pour-El and Richards (1983) can be seen by the classicist as limiting constructivist efforts to recover the mathematics for quantum mechanics. Although Bridges (1995) may be right that the constructivist would work with a different definition of 'closed operator', this does not affect my point that neither the classical unbounded operators standardly recognized in quantum mechanics nor their restrictions to constructive arguments are recognizable as objects by the constructivist. Constructive (...) substitutes that may still be possible necessarily involve additional 'incompleteness' in the mathematical representation of quantum phenomena. Concerning a second line of reasoning in Hellman (1993), its import is that constructivist practice is consistent with a 'liberal' stance but not with a 'radical', verificationist philosophical position. Whether such a position is actually espoused by certain leading constructivists, they are invited to clarify. (shrink)
We introduce a general notion of semantic structure for first-order theories, covering a variety of constructions such as Tarski and Kripke semantics, and prove that, over Zermelo–Fraenkel set theory, the completeness of such semantics is equivalent to the Boolean prime ideal theorem. Using a result of McCarty, we conclude that the completeness of Kripke semantics is equivalent, over intuitionistic Zermelo–Fraenkel set theory, to the Law of Excluded Middle plus BPI. Along the way, we also prove the equivalence, over ZF, between (...) BPI and the completeness theorem for Kripke semantics for both first-order and propositional theories. (shrink)
This paper discusses Michael Dummett’s attempt to base the use of intuitionistic logic in mathematics on a proof-conditional semantics. This project is shown to face significant obstacles resulting from the existence of variants of standard intuitionistic logic. In order to overcome these obstacles, Dummett and his followers must give an intuitionistically acceptable completeness proof for intuitionistic logic relative to the BHK interpretation of the logical constants, but there are reasons to doubt that such a proof is possible. The paper (...) concludes by proposing an alternative way of thinking about why one should use intuitionistic logic when doing mathematics. (shrink)
We give an overview of the role of equicontinuity of sequences of real-valued functions on [0,1] and related notions in classical mathematics, intuitionistic mathematics, Bishop’s constructivemathematics, and Russian recursive mathematics. We then study the logical strength of theorems concerning these notions within the programme of Constructive Reverse Mathematics. It appears that many of these theorems, like a version of Ascoli’s Lemma, are equivalent to fan-theoretic principles.
The purpose of this paper is an axiomatic study of the interrelations between certain continuity properties. We show that every mapping is sequentially continuous if and only if it is sequentially nondiscontinuous and strongly extensional, and that "every mapping is strongly extensional", "every sequentially nondiscontinuous mapping is sequentially continuous", and a weak version of Markov's principle are equivalent. Also, assuming a consequence of Church's thesis, we prove a version of the Kreisel-Lacombe-Shoenfield-Tsĕitin theorem.
Context: It is often suggested that the methodology of the programme of Constructive Reverse Mathematics (CRM) can be sufficiently clarified by a thorough understanding of Brouwer’s intuitionism, Bishop’s constructivemathematics, and classical Reverse Mathematics. In this paper, the correctness of this suggestion is questioned. Method: We consider the notion of a mathematical programme in order to compare these schools of mathematics in respect of their methodologies. Results: Brouwer’s intuitionism, Bishop’s constructivemathematics, and (...) classical Reverse Mathematics are historical influences upon the origin and development of CRM, but do not give a full “methodological explanation” for it. Implications: Discussion on the methodological issues concerning CRM is needed. Constructivist content: It is shown that the characterisation and comparison of varieties of constructivemathematics should include methodological aspects (as understood from their practices). (shrink)