Our regimentation of Goodman and Myhill’s proof of Excluded Middle revealed among its premises a form of Choice and an instance of Separation.Here we revisit Zermelo’s requirement that the separating property be definite. The instance that Goodman and Myhill used is not constructively warranted. It is that principle, and not Choice alone, that precipitates Excluded Middle.Separation in various axiomatizations of constructive set theory is examined. We conclude that insufficient critical attention has been paid to how those forms of Separation fail, (...) in light of the Goodman–Myhill result, to capture a genuinely constructive notion of set. (shrink)

The one-page 1978 informal proof of Goodman and Myhill is regimented in a weak constructive set theory in free logic. The decidability of identities in general (⁠|$a\!=\!b\vee\neg a\!=\!b$|⁠) is derived; then, of sentences in general (⁠|$\psi\vee\neg\psi$|⁠). Martin-Löf’s and Bell’s receptions of the latter result are discussed. Regimentation reveals the form of Choice used in deriving Excluded Middle. It also reveals an abstraction principle that the proof employs. It will be argued that the Goodman–Myhill result does not provide the constructive set (...) theorist with a dispositive reason for not adopting (full) Choice. (shrink)

Intersemiotic translation (IT) was defined by Roman Jakobson (The Translation Studies Reader, Routledge, London, p. 114, 2000) as “transmutation of signs”—“an interpretation of verbal signs by means of signs of nonverbal sign systems.” Despite its theoretical relevance, and in spite of the frequency in which it is practiced, the phenomenon remains virtually unexplored in terms of conceptual modeling, especially from a semiotic perspective. Our approach is based on two premises: (i) IT is fundamentally a semiotic operation process (semiosis) and (ii) (...) IT is a deeply iconic-dependent process. We exemplify our approach by means of literature to dance IT and we explore some implications for the development of a general model of IT. (shrink)

Prominent constructive theories of sets as Martin-Löf type theory and Aczel and Myhill constructive set theory, feature a distinctive form of constructivity: predicativity. This may be phrased as a constructibility requirement for sets, which ought to be finitely specifiable in terms of some uncontroversial initial “objects” and simple operations over them. Predicativity emerged at the beginning of the 20th century as a fundamental component of an influential analysis of the paradoxes by Poincaré and Russell. According to this analysis the paradoxes (...) are caused by a vicious circularity in definitions; adherence to predicativity was therefore proposed as a systematic method for preventing such problematic circularity. In the following, I sketch the origins of predicativity, review the fundamental contributions by Russell and Weyl and look at modern incarnations of this notion. (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)

This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science. The range of contributions includes material on the extension of natural deduction with higher-order (...) rules, as opposed to higher-order connectives, and a paper discussing the application of natural deduction rules to dealing with equality in predicate calculus. The volume continues with a key chapter summarizing work on the extension of the Curry-Howard isomorphism, via methods of category theory that have been successfully applied to linear logic, as well as many other contributions from highly regarded authorities. With an illustrious group of contributors addressing a wealth of topics and applications, this volume is a valuable addition to the libraries of academics in the multiple disciplines whose development has been given added scope by the methodologies supplied by natural deduction. The volume is representative of the rich and varied directions that Prawitz work has inspired in the area of natural deduction. (shrink)

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)

The volume includes twenty-five research papers presented as gifts to John L. Bell to celebrate his 60th birthday by colleagues, former students, friends and admirers. Like Bell’s own work, the contributions cross boundaries into several inter-related fields. The contributions are new work by highly respected figures, several of whom are among the key figures in their fields. Some examples: in foundations of maths and logic ; analytical philosophy, philosophy of science, philosophy of mathematics and decision theory and foundations of economics. (...) Most articles are contributions to current philosophical debates, but contributions also include some new mathematical results, important historical surveys, and a translation by Wilfrid Hodges of a key work of arabic logic. (shrink)

