Intuitionism and Constructivism

Although Kant (1998) envisaged a prominent role for logic in the argumentative structure of his Critique of Pure Reason, logicians and philosophers have generally judged Kantgeneralformaltranscendental logics is a logic in the strict formal sense, albeit with a semantics and a definition of validity that are vastly more complex than that of first-order logic. The main technical application of the formalism developed here is a formal proof that Kants logic is after all a distinguished subsystem of first-order logic, namely what (...) is known as geometric logic. (shrink)

In this paper, we offer a Piagetian perspective on the construction of the logico-mathematical schemas which embody our knowledge of logic and mathematics. Logico-mathematical entities are tied to the subject's activities, yet are so constructed by reflective abstraction that they result from sensorimotor experience only via the construction of intermediate schemas of increasing abstraction. The axiom set does not exhaust the cognitive structure (schema network) which the mathematician thus acquires. We thus view truth not as something to be defined within (...) the closed world of a formal system but rather in terms of the schema network within which the formal system is embedded. We differ from Piaget in that we see mathematical knowledge as based on social processes of mutual verification which provide an external drive to any necessary dynamic of reflective abstraction within the individual. From this perspective, we argue that axiom schemas tied to a preferred interpretation may provide a necessary intermediate stage of reflective abstraction en route to acquisition of the ability to use formal systems in abstracto. (shrink)

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.

A bounded monotone sequence of reals without a limit is called a Specker sequence. In Russian constructive analysis, Church's Thesis permits the existence of a Specker sequence. In intuitionistic mathematics, Brouwer's Continuity Principle implies it is false that every bounded monotone sequence of real numbers has a limit. We claim that the existence of Specker sequences crucially depends on the properties of intuitionistic decidable sets. We propose a schema about intuitionistic decidability that asserts “there exists an intuitionistic enumerable set that (...) is not intuitionistic decidable” and show that the existence of a Specker sequence is equivalent to ED. We show that ED is consistent with some certain well known axioms of intuitionistic analysis as Weak Continuity Principle, bar induction, and Kripke Schema. Thus, the assumption of the existence of a Specker sequence is conceivable in intuitionistic analysis. We will also introduce the notion of double Specker sequence and study the existence of them. (shrink)

Using a slight generalization, due to Palmgren, of sheaf semantics, we present a term-model construction that assigns a model to any first-order intuitionistic theory. A modification of this construction then assigns a nonstandard model to any theory of arithmetic, enabling us to reproduce conservation results of Moerdijk and Palmgren for nonstandard Heyting arithmetic. Internalizing the construction allows us to strengthen these results with additional transfer rules; we then show that even trivial transfer axioms or minor strengthenings of these rules destroy (...) conservativity over HA. The analysis also shows that nonstandard HA has neither the disjunction property nor the explicit definability property. Finally, careful attention to the complexity of our definitions allows us to show that a certain weak fragment of intuitionistic nonstandard arithmetic is conservative over primitive recursive arithmetic. (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)

Some aspects of the theory of Boolean algebras and distributive lattices–in particular, the Stone Representation Theorems and the properties of filters and ideals–are analyzed in a constructive setting.

A basic result in intuitionism is Π02-conservativity. Take any proof p in classical arithmetic of some Π02-statement , with P decidable). Then we may effectively turn p in some intuitionistic proof of the same statement. In a previous paper [1], we generalized this result: any classical proof p of an arithmetical statement ∀x.∃y.P, with P of degree k, may be effectively turned into some proof of the same statement, using Excluded Middle only over degree k formulas. When k = 0, (...) we get the original conservativity result as particular case. This result was a by-product of a semantical construction. J. Avigad of Carnegie Mellon University, found a short, direct syntactical derivation of the same result, using H. Friedman's A-translation. His proof is included here with his permission. (shrink)

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.

Working within Bishop’s constructive framework, we examine the connection between a weak version of the Heine–Borel property, a property antithetical to that in Specker’s theorem in recursive analysis, and the uniform continuity theorem for integer-valued functions. The paper is a contribution to the ongoing programme of constructive reverse mathematics.

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.

Many existence propositions in constructive analysis are implied by the lesser limited principle of omniscience LLPO; sometimes one can even show equivalence. It was discovered recently that some existence propositions are equivalent to Bouwer's fan theorem FAN if one additionally assumes that there exists at most one object with the desired property. We are providing a list of conditions being equivalent to FAN, such as a unique version of weak König's lemma. This illuminates the relation between FAN and LLPO. Furthermore, (...) we give a short and elementary proof of the fact that FAN is equivalent to each positive valued function with compact domain having positive infimum. (shrink)

claims that constructive mathematics is inadequate for spacetime physics and hence that constructive mathematics cannot be considered as an alternative to classical mathematics. He also argues that the contructivist must be guilty of a form of a priorism unless she adopts a strong form of anti-realism for science. Here I want to dispute both claims. First, even if there are non-constructive results in physics this does not show that adequate constructive alternatives could not be formulated. Secondly, the constructivist adopts a (...) 'philosophy first' approach that Hellman rejects. This deep difference means that the viability of constructive mathematics cannot yet be decided by determining whether current scientific theories require classical mathematics. We need to decide which approach is most appropriate before we can even determine how we should go about deciding whether we should be constructive or classical mathematicians. (shrink)

