Intuitionism and Constructivism

This paper scrutinizes the debate over logical pluralism. I hope to make this debate more tractable by addressing the question of motivating data: what would count as strong evidence in favor of logical pluralism? Any research program should be able to answer this question, but when faced with this task, many logical pluralists fall back on brute intuitions. This sets logical pluralism on a weak foundation and makes it seem as if nothing pressing is at stake in the debate. The (...) present paper aims to improve this situation by looking at a promising case study and drawing general lessons about the kind of evidence that would support logical pluralism. I argue that the best motivation for logical pluralism will ultimately be rooted in certain kinds of performative data. (shrink)

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 (...) the following, I consider constructive set theories, which use intuitionistic rather than classical logic, and argue that they manifest a distinctive interdependence or an entanglement between sets and logic. In fact, Martin-Löf type theory identifies fundamental logical and set-theoretic notions. Remarkably, one of the motivations for this identification is the thought that classical quantification over infinite domains is problematic, while intuitionistic quantification is not. The approach to quantification adopted in Martin-Löf’s type theory is subtly interconnected with its predicativity. I conclude by recalling key aspects of an approach to predicativity inspired by Poincaré, which focuses on the issue of correct quantification over infinite domains and relate it back to Martin-Löf type theory. (shrink)

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.

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.

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. (...) In the second, I argue that the best explanation of how mathematics applies to nature for a constructivist is a thesis I call Copernicanism. In the third, I argue that the best explanation of how mathematics can be intersubjective for a constructivist is a thesis I call Ideality. In the fourth, I argue that once constructivism is conjoined with these two theses, it collapses into a form of mathematical Platonism. In the fifth, I confront some objections. (shrink)

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 (...) theory of sense and reference in the logical framework of Grundgesetze, his doctrine of truth values, and views on sameness of sense as equipollence of assertions. (shrink)

It is often said that a correct logical system should have no counterexample to its logical rules and the system must be revised if its rules have a counterexample. If a logical system (or theory) has a counterexample to its logical rules, do we have to revise the system? In this paper, focussing on the role of counterexamples to logical rules, we deal with the question. -/- We investigate two mutually exclusive theories of arithmetic - intuitionistic and paraconsistent theories. The (...) paraconsistent theory provides a (strong) counterexample to Ex Contradiction Quodlibet (ECQ). On the other hand, the intuitionistic theory gives a (weak) counterexample to the Double Negation Elimination (DNE) of the paraconsistent theory. If any counterexample undermines the legitimate use of logical rules, both theories must be revised. -/- After we investigate a paraconsistent counterexample to ECQ and the intuitionist’s answer against it, we arrive at the unwelcome conclusion that ECQ has both a justification and a counterexample. Moreover, we argue that if a logical rule were abolished whenever it has a counterexample, a promising conclusion would be logical nihilism which is the view that there is no valid logical inference, and so a correct logical system does not exist. Provided that the logical revisionist is not a logical nihilist, we claim that not every counterexample is the ground for logical revision. While logical rules of a given system have a justification, the existence of a counterexample loses its role for logical revision unless the rules and the counterexample share the same structure. (shrink)

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 (...) empirically equivalent to classical mechanics, but uses only finite-information numbers. This alternative classical mechanics is non-deterministic, despite the use of deterministic equations, in a way similar to quantum theory. Interestingly, both alternative classical mechanics and quantum theories can be supplemented by additional variables in such a way that the supplemented theory is deterministic. Most physicists straightforwardly supplement classical theory with real numbers to which they attribute physical existence, while most physicists reject Bohmian mechanics as supplemented quantum theory, arguing that Bohmian positions have no physical reality. (shrink)

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 (...) ordinal. A questão principal surge do fato de que parece ser problemático predicar ordinalmente infinitude de “estrelas”. Mesmo diante dessa possibilidade, Dummett sugere que o intuicionista poderia apenas reinterpretar infinitude cardinal como sendo infinitude ordinal. Ora, iremos mostrar que, se Dummett não fornece razões extras que sustentem essa posição, então será difícil interpretar um caso empírico infinitário como sendo também um caso ordinal ou potencial de infinitude. Para resolver esse problema de Dummett, em Brouwer se encontram alguns pressupostos idealistas necessários para argumentar em favor da ideia de que, mesmo em um contexto empírico, como o de uma infinitude de estrelas, poderíamos predicar infinitude ordinal. Então, depois de discutir as duas noções de “infinitude” e apresentar o problema de Dummett, será apresentada a abordagem idealista de Brouwer – a qual pelo menos explicaria de modo mais plausível as razões que poderiam motivar um intuicionista a predicar infinitude ordinal até mesmo de um caso empírico e espacial. (shrink)