Esta enciclopédia abrange, de uma forma introdutória mas desejavelmente rigorosa, uma diversidade de conceitos, temas, problemas, argumentos e teorias localizados numa área relativamente recente de estudos, os quais tem sido habitual qualificar como «estudos lógico-filosóficos». De uma forma apropriadamente genérica, e apesar de o território teórico abrangido ser extenso e de contornos por vezes difusos, podemos dizer que na área se investiga um conjunto de questões fundamentais acerca da natureza da linguagem, da mente, da cognição e do raciocínio humanos, bem (...) como questões acerca das conexões destes com a realidade não mental e extralinguística. A razão daquela qualificação é a seguinte: por um lado, a investigação em questão é qualificada como filosófica em virtude do elevado grau de generalidade e abstracção das questões examinadas (entre outras coisas); por outro, a investigação é qualificada como lógica em virtude de ser uma investigação logicamente disciplinada, no sentido de nela se fazer um uso intenso de conceitos, técnicas e métodos provenientes da disciplina de lógica. O agregado de tópicos que constitui a área de estudos lógico-filosóficos é já visível, pelo menos em parte, no Tractatus Logico-Philosophicus de Ludwig Wittgenstein, uma obra publicada em 1921. E uma boa maneira de ter uma ideia sinóptica do território disciplinar abrangido por esta enciclopédia, ou pelo menos de uma porção substancial dele, é extrair do Tractatus uma lista dos tópicos mais salientes aí discutidos; a lista incluirá certamente tópicos do seguinte género, muitos dos quais se podem encontrar ao longo desta enciclopédia: factos e estados de coisas; objectos; representação; crenças e estados mentais; pensamentos; a proposição; nomes próprios; valores de verdade e bivalência; quantificação; funções de verdade; verdade lógica; identidade; tautologia; o raciocínio matemático; a natureza da inferência; o cepticismo e o solipsismo; a indução; as constantes lógicas; a negação; a forma lógica; as leis da ciência; o número. (shrink)

This paper discusses the relevance of supertask computation for the determinacy of arithmetic. Recent work in the philosophy of physics has made plausible the possibility of supertask computers, capable of running through infinitely many individual computations in a finite time. A natural thought is that, if supertask computers are possible, this implies that arithmetical truth is determinate. In this paper we argue, via a careful analysis of putative arguments from supertask computations to determinacy, that this natural thought is mistaken: supertasks (...) are of no help in explaining arithmetical determinacy. (shrink)

We discuss the foundations of constructive mathematics, including recursive mathematics and intuitionism, in relation to classical mathematics. There are connections with the foundations of physics, due to the way in which the different branches of mathematics reflect reality. Many different axioms and their interrelationship are discussed. We show that there is a fundamental problem in BISH (Bishop’s school of constructive mathematics) with regard to its current definition of ‘continuous function’. This problem is closely related to the definition in BISH of (...) ‘locally compact’. Possible approaches to this problem are discussed. Topology seems to be a key to understanding many issues. We offer several new simplifying axioms, which can form bridges between the various branches of constructive mathematics and classical mathematics (‘reuniting the antipodes’). We give a simplification of basic intuitionistic theory, especially with regard to so-called ‘bar induction’. We then plead for a limited number of axiomatic systems, which differentiate between the various branches of mathematics. Finally, in the appendix we offer BISH an elegant topological definition of ‘locally compact’, which unlike the current definition is equivalent to the usual classical and/or intuitionistic definition in classical and intuitionistic mathematics, respectively. (shrink)

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)

Structuralist foundations of mathematics aim for an ‘invariant’ conception of mathematics. But what should be their basic objects? Two leading answers emerge: higher groupoids or higher categories. I argue in favor of the former over the latter. First, I explain why to choose between them we need to ask the question of what is the correct ‘categorified’ version of a set. Second, I argue in favor of groupoids over categories as ‘categorified’ sets by introducing a pre-formal understanding of groupoids as (...) abstract shapes. This conclusion lends further support to the perspective taken by the Univalent Foundations of mathematics. (shrink)

