Let me try to answer the question in an oblique way. I should apologise in advance for the poor quality scan below. I have been thinking about the distinction it illustrates quite a bit lately and this seemed like a good opportunity to put forth some of those thoughts.

To me the foundations of mathematics can be defined as that which you need in order to implement some system of mathematics. This implementation can be conceptual or actual. You might want to develop your lines of mathematical thought more systematically in order to understand what you are doing as a mathematician at some deeper conceptual level; or you might want (as I do) to implement an actual real world system that would help you and others to do mathematics on a computer and gain some confidence that what you are doing is correct according to some well defined criteria.

Returning to the first sentence of the last paragraph for a moment, it seems to me that, crucially, the foundations of mathematics cannot be mathematics itself. This is probably a contentious opinion but I will try to justify it, and find a way through it, later on.

Now suppose that you want to implement some system of mathematics. Very broadly speaking you need three things:

Some sort of type system. This gives you the concept of types, obviously, but also variables, constructors, etc and therefore terms, expressions, etc. Syntax, basically, and the rules that go with it. It might also give you the concept of equality. It used to be the case that second-order logic was employed to give you much of this. It is often stated that you can implement the axioms of Peano arithmetic in second-order logic, for example. These days, however, second-order logic appears to have been largely superseded by type theory. You can think of the type theory I refer to here as the LaTeX explanation of the type system, if that doesn't sound too glib.

Some sort of proof system. This gives you concepts of propositions as atomic things that can be treated as building blocks stuck together with inference rules. It gives you concepts of contexts, assumptions, suppositions and derivations. And it gives you the concept of something being true, or just holding. You actually don't need concepts of truth and falsity, funnily enough. Essentially some statement holds if there is a proof of it. So the system is intuitionistic in this sense. Note that I'm saying the it is the proof system itself that bears the stamp of being intuitionistic and not some logic or other. Also again I'm calling the proof theory the theoretical distillation of the proof system.

A vernacular. This gives you concepts of therems, axioms, etc and most importantly, proofs. It also provides the means of communication. Personally I'm always careful to avoid the word 'language' and prefer 'vernacular' even though it's a bit flowery. I won't try to justify my motives here.

Of course, you won't get agreement from anyone about what exactly constitutes these three parts or how they hang together. No doubt many would disagree wholly with all of this. I can only say that from personal experience this is what you need if you want to do some mathematics from the ground up. And I call all of this foundations of mathematics for that reason.

At this point I can safely dismiss set theory as foundations of mathematics entirely because it is itself mathematics and plays no part in the above.

Now I can come to the schematic below (apologies again for the poor quality):

I've seen it asserted many times that mathematics is circular. Here is an example and there are many others:

Does mathematics become circular at the bottom? What is at the bottom of mathematics?

Why the confusion and why is there seemingly no clarity on this? In my opinion the reason is that the distinction between foundational concepts and their mathematical counterparts seems to be hardly ever made. Let me give an example of what I mean by that in order to clarify.

In foundations you have the concept of a context. A context is a bunch of statements that have been proven to hold by way of a theorem or have been given as holding by way of an axiom. These statements are uniquely labelled so that they can be referenced. Theorems themselves have local contexts. Statements that hold can be assumed in, or imported into shall we say, a theorem, for use therein. You can, for example, make use of the fact that $\sqrt 2$ is irrational if you have proved it somewhere already in a theorem and labelled that theorem uniquely.

However, if you show a mathematician a context they will say something along the lines of ''sure, it's a set of ordered pairs'' or ''it's a mapping'' and won't be persuaded otherwise. They see a context as a mathematical object. A set, in fact. No surprises there!

But it isn't. It's a context, just a context. It's a foundational concept, not a mathematical one. Notice how I used to sloppy language to define it. I used the phrase ''bunch of''. This was quite deliberate. I didn't want to fall into mathematical language, but in fact often it's almost impossible not to when considering many foundational concepts. This begs the question:

Is it a legitimate pursuit to treat foundational concepts as mathematical ones?

I have two answers to what I regard as the most important of all questions (!):

- I don't know. I'm not smart enough to work it out.
- The question is moot. Because mathematicians have been and always will do it anyway.

Which brings me on to the whole Univalence thing. I dismiss this as foundations also. Why? Not because it appears to be really too clever and complicated for my liking. It is, but I know that's mostly my problem. I dismiss it because I think they are failing to make the above distinction.

It seems to me that those involved liken mathematics to some kind of computer language and that the aim, like most computer languages, is to get it to ''compile itself''. Nerds love this kind of thing but I think in mathematics it is misguided, although I'm lost for a way to express exactly why.

What I will write though, at the risk of repetition, is that it is important that anyone engaged in the study of foundations recognises the distinction between that and the mathematics it results in. And that they should at least try to justify, and indeed should consider seriously, the treatment of former in terms of the latter.

will they eventually replace set theory as a foundation of mathematicsis an appropriate question for this site. It would be more suitable at seer.stackexchange.com . $\endgroup$ – Emil Jeřábek Nov 24 '17 at 15:19notfind it compelling. (Perhaps set theorists?) Also, I'd like to know what the proof-theoretical status of univalent foundations is (as in "it proves the same theorems of arithmetic as this-or-that version of set theory"); maybe this should be another question (but I'm not even sure it's meaningful). $\endgroup$ – Gro-Tsen Nov 24 '17 at 20:3116more comments