Technically you can’t. You can prove it’s undecidable as long as your axiom system is consistent. However, it’s impossible for a consistent axiom system to prove its own consistency.
The problem is that no consistent system can prove it’s own consistency. (Of course, an inconsistent system can prove all statements, including both its own consistency and inconsistency.)
Consider a system S. You can add the axiom “S is consistent”, but now you have a new system that still doesn’t know that it’s consistent.
On the other hand, one can add the axiom “S is consistent even with this axiom added”. Your new system is now inconsistent for more or less the reason you used in formulating the above paradox.
I’m not sure that my paradox even requires the proof system to prove it’s own consistency.
But regardless, even if removing that does resolve the paradox, it’s not a very satisfying resolution. Of course a crippled logic can’t prove interesting things about Turing machines.
I’m not sure that my paradox even requires the proof system to prove it’s own consistency.
Your argument requires the proof system to prove it’s own consistency. As we discussed before, your argument relies on the assumption that the implication
If "φ is provable" then "φ"
Provable(#φ) → φ
is available for all φ. If this were the case, your theory would prove itself consistent. Why? Because you could take the contrapositive
If "φ is false" then "φ is not provable"
¬φ → ¬Provable(#φ)
and substitute “0=1” for φ. This gives you
if "0≠1" then "0=1 is not provable"
¬0=1 → ¬Provable(#(0=1))
The premise “0≠1” holds. Therefore, the consequence “0=1 is not provable” also holds. At this point your theory is asserting its own consistency: everything is provable in an inconsistent theory.
0 is not equal to 1, so it’s not inconsistent. I don’t understand what you are trying to say with that.
It would be really silly for a system not to believe it was consistent. And, if it were true, it would also apply to the mathematicians making such statements. The mathematicians are assuming it’s true, and it is obviously true, so I don’t see why a proof system should not have it.
In any case I don’t see how my system requires proving “x is provable implies x”. It searches through proofs in a totally unspecified proof system. It then proves the standard halting problem on a copy of itself, and shows that it will never halt. It then returns false, causing a paradox.
Are saying that it’s impossible to prove the halting problem?
everything is provable in an inconsistent theory
So if something is not provable in a theory, that proves it is consistent?
I did read your link but I don’t understand most of it.
TezlaKoil doesn’t include his whole argument here. Basically he is using Gödel’s second incompleteness theorem. The theorem proves that a theory sufficiently complex to express arithmetic cannot have a proof of the statement corresponding to “this theory is consistent” without being an inconsistent theory.
This doesn’t show that arithmetic has a proof of “this theory is inconsistent” either. If it does, then arithmetic is in fact inconsistent. Since we think arithmetic is consistent, we think that the arithmetical formula corresponding to “arithmetic is consistent” is true but undecidable from within arithmetic.
It also doesn’t imply that the theory composed of arithmetic plus “arithmetic is consistent” is inconsistent, because this theory is more complicated than arithmetic and does not assert its own consistency.
Of course we think the more complicated theory is true and consistent as well, but adding that would just lead to yet another theory, and so on.
If you try to use mathematical induction to form a theory that includes all such statements, that theory will have an infinite number of postulates and will not be able to be analyzed by a Turing machine.
If you try to use mathematical induction to form a theory that includes all such statements, that theory will have an infinite number of postulates and will not be able to be analyzed by a Turing machine.
This part is not quite accurate. Actually, the commonly used theories of arithmetic (and sets) have infinitely many axioms. The actually problem with your approach above is that the theory still won’t be able to prove its own consistency since any proof can only use finitely many of the axioms. One can of course add an additional axiom and keep going using transfinite induction, but now one will finally run into a theory that a Turing machine can’t analyze.
I would agree that it’s not very satisfying, in the sense that there is no satisfying resolution to the paradox of the liar.
But logic is actually crippled in reality in that particular way. You cannot assume either that “this is false” is true, or that it is false, without arriving at a contradiction.
I’m not sure that my paradox even requires the proof system to prove it’s own consistency.
If the system is inconsistent, your program will halt on all inputs with output dependent on whether it happens to find a proof of “this program halts” or “this program doesn’t halt” first.
Of course a crippled logic can’t prove interesting things about Turing machines.
Well, mathematicians have been proving interesting things about Turing machines for the past century despite these limitations.
If I can prove that the problem is undecidable, so can
H.Hsearches through all possible proofs, which must contain that proof too.If a problem is undecidable, that means no proof exists either way. Otherwise it would be decidable, in principle.
If no proof exists either way, and
Hsearches through all possible proofs, then it will not halt. It will keep searching forever.Therefore, if you can prove that it is undecidable, then you can prove that
Hwill not halt. AndHcan prove this too.So
Hhas proved that it will not halt, and returnsfalse. This causes a paradox.Technically you can’t. You can prove it’s undecidable as long as your axiom system is consistent. However, it’s impossible for a consistent axiom system to prove its own consistency.
Perhaps. If so just make it an axiom. It’s silly to use a system that doesn’t believe it’s consistent.
The problem is that no consistent system can prove it’s own consistency. (Of course, an inconsistent system can prove all statements, including both its own consistency and inconsistency.)
Consider a system S. You can add the axiom “S is consistent”, but now you have a new system that still doesn’t know that it’s consistent.
On the other hand, one can add the axiom “S is consistent even with this axiom added”. Your new system is now inconsistent for more or less the reason you used in formulating the above paradox.
I’m not sure that my paradox even requires the proof system to prove it’s own consistency.
But regardless, even if removing that does resolve the paradox, it’s not a very satisfying resolution. Of course a crippled logic can’t prove interesting things about Turing machines.
Your argument requires the proof system to prove it’s own consistency. As we discussed before, your argument relies on the assumption that the implication
is available for all φ. If this were the case, your theory would prove itself consistent. Why? Because you could take the contrapositive
and substitute “0=1” for φ. This gives you
The premise “0≠1” holds. Therefore, the consequence “0=1 is not provable” also holds. At this point your theory is asserting its own consistency: everything is provable in an inconsistent theory.
You might enjoy reading about the Turing Machine proof of Gödel’s first incompleteness theorem, which is closely related to your paradox.
0 is not equal to 1, so it’s not inconsistent. I don’t understand what you are trying to say with that.
It would be really silly for a system not to believe it was consistent. And, if it were true, it would also apply to the mathematicians making such statements. The mathematicians are assuming it’s true, and it is obviously true, so I don’t see why a proof system should not have it.
In any case I don’t see how my system requires proving “x is provable implies x”. It searches through proofs in a totally unspecified proof system. It then proves the standard halting problem on a copy of itself, and shows that it will never halt. It then returns false, causing a paradox.
Are saying that it’s impossible to prove the halting problem?
So if something is not provable in a theory, that proves it is consistent?
I did read your link but I don’t understand most of it.
TezlaKoil doesn’t include his whole argument here. Basically he is using Gödel’s second incompleteness theorem. The theorem proves that a theory sufficiently complex to express arithmetic cannot have a proof of the statement corresponding to “this theory is consistent” without being an inconsistent theory.
This doesn’t show that arithmetic has a proof of “this theory is inconsistent” either. If it does, then arithmetic is in fact inconsistent. Since we think arithmetic is consistent, we think that the arithmetical formula corresponding to “arithmetic is consistent” is true but undecidable from within arithmetic.
It also doesn’t imply that the theory composed of arithmetic plus “arithmetic is consistent” is inconsistent, because this theory is more complicated than arithmetic and does not assert its own consistency.
Of course we think the more complicated theory is true and consistent as well, but adding that would just lead to yet another theory, and so on.
If you try to use mathematical induction to form a theory that includes all such statements, that theory will have an infinite number of postulates and will not be able to be analyzed by a Turing machine.
This part is not quite accurate. Actually, the commonly used theories of arithmetic (and sets) have infinitely many axioms. The actually problem with your approach above is that the theory still won’t be able to prove its own consistency since any proof can only use finitely many of the axioms. One can of course add an additional axiom and keep going using transfinite induction, but now one will finally run into a theory that a Turing machine can’t analyze.
I would agree that it’s not very satisfying, in the sense that there is no satisfying resolution to the paradox of the liar.
But logic is actually crippled in reality in that particular way. You cannot assume either that “this is false” is true, or that it is false, without arriving at a contradiction.
If the system is inconsistent, your program will halt on all inputs with output dependent on whether it happens to find a proof of “this program halts” or “this program doesn’t halt” first.
Well, mathematicians have been proving interesting things about Turing machines for the past century despite these limitations.