Famously, Michael Dummett argues that considerations concerning the role of language in communication lead to the rejection of classical logic in favor of intuitionistic logic. Potentially, this results in massive revisions of established mathematics. Recently, Neil Tennant (“The law of excluded middle is synthetic a priori, if valid”, Philosophical Topics 24 (1996), 205-229) suggested that a Dummettian anti-realist can accept the law of excluded middle as a synthetic, a priori principle grounded on a metaphysical principle of determinacy. This article shows (...) that the for the anti-realist, the law of excluded middle entails that humans have wildly implausible abilities. The proposed synthesis between anti-realism and classical mathematics thus fails. (shrink)

The study is focused on the relation between theology and mathematics in the situation of increasing secularization. My main concern in the second part of this paper is the early-twentieth-century foundational crisis of mathematics. The hypothesis that pure mathematics partially fulfilled the functions of theology at that time is tested on the views of the leading figures of the three main foundationalist programs: Russell, Hilbert and Brouwer.

The purpose of this paper is to apply Crispin Wright’s criteria and various axes of objectivity to mathematics. I test the criteria and the objectivity of mathematics against each other. Along the way, various issues concerning general logic and epistemology are encountered.

In this paper, I use the cases of intuitionistic arithmetic with Church’s thesis, intuitionistic analysis, and smooth infinitesimal analysis to argue for a sort of pluralism or relativism about logic. The thesis is that logic is relative to a structure. There are classical structures, intuitionistic structures, and (possibly) paraconsistent structures. Each such structure is a legitimate branch of mathematics, and there does not seem to be an interesting logic that is common to all of them. One main theme of my (...) ante rem structuralism is that any coherent axiomatization describes a structure, or a class of structures. If one weakens the logic, then more axiomatizations become coherent. (shrink)

ABSTRACTAIan Rumfitt's new book presents a distinctive and intriguing philosophy of logic, one that ultimately settles on classical logic as the uniquely correct one–or at least rebuts some prominent arguments against classical logic. The purpose of this note is to evaluate Rumfitt's perspective by focusing on some themes that have occupied me for some time: the role and importance of model theory and, in particular, the place of counter-arguments in establishing invalidity, higher-order logic, and the logical pluralism/relativism articulated in my (...) own recent *Varieties of logic*. (shrink)

We are logical pluralists who hold that the right logic is dependent on the domain of investigation; different logics for different mathematical theories. The purpose of this article is to explore the ramifications for our pluralism concerning normativity. Is there any normative role for logic, once we give up its universality? We discuss Florian Steingerger’s “Frege and Carnap on the Normativity of Logic” as a source for possible types of normativity, and then turn to our own proposal, which postulates that (...) various logics are constitutive for thought within particular practices, but none are constitutive for thought as such. (shrink)

The answers to the questions in the title depend on the kind of pluralism one is talking about. We will focus here on our own views. The purpose of this article is to trace out some possible connections between these kinds of pluralism. We show how each of them might bear on the other, depending on how certain open questions are resolved.

Should weak forms of the axiom of choice really be accepted within constructive mathematics? A critical view of the Brouwer-Heyting-Kolmogorov interpretation, accompanied by the intention to include nondeterministic algorithms, leads us to subscribe to Richman's appeal for dropping countable choice. As an alternative interpretation of intuitionistic logic, we propose to renew dialogue semantics.

In his remarkable paper Formalism 64, Robinson defends his eponymous position concerning the foundations of mathematics, as follows:Any mention of infinite totalities is literally meaningless.We should act as if infinite totalities really existed. Being the originator of Nonstandard Analysis, it stands to reason that Robinson would have often been faced with the opposing position that ‘some infinite totalities are more meaningful than others’, the textbook example being that of infinitesimals. For instance, Bishop and Connes have made such claims regarding infinitesimals, (...) and Nonstandard Analysis in general, going as far as calling the latter respectively a debasement of meaning and virtual, while accepting as meaningful other infinite totalities and the associated mathematical framework. We shall study the critique of Nonstandard Analysis by Bishop and Connes, and observe that these authors equate ‘meaning’ and ‘computational content’, though their interpretations of said content vary. As we will see, Bishop and Connes claim that the presence of ideal objects in Nonstandard Analysis yields the absence of meaning. We will debunk the Bishop–Connes critique by establishing the contrary, namely that the presence of ideal objects in Nonstandard Analysis yields the ubiquitous presence of computational content. In particular, infinitesimals provide an elegant shorthand for expressing computational content. To this end, we introduce a direct translation between a large class of theorems of Nonstandard Analysis and theorems rich in computational content, similar to the ‘reversals’ from the foundational program Reverse Mathematics. The latter also plays an important role in gauging the scope of this translation. (shrink)

