It’s an example—but one that doesn’t relate to the problem at hand, which concerns whether a machine returns 1 - or not. If you ASSUME some particular axiom and proof system, the problem becomes easier. However, with no specified axiom system for generating proofs—and no specified proof checker—then the problem becomes poorly-specified.
Regarding Tarski’s theorem—you seem to be misinterpreting me. I am not saying that checking a proof with respect to an axiom system is necessarily difficult. I am saying that truth is not contained by any finite axiom system. So, there will be true statements that are unprovable within the system—but can still be proven in a larger system. That is also what Tarski’s theorem happens to say. Check it out:
“The undefinability theorem does not prevent truth in one theory from being defined in a stronger theory. For example, the set of (codes for) formulas of first-order Peano arithmetic that are true in N is definable by a formula in second order arithmetic. Similarly, the set of true formulas of the standard model of second order arithmetic (or n-th order arithmetic for any n) can be defined by a formula in first-order ZFC.”
Regarding Tarski’s theorem—you seem to be misinterpreting me. I am not saying that checking a proof with respect to an axiom system is necessarily difficult. I am saying that truth is not contained by any finite axiom system. So, there will be true statements that are unprovable within the system—but can still be proven in a larger system. Some of those unprovable truths will be of the form that I mentioned.
If that’s what you mean, then you seem to be even more confused than I realized. If you are just talking about the original context then the set of proofs that are below some fixed length cannot be a statement that is true and unproveable. The proof itself self-verifies. If the statement in question is true, there must exist a proof of the statement that is of the desired bounded size. This follows from consistency and the fact that there are only a finite collection of such proofs.
With a finite limit on proof length, the Godel sentence I mentioned might be longer than the limit—and so not fall within the set of proofs under consideration.
However, the point of mentioning the “Undefinability of Truth Theorem” was to illustrate how there might be truths that would be provably correct—under a more sophisticated set of axioms—but which are not captured by the axiom system being used. That can still be true if the limit on proof length is finite.
Incidentally, your rhetoric about me is getting out of control. Please calm down!
Tim, please reread what I wrote. PA is an example. The relevant point is that Tarski’s theorem doesn’t say what you seem to think it says.
It’s an example—but one that doesn’t relate to the problem at hand, which concerns whether a machine returns 1 - or not. If you ASSUME some particular axiom and proof system, the problem becomes easier. However, with no specified axiom system for generating proofs—and no specified proof checker—then the problem becomes poorly-specified.
Regarding Tarski’s theorem—you seem to be misinterpreting me. I am not saying that checking a proof with respect to an axiom system is necessarily difficult. I am saying that truth is not contained by any finite axiom system. So, there will be true statements that are unprovable within the system—but can still be proven in a larger system. That is also what Tarski’s theorem happens to say. Check it out:
“The undefinability theorem does not prevent truth in one theory from being defined in a stronger theory. For example, the set of (codes for) formulas of first-order Peano arithmetic that are true in N is definable by a formula in second order arithmetic. Similarly, the set of true formulas of the standard model of second order arithmetic (or n-th order arithmetic for any n) can be defined by a formula in first-order ZFC.”
http://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem
If that’s what you mean, then you seem to be even more confused than I realized. If you are just talking about the original context then the set of proofs that are below some fixed length cannot be a statement that is true and unproveable. The proof itself self-verifies. If the statement in question is true, there must exist a proof of the statement that is of the desired bounded size. This follows from consistency and the fact that there are only a finite collection of such proofs.
With a finite limit on proof length, the Godel sentence I mentioned might be longer than the limit—and so not fall within the set of proofs under consideration.
However, the point of mentioning the “Undefinability of Truth Theorem” was to illustrate how there might be truths that would be provably correct—under a more sophisticated set of axioms—but which are not captured by the axiom system being used. That can still be true if the limit on proof length is finite.
Incidentally, your rhetoric about me is getting out of control. Please calm down!