[FOM] The distinction between foundational concepts and their treatment as mathematics`

[James Smith]

Hi,

recently I replied to this question on mathoverflow:

https://mathoverflow.net/questions/286874/in-what-respect-are-univalent-foundations-better-than-set-theory

Here is my (admittedly somewhat oblique) reply:

https://mathoverflow.net/q/286896

To be honest, I was hoping for some comments that challenged my answer, 
in order that I might learn something. The answer might appear (but is 
certainly not meant to be) contentious, in that it rejects both set 
theory and univalent foundations as foundations for mathematics. I think 
I'm not alone in putting forward a combination of some kind of a type 
theory and some kind of a proof theory as foundations, however. As far 
as my understanding goes, modern proof assistants do just that.

The thrust of my answer highlights the need for an understanding of the 
seemingly commonplace practice of treating of these formal systems as 
mathematics and the problems that arise (for example, circularity) as a 
consequence. My own opinion, voiced in my answer, is that it is almost 
practically impossible to avoid such treatments. Seeking some 
justification for this practice might be an interesting and prescient 
topic of debate, however.

Kind regards,

James