Beall and Restall’s Logical Pluralism (2006) characterises pluralism about logical consequence in terms of the different ways cases can be selected in the analysis of logical consequence as preservation of truth over a class of cases. This is not the only way to understand or to motivate pluralism about logical consequence. Here, I will examine pluralism about logical consequence in terms of different standards of proof. We will focus on sequent derivations for classical logic, imposing two different restrictions on classical (...) derivations to produce derivations for intuitionistic logic and for dual intuitionistic logic. The result is another way to understand the manner in which we can have different consequence relations in the same language. Furthermore, the proof-theoretic perspective gives us a different explanation of how the one concept of negation can have three different truth conditions, those in classical, intuitionistic and dual-intuitionistic models. (shrink)

This is a survey of the concept of continuity. Efforts to explicate continuity have produced a plurality of philosophical conceptions of continuity that have provably distinct expressions within contemporary mathematics. I claim that there is a divide between the conceptions that treat the whole continuum as prior to its parts, and those conceptions that treat the parts of the continuum as prior to the whole. Along this divide, a tension emerges between those conceptions that favor philosophical idealizations of continuity and (...) those that are more readily available for mathematico-scientific use. (shrink)

When formalizing mathematics in constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids. In this note we consider two categories of setoids with equality on objects and show, within intensional Martin-Löf type theory, that they are isomorphic. Both categories are constructed from a fixed proof-irrelevant family F of setoids. The objects of the categories form the index setoid I of the family, whereas the definition of arrows differs. The first category (...) has for arrows triples →F)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\,\rightarrow \,F)$$\end{document} where f is an extensional function. Two such arrows are identified if appropriate composition with transportation maps makes them equal. In the second category the arrows are triples 2)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$^2)$$\end{document} where R is a total functional relation between the subobjects F,F↪Σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$F, F \hookrightarrow \Sigma $$\end{document} of the setoid sum of the family. This category is simpler to use as the transportation maps disappear. Moreover we also show that the full image of a category along an E-functor into an E-category is a category. (shrink)

A constructive definition of the continuum based on formal topology is given and its basic properties studied. A natural notion of Cauchy sequence is introduced and Cauchy completeness is proved. Other results include elementary proofs of the Baire and Cantor theorems. From a classical standpoint, formal reals are seen to be equivalent to the usual reals. Lastly, the relation of real numbers as a formal space to other approaches to constructive real numbers is determined.

In this paper, elementary but hitherto overlooked connections are established between Wittgenstein's remarks on mathematics, written during his transitional period, and free-variable finitism. After giving a brief description of theTractatus Logico-Philosophicus on quantifiers and generality, I present in the first section Wittgenstein's rejection of quantification theory and his account of general arithmetical propositions, to use modern jargon, as claims (as opposed to statements). As in Skolem's primitive recursive arithmetic and Goodstein's equational calculus, Wittgenstein represented generality by the use of free (...) variables. This has the effect that negation of unbounded universal and existential propositions cannot be expressed. This is claimed in the second section to be the basis for Wittgenstein's criticism of the universal validity of the law of excluded middle. In the last section, there is a brief discussion of Wittgenstein's remarks on real numbers. These show a preference, in line with finitism, for a recursive version of the continuum. (shrink)

