This book brings together philosophers, mathematicians and logicians to penetrate important problems in the philosophy and foundations of mathematics. In philosophy, one has been concerned with the opposition between constructivism and classical mathematics and the different ontological and epistemological views that are reflected in this opposition. The dominant foundational framework for current mathematics is classical logic and set theory with the axiom of choice. This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively pursued (...) today is predicativistic constructivism based on Martin-Löf type theory. Associated philosophical foundations are meaning theories in the tradition of Wittgenstein, Dummett, Prawitz and Martin-Löf. What is the relation between proof-theoretical semantics in the tradition of Gentzen, Prawitz, and Martin-Löf and Wittgensteinian or other accounts of meaning-as-use? What can proof-theoretical analyses tell us about the scope and limits of constructive and predicative mathematics? (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)

This volume is the first ever collection devoted to the field of proof-theoretic semantics. Contributions address topics including the systematics of introduction and elimination rules and proofs of normalization, the categorial characterization of deductions, the relation between Heyting's and Gentzen's approaches to meaning, knowability paradoxes, proof-theoretic foundations of set theory, Dummett's justification of logical laws, Kreisel's theory of constructions, paradoxical reasoning, and the defence of model theory. The field of proof-theoretic semantics has existed for almost 50 years, but the term (...) itself was proposed by Schroeder-Heister in the 1980s. Proof-theoretic semantics explains the meaning of linguistic expressions in general and of logical constants in particular in terms of the notion of proof. This volume emerges from presentations at the Second International Conference on Proof-Theoretic Semantics in Tübingen in 2013, where contributing authors were asked to provide a self-contained description and analysis of a significant research question in this area. The contributions are representative of the field and should be of interest to logicians, philosophers, and mathematicians alike. (shrink)

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.

We may try to explain proofs as chains of valid inference, but the concept of validity needed in such an explanation cannot be the traditional one. For an inference to be legitimate in a proof it must have sufficient epistemic power, so that the proof really justifies its final conclusion. However, the epistemic concepts used to account for this power are in their turn usually explained in terms of the concept of proof. To get out of this circle we may (...) consider an idea within intuitionism about what it is to justify the assertion of a proposition. It depends on Heyting’s view of the meaning of a proposition, but does not presuppose the concept of inference or of proof as chains of inferences. I discuss this idea and what is required in order to use it for an adequate notion of valid inference. (shrink)

This paper presents the content of the unpublished notes that the Dutch mathematician Arend Heyting wrote in different periods of his life on solipsism and that are preserved in Heyting's archive at the University of Amsterdam. Most of the notes are quoted here and translated into English. Their study shows the originality of Heyting's reflections on a subject that was typical of his master, L. E. J. Brouwer, the father of intuitionism.

At the beginning of the twentieth century, among the foundational schools of mathematics appeared ‘intuitionism’ by Dutchman L. E. J. Brouwer, who based arithmetic on the intuition of time and all mental constructions that could be made out of it. His pupil Arend Heyting was the first populariser of intuitionism, and he repeatedly emphasised that no philosophy was required to practise intuitionism so that such mathematics could be shared by anyone. Still, stimulated by invitations to humanistic conferences, he wrote a (...) series of notes, preserved in the State Archives, Haarlem, about solipsism. In them, he operated a series of theoretical reflections consisting of the stripping away of the patterns that are part of our consciousness and their subsequent progressive re-introduction, in order to understand the formation of our Self as distinct from the natural world and other humans. In 1996, following a stroke, neuroscientist Jill Bolte Taylor experienced the deprivation of certain abilities in her brain and their successive regaining. In her experience there are remarkable similarities with what Heyting had hypothesised about the formation of the self. The purpose of this article is to highlight them and point out how Heyting's theoretical construct was found to be embodied in the brain. (shrink)

The aims of this paper are twofold: firstly, to say something about that philosophy of mathematics known as 'intuitionism' and, secondly, to fit these remarks into a more general message for the philosophy of mathematics as a whole. What I have to say on the first score can, without too much inaccuracy, be compressed into two theses. The first is that the intuitionistic critique of classical mathematics can be seen as based primarily on epistemological rather than on meaning-theoretic considerations. The (...) second is that the intuitionist's chief objection to the classical mathematician's use of logic does not center on the use of particular logical principles (in particular, the law of excluded middle and its ilk). Rather on the role the classical mathematician assigns (or at least extends) generally (i.e. regardless of the particular principles used) to the use of logic in the production mathematical proofs. Thus, the intuitionist critique of logic that we shall be presenting is far more radical than that which has commonly been presented. -/- Concerning the second, more general, theme, my claim is this: some restriction of the role of logical inference in mathematical proof such as that mentioned above is necessary if one is to account for the seeming difference in the epistemic conditions of provers whose reasoning is based on genuine insight into the subject-matter being investigated, and would-be provers whose reasoning is based not on such insight, but rather on principles of inference which hold of every subject-matter indifferently. (shrink)

Penelope Maddy has recently addressed the set-theoretic multiverse, and expressed reservations on its status and merits ([Maddy, 2017]). The purpose of the paper is to examine her concerns, by using the interpretative framework of set-theoretic naturalism. I first distinguish three main forms of 'multiversism', and then I proceed to analyse Maddy's concerns. Among other things, I take into account salient aspects of multiverse-related mathematics , in particular, research programmes in set theory for which the use of the multiverse seems to (...) be crucial, and show how one may provide responses to Maddy's concerns based on a careful analysis of 'multiverse practice'. (shrink)