On the basis of Martin-Löf’s meaning explanations for his type theory a detailed justification is offered of the rule of identity elimination. Brief discussions are thereafter offered of how the univalence axiom fares with respect to these meaning explanations and of some recent work on identity in type theory by Ladyman and Presnell.

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 (...) higher-order eta rule does, accord with the understanding of judgemental identity as definitional identity. A subsidiary aim is to clarify precisely what an eta rule is. This will involve showing how such rules relate to various other notions of type theory, proof theory, and category theory. (shrink)

ABSTRACTAccording to a famous argument by Dummett, the concept of set is indefinitely extensible, and the logic appropriate for reasoning about the instances of any such concept is intuitionistic, not classical. But Dummett's argument is widely regarded as obscure. This note explains how the final chapter of Rumfitt's important new book advances our understanding of Dummett's argument, but it also points out some problems and unanswered questions. Finally, Rumfitt's reconstruction of Dummett's argument is contrasted with my own preferred alternative.

The notion of potential infinity dominated in mathematical thinking about infinity from Aristotle until Cantor. The coherence and philosophical importance of the notion are defended. Particular attention is paid to the question of whether potential infinity is compatible with classical logic or requires a weaker logic, perhaps intuitionistic.

The dissertation provides an analysis and elaboration of Michael Dummett's proof-theoretic notions of validity. Dummett's notions of validity are contrasted with standard proof-theoretic notions and formally evaluated with respect to their adequacy to propositional intuitionistic logic.

The aim of the present thesis is twofold. First we propose a constructive solution to Frege's puzzle using an approach based on homotopy type theory, a newly proposed foundation of mathematics that possesses a higher-dimensional treatment of equality. We claim that, from the viewpoint of constructivism, Frege's solution is unable to explain the so-called ‘cognitive significance' of equality statements, since, as we shall argue, not only statements of the form 'a = b', but also 'a = a' may contribute to (...) an extension of knowledge. Second, we study this higher-dimensional account of equality from a constructive (computational) standpoint and, based on these considerations, we offer a new perspective to the project proposed by Peter Aczel of developing conventions and notations for an informal style of doing mathematics in type theory. To that end, we adopt the cubical type theory of Angiuli, Favonia and Harper, a framework that can be seen as constructive refinement of the ideas of homotopy type theory. (shrink)

Cantor’s proof that the reals are uncountable forms a central pillar in the edifices of higher order recursion theory and set theory. It also has important applications in model theory, and in the foundations of topology and analysis. Due partly to these factors, and to the simplicity and elegance of the proof, it has come to be accepted as part of the ABC’s of mathematics. But even if as an Archimedean point it supports tomes of mathematical theory, there is a (...) question that demands clarification: What, exactly, does Cantor’s proof show? One of few places where this question is addressed is Appendix II of Wittgenstein’s Remarks on the Foundations of Mathematics. This essay is devoted to clarifying Wittgenstein’s remarks in that section. (shrink)

Gentzen's three consistency proofs for elementary number theory have a common aim that originates from Hilbert's Program, namely, the aim to justify the application of classical reasoning to quantified propositions in elementary number theory. In addition to this common aim, Gentzen gave a “finitist” interpretation to every number-theoretic proposition with his 1935 and 1936 consistency proofs. In the present paper, we investigate the relationship of this interpretation with intuitionism in terms of the debate between the Hilbert School and the Brouwer (...) School over the significance of consistency proofs. First, we argue that the interpretation had the role of responding to a Brouwer-style objection against the significance of consistency proofs. Second, we propose a way of understanding Gentzen's response to this objection from an intuitionist perspective. (shrink)

This paper is about Poincaré’s view of the foundations of geometry. According to the established view, which has been inherited from the logical positivists, Poincaré, like Hilbert, held that axioms in geometry are schemata that provide implicit definitions of geometric terms, a view he expresses by stating that the axioms of geometry are “definitions in disguise.” I argue that this view does not accord well with Poincaré’s core commitment in the philosophy of geometry: the view that geometry is the study (...) of groups of operations. In place of the established view I offer a revised view, according to which Poincaré held that axioms in geometry are in fact assertions about invariants of groups. Groups, as forms of the understanding, are prior in conception to the objects of geometry and afford the proper definition of those objects, according to Poincaré. Poincaré’s view therefore contrasts sharply with Kant’s foundation of geometry in a unique form of sensibility. According to my interpretation, axioms are not definitions in disguise because they themselves implicitly define their terms, but rather because they disguise the definitions which imply them. (shrink)