We apply some tools developed in categorical logic to give an abstract description of constructions used to formalize constructive mathematics in foundations based on intensional type theory. The key concept we employ is that of a Lawvere hyperdoctrine for which we describe a notion of quotient completion. That notion includes the exact completion on a category with weak finite limits as an instance as well as examples from type theory that fall apart from this.

We investigate in intuitionistic first-order logic various principles of preference relations alternative to the standard ones based on the transitivity and completeness of weak preference. In particular, we suggest two ways in which completeness can be formulated while remaining faithful to the spirit of constructive reasoning, and we prove that the cotransitivity of the strict preference relation is a valid intuitionistic alternative to the transitivity of weak preference. Along the way, we also show that the acyclicity axiom is not finitely (...) axiomatizable in first-order logic. (shrink)

The present work contains an axiomatic treatment of some parts of the restricted version of intuitionistic mathematics advocated by G. F. C. Griss, also known as negationless intuitionistic mathematics.Formal systems NPC, NA, and FIMN for negationless predicate logic, arithmetic, and analysis are proposed. Our Theorem 4 in Section 2 asserts the translatability of Heyting's arithmetic HAinto NA. The result can in fact be extended to a large class of intuitionistic theories based on HAand their negationless counterparts. For instance, in Section (...) 3 this is shown for Kleene's system of intuitionistic analysis FIMand our FIMN. (shrink)

This work is a sequel to our [16]. It is shown how Theorem 4 of [16], dealing with the translatability of HA(Heyting's arithmetic) into negationless arithmetic NA, can be extended to the case of intuitionistic arithmetic in higher types.

Attempts to lay a foundation for the sciences based on modern mathematics are questioned. In particular, it is not clear that computer science should be based on set-theoretic mathematics. Set-theoretic mathematics has difficulties with its own foundations, making it reasonable to explore alternative foundations for the sciences. The role of computation within an alternative framework may prove to be of great potential in establishing a direction for the new field of computer science.Whitehead''s theory of reality is re-examined as a foundation (...) for the sciences. His theory does not simply attempt to add formal rigor to the sciences, but instead relies on the methods of the biological and social sciences to construct his world-view. Whitehead''s theory is a rich source of notions that are intended to explain every element of experience. It is a product of Whitehead''s earlier attempt to provide a mathematical foundation for the physical sciences and is still consistent with modern physics. (shrink)

The strong continuity principle reads “every pointwise continuous function from a complete separable metric space to a metric space is uniformly continuous near each compact image.” We show that this principle is equivalent to the fan theorem for monotone \ bars. We work in the context of constructive reverse mathematics.

We apply a framework developed by C. S. Peirce to analyze the concept of clarity, so as to examine a pair of rival mathematical approaches to a typical result in analysis. Namely, we compare an intuitionist and an infinitesimal approaches to the extreme value theorem. We argue that a given pre-mathematical phenomenon may have several aspects that are not necessarily captured by a single formalisation, pointing to a complementarity rather than a rivalry of the approaches.

We analyze the developments in mathematical rigor from the viewpoint of a Burgessian critique of nominalistic reconstructions. We apply such a critique to the reconstruction of infinitesimal analysis accomplished through the efforts of Cantor, Dedekind, and Weierstrass; to the reconstruction of Cauchy’s foundational work associated with the work of Boyer and Grabiner; and to Bishop’s constructivist reconstruction of classical analysis. We examine the effects of a nominalist disposition on historiography, teaching, and research.

This paper describes an axiomatic theory BT, which is a suitable formal theory for developing constructive mathematics, due to its expressive language with countable number of set types and its constructive properties such as the existence and disjunction properties, and consistency with the formal Church thesis. BT has a predicative comprehension axiom and usual combinatorial operations. BT has intuitionistic logic and is consistent with classical logic. BT is mutually interpretable with a so called theory of arithmetical truth PATr and with (...) a second-order arithmetic SA that contains infinitely many sorts of sets of natural numbers. We compare BT with some standard second-order arithmetics and investigate the proof-theoretical strengths of fragments of BT, PATr and SA. (shrink)

The existence of fundamental moral disagreements is a central problem for moral realism and has often been contrasted with an alleged absence of disagreement in mathematics. However, mathematicians do in fact disagree on fundamental questions, for example on which set-theoretic axioms are true, and some philosophers have argued that this increases the plausibility of moral vis-à-vis mathematical realism. I argue that the analogy between mathematical and moral disagreement is not as straightforward as those arguments present it. In particular, I argue (...) that pluralist accounts of mathematics render fundamental mathematical disagreements compatible with mathematical realism in a way in which moral disagreements and moral realism are not. 11. (shrink)

From ancient times to the present, the discovery and presentation of new proofs of previously established theorems has been a salient feature of mathematical practice. Why? What purposes are served by such endeavors? And how do mathematicians judge whether two proofs of the same theorem are essentially different? Consideration of such questions illuminates the roles that proofs play in the validation and communication of mathematical knowledge and raises issues that have yet to be resolved by mathematical logicians. The Appendix, in (...) which several proofs of the Fundamental Theorem of Arithmetic are compared, provides a miniature case study. (shrink)

Consistency with the formal Church’s thesis, for short CT, and the axiom of choice, for short AC, was one of the requirements asked to be satisfied by the intensional level of a two-level foundation for constructive mathematics as proposed by Maietti and Sambin From sets and types to topology and analysis: practicable foundations for constructive mathematics, Oxford University Press, Oxford, 2005). Here we show that this is the case for the intensional level of the two-level Minimalist Foundation, for short MF, (...) completed in 2009 by the second author. The intensional level of MF consists of an intensional type theory à la Martin-Löf, called mTT. The consistency of mTT with CT and AC is obtained by showing the consistency with the formal Church’s thesis of a fragment of intensional Martin-Löf’s type theory, called \, where mTT can be easily interpreted. Then to show the consistency of \ with CT we interpret it within Feferman’s predicative theory of non-iterative fixpoints \ by extending the well known Kleene’s realizability semantics of intuitionistic arithmetics so that CT is trivially validated. More in detail the fragment \ we interpret consists of first order intensional Martin-Löf’s type theory with one universe and with explicit substitution rules in place of usual equality rules preserving type constructors -rule which is not valid in our realizability semantics). A key difficulty encountered in our interpretation was to use the right interpretation of lambda abstraction in the applicative structure of natural numbers in order to model all the equality rules of \ correctly. In particular the universe of \ is modelled by means of \-fixpoints following a technique due first to Aczel and used by Feferman and Beeson. (shrink)

