You are here
Colloque : Intuitionism, Computation, and Proof: Selected themes from the research of G. Kreisel
This workshop will critically explore Georg Kreisel’s seminal contributions to logic and the philosophy of mathematics, by bringing together a number of experts to discuss developments initiated or significantly advanced by Kreisel's work in different areas. The discussion will revolve around three main topics: the “unwinding program” in proof theory, new insights about intuitionism and finitism in the foundations of mathematics, and Church’s thesis and informal rigor in computability and philosophy of mathematics.
- Mark van Atten (CNRS)
- Walter Dean (University of Warwick)
- Michael Detlefsen (University of Notre Dame)
- Daniel Isaacson (University of Oxford)
- Reinhard Kahle (Universidade Nova de Lisboa)
- Ulrich Kohlenbach (Technische Universität Darmstadt)
- Angus Macintyre (Queen Mary University of London)
- David Charles McCarty (University of Indiana)
- Joan Rand Moschovakis (Occidental College)
- Dana Scott (Carnegie Mellon University)
- Annika Siders (University of Helsinki)
- Göran Sundholm (Leiden University)
Friday 10th June, 2016
09:00 - 9:30 - Welcome and coffee
09:30 - 09:50 - Introduction
09:50 - 11:20 - Opening Lecture: Dana Scott - Types and Type-free Lambda-Calculus
11:20 - 12:30 - Walter Dean - Kreisel, the Liar, and the Arithmetized Completeness Theorem
12:30 - 14:00 - Lunch break
INTUITIONISM & CONSTRUCTIVE NOTIONS OF PROOF
14:10 - 15:20 - David Charles McCarty - Incompleteness and Informal Rigour
15:20 - 16:30 - Joan Rand Moschovakis - Markov's Rule, Markov's Principle and the Notion of Constructive Proof
16:30 - 17:00 - Coffee break
17:00 - 18:10 - Mark van Atten - On Two Problems with the Theory of the Creating Subject
18:10 - 19:20 - Annika Siders - From Consistency Reductions to Normalisation
Saturday 11th June, 2016
UNWINDING OF PROOFS
09:00 - 10:10 - Reinhard Kahle - Hilbert's Programme and Georg Kreisel
10:10 - 11:20 - Ulrich Kohlenbach - From Kreisel's 'Unwinding of Proofs' to the Program of 'Proof Mining'
11:20 - 11:40 - Coffee break
11:40 - 12:50 - Angus Macintyre - Examples of Unwinding in Kreisel Style
13:00 - 14:30 - Lunch break
PHILOSOPHY OF MATHEMATICS
14:30 - 15:40 - Daniel Isaacson - Kreisel's Philosophy of Mathematics
15:40 - 16:50 - Michael Detlefsen - Kreisel on Formalism
16:50 - 17:10 - Coffee break
17:10 - 18:30 - Closing Lecture: Göran Sundholm - Constructivist Options: Kreiselian Choices of Formal Systems
Titles and abstracts
Mark van Atten (CNRS)
On two problems with the Theory of the Creating Subject
Kreisel introduced the Theory of the Creating Subject to isolate and formulate explicitly the properties of the thinking subject that Brouwer used in certain arguments. Characteristic of these arguments is their exploitation of the fact that the activity of making mathematical constructions has itself a mathematical structure. In this talk, I will discuss two problems that have arisen with this theory. The first, perceived by Kreisel himself, lies in the fact that the Creating Subject's activity is supposed to proceed in an omega-sequence of steps, yet Brouwer also accepted proofs of transfinite length. The second, Troelstra's Paradox, suggests that there is too much self-reflexivity in the Theory of the Creating Subject. I will argue that Kreisel's objection is mistaken, and present a new solution to Troelstra's Paradox.
Walter Dean (University of Warwick)
Kreisel, the Liar, and the Arithmetized Completeness Theorem
In one of his earliest papers in mathematical logic (“Note on arithmetic models for consistent formulae of the predicate calculus”, 1950) Kreisel showed how the Arithmetized Completeness Theorem of Hilbert & Bernays (1939) can be used to construct statements formally independent of Gödel-Bernays set theory. I will first reconstruct Kreisel’s method (which involves an arithmetization of Russell’s paradox) and show how it can also be used to demonstrate the independence of various Liar-like sentences from arithmetical theories such as ACA0. I will then attempt to assess what light this sheds on the role of the paradoxes and of the Gödel (1929) completeness theorem on the development of the Hilbert program.
Michael Detlefsen (University of Notre Dame)
Kreisel on formalism
Various statements by Kreisel concerning his understanding of what is involved in a formalist conception of mathematics are identified and discussed. Particular attention is given to the similarities and differences between Kreisel’s view(s) of formalism and those of other thinkers with whose names formalism has often been associated.
Daniel Isaacson (University of Oxford)
Kreisel’s philosophy of mathematics
Kreisel has written how his interest in foundations of mathematics arose early on: “Since my school days I had had those interests in foundations that force themselves on beginners when they read Euclid's Elements (which was then still done at school in England), or later when they are introduced to the differential calculus.” At the same time, he had a mathematician’s distrust of philosophers of mathematics, even though he was one himself, in the way in which other mathematicians such as Cantor, Dedekind, Hilbert, Brouwer, Weyl, and Gödel have been philosophers of mathematics. Among Kreisel’s more than 200 publications, a relatively small number are explicitly philosophical, but these grow out of and at the same time inform the whole body of his work. Even so, while recognizing that Kreisel was a philosopher of mathematics, it’s not very easy to say what philosophy of mathematics should be labeled as his, unlike for each of the six other mathematicians I just mentioned. I shall attempt in this lecture to characterize Kreisel’s philosophy of mathematics.
Reinhard Kahle (Universidade Nova de Lisboa)
Hilbert's Programme and Georg Kreisel
Georg Kreisel is known for his constant and catching criticism of the philosophy behind Hilbert's Programme. In this talk we shall review these criticisms in view of a broader understanding of Hilbert's original aims. We shall also discuss how Kreisel's own proof-theoretic research fits in what could be called Hilbert's Larger Programme.
Ulrich Kohlenbach (Technische Universität Darmstadt)
From Kreisel's 'unwinding of proofs' to the program of 'proof mining'
Profoundly inspired by Georg Kreisel's pioneering work on the `unwinding of proofs' a systematic program of `proof mining' emerged during the past decades as a new applied form of proof theory. This program is concerned with the proof-theoretic extraction of hidden combinatorial and numerical content from given proofs. The main logical tools for this extraction are novel forms and extensions of Kurt Goedel's famous functional ('Dialectica') interpretation. Logical metatheorems based on such interpretations have been applied with particular success in the context of nonlinear analysis, ergodic theory, convex optimization and abstract Cauchy problems. The combinatorial content can manifest itself both in explicit effective bounds as well as in uniformity results. We will give a survey on some of these developments.
Angus Macintyre (Queen Mary University of London)
Examples of Unwinding in Kreisel style
I will concentrate on Kreisel's longterm interest in the logic of the Riemann zeta function, and on our joint work (from the 1980's) on unwinding of finiteness theorems in number theory.
David Charles McCarty (University of Indiana)
Incompleteness and Informal Rigour
In the course of his writings, Kreisel returned often to questions of completeness and incompleteness for formal intuitionistic logic. We will summarize Kreisel’s remarks and results on that topic, and compare them with more recent ideas and theorems. In the light of those results, we will investigate the troubled notion of informal rigour as presented in a number of Kreisel’s essays.
Joan Rand Moschovakis (Occidental College)
Markov's Rule, Markov's Principle and the notion of constructive proof
Markov's Rule is admissible for intuitionistic predicate logic and the usual formal systems for constructive and intuitionistic arithmetic and analysis. While the logical form of Markov's Principle is clearly non-constructive, the mathematical forms (which do not increase consistency strength) may be viewed as imposing conditions on the intended ranges of the variables, thus enhancing the notion of constructive proof.
Dana Scott (Carnegie Mellon University)
Types and Type-free Lambda-Calculus
Enumeration operators not only model Lambda-Calculus, but by using well known methods it is easy to add a rich type structure to the model to have the rules of Martin-Löf extensional type theory.
Annika Siders (University of Helsinki)
From consistency reductions to normalization
The reductions of Takeuti's presentation of the proof of Con(PA) can be explained as a restricted normalization proof.
Göran Sundholm (Leiden University)
Constructivist options: Kreiselian choices of formal systems
In my talk I wish to turn the tables on Kreisel and apply (the insight behind) his question to three of his contributions to the foundations of intuitionism:
Attending the workshop is free, but since space is limited we ask the participants to register by sending an email to firstname.lastname@example.org.