Martin-Löf Conference on the Foundations of Mathematics: Day 1

I’m in Uppsala, Sweden, for the Foundations of Mathematics Conference dedicated to Per Martin-Löf on the occasion of his retirement. I’ve travelled up here together with fellow Archean Stewart Shapiro who’s giving a talk on Wednesday (incidentally on logical pluralism). So far the event has been well-organised and well-attended, with an impressive venue at the Swedish Collegium for Advanced Study. I applaud the fact that there was no registration fee for the conference!

When you go to top heavy conferences – like this one – you often end up surprised by which talks catch your fancy. Day 1 had names in proof-theory like William Tait and Giovanni Sambin, both of which I much looked forward to hearing for the first time, but in the end others stole the show. Tait’s talk was a largely historical discussion entitled ‘The Myth of Intuition’, where the role of Kantian intuition in Hilbert’s finitism was analysed. Sambin’s talk was perhaps the biggest surprise of the conference: A proposal for a new foundations of mathematics (and most other things!) roughly based on principles of abstraction and application, a machinery which he employed for his Basic logic in the papers of his that I’m familiar with. I readily admit that I didn’t anticipate that these techniques would be extended to foundational issues. Apparently, there is a forthcoming book with OUP called The Basic Picture which will provide a framework for the fifty mintues we got at the conference. Meanwhile, I’ll have to return to his earlier work for the proof-theory.

That is not to say that we didn’t get more technical talks. Peter Aczel’s gave an impressive but impenetrable (for yours truly) talk about type setups. Michael Rathjen gave us a very interesting peek into the world of constructive set theory. In constructive ZF you gain the option of adding axioms which would render classical set theory inconsistent – weaker logic means more things are consistent. One example, used by Stewart Shapiro, is that of adding an axiom schema for intuitionistic Church’s Thesis.

However, adding full axiom of choice (AC) to constructive set theory yields excluded middle, so that option is ruled out. More intuitively, AC asserts the existence of a function without saying anything about its definability, a feature that is typically taken to be constructively objectionable. Instead, Rathjen discusses alternative weaker choice principles, and how the addition of these can be justified with the help of constructive type-theory.