Philosophy of Mathematics Seminar (Monday - Week 6, MT18)

Constructive forms of mathematics are gaining renewed attention within today's mathematics under the stimulus of computer applications. Foundational systems for constructive mathematics, such as Martin-Löf type theory and Myhill and Aczel constructive set theory, have been proposed since the 1970's. These theories employ intuitionistic logic and also comply with a form of predicativity. It is often thought that intuitionistic logic and predicativity are wholly independent features of these non-standard foundational theories. In fact, the mathematical literature presents us with classical predicative theories (e.g. Feferman's system W) as well as intuitionistic impredicative theories (as Friedman's IZF). However, in Martin-Löf type theory compliance with a form of predicativity and intuitionistic logic are intriguingly interconnected, due to the so-called Curry-Howard isomorphism. In this talk, I focus on Michael Dummett's argument for intuitionistic logic from indefinite extendibility. A crucial component of that argument is the claim that the natural number concept is indefinitely extensible. I discuss the case of the indefinite extensibility of the natural numbers by employing ideas from the debate on predicativity. I argue that here, too, predicativity and intuitionistic logic are deeply interconnected.

Philosophy of Mathematics Seminar Convenors: Dr Daniel Isaacson and Prof Volker Halbach