|
|
|
|
|
|
by mananaysiempre
705 days ago
|
|
|
If you’re using ZFC, there is (TFA mentions the state of the art is BB(745); Yedida and Aaronson’s original work on BB(8000)[1] is quite fun to read from a programmer’s point of view). But the second form still exists (if you accept excluded middle)—you just can’t prove which one it is! Specifically, ZFC is consistent iff ZFC+“Y&A’s machine does halt” is consistent iff ZFC+“Y&A’s machine never halts” is consistent (a theorem in a fairly weak ambient metalogic). So you can take a stronger set theory that does prove the answer, it’s just that thus far we have no reason to prefer theories that answer yes to theories that answer no. (You don’t have to accept excluded middle, and it can on occasion be useful not to[2], but pragmatically you’re going to have a lot of difficulties even with first-year calculus unless you do.) [1] https://scottaaronson.blog/?p=2725 [2] https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016... |
|
|