Ah, I think I see it. The set of infinite, non-deterministic execution traces is uncountable (same reason real numbers composed of infinite sequences of digits

Ah, I think I see it. The set of infinite, non-deterministic execution traces is uncountable (same reason real numbers composed of infinite sequences of digits from a finite set are uncountable). On the other hand, the set of infinite execution traces which can result from any deterministic, finite-size program is countable (because the set of programs is). But programs take inputs. And the set of possible inputs to an infinite execution trace is uncountable (same reason as reals, above). The prover needs to show that a program behaves correctly when given any sequence of inputs, even if the program never terminates and keeps taking new inputs forever. That requires proofs over an uncountable set of infinite execution traces.