About this topic
Summary Intuitionism is a variety of constructive mathematics proposed by L. E. J. Brouwer which maintains that mathematical objects and truths are derived from mental constructions given in intuition. More generally, constructive mathematics is a form of mathematics according to which the only way to ensure the existence of a mathematical object is to give a construction of it. In addition to intuitionism, other traditional varieties of constructive mathematics include finitism, recursive constructivism, and Bishop's constructive mathematics. Bishop's constructive mathematics, in particular, has experienced a resurgence of interest among mathematicians over the last five decades. Intuitionism and constructivism are commonly associated with a wide selection of topics ranging from intuition, the creating subject, choice sequences, Kant's transcendental idealism, Husserl's phenomenology, intuitionistic logic, the BHK explanation of the intuitionistic logical connectives, Dummett's meaning-theoretic turn, the double negation translation, the Dialectica interpretation, realizability semantics, Markov's principle, the principle of countable choice, intuitionistic set theory, constructive set theory, Martin-Löf type theory, and, more recently, homotopy type theory and univalent foundations, to name a few topics. 
Key works For comprehensive primary accounts of intuitionism, see Brouwer 1981, Heyting 1956, and Dummett 1977. The germs of intuitionism are found in Brouwer 1907 and its first formulation in Brouwer 1913. English translations are available in Brouwer's collected works edited by Heyting 1975. The repudiation of the law of excluded middle is initiated in Van Atten & Sundholm 2017. For early formulations of the BHK explanation, see Heyting 1934, Heyting 1931, Kolmogorov 1932.  Other constructivist programs that deserve mention include the brand of constructive mathematics put forward by Bishop 1967, the finitism defended by Tait 1981, and constructive type theory Martin-Löf 1980.
Introductions Introductions to intuitionism: Heyting 1956, Troelstra 1969, Dummett 1977, Dragalin 1988, Posy 2020; Introductory books on constructivism in general: Troelstra & Van Dalen 1988, Bridges & Richman 1987. Handbook: Bridges et al 2023
Related

