metamodels.md

We are also subject to the limits of the formal method, as manifested in Gödel's incompleteness theorems: With some effort (mainly by interpreting $\mathsf{PA}$ in $\ZF$), one can show that

• $\ZF$ is incomplete, i.e. there are statement in the language of set theory that $\ZF$ does not decide (of course, a famous example is the Continuum Hypothesis $\CH$),
• $\ZF$ cannot prove its own consistency.

The second part is particularly interesting. Since model theory itself can be formalized in $\ZF$ (more on that later), it means that the formal counterpart of the statement "There exists a model of $\ZF$*" cannot be proved in $\ZF$.