$\epsilon$-Formalization of Undecidability of CH

Question

Can the statement

CH is not provable in ZFC

be formalized as en $\epsilon$-Formula $\phi$ s.t. $ZFC \vdash \phi $

If so why is it refered to as an "metatheorem".

Answer 1

If ZFC is consistent, then no, it does not prove the assertion "CH is not provable in ZFC", since the non-provability of any assertion in a theory implies the consistency of that theory, and so this would mean that ZFC proves its own consistency, contrary to the incompleteness theorem.

However, you probably mean to refer to the relative consistency assertion

If ZFC is consistent, then CH is not provable in ZFC.

This indeed is formalizable as an assertion of number theory, and it can be proved in PA and indeed much weaker systems. In particular, yes, it can also be formalized in the language of set theory and proved in ZFC itself.

Such theorems are refered to as metatheorems because they are theorems about what is and is not provable. Generally the metatheorems are provable in extremely weak theories of arithmetic, simply because we do not generally make substantial mathematical assumptions in the metatheory, but only in the object theories.

But of course, inspecting such an assertion in the pure language of set theory would shed almost no illumination on the mathematics of the situation---it would be like inspecting the assembly language instruction set resulting from compiling a program written in a high-level language. But in principle, yes, such statements can be formalized this way.