The speaker says "the regression of relative consistency proofs will only
be stopped by a metamathematical theory says Shapiro" and I can agree
with that, but, I try to never say "I want..." when talking about fundamental
objects, then pretty much also don't say "I'm a structuralist and it's category theory,
as if".
So I'm interested in Shapiro's "consistency problem" because it would have to have
a true universe of objects like a Comenius language. ("... some true theory as a foundation,
that's getting us into problems, ...", as the speaker puts it.)
"We've got to know that our mathemtical theories are consistent...". Yeah....
Also the "We all say ... vacuous truth ..." it's like no, we do not all say.
Also "pragmatic and empirical theories" are not fundamental platonic theories.
So, it sort of seems like an excusal-ism.
A usual model of category theory is usually basically as strong as equi-interpretable
as ZF, and, adding univalency is usually deemed "with two large cardinal axioms",
which, is for one to keep in mind, that large cardinals are neither cardinals nor sets,
and, it's selective hearing.
There's lots of great concepts and words but it's not very fulfilling and not representing
an adequate account of ontological commitment to logic and truth.
Basically such ontological commitment to the objects as structures involves having
to address the logical paradoxes and existential entailments head on, "as is", not "as if".
There's also that it's "one theory" from some "universe", if it's "true".
I.e., the language of a true theory is a Comenius language, where only truths are
well-formed formulas, and, it's not so tractable by itself except as being a space of those.