In this paper it is argued that the understanding of Brouwer as replacing truth conditions with assertability or proof conditions, in particular as codified in the so-called Brouwer-Heyting-Kolmogorov Interpretation, is misleading and conflates a weak and a strong notion of truth that have to be kept apart to understand Brouwer properly: truth-as-anticipation and truth- in-content. These notions are explained, exegetical documentation provided, and semi-formal recursive definitions are given.

The derivative is a basic concept of differential calculus. However, if we calculate the derivative as change in distance over change in time, the result at any instant is 0/0, which seems meaningless. Hence, Newton and Leibniz used the limit to determine the derivative. Their method is valid in practice, but it is not easy to intuitively accept. Thus, this article describes the novel method of differential calculus based on the double contradiction, which is easier to accept intuitively. Next, the (...) geometrical meaning of the double contradiction is considered as follows. A tangent at a point on a convex curve is iterated. Then, the slope of the tangent at the point is sandwiched by two kinds of lines. The first kind of line crosses the curve at the original point and a point to the right of it. The second kind of line crosses the curve at the original point and a point to the left of it. Then, the double contradiction can be applied, and the slope of the tangent is determined as a single value. Finally, the meaning of this method for the foundation of mathematics is considered. We reflect on Dehaene’s notion that the foundation of mathematics is based on the intuitions, which evolve independently. Hence, there may be gaps between intuitions. In fact, the Ancient Greeks identified inconsistency between arithmetic and geometry. However, Eudoxus developed the theory of proportion, which is equivalent to the Dedekind Cut. This allows the iteration of an irrational number by rational numbers as precisely as desired. Simultaneously, we can define the irrational number by the double contradiction, although its existence is not guaranteed. Further, an area of a curved figure is iterated and defined by rectilinear figures using the double contradiction. (shrink)

The lives of few mathematicians offer the drama that is presented by the life of L. E. J. Brouwer, correctly identified on the cover of this book as a topologist, intuitionist, and philosopher, and before we go any further, it will be worth indicating why.It is not just that Brouwer would rank high among mathematicians for his work in topology alone: he set standards for rigour and created a theory of dimension for topological spaces, and his fixed-point theorem is of (...) great importance. Nor is it just that his philosophy of intuitionism created a new and vibrant branch of logic, that is, arguably, the only viable alternative to naïve, classical logic outside the enclave of professional logicians. Rather, it is that there is a tension, popularly taken to amount to a contradiction, in the fundamental ideas behind his topology and his intuitionism. Added to that, he took a highly principled stand on mathematical issues that led him into confrontations with major figures and a certain degre .. (shrink)

Revision sequences are a kind of transfinite sequences which were introduced by Herzberger and Gupta in 1982 as the main mathematical tool for developing their respective revision theories of truth. We generalise revision sequences to the notion of cofinally invariant sequences, showing that several known facts about Herzberger’s and Gupta’s theories also hold for this more abstract kind of sequences and providing new and more informative proofs of the old results.

We show that, by choosing definitions carefully, a version of Frege's theorem can be proved in intuitionistic logic.

The paper examines Andrei A. Markov’s critical attitude towards L.E.J. Brouwer’s intuitionism, as is expressed in his endnotes to the Russian translation of Heyting’s Intuitionism, published in Moscow in 1965. It is argued that Markov’s algorithmic approach was shaped under the impact of the mathematical style and values prevailing in the Petersburg mathematical school, which is characterized by the proclaimed primacy of applications and the search for rigor and effective solutions.

The recent discovery of an interpretation of constructive type theory into abstract homotopy theory suggests a new approach to the foundations of mathematics with intrinsic geometric content and a computational implementation. Voevodsky has proposed such a program, including a new axiom with both geometric and logical significance: the Univalence Axiom. It captures the familiar aspect of informal mathematical practice according to which one can identify isomorphic objects. While it is incompatible with conventional foundations, it is a powerful addition to homotopy (...) type theory. It also gives the new system of foundations a distinctly structural character. (shrink)

This paper argues that Weyl took formalism to prevail over intuitionism with respect to supporting scientific objectivity, rather than grounding classical mathematics, and that he thought this was enough for rejecting pure phenomenology as well.

