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.