§ Proof that there is a TM whose halting is independent of ZFC

• Start by assuming that ZFC is consistent.
• Consider a TM which enumerates proofs in ZFC (ie, sequents if we want to use sequent calculus), looking for a sequent that proves the inoncsistency of ZFC.
• If this TM halts, then it has proven inconsistency of ZFC, which contradicts our hypothesis.
• If it does not halt, then this means that we have proven the consistency of ZFC in ZFC, which contradicts Godel's incompleteness theorem.
• Thus, it is independent of ZFC whether TM M halts or not.