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.
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.