5 ms·

> consider again a Turing machine M that halts if and only if there’s a contradiction in ZF set theory. Clearly such a machine could be built, with some finite

> consider again a Turing machine M that halts if and only if there’s a contradiction in ZF set theory. Clearly such a machine could be built, with some finite number of states k. I am a small brain here. How is this so clear?

_a_a_a_ 3y ago
Because it says 'clearly'. (but yeah, agree with you)
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 ago
    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 3y ago
  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 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]
tomstuart 3y ago
I wouldn’t defend the idea that it’s “clear”, but the idea is to build a machine that combines the axioms of ZF set theory in all possible ways to generate all possible conclusions, checking each one for contradiction as it goes. If it never generates a contradictory conclusion from those axioms, it’ll run forever.
- ijustlovemath 3y ago
  This sounds like it relies on the halting problem, or maybe the other way around? Really interesting stuff, been a while since I read about a higher level math topic and been able to sorta kinda understand the "quanta-level" summaries out there
  - jtolmar 3y ago
    The Nth Busy Beaver number lets you solve the halting problem for Turing Machines up to size N. Only a handful of them are known, for very small N, and they increase incredibly rapidly. For the most common version of the problem (S for 2-symbol machines), they go: 1, 6, 21, 107, some number greater than or equal to 47176870, and some number greater than 10⇈15 (that's up arrow notation on the last one).
    - ijustlovemath 3y ago
      Ooh, are they basically the number of possible turing programs encodable in a state of N?
      - readams 3y ago
        It's the maximum amount of time a Turing machine of size N can run. So if you want to know whether a Turning machine of size N or less will halt, just run it for BB(N) steps. If it hasn't halted by then, it never will.
- stouset 3y ago
  I think the part that eludes me here is that it's not clear that such a Turing machine could be built from a finite number of states.

_a_a_a_ 3y ago

Because it says 'clearly'. (but yeah, agree with you)

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 ago
  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 3y ago
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 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]

tomstuart 3y ago

I wouldn’t defend the idea that it’s “clear”, but the idea is to build a machine that combines the axioms of ZF set theory in all possible ways to generate all possible conclusions, checking each one for contradiction as it goes. If it never generates a contradictory conclusion from those axioms, it’ll run forever.

ijustlovemath 3y ago
This sounds like it relies on the halting problem, or maybe the other way around? Really interesting stuff, been a while since I read about a higher level math topic and been able to sorta kinda understand the "quanta-level" summaries out there
- jtolmar 3y ago
  The Nth Busy Beaver number lets you solve the halting problem for Turing Machines up to size N. Only a handful of them are known, for very small N, and they increase incredibly rapidly. For the most common version of the problem (S for 2-symbol machines), they go: 1, 6, 21, 107, some number greater than or equal to 47176870, and some number greater than 10⇈15 (that's up arrow notation on the last one).
  - ijustlovemath 3y ago
    Ooh, are they basically the number of possible turing programs encodable in a state of N?
    - readams 3y ago
      It's the maximum amount of time a Turing machine of size N can run. So if you want to know whether a Turning machine of size N or less will halt, just run it for BB(N) steps. If it hasn't halted by then, it never will.
stouset 3y ago
I think the part that eludes me here is that it's not clear that such a Turing machine could be built from a finite number of states.