Contents
401 found
Order:
1 — 50 / 401
  1. Analyticity and Syntheticity in Type Theory Revisited.Bruno Bentzen - forthcoming - Review of Symbolic Logic:1-27.
    I discuss problems with Martin-Löf's distinction between analytic and synthetic judgments in constructive type theory and propose a revision of his views. I maintain that a judgment is analytic when its correctness follows exclusively from the evaluation of the expressions occurring in it. I argue that Martin-Löf's claim that all judgments of the forms a : A and a = b : A are analytic is unfounded. As I shall show, when A evaluates to a dependent function type (x : (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  2. Weyl and Two Kinds of Potential Domains.Laura Crosilla & Øystein Linnebo - forthcoming - Noûs.
    According to Weyl, “‘inexhaustibility’ is essential to the infinite”. However, he distinguishes two kinds of inexhaustible, or merely potential, domains: those that are “extensionally determinate” and those that are not. This article clarifies Weyl's distinction and explains its enduring logical and philosophical significance. The distinction sheds lights on the contemporary debate about potentialism, which in turn affords a deeper understanding of Weyl.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3. Free Definite Description Theory – Sequent Calculi and Cut Elimination.Andrzej Indrzejczak - forthcoming - Logic and Logical Philosophy:1.
    We provide an application of a sequent calculus framework to the formalization of definite descriptions. It is a continuation of research undertaken in [20, 22]. In the present paper a so-called free description theory is examined in the context of different kinds of free logic, including systems applied in computer science and constructive mathematics for dealing with partial functions. It is shown that the same theory in different logics may be formalised by means of different rules and gives results of (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4. Correctness of assertion and validity of inference.Per Martin-Löf - forthcoming - Theoria.
    This is a slightly edited transcript of a lecture given by Per Martin‐Löf on 26 October 2022 at the Rolf Schock Symposium in Stockholm. In 2020, the Rolf Schock Prize in Logic and Philosophy was awarded to Dag Prawitz and Per Martin‐Löf, and the symposium was organised in their honour. The transcript was prepared by Ansten Klev and edited by the author.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  5. Constructive Validity of a Generalized Kreisel–Putnam Rule.Ivo Pezlar - forthcoming - Studia Logica.
    In this paper, we propose a computational interpretation of the generalized Kreisel–Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry–Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  6. On combining intuitionistic and S4 modal logic.João Rasga & Cristina Sernadas - forthcoming - Bulletin of the Section of Logic.
    We address the problem of combining intuitionistic and S4 modal logic in a non-collapsing way inspired by the recent works in combining intuitionistic and classical logic. The combined language includes the shared constructors of both logics namely conjunction, disjunction and falsum as well as the intuitionistic implication, the classical implication and the necessity modality.We present a Gentzen calculus for the combined logic defined over a Gentzen calculus for the host S4 modal logic. The semantics is provided by Kripke structures. The (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  7. Intuitionistic sets and numbers: small set theory and Heyting arithmetic.Stewart Shapiro, Charles McCarty & Michael Rathjen - forthcoming - Archive for Mathematical Logic.
    It has long been known that (classical) Peano arithmetic is, in some strong sense, “equivalent” to the variant of (classical) Zermelo–Fraenkel set theory (including choice) in which the axiom of infinity is replaced by its negation. The intended model of the latter is the set of hereditarily finite sets. The connection between the theories is so tight that they may be taken as notational variants of each other. Our purpose here is to develop and establish a constructive version of this. (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  8. Sets Completely Separated by Functions in Bishop Set Theory.Iosif Petrakis - 2024 - Notre Dame Journal of Formal Logic 65 (2):151-180.
    Within Bishop Set Theory, a reconstruction of Bishop’s theory of sets, we study the so-called completely separated sets, that is, sets equipped with a positive notion of an inequality, induced by a given set of real-valued functions. We introduce the notion of a global family of completely separated sets over an index-completely separated set, and we describe its Sigma- and Pi-set. The free completely separated set on a given set is also presented. Purely set-theoretic versions of the classical Stone–Čech theorem (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  9. Peter Schroeder-Heister on Proof-Theoretic Semantics.Thomas Piecha & Kai F. Wehmeier (eds.) - 2024 - Springer.
    This open access book is a superb collection of some fifteen chapters inspired by Schroeder-Heister's groundbreaking work, written by leading experts in the field, plus an extensive autobiography and comments on the various contributions by Schroeder-Heister himself. For several decades, Peter Schroeder-Heister has been a central figure in proof-theoretic semantics, a field of study situated at the interface of logic, theoretical computer science, natural-language semantics, and the philosophy of language. -/- The chapters of which this book is composed discuss the (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  10. Intuition, Iteration, Induction.Mark van Atten - 2024 - Philosophia Mathematica 32 (1):34-81.
    Brouwer’s view on induction has relatively recently been characterised as one on which it is not only intuitive (as expected) but functional, by van Dalen. He claims that Brouwer’s ‘Ur-intuition’ also yields the recursor. Appealing to Husserl’s phenomenology, I offer an analysis of Brouwer’s view that supports this characterisation and claim, even if assigning the primary role to the iterator instead. Contrasts are drawn to accounts of induction by Poincaré, Heyting, and Kreisel. On the phenomenological side, the analysis provides an (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  11. Connecting the revolutionary with the conventional: Rethinking the differences between the works of Brouwer, Heyting, and Weyl.Kati Kish Bar-On - 2023 - Philosophy of Science 90 (3):580–602.
    Brouwer’s intuitionism was a far-reaching attempt to reform the foundations of mathematics. While the mathematical community was reluctant to accept Brouwer’s work, its response to later-developed brands of intuitionism, such as those presented by Hermann Weyl and Arend Heyting, was different. The paper accounts for this difference by analyzing the intuitionistic versions of Brouwer, Weyl, and Heyting in light of a two-tiered model of the body and image of mathematical knowledge. Such a perspective provides a richer account of each story (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  12. Brouwer's Intuition of Twoity and Constructions in Separable Mathematics.Bruno Bentzen - 2023 - History and Philosophy of Logic 45 (3).
    My first aim in this paper is to use time diagrams in the style of Brentano to analyze constructions in Brouwer's separable mathematics more precisely. I argue that constructions must involve not only pairing and projecting as basic operations guaranteed by the intuition of twoity, as sometimes assumed in the literature, but also a recalling operation. My second aim is to argue that Brouwer's views on the intuition of twoity and arithmetic lead to an ontological explosion. Redeveloping the constructions of (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  13. Propositions as Intentions.Bruno Bentzen - 2023 - Husserl Studies 39 (2):143-160.
    I argue against the interpretation of propositions as intentions and proof-objects as fulfillments proposed by Heyting and defended by Tieszen and van Atten. The idea is already a frequent target of criticisms regarding the incompatibility of Brouwer’s and Husserl’s positions, mainly by Rosado Haddock and Hill. I raise a stronger objection in this paper. My claim is that even if we grant that the incompatibility can be properly dealt with, as van Atten believes it can, two fundamental issues indicate that (...)
    Remove from this list   Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  14. Handbook of Constructive Mathematics.Douglas Bridges, Hajime Ishihara, Michael Rathjen & Helmut Schwichtenberg (eds.) - 2023 - Cambridge: Cambridge University Press.
    Constructive mathematics – mathematics in which ‘there exists’ always means ‘we can construct’ – is enjoying a renaissance. Fifty years on from Bishop’s groundbreaking account of constructive analysis, constructive mathematics has spread out to touch almost all areas of mathematics and to have profound influence in theoretical computer science. This handbook gives the most complete overview of modern constructive mathematics, with contributions from leading specialists surveying the subject’s myriad aspects. Major themes include: constructive algebra and geometry, constructive analysis, constructive topology, (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  15. Negation in Negationless Intuitionistic Mathematics.Thomas Macaulay Ferguson - 2023 - Philosophia Mathematica 31 (1):29-55.
    The mathematician G.F.C. Griss is known for his program of negationless intuitionistic mathematics. Although Griss’s rejection of negation is regarded as characteristic of his philosophy, this is a consequence of an executability requirement that mental constructions presuppose agents’ executing corresponding mental activity. Restoring Griss’s executability requirement to a central role permits a more subtle characterization of the rejection of negation, according to which D. Nelson’s strong constructible negation is compatible with Griss’s principles. This exposes a ‘holographic’ theory of negation in (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  16. Verified completeness in Henkin-style for intuitionistic propositional logic.Huayu Guo, Dongheng Chen & Bruno Bentzen - 2023 - In Bruno Bentzen, Beishui Liao, Davide Liga, Reka Markovich, Bin Wei, Minghui Xiong & Tianwen Xu (eds.), Logics for AI and Law: Joint Proceedings of the Third International Workshop on Logics for New-Generation Artificial Intelligence and the International Workshop on Logic, AI and Law, September 8-9 and 11-12, 2023, Hangzhou. College Publications. pp. 36-48.
    This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models. The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization. We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model. Our implementation is restricted to a system of intuitionistic propositional logic with (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  17. Maria Hämeen-Anttila* and Jan von Plato,** eds, Kurt Gödel: The Princeton Lectures on Intuitionism.Ulrich Kohlenbach - 2023 - Philosophia Mathematica 31 (1):112-119.
    This book publishes for the first time notes from two notebooks of Gödel which formed the basis of a course on intuitionism Gödel delivered at Princeton in the.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  18. From Philosophical Traditions to Scientific Developments: Reconsidering the Response to Brouwer’s Intuitionism.Kati Kish Bar-On - 2022 - Synthese 200 (6):1–25.
    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 (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  19. On Farkas' lemma and related propositions in BISH.Josef Berger & Gregor Svindland - 2022 - Annals of Pure and Applied Logic 173 (2):103059.
    In this paper we analyse in the framework of constructive mathematics (BISH) the validity of Farkas' lemma and related propositions, namely the Fredholm alternative for solvability of systems of linear equations, optimality criteria in linear programming, Stiemke's lemma and the Superhedging Duality from mathematical finance, and von Neumann's minimax theorem with application to constructive game theory.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  20. Divergent Potentialism: A Modal Analysis With an Application to Choice Sequences.Ethan Brauer, Øystein Linnebo & Stewart Shapiro - 2022 - Philosophia Mathematica 30 (2):143-172.
    Modal logic has been used to analyze potential infinity and potentialism more generally. However, the standard analysis breaks down in cases of divergent possibilities, where there are two or more possibilities that can be individually realized but which are jointly incompatible. This paper has three aims. First, using the intuitionistic theory of choice sequences, we motivate the need for a modal analysis of divergent potentialism and explain the challenges this involves. Then, using Beth–Kripke semantics for intuitionistic logic, we overcome those (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  21. Carl J. Posy. Mathematical Intuitionism.Roy T. Cook - 2022 - Philosophia Mathematica 30 (1):111-116.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  22. Predicativity and constructive mathematics.Laura Crosilla - 2022 - In Gianluigi Oliveri, Claudio Ternullo & Stefano Boscolo (eds.), Objects, Structures, and Logics. Cham (Switzerland): Springer.
    In this article I present a disagreement between classical and constructive approaches to predicativity regarding the predicative status of so-called generalised inductive definitions. I begin by offering some motivation for an enquiry in the predicative foundations of constructive mathematics, by looking at contemporary work at the intersection between mathematics and computer science. I then review the background notions and spell out the above-mentioned disagreement between classical and constructive approaches to predicativity. Finally, I look at possible ways of defending the constructive (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  23. The entanglement of logic and set theory, constructively.Laura Crosilla - 2022 - Inquiry: An Interdisciplinary Journal of Philosophy 65 (6).
    ABSTRACT Theories of sets such as Zermelo Fraenkel set theory are usually presented as the combination of two distinct kinds of principles: logical and set-theoretic principles. The set-theoretic principles are imposed ‘on top’ of first-order logic. This is in agreement with a traditional view of logic as universally applicable and topic neutral. Such a view of logic has been rejected by the intuitionists, on the ground that quantification over infinite domains requires the use of intuitionistic rather than classical logic. In (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  24. The Varieties of Agnosticism.Filippo Ferrari & Luca Incurvati - 2022 - Philosophical Quarterly 72 (2):365-380.
    We provide a framework for understanding agnosticism. The framework accounts for the varieties of agnosticism while vindicating the unity of the phenomenon. This combination of unity and plurality is achieved by taking the varieties of agnosticism to be represented by several agnostic stances, all of which share a common core provided by what we call the minimal agnostic attitude. We illustrate the fruitfulness of the framework by showing how it can be applied to several philosophical debates. In particular, several philosophical (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  25. V.A. Yankov on Non-Classical Logics, History and Philosophy of Mathematics.Vandoulakis Ioannis & Alex Citkin (eds.) - 2022 - Springer. Outstanding Contributions to Logic (Volume 24).
    This book is dedicated to V.A. Yankov’s seminal contributions to the theory of propositional logics. His papers, published in the 1960s, are highly cited even today. The Yankov characteristic formulas have become a very useful tool in propositional, modal and algebraic logic. The papers contributed to this book provide the new results on different generalizations and applications of characteristic formulas in propositional, modal and algebraic logics. In particular, an exposition of Yankov’s results and their applications in algebraic logic, the theory (...)
    Remove from this list  
     
    Export citation  
     
    Bookmark  
  26. Generality Explained.Øystein Linnebo - 2022 - Journal of Philosophy 119 (7):349-379.
    What explains the truth of a universal generalization? Two types of explanation can be distinguished. While an ‘instance-based explanation’ proceeds via some or all instances of the generalization, a ‘generic explanation’ is independent of the instances, relying instead on completely general facts about the properties or operations involved in the generalization. This intuitive distinction is analyzed by means of a truthmaker semantics, which also sheds light on the correct logic of quantification. On the most natural version of the semantics, this (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  27. A marriage of Brouwer’s intuitionism and Hilbert’s finitism I: Arithmetic.Takako Nemoto & Sato Kentaro - 2022 - Journal of Symbolic Logic 87 (2):437-497.
    We investigate which part of Brouwer’s Intuitionistic Mathematics is finitistically justifiable or guaranteed in Hilbert’s Finitism, in the same way as similar investigations on Classical Mathematics already done quite extensively in proof theory and reverse mathematics. While we already knew a contrast from the classical situation concerning the continuity principle, more contrasts turn out: we show that several principles are finitistically justifiable or guaranteed which are classically not. Among them are: fan theorem for decidable fans but arbitrary bars; continuity principle (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  28. On V.A. Yankov’s Contribution to the History of Foundations of Mathematics.Ioannis M. Vandoulakis - 2022 - In Alex Citkin & Ioannis M. Vandoulakis (eds.), V.A. Yankov on Non-Classical Logics, History and Philosophy of Mathematics. Springer, Outstanding Contributions To Logic (volume 24). pp. 247-270.
    The paper examines Yankov’s contribution to the history of mathematical logic and the foundations of mathematics. It concerns the public communication of Markov’s critical attitude towards Brouwer’s intuitionistic mathematics from the point of view of his constructive mathematics and the commentary on A.S. Esenin-Vol’pin program of ultra-intuitionistic foundations of mathematics.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  29. Towards a new philosophical perspective on Hermann Weyl’s turn to intuitionism.Kati Kish Bar-On - 2021 - Science in Context 34 (1):51-68.
    The paper explores Hermann Weyl’s turn to intuitionism through a philosophical prism of normative framework transitions. It focuses on three central themes that occupied Weyl’s thought: the notion of the continuum, logical existence, and the necessity of intuitionism, constructivism, and formalism to adequately address the foundational crisis of mathematics. The analysis of these themes reveals Weyl’s continuous endeavor to deal with such fundamental problems and suggests a view that provides a different perspective concerning Weyl’s wavering foundational positions. Building on a (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  30. Naive cubical type theory.Bruno Bentzen - 2021 - Mathematical Structures in Computer Science 31:1205–1231.
    This article proposes a way of doing type theory informally, assuming a cubical style of reasoning. It can thus be viewed as a first step toward a cubical alternative to the program of informalization of type theory carried out in the homotopy type theory book for dependent type theory augmented with axioms for univalence and higher inductive types. We adopt a cartesian cubical type theory proposed by Angiuli, Brunerie, Coquand, Favonia, Harper, and Licata as the implicit foundation, confining our presentation (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  31. A parametrised functional interpretation of Heyting arithmetic.Bruno Dinis & Paulo Oliva - 2021 - Annals of Pure and Applied Logic 172 (4):102940.
  32. Sense and reference from a constructivist standpoint.Michael Dummett - 2021 - Bulletin of Symbolic Logic 27 (4):485-500.
    Editorial NoteThis paper was read by Michael Dummett at Leiden University on September 26, 1992 at the invitation by Göran Sundholm to address the topic mentioned in the title. Dummett’s lecture was part of a workshop, Meaning Theory and Intuitionism, with 12 invited speakers over three days. After the workshop, Dummett gave a copy of the manuscript to Sundholm together with permission to publish it. At the time, nothing came of the publication plans, nor did Dummett publish it in any (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  33. A Dilemma for Mathematical Constructivism.Samuel Kahn - 2021 - Axiomathes 31 (1):63-72.
    In this paper I argue that constructivism in mathematics faces a dilemma. In particular, I maintain that constructivism is unable to explain (i) the application of mathematics to nature and (ii) the intersubjectivity of mathematics unless (iii) it is conjoined with two theses that reduce it to a form of mathematical Platonism. The paper is divided into five sections. In the first section of the paper, I explain the difference between mathematical constructivism and mathematical Platonism and I outline my argument. (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  34. Identity in Martin‐Löf type theory.Ansten Klev - 2021 - Philosophy Compass 17 (2):e12805.
    The logic of identity contains riches not seen through the coarse lens of predicate logic. This is one of several lessons to draw from the subtle treatment of identity in Martin‐Löf type theory, to which the reader will be introduced in this article. After a brief general introduction we shall mainly be concerned with the distinction between identity propositions and identity judgements. These differ from each other both in logical form and in logical strength. Along the way, connections to philosophical (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  35. Intuitionistic mereology.Paolo Maffezioli & Achille C. Varzi - 2021 - Synthese 198 (Suppl 18):4277-4302.
    Two mereological theories are presented based on a primitive apartness relation along with binary relations of mereological excess and weak excess, respectively. It is shown that both theories are acceptable from the standpoint of constructive reasoning while remaining faithful to the spirit of classical mereology. The two theories are then compared and assessed with regard to their extensional import.
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  36. The sense/reference distinction in constructive semantics.Per Martin-löf - 2021 - Bulletin of Symbolic Logic 27 (4):501-513.
    Editorial NoteThis lecture was given by Per Martin-Löf at Leiden University on August 25, 2001 at the invitation by Göran Sundholm to address the topic mentioned in the title and to reflect on Dummett’s earlier effort of almost a decade before. The lecture was part of a three-day conference on Gottlob Frege. Sundholm arranged for the lecture to be recorded and commissioned Bjørn Jespersen to make a transcript. The information in footnote 1, which Sundholm provided, has been independently confirmed by (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  37. Proof that Intuitionistic Logic is not Three-Valued.Micah Phillips-Gary - 2021 - The Hemlock Papers 18:4-14.
    In this paper, we give an introduction to intuitionistic logic and a defense of it from certain formal logical critiques. Intuitionism is the thesis that mathematical objects are mental constructions produced by the faculty of a priori intuition of time. The truth of a mathematical proposition, then, consists in our knowing how to construct in intuition a corresponding state of affairs. This understanding of mathematical truth leads to a rejection of the principle, valid in classical logic, that a proposition is (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  38. Sense, reference, and computation.Bruno Bentzen - 2020 - Perspectiva Filosófica 47 (2):179-203.
    In this paper, I revisit Frege's theory of sense and reference in the constructive setting of the meaning explanations of type theory, extending and sharpening a program–value analysis of sense and reference proposed by Martin-Löf building on previous work of Dummett. I propose a computational identity criterion for senses and argue that it validates what I see as the most plausible interpretation of Frege's equipollence principle for both sentences and singular terms. Before doing so, I examine Frege's implementation of his (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  39. On Different Ways of Being Equal.Bruno Bentzen - 2020 - Erkenntnis 87 (4):1809-1830.
    The aim of this paper is to present a constructive solution to Frege's puzzle (largely limited to the mathematical context) based on type theory. Two ways in which an equality statement may be said to have cognitive significance are distinguished. One concerns the mode of presentation of the equality, the other its mode of proof. Frege's distinction between sense and reference, which emphasizes the former aspect, cannot adequately explain the cognitive significance of equality statements unless a clear identity criterion for (...)
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  40. Intuitionism in the Philosophy of Mathematics: Introducing a Phenomenological Account.Philipp Berghofer - 2020 - Philosophia Mathematica 28 (2):204-235.
    The aim of this paper is to establish a phenomenological mathematical intuitionism that is based on fundamental phenomenological-epistemological principles. According to this intuitionism, mathematical intuitions are sui generis mental states, namely experiences that exhibit a distinctive phenomenal character. The focus is on two questions: what does it mean to undergo a mathematical intuition and what role do mathematical intuitions play in mathematical reasoning? While I crucially draw on Husserlian principles and adopt ideas we find in phenomenologically minded mathematicians such as (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  41. Brouwer’s Weak Counterexamples and the Creative Subject: A Critical Survey.Peter Fletcher - 2020 - Journal of Philosophical Logic 49 (6):1111-1157.
    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 (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  42. Choice Sequences and the Continuum.Casper Storm Hansen - 2020 - Erkenntnis 87 (2):517-534.
    According to L.E.J. Brouwer, there is room for non-definable real numbers within the intuitionistic ontology of mental constructions. That room is allegedly provided by freely proceeding choice sequences, i.e., sequences created by repeated free choices of elements by a creating subject in a potentially infinite process. Through an analysis of the constitution of choice sequences, this paper argues against Brouwer’s claim.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  43. Higher Groups via Displayed Univalent Reflexive Graphs in Cubical Type Theory.Johannes Philipp Manuel Schipp von Branitz - 2020 - Dissertation, Technische Universität Darmstadt
    This thesis introduces displayed univalent reflexive graphs, a natural analogue of displayed categories, as a framework for uniformly internalizing composite mathematical structures in homotopy or cubical type theory. This framework is then used to formalize the definition of and equivalence of strict 2-groups and crossed modules. Lastly, foundations for the development of higher groups from the classifying space perspective in cubical type theory are laid. Most results are formalized in Cubical Agda.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  44. Proof vs Provability: On Brouwer’s Time Problem.Palle Yourgrau - 2020 - History and Philosophy of Logic 41 (2):140-153.
    Is a mathematical theorem proved because provable, or provable because proved? If Brouwer’s intuitionism is accepted, we’re committed, it seems, to the latter, which is highly problematic. Or so I will argue. This and other consequences of Brouwer’s attempt to found mathematics on the intuition of a move of time have heretofore been insufficiently appreciated. Whereas the mathematical anomalies of intuitionism have received enormous attention, too little time, I’ll try to show, has been devoted to some of the temporal anomalies (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  45. Intuition in Poincarés Philosophy of Mathematics.Koray Akçagüner - 2019 - Beytulhikme An International Journal of Philosophy 9 (9:4):925-940.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  46. Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts.Stefania Centrone, Deborah Kant & Deniz Sarikaya (eds.) - 2019 - Springer Verlag.
    This edited work presents contemporary mathematical practice in the foundational mathematical theories, in particular set theory and the univalent foundations. It shares the work of significant scholars across the disciplines of mathematics, philosophy and computer science. Readers will discover systematic thought on criteria for a suitable foundation in mathematics and philosophical reflections around the mathematical perspectives. The first two sections focus on the two most prominent candidate theories for a foundation of mathematics. Readers may trace current research in set theory, (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  47. Indeterminism in Physics, Classical Chaos and Bohmian Mechanics: Are Real Numbers Really Real?Nicolas Gisin - 2019 - Erkenntnis (6):1-13.
    It is usual to identify initial conditions of classical dynamical systems with mathematical real numbers. However, almost all real numbers contain an infinite amount of information. I argue that a finite volume of space can’t contain more than a finite amount of information, hence that the mathematical real numbers are not physically relevant. Moreover, a better terminology for the so-called real numbers is “random numbers”, as their series of bits are truly random. I propose an alternative classical mechanics, which is (...)
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  48. Considerações de Brouwer sobre espaço e infinitude: O idealismo de Brouwer Diante do Problema Apresentado por Dummett Quanto à Possibilidade Teórica de uma Infinitude Espacial.Paulo Júnio de Oliveira - 2019 - Kinesis 11:94-108.
    Resumo Neste artigo, será discutida a noção de “infinitude cardinal” – a qual seria predicada de um “conjunto” – e a noção de “infinitude ordinal” – a qual seria predicada de um “processo”. A partir dessa distinção conceitual, será abordado o principal problema desse artigo, i.e., o problema da possibilidade teórica de uma infinitude de estrelas tratado por Dummett em sua obra Elements of Intuitionism. O filósofo inglês sugere que, mesmo diante dessa possibilidade teórica, deveria ser possível predicar apenas infinitude (...)
    Remove from this list  
     
    Export citation  
     
    Bookmark  
  49. A Comparison of Type Theory with Set Theory.Ansten Klev - 2019 - In Stefania Centrone, Deborah Kant & Deniz Sarikaya (eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts. Springer Verlag. pp. 271-292.
    This paper discusses some of the ways in which Martin-Löf type theory differs from set theory. The discussion concentrates on conceptual, rather than technical, differences. It revolves around four topics: sets versus types; syntax; functions; and identity. The difference between sets and types is spelt out as the difference between unified pluralities and kinds, or sorts. A detailed comparison is then offered of the syntax of the two languages. Emphasis is put on the distinction between proposition and judgement, drawn by (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  50. Eta-rules in Martin-löf type theory.Ansten Klev - 2019 - Bulletin of Symbolic Logic 25 (3):333-359.
    The eta rule for a set A says that an arbitrary element of A is judgementally identical to an element of constructor form. Eta rules are not part of what may be called canonical Martin-Löf type theory. They are, however, justified by the meaning explanations, and a higher-order eta rule is part of that type theory. The main aim of this paper is to clarify this somewhat puzzling situation. It will be argued that lower-order eta rules do not, whereas the (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
1 — 50 / 401