§ 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.