# Formalizing model-theoretical large cardinals in a formal system for ZFC

I work with the Metamath formal system, which is expressive enough to define ZFC and prove some nontrivial stuff, but my current goal is to define large cardinals, and I'm hitting a wall somewhere around Mahlo cardinals, because it becomes difficult to write down what the properties of a given cardinal actually are. For example, I've devised the following definition for a strongly inaccessible cardinal:

$${\rm Inacc\ }\kappa\leftrightarrow\kappa\ne\emptyset\wedge{\rm cf\,}\kappa=\kappa\wedge\forall\alpha\in\kappa\ {\cal P}(\alpha)\prec\kappa$$

Since all the concepts are "internal" (existence of injective functions from well defined sets, etc.), this is an easy enough definition to make. Contrast this with the definition of a Woodin cardinal:

A cardinal $\kappa$ is a Woodin cardinal iff for all $f:\kappa\to\kappa$ there is an $\alpha<\kappa$ with $f\,`\alpha\subseteq \alpha$ and a $j:V\prec M$ with ${\rm crit}(j)=\alpha$ and $V_{j(f)(\alpha)}\subseteq M$. [Kanamori p. 360]

This definition depends on the concept of an elementary embedding $j:V\prec M$, so I'll hunt down that definition too:

$j$ is a ($\Sigma_1$-)elementary embedding from $N$ into $M$, denoted $j:N\prec M$, iff for any $\Sigma_1$ formula $\varphi$ in the language $\cal L_\in$ and $x_1,\dots,x_n\in N$, $$\langle N,\in\rangle\models\varphi[x_1,\dots,x_n]\quad{\rm iff}\quad\langle M,\in\rangle\models\varphi[j(x_1),\dots,j(x_n)].$$ [Kanamori p. 45]

At this stage, I'm lost. How can I possibly write this concept down as a formula? How am I supposed to formalize the $\models$ relation? I can't quantify over formulas.

Edit: I realize now this is a question about defining model theory in ZFC, although @AndresCaicedo's comment below suggests a way to define most large cardinals without any model theory. I'm going to show my planned definition of the satisfaction predicate, although it's necessarily quite complicated. Hopefully, this is the only definition of this level of complexity that will be necessary.

\begin{align} {\rm Sat}_0=\{\langle x,\gamma\rangle\mid\exists i,j\in\omega\,(\!&(x=\langle 0,\langle i,j\rangle\rangle\wedge\gamma=\{a\in M^\omega\mid a(i)=a(j)\}) \\ \vee&(x=\langle 1,\langle i,j\rangle\rangle\wedge\gamma=\{a\in M^\omega\mid a(i)\,\varepsilon\,a(j)\}))\} \end{align} \begin{align} {\rm Sat}_{n+1}={\rm Sat}_n\cup&\big\{\langle x,\gamma\rangle\mid\exists\langle y,\eta\rangle\in{\rm Sat}_n \\ \big(\!&\exists\langle z,\theta\rangle\in{\rm Sat}_n(x=\langle 2,\langle y,z\rangle\rangle\wedge\gamma=\eta\cap\theta) \\ \vee&(x=\langle 3,y\rangle\wedge\gamma=M^\omega\setminus\eta) \\ \vee&\exists i\in\omega\,(x=\langle 4,\langle i,y\rangle\rangle\wedge\gamma=\{a\in M^\omega\mid\forall s\in M\,a[i/s]\in\eta\})\big)\!\big\} \end{align} $${\rm Sat}=\bigcup_{n\in\omega}{\rm Sat}_n$$

I am hoping this definition (of my own devising) is the only one at this level of complexity. (One piece of unusual notation, for brevity: $a[i/s]:\omega\to M$ is the function defined from $a$ by $a[i/s](j)=a(j)$ if $j\ne i$ and $a[i/s](i)=s$.) The interpretation of this recursively defined function is that the domain of ${\rm Sat}$ is the set of all wffs over the language $\{=,\in,\wedge,\neg,\forall\}$, where the coding scheme is: \begin{align} \ulcorner v_i=v_j\urcorner&=\langle 0,\langle i,j\rangle\rangle \\ \ulcorner v_i\in v_j\urcorner&=\langle 1,\langle i,j\rangle\rangle \\ \ulcorner\phi\wedge\psi\urcorner&=\langle 2,\langle\ulcorner\phi\urcorner,\ulcorner\psi\urcorner\rangle\rangle \\ \ulcorner\neg\phi\urcorner&=\langle 3,\ulcorner\phi\urcorner\rangle \\ \ulcorner\forall v_i\,\phi\urcorner&=\langle 4,\langle i,\ulcorner\phi\urcorner\rangle\rangle \end{align} Given a formula $\phi(v_0,v_1,\dots)$, ${\rm Sat}(\ulcorner\phi\urcorner)$ is the set of all assignments $a\in M^\omega$ such that $\phi(a(0),a(1),\dots)$ holds, where the membership relation is interpreted as the $\varepsilon$ binary relation on $M$ (both $M$ and $\varepsilon$ are held fixed for this definition, which is more appropriately ${\rm Sat}_{\langle M,\varepsilon\rangle}$).

I have a few questions following this definition: is this sufficient to develop model theory? In particular, how do we define the concept of provability, with axioms and inference rules? Also, are there any issues I might encounter with this setup? This differs from some other developments in that I don't bound the number of free variables in the formula (by compactness, I don't need all $\omega$ free variables in any proof, even if they are available) because I didn't see why it would be necessary. Also, for this definition to work, I need $M$ to be a set, which is a problem sometimes in uses of the satisfaction predicate.

-
Sure you can. You just have to keep the levels of logic separate in some fashion. $\mathcal L_\in$ is considered purely formally: it's a bunch of letters and strings and such with no inherent meaning. I don't know nearly enough about these issues to get into details. –  dfeuer Jun 11 '13 at 2:09
You do not need to worry about quantification over proper classes and issues about satisfaction predicates. All these large cardinal notions described in terms of embeddings are formalizable in $\mathsf{ZFC}$ via the notions of ultrafilters, extenders, and ultrapowers. Kanamori's book on large cardinals presents all the details. Typically, rather than saying "there is a transitive proper class $M$ and an elementary $j:V\to M$ such that ..." one states that "there is an extender (with some properties) such that ..." –  Andres Caicedo Jun 11 '13 at 3:56
@AndresCaicedo I would be interested to see the details of this. I have Kanamori's book The Higher Infinite (which I started reading because everyone seems to cite it); do you have a particular reference? –  Mario Carneiro Jun 11 '13 at 5:48
@AndresCaicedo I've made an edit to the post documenting some of my work on defining the satisfaction predicate. I should have been more specific; although I am interested in your suggestion of avoiding model theory in the definitions of large cardinals, I think model theory is quite necessary to talk about consistency strength, which explicitly refers to provability. What the hell is hiding behind the curtain in the statement ${\rm Con}({\sf ZFC})$? –  Mario Carneiro Jun 11 '13 at 11:16
@Mario: Andres comments is correct, but I suggest you start with 1) a more accesible book like the one by Jech and Hrbacek, or Wikipedia 2) a lower level cardinal like measurable. –  Eran Jun 12 '13 at 20:45