The paper is a contribution to intuitionistic reverse mathematics. We introduce a formal system called Basic Intuitionistic MathematicsBIM, and then search for statements that are, over BIM, equivalent to Brouwer’s Fan Theorem or to its positive denial, Kleene’s Alternative to the Fan Theorem. The Fan Theorem is true under the intended intuitionistic interpretation and Kleene’s Alternative is true in the model of BIM consisting of the Turing-computable functions. The task of finding equivalents of Kleene’s Alternative is, intuitionistically, a nontrivial extension (...) of the task of finding equivalents of the Fan Theorem, although there is a certain symmetry in the arguments that we shall try to make transparent. We introduce closed-and-separable subsets of Baire space N\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal{N}}$$\end{document} and of the set R\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal{R}}$$\end{document} of the real numbers. Such sets may be compact and also positively noncompact. The Fan Theorem is the statement that Cantor space C\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal{C}}$$\end{document}, or, equivalently, the unit interval [0, 1], is compact and Kleene’s Alternative is the statement that C\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal{C}}$$\end{document}, or, equivalently, [0, 1], is positively noncompact. The class of the compact closed-and-separable sets and also the class of the closed-and-separable sets that are positively noncompact are characterized in many different ways and a host of equivalents of both the Fan Theorem and Kleene’s Alternative is found. (shrink)

An extension of intuitionism to empirical discourse, a project most seriously taken up by Dummett and Tennant, requires an empirical negation whose strength lies somewhere between classical negation (‘It is unwarranted that. . . ’) and intuitionistic negation (‘It is refutable that. . . ’). I put forward one plausible candidate that compares favorably to some others that have been propounded in the literature. A tableau calculus is presented and shown to be strongly complete.

A remembrance of Dummett's work on philosophy of mathematcis.

The subject of this article is Modal-Epistemic Arithmetic (MEA), a theory introduced by Horsten to interpret Epistemic Arithmetic (EA), which in turn was introduced by Shapiro to interpret Heyting Arithmetic. I will show how to interpret MEA in EA such that one can prove that the interpretation of EA is MEA is faithful. Moreover, I will show that one can get rid of a particular Platonist assumption. Then I will discuss models for MEA in light of the problems of logical (...) omniscience and logical competence. Awareness models, impossible worlds models and syntactical models have been introduced to deal with the first problem. Certain conditions on the accessibility relations are needed to deal with the second problem. I go on to argue that those models are subject to the problem of quantifying in, for which I will provide a solution. (shrink)

Strictly intuitionistic inferences are employed to demonstrate that three conditions—the existence of Brouwerian weak counterexamples to _Test_, the recognition condition, and the _BHK_ interpretation of the logical signs—are together inconsistent. Therefore, if the logical signs in mathematical statements governed by the recognition condition are constructive in that they satisfy the clauses of the _BHK_, then every relevant instance of the classical principle _Test_ is true intuitionistically, and the antirealistic critique of conventional logic, once thought to yield such weak counterexamples, is (...) seen, in this instance, to fail. (shrink)

Straightforwardly and strictly intuitionistic inferences show that the Brouwer– Heyting–Kolmogorov interpretation, in the presence of a formulation of the recognition principle, entails the validity of the Law of Testability: that the form ¬ f V ¬¬ f is valid. Therefore, the BHK and recognition, as described here, are inconsistent with the axioms both of intuitionistic mathematics and of Markovian constructivism. This finding also implies that, if the BHK and recognition are suitably formulated, then Brouwer’s original weak counterexample reasoning was fallacious. (...) The results of the present article extend and refine those of McCarty, C.. Antirealism and Constructivism: Brouwer’s Weak Counterexamples. The Review of Symbolic Logic. First View. Cambridge University Press. (shrink)

An important open problem in Reverse Mathematics is the reduction of the first-order strength of the base theory from IΣ1IΣ1 to IΔ0+expIΔ0+exp. The system ERNA, a version of Nonstandard Analysis based on the system IΔ0+expIΔ0+exp, provides a partial solution to this problem. Indeed, weak Königʼs lemma and many of its equivalent formulations from Reverse Mathematics can be ‘pushed down’ into ERNA, while preserving the equivalences, but at the price of replacing equality with ‘≈’, i.e. infinitesimal proximity . The logical principle (...) corresponding to weak Königʼs lemma is the universal transfer principle from Nonstandard Analysis. Here, we consider the intermediate and mean value theorem and their uniform generalizations. We show that ERNAʼs Reverse Mathematics mirrors the situation in classical Reverse Mathematics. This further supports our claim from Sanders [19] that the Reverse Mathematics of ERNA plus universal transfer is a copy up to infinitesimals of that of WKL0. We discuss some of the philosophical implications of our results. (shrink)

I begin by drawing a parallel between the intuitionistic understanding of quantification over all natural numbers and the generality relativist understanding of quantification over absolutely everything. I then argue that adoption of an intuitionistic reading of relativism not only provides an immediate reply to the absolutist's charge of incoherence but it also throws a new light on the debates surrounding absolute generality.

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 constructive mathematics, 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.

Let A be a subset of the constructive real line. What are the necessary and sufficient conditions for the set A such that A is continuously separated from other reals, i.e., there exists a continuous function f with f−1 = A? In this paper, we study the notions of closed sets and closure maps in constructive reverse mathematics.