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.