Texte intégral en libre accès disponible depuis le 01 septembre 2009.
1This volume focuses on constructivism, which is here intended as a general philosophical attitude arising from reflection upon mathematics. We are concerned with the ways in which this idea is applied in science and with the theoretical reflections these applications give rise to. For this purpose this volume presents different sides of the general idea of constructivity, with the intention of getting a broader, and hopefully insightful, understanding of questions such as ‘what is a construction’, ‘what constructs what’ and so on.
- 1 The interested reader may consult for example A. Troelstra, History of Constructivism in the 20th (...)
2What interests us, then, is not so much the history of constructivism1 but the ideas behind it, and their possible applications.
3We attempt to present the problem with recourse to an analogy. The dichotomy constructive / non-constructive, in fact, resembles a little the more general concrete / abstract distinction. Concerning mathematical objects, the complication is that what we speak about are abstract (not having a physical reality) objects, so that in our case what the distinction amounts to is one between ‘abstract’ and ‘too abstract’ where the difference is not just a question of emphasis. One might say that in such an ethereal sphere as that of mathematics, to have a (abstract) construction for an object is the only way to achieve some kind of concreteness, as far as this is possible. As in the case of the concrete / abstract distinction, also in the case of the constructive / non-constructive dichotomy there is no standard account of how the distinction is to be drawn. What is needed is indeed an explanation or a description of what would make for constructivity. As it turns out, many different answers are possible, depending on the sense in which one thinks mathematical objects can be built.
4In the concrete / abstract dichotomy one thematizes the concept of concrete (as we think we have a better understanding of it) and attempts to define the abstract objects as those that lack typical features possessed by concrete things, singling out, by way of negation, some criteria for abstractness (e.g., non-spatiality, causal inefficacy). In the constructive / non-constructive dichotomy one thematizes instead the concept of non-constructive, for, with a little exaggeration, that might be said to be the default position in modern mathematics, and thus a fortiori what is taken to be better understood. The situation is then specular, and one says that constructive objects as those possessing certain features that non-constructive objects lack. For example one might say that constructive objects are those possessing a computational content. This is the way the mathematicians of Bishop’s school understand the word ‘constructive’.
5While it is easy to see why computable mathematical entities (those given, for example, by means of an algorithm) can be accepted as constructive, in other approaches to see the idea which lies behind ‘being a constructive object’ is more elaborate. L.E.J. Brouwer (1881-1966), the initiator of intuitionism, for example accepted as mathematical objects non-algorithmic infinite sequences of natural numbers which are incomplete and which cannot be completed. These are Brouwer’s infinitely proceeding sequences (choice sequences), the conceptual building blocks of the intuitionistic theory of the continuum. The idea which motivates the possibility of considering such entities as constructive is that computations involving infinitely proceeding sequences only use a finite amount of information, namely an initial segment of the infinite sequences.
- 2 Constructive Mathematics: A Foundation for Computable Analysis, in Theoretical Computer Science, 2 (...)
6While there is substantial disagreement among the constructivists on what counts as a constructive object, there is substantial accord on what counts as the logic of constructive mathematics: intuitionistic logic. In the words of Douglas Bridges, this is the logic that is “forced upon us when we want to work constructively”.2 The supporting reason is that the intuitionistic interpretation of connectives and quantifiers would reflect the meaning they have in mathematical constructive proofs.
- 3 This is the so-called Quine-Putnam indispensability argument.
- 4 For the case of the semi-constructive predicative mathematics one such example is given by Feferma (...)
7The constructive / non-constructive distinction matters in philosophy, because both constructive and non-constructive objects and reasonings appear to present certain general problems in epistemology and in the philosophy of mathematics. For example, according to construc-tivists, it is impossible to have genuine knowledge of non-constructive objects. The problem for constructivists is then to show that non-constructive objects are especially problematic and to offer a viable alternative. More pointedly, from a philosophical point of view the constructivist ideally must show that it is possible to do mathematics without non-constructive assumptions or at least show how far one can go constructively. Another related question is that of the relation between constructive mathematics and science. Classical mathematics, at least some parts of it, is successfully applied in science, so that the non-constructivist can claim that science requires and at the same time justifies classical mathematics.3 While this does not imply that constructive mathematics has no application in science, the constructivist is asked to react in some way, either by saying that being applicable is not the main concern of mathematics or by showing how constructive theories indeed relate to science.4
8In the first article Constructing Ordinals Herman Ruge Jervell presents his own way of representing ordinals by finite trees, and thus building up the Veblen hierarchy. Towards the end of the paper the author mentions the difficulty of extending his ideas further in a constructive way.
9The second paper Brouwer’s Real Thesis on Bars by Wim Veldman, a piece in traditional intuitionistic mathematics, focuses on the intuitio-nistic Bar theorem presenting a possible formulation of Brouwer’s Thesis on Bars. The formulation uses the formalism of Kleene-Vesley. The last section deals with some examples of the applications of Brouwer’s thesis on bars in intuitionistic analysis.
10The third paper Reverse Mathematics in Bishop’s Constructive Mathematics by Hajime Hishihara begins with a vivid description of constructive reverse mathematics, which consists in classifying theorems in analysis in terms of their degree of constructivity. The connections and differences of this discipline to classical reverse mathematics are shown. The main part of the article consist in a comprehensive survey of results. In Section 5, the notion of representability for pointwise continuous functions is introduced.
11In the fourth article, Equality in the Presence of Apartness: An Application of Structural Proof Analysis to Intuitionistic Axiomatics, Bianca Boretti and Sara Negri present, through contraction- and cut-free sequent calculi, the theories of apartness, equality, and n-stable equality. By methods of proof analysis they obtain a purely proof-theoretic characterization of the equality fragment of apartness.
12The article At the Heart of Analysis: Intuitionism and Philosophy by David McCarty is concerned with contrasting various forms of intuitioni-stic mathematics with the classical, and argues that intuitionism is first and foremost mathematics, and only subsequently involves a philosophical stance.
13Colin McLarty’s article Two Constructivist Aspects of Category Theory is about the (unexpected) links of category theory to constructivism, namely the closeness of topos logic to intuitionistic logic, and the fact that much of general category theory is somehow constructive.
- 5 Dialogue Systems as Proof Editors, Journal of Logic, Language and Information 13 (2004), 225-240.
14The last article, Type Theory and Universal Grammar by Aarne Ran-ta, takes a look at the history of the idea of universal grammar and compares it with multilingual grammars, as formalized in the Grammatical Framework, GF, previously introduced by Ranta.5 The constructivist idea of formalizing mathematics piece by piece, in a weak logical framework, rather than trying to reduce everything to one single strong theory, is the model that guides the development of grammars in GF.
2 Constructive Mathematics: A Foundation for Computable Analysis, in Theoretical Computer Science, 219 (1999), 95-109.
3 This is the so-called Quine-Putnam indispensability argument.
4 For the case of the semi-constructive predicative mathematics one such example is given by Feferman’s system W of variable finite types that seems to be sufficient for all mathematics necessary for doing science and can be proved theoretically reducible to first order Peano arithmetic. See S. Feferman, Why a Little Bit Goes a Long Way: Logical Foundations of Scientifically Applicable Mathematics, PSA 1992 Vol. 2 (1993). Reprinted with minor corrections and additions in S. Feferman, In the Light of Logic, Oxford University Press, 1998, 284ff.
5 Dialogue Systems as Proof Editors, Journal of Logic, Language and Information 13 (2004), 225-240.Haut de page
Pour citer cet article
Gerhard Heinzmann et Giuseppina Ronzitti, « Foreword », Philosophia Scientiæ [En ligne], CS 6 | 2006, mis en ligne le 01 septembre 2009, consulté le 19 mai 2013. URL : http://philosophiascientiae.revues.org/400 ; DOI : 10.4000/philosophiascientiae.400Haut de page
Tous droits réservésHaut de page