Comment by gpm
8 months ago
Is there reason to believe that there's not a similarly sized turing machine that halts iff Con(ZFC + Con(ZFC)) (which is independent of ZFC+Con(ZFC) by godel's)?
Certainly there's some sized machine that does that... it seems to me that all you're doing is playing games with adding axioms to maybe change the exact value of "748"... and I don't even see that you've established that you've successfully changed it.
Well, yes, my previous comment was sloppy. Of course it's also possible that 748 is such a high upper limit that we can add a lot of axioms to ZFC and BB(748) is still independent to it. We just don't know it.