\label{def:zfc-as-e2-vm}
The \textbf{ZFC virtual machine} is the $\Elayer{2}$ quadruple
\begin{equation}\label{eq:ch64-zfc-vm}
\mathrm{ZFC\textrm{-}VM} \;=\; \bigl(\,\mathrm{Sent}_{\mathrm{ZFC}},\; {\vdash}_{\mathrm{ZFC}},\; \ulcorner\cdot\urcorner,\; \mathrm{Con}(\mathrm{ZFC})\,\bigr),
\end{equation}
where the four components are:
\begin{enumerate}
\item\emph{(Carrier.)}
$\mathrm{Sent}_{\mathrm{ZFC}}$ is the set of well-formed sentences in the first-order language of ZFC.  These sentences are self-referential via G\"odel numbering: the sentence ``this sentence is not derivable'' is a legitimate element of the carrier.

\item\emph{(Predicate.)}
${\vdash}_{\mathrm{ZFC}}$ is the derivability relation.  Given a finite set of axioms and the rules of first-order logic, derivability decides which sentences are theorems.  Derivability is the operational closure of the inference rules: the output of applying rules to axioms is another sentence, which is itself subject to further rules.

\item\emph{(Decoder.)}
$\ulcorner\cdot\urcorner \colon \mathrm{Sent}_{\mathrm{ZFC}} \to \mathbb{N}$ is G\"odel numbering.  The decoder maps sentences to natural numbers and, crucially, admits an inverse: given a G\"odel number $n$, the decoding function recovers the sentence $\varphi$ such that $\ulcorner\varphi\urcorner = n$.  The decoder closes the self-referential loop: a sentence can reference its own code.

\item\emph{(Invariant.)}
$\mathrm{Con}(\mathrm{ZFC})$ is the consistency statement $\nvdash_{\mathrm{ZFC}} (0 = 1)$.  The invariant asserts that the VM never crashes: the derivability engine, applied to the axioms, never produces a contradiction.  Without this invariant, the VM would derive every sentence (by \emph{ex falso quodlibet}), and the carrier would collapse to triviality.
\end{enumerate}