[meithecatte]

Checking whether a string of bits encodes a proof of False in ZF is decidable. Now enumerate the bitstrings and check each.

[klyrs]

> and check each.

"Now, draw the rest of the owl." Not saying you're wrong, just, this jump is super non-obvious even to most mathematicians.

[CaptainNegative]

If you can check any given bitstring for whether it encodes a valid ZFC proof of the (in)consistency of ZFC in finite time, then you can write a program to enumerate over all possible bit strings in shortlex order and halt the first time you see a valid proof.

[WindyLakeReturn]

There are infinite many such strings, so that alone can't be used to prove the Turing machine of k states can check all strings. So that leaves open the original question, how do we know that a Turing machine of k states is able to have one of the stated outcomes for any possible bit string?

[nyssos]

> There are infinite many such strings

And they can be enumerated by a finite program. For example, in lazily evaluated pseudocode:

    bits = ["0", "1"]
    bitstrings = bits + [(bit + suffix for bit in bits) for suffix in bitstrings]