Comment by hyperpape

I believe he's correct. The trick is that while ZFC

1. can prove the machine halts for any machine that halts, but

2. cannot necessarily prove that non-halting machines don't halt

This is the distinction between recursively enumerable sets and decidable sets, and it comes up everywhere. The first implies that "for every true p, you'll eventually find a proof" and the second says "for every p, you'll eventually either find a proof of p or a disproof."