%
\label{def:proof-theory-as-e3}
\textbf{Proof theory} is the $\Elayer{3}$ self-modelling applied to $\Elayer{2}$ code.
Its four template components are:
\begin{enumerate}
    \item[\emph{(Carrier.)}]
    Formal systems as objects.
    The carrier is the class of $\Elayer{2}$ virtual machines---ZFC-VM
    (Definition~\ref{def:zfc-as-e2-vm}), Peano Arithmetic, type theories---each viewed
    not as a tool to be used but as a mathematical object to be studied.

    \item[\emph{(Predicate.)}]
    Provability about provability.
    Metatheoretic reasoning about a formal system must not contradict the system's own
    derivation behaviour: the metatheory is sound with respect to the object theory.

    \item[\emph{(Decoder.)}]
    Interpretation of metatheoretic results.
    The $\Elayer{3}$ decoder translates a syntactic metatheorem
    (e.g., ``ZFC does not prove $\mathrm{Con}(\mathrm{ZFC})$'')
    into a structural diagnosis (e.g., ``consistency is a host-level property'').

    \item[\emph{(Invariant.)}]
    Metatheoretic consistency.
    The host-level property of Chapter~\ref{ch:goedel-and-the-vm-boundary}
    is now the \emph{object of study}.
    At $\Elayer{2}$, consistency was the invariant---the property that the VM never crashes.
    At $\Elayer{3}$, proof theory investigates this invariant:
    which systems prove their own consistency?  Which do not?
    The $\Elayer{3}$ invariant is the stability of these conclusions
    under changes of metatheory.
\end{enumerate}