Great post, let me just add one point: > The 21-century understanding is something like: there's no need for there to be "ultimate" foundations. The modern vi

Great post, let me just add one point: > The 21-century understanding is something like: there's no need for there to be "ultimate" foundations. The modern view is that there simply is no ultimate foundation. Large cardinal axioms in set theory can be seen as adding more and more inner models of set theory (with fewer large cardinals) into an ambient theory. This is basically the same thing as asserting that "the previous theory is consistent". You can play this game forever and it will not converge - the result hinted at in the article states something different. --- In the end we use set theory as an alibi. We tell people that ultimately all of mathematics can be encoded in set theory, but it is neither a natural encoding, nor is it really true since we are talking about different flavors of "set theory". Algebraic geometry is a good example. To begin with, you are not using ZFC to encode categories - since you need to be able to manipulate proper classes as if they were sets - so we need to use some extension such as NBG set theory instead. Then, in order to construct the localisation of a large category you suddenly need large cardinals, even though intuitively the localisation is in some sense no larger than the category you start with. And this is the point where we forget this construction again, because it doesn't give any useful insights.