An automated proof-checker can identify some correct proofs—but not all of them.
That’s a consequence of “Tarski’s Undefinability of Truth Theorem”:
No. That’s not what Tarski’s theorem says. Tarski’s theorem is a statement about first-order arithmetic descriptions of truth (it can be generalized slightly beyond that but this is the easiest way of thinking about it). It asserts that there’s no first-order description of what statements are true in a system that lies in the system.
Proof checking is a very different issue. Proof checking is straightforward. Indeed, most of the time we insist that axiomatic systems have proofs checkable as a primitive recursive function. We can do this in Peano Arithmetic for example, and in PA every proof can be verified by a straightforward algorithm.
[Tarski’s theorem] asserts that there’s no first-order description of what statements are true in a system that lies in the system.
You’d need be careful about what “system” or “description” are you talking about, since you can weakly represent, say, the set of statements true in Robinson arithmetic (which is recursively enumerable), in Robinson arithmetic. There is a formula s(-) with one free variable such that
Q |- s(gn(f)) iff Q |- f
where gn(f) is the Gödel number of (arbitrary) statement f and Q is Robinson arithmetic.
Yes, I know that. I was being deliberately imprecise because it is very easy in this case to get lost in the technical details. My intention was not to convey the theorem’s precise statement but rather convey to Tim why it doesn’t apply in the context he’s trying to use it.
I know you know that, but I couldn’t quite naturally interpret your informal statement as saying the formally correct thing, so had to make the clarification.
Here we are not talking about Peano Arithmetic. We are talking about whether a computer program returns 1 - or not. If you want to talk about how easy it is to verify proofs based on the axioms of Peano Arithmetic, I think you first need to explain why you think that is relevant to the problem—which says it is talking about “all possible proofs” and doesn’t refer to a specified axiom set.
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!
No. That’s not what Tarski’s theorem says. Tarski’s theorem is a statement about first-order arithmetic descriptions of truth (it can be generalized slightly beyond that but this is the easiest way of thinking about it). It asserts that there’s no first-order description of what statements are true in a system that lies in the system.
Proof checking is a very different issue. Proof checking is straightforward. Indeed, most of the time we insist that axiomatic systems have proofs checkable as a primitive recursive function. We can do this in Peano Arithmetic for example, and in PA every proof can be verified by a straightforward algorithm.
You’d need be careful about what “system” or “description” are you talking about, since you can weakly represent, say, the set of statements true in Robinson arithmetic (which is recursively enumerable), in Robinson arithmetic. There is a formula s(-) with one free variable such that
Q |- s(gn(f)) iff Q |- f
where gn(f) is the Gödel number of (arbitrary) statement f and Q is Robinson arithmetic.
Yes, I know that. I was being deliberately imprecise because it is very easy in this case to get lost in the technical details. My intention was not to convey the theorem’s precise statement but rather convey to Tim why it doesn’t apply in the context he’s trying to use it.
I know you know that, but I couldn’t quite naturally interpret your informal statement as saying the formally correct thing, so had to make the clarification.
Here we are not talking about Peano Arithmetic. We are talking about whether a computer program returns 1 - or not. If you want to talk about how easy it is to verify proofs based on the axioms of Peano Arithmetic, I think you first need to explain why you think that is relevant to the problem—which says it is talking about “all possible proofs” and doesn’t refer to a specified axiom set.
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!