%
\label{def:self-hosting-degree}
The \textbf{self-hosting degree} of a formal system $S$
is classified into four levels:
\begin{enumerate}[\normalfont(i)]
    \item \textbf{None.}
          $S$ has no internal representation
          of its own proof theory.
          Proofs in $S$ are syntactic objects
          manipulated by an external meta-theory;
          $S$ itself has no way
          to state or reason about
          the structural rules that govern its proofs.
          Examples: ZFC (set membership is the only primitive;
          proof theory is entirely external),
          PA (first-order arithmetic; no internal proof objects),
          HoTT as currently practiced
          (internal language of $(\infty,1)$-toposes,
          but meta-theory remains external).
    \item \textbf{Partial.}
          $S$ encodes its own syntax
          but not its structural rules.
          $S$ can form sentences about its own sentences,
          prove theorems about provability,
          and exhibit self-referential statements.
          But the structural rules ---
          contraction, weakening, exchange,
          the cut rule, the substitution operation ---
          remain properties of $S$
          that $S$ cannot access.
          Examples: Peano arithmetic via G\"odel numbering,
          any sufficiently strong recursively enumerable theory
          via arithmetization.
    \item \textbf{Fragment.}
          $S$ internalizes a significant fragment
          of its own meta-theory,
          but the internalization requires
          a strictly stronger ambient system.
          The fragment may include
          normalization, type-checking, completeness,
          or other metatheorems ---
          proved ``internally'' in the sense
          that the proofs live inside a formal system,
          but the formal system used
          is strictly stronger than the system described.
          Examples: Altenkirch--Kaposi's type theory in type theory
          (dependent type theory internalized in CIC
          with quotient inductive types~\cite{AltenkirchKaposi2016}),
          Joyal's arithmetic universes
          (internalize enough to prove
          G\"odel's theorem internally~\cite{vanDijkGietelinkOldenziel2020}),
          Bocquet--Kaposi--Sattler's internal sconing
          (metatheorems via internal
          gluing~\cite{BocquetKaposiSattler2023}).
    \item \textbf{Full.}
          $S$ reasons about its own proof theory,
          structural rules, and consistency
          using only its own resources.
          The meta-language and the object language coincide.
          No external substrate remains.
          No known example at meaningful mathematical strength.
\end{enumerate}