Now here is the weird and confusing part. If the above is a valid proof, then H will eventually find it. It searches all proofs, remember?
Fortunately, H will never find your argument because it is not a correct proof. You rely on hidden assumptions of the following form (given informally and symbolically):
If φ is provable, then φ holds.
Provable(#φ) → φ
where #φ denotes the Gödel number of the proposition φ.
Statements of these form are generally not provable. This phenomenon is known as Löb’s theorem—featured in Main back in 2008.
You use these invalid assumptions to eliminate the first two options from Either H returns true, or false, or loops forever. For example, if H returns true, then you can infer that “FF halts on input FF” is provable, but that does not contradict FF does not halt on input FF.
It is not that these statements are “not generally valid”, but that they are not included within the axiom system used by H. If we attempt to include them, there will be a new statement of the same kind which is not included.
Obviously such statements will be true if H’s axiom system is true, and in that sense they are always valid.
It is not that these statements are “not generally valid”
The intended meaning of valid in my post is “valid step in a proof” in the given formal system. I reworded the offending section.
Obviously such statements will be true if H’s axiom system is true, and in that sense they are always valid.
Yes, and one also has to be careful with the use of the word “true”. There are models in which the axioms are true, but which contain counterexamples to Provable(#φ) → φ.
Fortunately, H will never find your argument because it is not a correct proof. You rely on hidden assumptions of the following form (given informally and symbolically):
where #φ denotes the Gödel number of the proposition φ.
Statements of these form are generally not provable. This phenomenon is known as Löb’s theorem—featured in Main back in 2008.
You use these invalid assumptions to eliminate the first two options from Either H returns true, or false, or loops forever. For example, if H returns true, then you can infer that “FF halts on input FF” is provable, but that does not contradict FF does not halt on input FF.
I’m very confused. Of course if φ is provable then it’s true. That’s the whole point of using proofs.
But that statement isn’t provable.
Then just assume it as an axiom.
Then the paradox you were describing fires and the system becomes inconsistent.
Yes, but it may be true without being provable.
It is not that these statements are “not generally valid”, but that they are not included within the axiom system used by H. If we attempt to include them, there will be a new statement of the same kind which is not included.
Obviously such statements will be true if H’s axiom system is true, and in that sense they are always valid.
The intended meaning of valid in my post is “valid step in a proof” in the given formal system. I reworded the offending section.
Yes, and one also has to be careful with the use of the word “true”. There are models in which the axioms are true, but which contain counterexamples to
Provable(#φ) → φ.