3 ms·
Checking whether a string of bits encodes a proof of False in ZF is decidable. Now enumerate the bitstrings and check each.
by meithecatte 3y ago
Checking whether a string of bits encodes a proof of False in ZF is decidable. Now enumerate the bitstrings and check each.
- klyrs 3y ago> 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 3y agoIf 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 3y agoThere 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 3y ago> 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]