Intuitionism and Constructivism

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.

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)

: Bereft of the illusion of an epistemic vantage point external to science, what should be our commitment towards the categories, concepts and terms of that very science? Should we, despaired of the possibility to found these concepts on rock bottom, adopt empiricist skepticism? Or perhaps the inexistence of external foundations implies, rather, immunity for scientific ontology from epistemological criticism? Philosophy's "realism debate" died out without providing a satisfactory answer to the dilemma, which was taken over by the neighboring disciplines. (...) The "symmetry principle" of the "StrongProgramme" for the sociology of science-the requirement that truth and error receive the same kind of causal explanations-offered one bold metaphysical answer, under the guise of a methodological decree. Recently, however, it has been argued that this solution is not bold enough, that the social constructivists replaced the naïve presumption of an independent nature which adjudicates our beliefs with a mirror-image presumption of a sui generis society which furnishes these beliefs autonomously. The proper metaphysics for a foundationless epistemology, argues Bruno Latour, is one which grants nature and society, object and subject, equal roles in the success and failure of science and technology; one in which history of society merges with a history of things-in-themselves. The paper analyzes the philosophical and methodological motivations and ramifications of this extraordinary suggestion. (shrink)

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.

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)

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)

I introduce a formalization of probability which takes the concept of 'evidence' as primitive. In parallel to the intuitionistic conception of truth, in which 'proof' is primitive and an assertion A is judged to be true just in case there is a proof witnessing it, here 'evidence' is primitive and A is judged to be probable just in case there is evidence supporting it. I formalize this outlook by representing propositions as types in Martin-Lof type theory (MLTT) and defining a (...) 'probability type' on top of the existing machinery of MLTT, whose inhabitants represent pieces of evidence in favor of a proposition. One upshot of this approach is the potential for a mathematical formalism which treats 'conjectures' as mathematical objects in their own right. Other intuitive properties of evidence occur as theorems in this formalism. (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.

In the early 1920s, the German mathematician David Hilbert (1862–1943) put forward a new proposal for the foundation of classical mathematics which has come to be known as Hilbert's Program. It calls for a formalization of all of mathematics in axiomatic form, together with a proof that this axiomatization of mathematics is consistent. The consistency proof itself was to be carried out using only what Hilbert called “finitary” methods. The special epistemological character of finitary reasoning then yields the required justification (...) of classical mathematics. Although Hilbert proposed his program in this form only in 1921, various facets of it are rooted in foundational work of his going back until around 1900, when he first pointed out the necessity of giving a direct consistency proof of analysis. Work on the program progressed significantly in the 1920s with contributions from logicians such as Paul Bernays, Wilhelm Ackermann, John von Neumann, and Jacques Herbrand. It was also a great influence on Kurt Gödel, whose work on the incompleteness theorems were motivated by Hilbert's Program. Gödel's work is generally taken to show that Hilbert's Program cannot be carried out. It has nevertheless continued to be an influential position in the philosophy of mathematics, and, starting with the work of Gerhard Gentzen in the 1930s, work on so-called Relativized Hilbert Programs have been central to the development of proof theory. (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)

The main result of this paper is a weak constructive version of the uniform continuity theorem for pointwise continuous, real-valued functions on a convex subset of a normed linear space. Recursive examples are given to show that the hypotheses of this theorem are necessary. The remainder of the paper discusses conditions which ensure that a sequentially continuous function is continuous. MSC: 03F60, 26E40, 46S30.

The program of Reverse Mathematics (Simpson 2009) has provided us with the insight that most theorems of ordinary mathematics are either equivalent to one of a select few logical principles, or provable in a weak base theory. In this paper, we study the properties of the Dirac delta function (Dirac 1927; Schwartz 1951) in two settings of Reverse Mathematics. In particular, we consider the Dirac Delta Theorem, which formalizes the well-known property ${\int_\mathbb{R}f(x)\delta(x)\,dx=f(0)}$ of the Dirac delta function. We show that (...) the Dirac Delta Theorem is equivalent to weak König’s Lemma (see Yu and Simpson in Arch Math Log 30(3):171–180, 1990) in classical Reverse Mathematics. This further validates the status of WWKL0 as one of the ‘Big’ systems of Reverse Mathematics. In the context of ERNA’s Reverse Mathematics (Sanders in J Symb Log 76(2):637–664, 2011), we show that the Dirac Delta Theorem is equivalent to the Universal Transfer Principle. Since the Universal Transfer Principle corresponds to WKL, it seems that, in ERNA’s Reverse Mathematics, the principles corresponding to WKL and WWKL coincide. Hence, ERNA’s Reverse Mathematics is actually coarser than classical Reverse Mathematics, although the base theory has lower first-order strength. (shrink)

The relationship of Grundy and chromatic numbers of graphs in the context of Reverse Mathematics is investi-gated.

We represent continuous functions on compact intervals by sequences of functions defined on finite sets of rational numbers. We call this an exact representation. This enables us to calculate the values of the function arbitrarily exactly, without roundoff errors. As an application we develop a procedure to transfer an exact representation of an increasing function into an exact representation of the corresponding inverse function.

Gödel and others held that impredicative specification is illegitimate in a constructivist framework but legitimate elsewhere. Michael Dummett argues to the contrary that impredicativity, though not necessarily illicit, needs justification regardless of whether one assumes the context is realist or constructivist. In this paper I defend the Gödelian position arguing that Dummett seeks a reduction of impredicativity to predicativity which is neither possible nor necessary. The argument is illustrated by considering first highly predicative versions of the equinumerosity axiom for cardinal (...) number and Axiom V for sets, on the one hand, then classically consistent disjunctivised versions of Axiom V which are impredicative but can prove the well-foundedness of the semantics of weaker such systems, on the other. (shrink)

Here is Hilbert is his famous address of 1900: The supply of problems in mathematics is inexhaustible, and as soon as one problem is solved numerous others come forth in its place. Permit me in the following, tentatively as it were, to mention particular definite problems, drawn from various branches of mathematics, from the discussion of which an advancement of science may be expected.

In his paper "Finitism" (1981), W.W. Tait maintains that the chief difficulty for everyone who wishes to understand Hilbert's conception of finitist mathematics is this: to specify the sense of the provability of general statements about the natural numbers without presupposing infinite totalities. Tait further argues that all finitist reasoning is essentially primitive recursive. In this paper, we attempt to show that his thesis "The finitist functions are precisely the primitive recursive functions" is disputable and that another, likewise defended by (...) him, is untenable. The second thesis is that the finitist theorems are precisely the universal closures of the equations that can be proved in PRA. /// En su articulo "Finitism" (1981), W.W. Tait sostiene que la dificultad principal para quien quiere comprender la concepción hilbertiana de la matemática finitista es ésta: especificar el sentido de la demostrabilidad de enunciados generales sobre los números naturales sin presuponer totalidades infinitas. Además, Tait argumenta que todo razonamiento finitista es esencialmente primitivo recursivo. En este artículo tratamos de mostrar que su tesis "Las funciones finitistas son precisamente las funciones primitivas recursivas" es discutible y que otra, también defendida por él, resulta insostenible. La segunda tesis es que los teoremas finitistas son precisamente las clausuras universales de las ecuaciones que pueden demostrarse en PRA. (shrink)

We define DNA sequence by a bottom-up approach, starting with a real sequence from an actual biological sample. By providing axioms for notions of string, substring and strand, we formally define a DNA sequence, and a DNA molecule as composed of two antiparallel strands. We note that a sequence is a kind of group in which each member stands a certain relation to every other. The spatial aspects of a DNA sequence are also described.

The background of these remarks is that in 1967, in ‘’Constructive reasoning” [27], I sketched an argument that finitist arithmetic coincides with primitive recursive arithmetic, P RA; and in 1981, in “Finitism” [28], I expanded on the argument. But some recent discussions and some of the more recent literature on the subject lead me to think that a few further remarks would be useful.

Self‐evidently the standard work on the topic its whole title defines, Sir Michael Dummett’s Frege: Philosophy of Mathematics (FPM) is also the most profound and creative discussion in recent decades of the problems confronting the branch of philosophy mentioned after the colon. Chapters 14‐18 and 23‐24 of this book constitute a continuous and challenging diagnosis of these problems.1 They culminate in the proposal that these problems present an impasse that can be escaped only by adopting a constructivist understanding of mathematical (...) generality. Dummett’s case for that conclusion is no less complexly over‐layered than the problems themselves. By contrast my aims in this discussion of his case are limited in various ways, and three of these should be mentioned straightaway. In the first place, I will aim to consider a case that, if sound, would warrant a constructivist understanding of generality in mathematics generally (and so I will not be considering lines of argument specific to set theory, or to those parts of mathematics plausibly dependent on notions intrinsic to set theory). Secondly, I aim to consider a case which, while general in its application within mathematics, is not more general than that (and so would not warrant a broader anti‐realism). Reasons for these first two limitations are discussed in section 1. A third limitation is that I will aim only to understand Dummett’s case, and not to assess it. Perhaps some will think this third limitation calls for explanation or excuse. I think it needs no excuse and that the explanation is obvious. When we are dealing with fundamentally important work by a great philosopher, understanding is often ambition enough. In Michael Dummett’s work, that is what we are dealing with. (shrink)

Reviews Dummett's "Elements of intuitionism".

It is shown that, relative to Bishop-style constructive mathematics, the boundedness principle BD-N is equivalent both to a general result about the convergence of double sequences and to a particular one about Cauchyness in a semi-metric space.

Working within Bishop-style constructive mathematics, we derive a number of results relating the nonconstructive LPO and sequential compactness property on the one hand, and the intuitionistically reasonable anti-Specker property on the other.

In 1970 Vesley proposed a substitute of Kripke's Scheme. In this paper it is shown that —over Bishop's constructive mathematics— the indecomposability of negative dense subsets of ℝ is equivalent to a weakening of Vesley's proposal. This result supports the idea that full Kripke's Scheme might not be necessary for most of intuitionistic mathematics. At the same time it contributes to the programme of Constructive Reverse Mathematics and gives a new answer to a 1997 question of Van Dalen.

It is shown that—over Bishop's constructive mathematics—the indecomposability of ℝ is equivalent to the statement that all functions from a complete metric space into a metric space are sequentially nondiscontinuous. Furthermore we prove that the indecomposability of ℝ \ {0} is equivalent to the negation of the disjunctive version of Markov's Principle. These results contribute to the programme of Constructive Reverse Mathematics.

A weak constructive sequential compactness property of metric spaces is introduced. It is proved that for complete, totally bounded metric spaces this property is equivalent to Brouwer's fan theorem for detachable bars. Our results form a part of constructive reverse mathematics.

The dissertation studies the mathematical strength of strict constructivism, a finitistic fragment of Bishop's constructivism, and explores its implications in the philosophy of mathematics. ;It consists of two chapters and four appendixes. Chapter 1 presents strict constructivism, shows that it is within the spirit of finitism, and explains how to represent sets, functions and elementary calculus in strict constructivism. Appendix A proves that the essentials of Bishop and Bridges' book Constructive Analysis can be developed within strict constructivism. Appendix B further (...) develops, within strict constructivism, the essentials of the functional analysis applied in quantum mechanics, including the spectral theorem, Stone's theorem, and the self-adjointness of some common quantum mechanical operators. Some comparisons with other related work, in particular, a comparison with S. Simpson's partial realization of Hilbert's program, and a discussion of the relevance of M. B. Pour-El and J. I. Richards' negative results in recursive analysis are given in Appendix C. ;Chapter 2 explores the possible philosophical implications of these technical results. It first suggests a fictionalistic account for the ontology of pure mathematics. This leaves a puzzle about how truths about fictional mathematical entities are applicable to science. The chapter then explains that for those applications of mathematics that can be reduced to applications of strict constructivism, fictional entities can be eliminated in the applications and the puzzle of applicability can be resolved. Therefore, if strict constructivism were essentially sufficient for all scientific applications, the applicability of mathematics of mathematics in science would be accountable. The chapter then argues that the reduction of mathematics to strict constructivism also reduces the epistemological question about mathematics to that about elementary arithmetic. The dissertation ends with a suggestion that a proper epistemological basis for arithmetic is perhaps a mixture of Mill's empiricism and the Kantian views. (shrink)

Within Bishop's constructive mathematics we provide conditions that ensure weak continuity properties of mappings between metric and normed spaces.