This paper explores strengths and limitations of both predicativism and nominalism, especially in connection with the problem of characterizing the continuum. Although the natural number structure can be recovered predicatively (despite appearances), no predicative system can characterize even the full predicative continuum which the classicist can recognize. It is shown, however, that the classical second-order theory of continua (third-order number theory) can be recovered nominalistically, by synthesizing mereology, plural quantification, and a modal-structured approach with essentially just the assumption that an (...) -sequence of concrete atoms be possible. Predicative flexible type theory may then be used to carry out virtually all of scientifically applicable mathematics in a natural way, still without ultimate need of the platonist ontology of classes and relations. (shrink)

To what extent can constructive mathematics based on intuitionistc logic recover the mathematics needed for spacetime physics? Certain aspects of this important question are examined, both technical and philosophical. On the technical side, order, connectivity, and extremization properties of the continuum are reviewed, and attention is called to certain striking results concerning causal structure in General Relativity Theory, in particular the singularity theorems of Hawking and Penrose. As they stand, these results appear to elude constructivization. On the philosophical side, it (...) is argued that any mentalist-based radical constructivism suffers from a kind of neo-Kantian apriorism. It would be at best a lucky accident if objective spacetime structure mirrored mentalist mathematics. the latter would seem implicitly committed to a Leibnizian relationist view of spacetime, but is it doubtful if implementation of such a view would overcome the objection. As a result, an anti-realist view of physics seems forced on the radical constructivist. (shrink)