When Bishop published Foundations of Constructive Analysis he showed that it was possible to do ordinary analysis within a constructive framework. Bishop's reasons for doing his mathematics constructively are explicitly philosophical. In this paper, I will expound, examine, and amplify his philosophical arguments for constructivism in mathematics. In the end, however, I argue that Bishop's philosophical comments cannot be rounded out into an adequate philosophy of constructive mathematics.

Friedrich Waismann, a little-known mathematician and onetime student of Wittgenstein's, provides answers to problems that vexed Wittgenstein in his attempt to explicate the foundations of mathematics through an analysis of its practice. Waismann argues in favor of mathematical intuition and the reality of infinity with a Wittgensteinian twist. Waismann's arguments lead toward an approach to the foundation of mathematics that takes into consideration the language and practice of experts.

It is well known that in Bishop-style constructive mathematics, the closure of the union of two subsets of ℝ is ‘not’ the union of their closures. The dual situation, involving the complement of the closure of the union, is investigated constructively, using completeness of the ambient space in order to avoid any application of Markov's Principle.

This is an introduction to, and survey of, the constructive approaches to pure mathematics. The authors emphasise the viewpoint of Errett Bishop's school, but intuitionism. Russian constructivism and recursive analysis are also treated, with comparisons between the various approaches included where appropriate. Constructive mathematics is now enjoying a revival, with interest from not only logicans but also category theorists, recursive function theorists and theoretical computer scientists. This account for non-specialists in these and other disciplines.

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

The spectral mapping theorem in a unital Banach algebra is examined for its constructive content.

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.

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.

In this chapter, which has evolved over the last ten years to what I hope will be its perfect Platonic form, I shall first discuss those features of constructive mathematics that distinguish it from its traditional, or classical, counterpart, and then illustrate the practice of that distinction in aspects of complex analysis whose classical treatment ought to be familiar to a beginning graduate student of pure mathematics.

In the informal setting of Bishop-style constructive reverse mathematics we discuss the connection between the antithesis of Specker’s theorem, Ishihara’s principle BD-N, and various types of equicontinuity. In particular, we prove that the implication from pointwise equicontinuity to uniform sequential equicontinuity is equivalent to the antithesis of Specker’s theorem; and that, for a family of functions on a separable metric space, the implication from uniform sequential equicontinuity to uniform equicontinuity is equivalent to BD-N.

Continuing the study of apartness in lattices, begun in [8], this paper deals with axioms for a product a-frame and with their consequences. This leads to a reasonable notion of proximity in an a-frame, abstracted from its counterpart in the theory of set-set apartness.

The nature of modern constructive mathematics, and its applications, actual and potential, to classical and quantum physics, are discussed.

It is argued that Hellman's arguments purporting to demonstrate that constructive mathematics cannot cope with unbounded operators on a Hilbert space are seriously flawed, and that there is no evidence that his thesis is correct.

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.

Working within Bishop-style constructive mathematics, we examine some of the consequences of the anti-Specker property, known to be equivalent to a version of Brouwer's fan theorem. The work is a contribution to constructive reverse mathematics.

We examine, from a constructive perspective, the relation between the complements of S, T, and S ∩ T in X, where X is either a metric space or a normed linear space. The fundamental question addressed is: If x is distinct from each element of S ∩ T, if s ϵ S, and if t ϵ T, is x distinct from s or from t? Although the classical answer to this question is trivially affirmative, constructive answers involve Markov's principle and (...) the completeness of metric spaces. (shrink)

The glueing of (sequentially, pointwise, or uniformly) continuous functions that coincide on the intersection of their closed domains is examined in the light of Bishop-style constructive analysis. This requires us to pay attention to the way that the two domains intersect.

This paper is dedicated to Prof. Dr. Günter Asser, whose work in founding this journal and maintaining it over many difficult years has been a major contribution to the activities of the mathematical logic community.At first sight it appears highly unlikely that Urysohn's Lemma has any significant constructive content. However, working in the context of an apartness space and using functions whose values are a generalisation of the reals, rather than real numbers, enables us to produce a significant constructive version (...) of that lemma. (shrink)

It is proved, within Bishop's constructive mathematics , that, in the context of a Hilbert space, the Open Mapping Theorem is equivalent to a principle that holds in intuitionistic mathematics and recursive constructive mathematics but is unlikely to be provable within BISH.

It is shown that in any model of constructive mathematics in which a certain omniscience principle is false, for strongly extensional functions on an interval the distinction between sequentially continuous and regulated disappears. It follows, without the use of Markov's Principle, that any recursive function of bounded variation on a bounded closed interval is recursively sequentially continuous.

The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop's constructive mathematics (BISH). it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructive mathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.