Intuitionism’s disagreement with classical logic is standardly based on its specific understanding of truth. But different intuitionists have actually explicated the notion of truth in fundamentally different ways. These are considered systematically and separately, and evaluated critically. It is argued that each account faces difficult problems. They all either have implausible consequences or are viciously circular.

Brouwer’s intuitionistic program was an intriguing attempt to reform the foundations of mathematics that eventually did not prevail. The current paper offers a new perspective on the scientific community’s lack of reception to Brouwer’s intuitionism by considering it in light of Michael Friedman’s model of parallel transitions in philosophy and science, specifically focusing on Friedman’s story of Einstein’s theory of relativity. Such a juxtaposition raises onto the surface the differences between Brouwer’s and Einstein’s stories and suggests that contrary to Einstein’s (...) story, the philosophical roots of Brouwer’s intuitionism cannot be traced to any previously established philosophical traditions. The paper concludes by showing how the intuitionistic inclinations of Hermann Weyl and Abraham Fraenkel serve as telling cases of how individuals are involved in setting in motion, adopting, and resisting framework transitions during periods of disagreement within a discipline. (shrink)

A comprehensive survey of Martin-Löf's constructive type theory, considerable parts of which have only been presented by Martin-Löf in lecture form or as part of conference talks. Sommaruga surveys the prehistory of type theory and its highly complex development through eight different stages from 1970 to 1995. He also provides a systematic presentation of the latest version of the theory, as offered by Martin-Löf at Leiden University in Fall 1993. This presentation gives a fuller and updated account of the system. (...) Earlier, brief presentations took no account of the issues related to the type-theoretical approach to logic and the foundations of mathematics, while here they are accorded an entire part of the book. Readership: Comprehensive accounts of the history and philosophy of constructive type theory and a considerable amount of related material. Readers need a solid background in standard logic and a first, basic acquaintance with type theory. (shrink)

Ranging from Alan Turing’s seminal 1936 paper to the latest work on Kolmogorov complexity and linear logic, this comprehensive new work clarifies the relationship between computability on the one hand and constructivity on the other. The authors argue that even though constructivists have largely shed Brouwer’s solipsistic attitude to logic, there remain points of disagreement to this day. Focusing on the growing pains computability experienced as it was forced to address the demands of rapidly expanding applications, the content maps the (...) developments following Turing’s ground-breaking linkage of computation and the machine, the resulting birth of complexity theory, the innovations of Kolmogorov complexity and resolving the dissonances between proof theoretical semantics and canonical proof feasibility. Finally, it explores one of the most fundamental questions concerning the interface between constructivity and computability: whether the theory of recursive functions is needed for a rigorous development of constructive mathematics. This volume contributes to the unity of science by overcoming disunities rather than offering an overarching framework. It posits that computability’s adoption of a classical, ontological point of view kept these imperatives separated. In studying the relationship between the two, it is a vital step forward in overcoming the disagreements and misunderstandings which stand in the way of a unifying view of logic. (shrink)

I survey Brouwer’s weak counterexamples to classical theorems, with a view to discovering what useful mathematical work is done by weak counterexamples; whether they are rigorous mathematical proofs or just plausibility arguments; the role of Brouwer’s notion of the creative subject in them, and whether the creative subject is really necessary for them; what axioms for the creative subject are needed; what relation there is between these arguments and Brouwer’s theory of choice sequences. I refute one of Brouwer’s claims with (...) a weak counterexample of my own. I also examine Brouwer’s 1927 proof of the negative continuity theorem, which appears to be a weak counterexample reliant on both the creative subject and the concept of choice sequence; I argue that it provides a good justification for the weak continuity principle, but it is not a weak counterexample and it does not depend essentially on the creative subject. (shrink)

In this paper we discuss a particular example of the passage from the informal, but rigorous description of a concept to the axiomatic formulation of principles holding for the concept; in particular, we look at the principles of continuity and lawlike choice in the theory of lawless sequences. Our discussion also leads to a better understanding of the rôle of the so-called density axiom for lawless sequences.

Brouwer's papers after 1945 are characterized by a technique known as the method of the creating subject. It has been supposed that the method was radically new in his work, since Brouwer seems to introduce an idealized mathematician into his mathematical practice. A newly opened source, the unpublished text of a lecture of Brouwer from 1934, fully supports the conclusions of our analysis that: - There is no idealized mathematician involved in the method;- The method was not new at all;- (...) Brouwer uses an incomplete sequence, also known as choice sequence, in this method, which is special. The method does not take its place in the standard works on choice sequences. (shrink)

Most empirical accounts of design suggest that designing is an activity where objects and representations are progressively constructed. Despite this fact, whether design is a constructive process or not is not a question directly addressed in the current design research. By contrast, in other fields such as Mathematics or Psychology, the notion of constructivism is seen as a foundational issue. The present paper defends the point of view that forms of constructivism in design need to be identified and integrated as (...) a founda- tional element in design research as well. In fact, a look at the literature reveals at least two types of constructive processes that are well embedded in design research: first, an interac- tive constructivism, where a designer engages a conversation with media, that allows changing the course of the activity as a result of this interaction; second, a social constructivism, where designers need to handle communication and nego- tiation aspects, that allows integrating individuals' expertise into the global design process. A key feature lacking these well-established paradigms is the explicit consideration of creativity as a central issue of design. To explore how cre- ative and constructivist aspects of design can be taken into account conjointly, the present paper pursues a theoretical approach. We consider the roots of constructivism in math- ematics, namely the Intuitionist Mathematics, in order to shed light on the original insights that led to the development of a notion of constructivism. Intuitionists describe mathe- matics as the process of mental mathematical constructions realized by a creative subject over time. One of the most original features of intuitionist constructivism is the intro- duction of incomplete objects into the heart of mathematics by means of lawless sequences and free choices. This allows the possibility to formulate undecided propositions and the consideration of creative acts within a formal constructive process. We provide an in-depth analysis of intuitionism from a design standpoint showing that the original notion is more than a pure constructivism where new objects are a mere bottom-up combination of already known objects. Rather, intuitionism describes an imaginative constructivist process that allows combining bottom-up and top-down processes and the expansion of both propositions and objects with free choices of a creative subject. We suggest that this new form of constructivism we identify is also relevant in interpreting conventional design processes and discuss its status with respect to other forms of constructivism in design. (shrink)