There are multiple languages to describe all of mathematics, and there are some equivalences between them, some more successful then others. My question is can we describe some requirements (in some logic system) that any foundational language must satisfy?
In praticular, I have been thinking about two requirements:
It can describe the logic system it lives in, for example in category theory we have the notion of a topos.
It can talk about itself, this is some kind of version of large-cardinal axioms: This is going to be very vague, but please bear with me: Let $\cal{L}$ be a language (in whatever logic system we need to make this rigurous). We can extend it to include another generic object, $\cal{L}[U]$ which would serve as the universe. We require the following template of axioms on $\cal{L}[U][E]$: Every predicate in $\cal{L}$ can be extended to one on $\cal{L}[U][E]$, we reuqiure it has an interpretation in every "internal universe" $U$ and is satisfied in $\cal{L}$ iff it is satisfied in every $U$
In set theory, those $U$ are inaccessible cardinals and this axiom is both the existance of arbitrarly large inaccessible ones, and the fact that to prove a theorem in set theory, is the same as proving it in every inaccessible cardinal. So in a sense, GNB set theory satisfies these axioms.
Can we make this rigorous? Is there a logic system that we can formulate this in? Another thing to ask, are all "universes" that can internalize the logic system they are defined in equivalent?
