Comment by jbapple
11 years ago
> But if the machine that stops when it has proven ZFC is inconsistent does not halt, then surely it means there is no proof of the inconsistency of ZFC?
I'm not sure what this question means. Are you referencing an earlier discussion of a machine that demonstrated a proof of "0=1" using the axioms of ZFC? If so, what is your concern?
When thinking about undecidability/independence from a computational perspective, it's helpful to be cautious about the phrase "does not halt". How would you know a machine "does not halt"? You might run it for a long time and observe that it has not halted yet, but that's not the same.
Instead, you can talk about "a proof in $AXIOM_SYSTEM that this machine does not halt".
So, using that terminology, consider a machine that enumerates all valid proofs of ZFC and checks if their conclusion is "0 = 1". Certainly, if ZFC is inconsistent, this machine will find a proof and halt. However, if there is no such proof, then ZFC is consistent, the machine will not halt, but there will be no proof in ZFC that the machine will not halt.
This ability to enumerate the proofs is related to semidecidability/recursive-enumerability.
When you say "for sufficiently large n, we won't be able to prove that BB(n) = N", I agree. There is some n that is so large that there is a Turing machine of size n that does loop, but the fact that it loops will not be provable in ZFC.
Well you said "if ZFC, a rather strong axiom system, cannot prove a machine halts, it does not halt.". This particular statement is what I was replying to. I agree that a non-halting Turing machine is not a very well defined concept in the general sense (hence my reply), but I would think the onus is on the one who used it first to define what they meant by it :-)
> I would think the onus is on the one who used it first to define what they meant by it :-)
That's a very fair criticism.
My writing is muddy, for sure. Let me try again. You ask:
> But if the machine that stops when it has proven ZFC is inconsistent does not halt, then surely it means there is no proof of the inconsistency of ZFC? Hence ZFC is consistent? Which is contradicted by Godel.
I do not think this is contradicted by Goedel. Goedel's theorem implies that ZFC can't prove its own consistency unless it is inconsistent. So, how can this machine that searches for an inconsistency in ZFC (by enumerating all possible valid ZFC proofs so that for any proof p, there is some time t such that the machine checks p by time t) run forever, thereby proving ZFC consistent?
It is by the unprovability in ZFC (unless ZFC is inconsistent) of the fact that this machine will run forever.
The fact that this machine will run forever implies the consistency of ZFC, and the consistency of ZFC implies the machine will run forever.
After looking more closely at your linked post by Terence Tao, are you by chance basing your statements such as "it does not halt" in what he calls the informal platonic reasoning system (which presumably assumes ZFC as well as its consistency)?
If so, I think I understand what you mean and I agree with you.
My thoughts were a bit confused on these topics so my posts probably contain some reasoning errors, but in the end I think what matters is we agree on the answer to OP's question, i.e.
For any given theory T at least as strong as ZFC (and maybe even some weaker ones) then
- BB as function is well defined in T - However there is some number n_T after which T can't prove any upper bound for BB(n) for any n > n_T
I think this is a very interesting result because the fact that any axiomatic system will be powerless to describe this function's growth after only a small number of steps expresses pretty well how mind numbingly fast it grows.
I believe he's correct. The trick is that while ZFC
1. can prove the machine halts for any machine that halts, but
2. cannot necessarily prove that non-halting machines don't halt
This is the distinction between recursively enumerable sets and decidable sets, and it comes up everywhere. The first implies that "for every true p, you'll eventually find a proof" and the second says "for every p, you'll eventually either find a proof of p or a disproof."