Constructivist views of mathematics have several intriguing philosophical advantages. Perhaps most promising is that they provide a neat resolution of the access problem, because the ability of humans to grasp mathematical objects is built into the metaphysical picture of what those objects are. This provides a resolution of both the epistemic and semantic problems concerning how we can know, reason about, and refer to mathematical objects. The notion of a construction, however, has always been problematic. Many authors take it for granted as a primitive notion. Others give an operational definition (usually in terms of computation). And some philosophers have faced up to the metaphysical challenge of explaining what constructions are. Despite this, no generally accepted account has emerged. At the same time, generalizations of the constructive outlook have been pursued under the various guises of predicativism, potentialism, stage theory, and elsewhere. This more general family of views have been called "constructional", to distinguish them from the traditional constructive view.
The overarching question of this workshop is: what is a mathematical construction and what makes a mathematical theory constructive?
Under this heading, subsidiary questions of interest include:
- Given an account of construction, are the alleged benefits of constructivism genuine?
- How does the notion of construction relate to the more general "constructional" outlooks?
- Do those generalized constructional views enjoy the same benefits as constructivism itself?
- Traditional constructivism idealizes from limits on memory, time, etc., in order to avoid collapsing into strict finitism. How, precisely, can those idealizations be defined? And can they be justified in such a way that first-order intuitionistic mathematics is justified, but not stronger outlooks?
Speakers: Ethan Brauer (Oslo), Michele Contente (Prague), Laura Crosilla (Florence), Mirja Hartimo (Helsinki), Ansten Klev (Prague), Øystein Linnebo (Oslo), Stephen Mackereth (Dartmouth), Michael Rathjen (Leeds)
Schedule
Day 1 (27 August)
8:45-9. Welcome and coffee
9:00 – 10:20. Laura Crosilla, “Weyl’s constructivism”
10:40 – 12:10. Michael Rathjen, “On recent critiques of the Kreisel-Feferman-Schütte approach to predicativity”
12:10 – 1:40. Lunch
1:40 – 3:00. Ethan Brauer, “Weyl on symbolic construction”
3:20 – 4:40. Michele Contente, “Predicativity: Classical and Constructive”
Day 2 (28 August)
8:45-9. Welcome and coffee
9:00 – 10:20. Ansten Klev, “Meaningful formalism and infinitary objects”
10:40 – 12:10. Stephen Mackereth, “How constructive is Gödel’s Dialectica Interpretation?”
12:10 – 1:40. Lunch
1:40 – 3:00. Mirja Hartimo, “Constructivism, constructionalism, and constitution”
3:20 – 4:40. Øystein Linnebo, “Constructional ontology: why and how?”
Abstracts
Laura Crosilla, “Weyl’s Constructivism”
Commentators often distinguish distinct phases in Weyl's thought on the foundations of mathematics. In fact, Weyl has been criticized for repeatedly changing his views on foundations. While there are clearly significant shifts in Weyl's views, it is also undeniable that some key features permane throughout his foundational reflection. In fact, a constructivistic attitude is one of the most prominent constant features in his thought.
I will review the main aspects of Weyl's constructive approach to the foundations of mathematics, focusing especially on the early Weyl.
Michael Rathjen, “On recent critiques of the Kreisel-Feferman-Schütte approach to predicativity”
The goal is to examine whether the charge of illegitimate impredicative moves in the KFS-characterization of predicativity is warranted.
Ethan Brauer, “Weyl on symbolic construction”
Throughout the last 30 years of his life, Weyl describes mathematics and theoretical physics in terms of the method of symbolic construction. I will outline how he understands this method, highlighting how it differs from the mathematical process of Das Kontinuum, and drawing attention to its both realist and anti-realist elements.
Michele Contente, “Predicativity: Classical and Constructive”
The notion of predicativity is not univocal and admits a plurality of characterisations. The classical notion of predicativity, which takes for granted the natural numbers structure, has been elegantly characterised by Feferman and Schütte, who identified the limit of predicative reasoning in this sense. Independently, a more generous conception of predicativity has been developed within constructive mathematics, though it lacks a comparably sharp characterization.
The aim of this talk is to investigate how the notion of predicativity is affected by the choice of underlying logic. In the first part, I shall examine the conception developed by Weyl in Das Kontinuum, focusing on the set-formation procedure - 'the mathematical process' - described in the opening sections of the book.
In the second part, I will turn to the constructive, or generalized, conception of predicativity as embodied in Martin-Löf type theory, and discuss how it can be justified on the basis of Martin-Löf's meaning explanations. Finally, I will consider whether this perspective offers any hints concerning the limits of constructive predicativity and the challenges that arise when one attempts to reconcile it with classical logic.
Ansten Klev, “Meaningful formalism and infinitary objects”
The basic tenet of constructive logic is that every existential assertion must be backed up by a witness. It follows from this that every object reasoned about must be finitely presentable. Taking an intensional view of mathematical ontology, I shall regard the presentation of an object as its form. If an object is uniquely determined by its form, as in traditional formalism, then constructivism rules out infinitary objects. If we instead allow objects to have both form and content, as in the view I call meaningful formalism, then infinitary objects are constructively acceptable. I will explain how the analysis of the content of an object takes the form of a tree. The tree is, in general, infinite, but since it portrays a process, the infinity in question is potential.
Stephen Mackereth, “How constructive is Gödel’s Dialectica Interpretation?”
Gödel intended his Dialectica interpretation to provide a foundational reduction of first-order arithmetic to a strictly constructive theory T, that is, a quantifier-free theory with decidable primitives. It has widely been objected, however, that Gödel’s system T tacitly presupposes quantificational logic, hidden within its complicated definition of "computable function of finite type." This would render the translation philosophically circular. Gödel was adamant that there was no circularity here. He sketched a defense of this claim in a page-long footnote, which however has left readers baffled. In this talk, I will explain Gödel’s footnote and argue that there really is no circularity here. Thus, Gödel has achieved a significant foundational reduction. The foundations of T turn out to be stranger than meets the eye; they utilize a broadly Leibnizian notion of analyticity in a surprising way.
Mirja Hartimo, “Constructivism, constructionalism, and constitution”
This paper aims to clarify the differences between constructivism and some forms of constructionalism in terms of their phenomenological constitution. It will be argued that the differences in the evidence with which the transcendent mathematical objects and theories are given together with the presuppositions of the given research approach explain these differences rather than some of them being more “subjective” as opposed to “objective.” The paper will also consider how the putative philosophical benefits of constructivism should be understood from the phenomenological point of view.
Øystein Linnebo, “Constructional ontology: why and how?”
Gödel and others have suggested that a set can be regarded as constructed from its elements. Given any objects, we can apply the “set of” operation to construct the set of these objects. Inspired by Gödel’s suggestion, this talk presents a far more general constructional approach to ontology. First, I clarify what it is for some objects to be “constructed” from others. The key is that all truths about the “new” objects that are constructed must reduce to truths about the “old” objects on which the construction is based. Then, I explain the central role of criteria of identity in the constructional approach. When constructing “new” objects, it is particularly important to stipulate what it takes for them to be identical or distinct. A variety of examples are provided, including mereological sums, ordered pairs, as well as cardinal and ordinal numbers. Finally, I present a logical framework in which this constructional approach can be developed. In this framework, a large and natural family of forms of construction can be proved to be consistent.