You can make a Godel sentence for any supplied finite proof checker that essentially says: “This proof checker can never prove this statement to be true”. Sure enough, the proof checker won’t approve any proofs that the statement is correct—but the statement is true—and that can be proven.
Checking a proof in a recursively axiomatizable theory for correctness is decidable. The post topic programs only check proofs up to some length in, say, Peano arithmetic, which is recursively axiomatizable. Tarski’s undefinability theorem is about complete theories of arithmetic.
There is no such thing as a “complete theory of arithmetic”—see Godel’s incompleteness theorems.
The above statement isn’t true. What Godel’s theorem says is that any effectively generatable theory which is strong enough to model PA is either incomplete or inconsistent. Effectively generatable for our purposes can be taken to mean that valid proofs in the system are enumerable and that there’s a primitive recursive procedure to determine whether a given proof is valid.
If one removes the effectively generatable condition then one can easily produce a complete, consistent system. Consider for example the following system: Consider some lexicographic ordering of well-formed statements in the language of PA, and let S(i) be the ith statement in this list. Let P(0) be PA, and generate P(n) by asking whether S(n) or ~S(n) is a theorem in P(n-1). If so, then set P(n) = P(n-1). If not, then let P(n) be P(n-1) with the additional axiom of S(n). Now, consider P(infinity) defined as the union of all P(n). This theory is complete and consistent but it is very much not effectively generatable since we can’t even recursively enumerate the system’s axioms.
It might help for you to take a model theory or logic course since there are a lot of subtle issues here that you seem to be missing.
I suppose there are complete inconsistent theories of arithmetic. However, here the discussion concerns whether a machine returns 1 - or not. Systems of math that are useless, or have infinitely many axioms and so can’t be implemented don’t really enter into the picture.
Tim, you’re making false statements. You’ve now misapplied both Godel’s theorem and Tarski’s theorem.You also seem to be under the impression that proof checking is not generally doable in an axiomatic system, which is also wrong. Let me suggest that you simply don’t have the background expertise to discuss these issues. These are subtle issues. Indeed, even your above reply runs into new issues (For example having infinitely many axioms doesn’t prevent a system of axioms from being effectively generatable. Indeed many well behaved axiomatic systems have axiom schema which do just this.) You may be running into a Dunning-Kruger type problem. I’m a professional mathematician (ok, a grad student but close enough for this purpose), and I find these issues difficult. Vladimir, I and others have pointed out what is wrong with your reasoning but you don’t seem to be following the explanations. Please take a logic course or read a textbook.
Not every possible set. All you need is a primitive recursive procedure to decide whether a given statement is an axiom, and primitive recursive procedures to check whether each rule of inference is correctly followed in going from one step to another.
Right: automated proof checking is not really “generally doable” in an axiomatic system—how hard it is depends entirely on the axiomatic system under discussion.
It is possible that I wasn’t clear enough (my phrasing could certainly use work). I was thinking of statements such as your remark that “An automated proof-checker can identify some correct proofs—but not all of them” whereas we generally don’t call something an automated proof checker unless it terminates on any proof and returns correctly if that’s a valid proof or not in the axiomatic system. Sometimes we insist that this be a primitively recursive process. Sometimes this is also generalizable in a natural way such that the proofchecker can do this given some specific oracle (there are results about how these sorts of things can behave if they have access to a Halting oracle for example. I don’t fully understand these except in vague generality.)
FWIW, I was thinking of unprovable truths, (wrt some chosen axioms) that are provable with stronger axioms. There, a proof checker based on a finite axiom set would return “false”, for true and provable statements.
Many statements aren’t simply “true”; if a statement isn’t logically valid, it’s only true in a specific theory, or about a specific structure. A given satisfiable non-valid statement is true about one structure, and false about another, true in one theory, false in another theory, independent in the third one.
That’s irrelevant to a proof-checker. Proof-checkers reside in a specific axiomatic system. It doesn’t matter if there’s an axiomatic system that would give stronger results for the purpose that was under discussion, it just matters if there’s one of a given length in whatever formalism we want.
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!
The proof checker checks proofs within some formal theory. The Godel sentence for the checker is certainly true and provable by us, given the consistency of that formal theory. (If the theory were inconsistent, the checker would be able to prove any sentence.) But this doesn’t work as a proof within the theory! The theory cannot believe its own consistency (Godel’s second incompleteness theorem), so the checker cannot assume it when checking proofs. So your argument doesn’t actually give an example of a valid proof rejected by the checker.
Worse, it’s only “true” that a consistent theory is consistent in some unclear sense, because you can extend the theory with a statement that asserts inconsistency of the original theory, and the resulting theory will remain consistent.
What you’re saying is certainly true (onlookers, see pages 5-6 of this pdf for as especially clear explanation), but I like to think that you can’t actually exhibit a proof string that shows the inconsistency of PA. If you could, we’d all be screwed!
I like to think that you can’t actually exhibit a proof string that shows the inconsistency of PA.
Proof in what theory, “can’t” by what definition of truth? In the extension of PA with inconsistency-of-PA axiom, it’s both provable and true that PA is inconsistent.
A proof in PA that 1+1=3 would suffice. Or, if you will, the Goedel number of this proof: an integer that satisfies some equations expressible in ordinary arithmetic. I agree that there’s something Platonic about the belief that a system of equations either has or doesn’t have an integer solution, but I’m not willing to give up that small degree of Platonism, I guess.
You would demand that particular proof, but why? PA+~Con(PA) doesn’t need such eccentricities. You already believe Con(PA), so you can’t start from ~Con(PA) as an axiom. Something in your mind makes that choice.
I promised to explain why the Incompleteness Theorem doesn’t contradict the Completeness Theorem. The easiest way to do this is probably through an example. Consider the “self-hating theory” PA+Not(Con(PA)), or Peano Arithmetic plus the assertion of its own inconsistency. We know that if PA is consistent, then this strange theory must be consistent as well—since otherwise PA would prove its own consistency, which the Incompleteness Theorem doesn’t allow. It follows, by the Completeness Theorem, that PA+Not(Con(PA)) must have a model. But what could such a model possibly look like? In particular, what you happen if, within that model, you just asked to see the proof that PA was inconsistent?
I’ll tell you what would happen: the axioms would tell you that proof of PA’s inconsistency is encoded by a positive integer X. And then you would say, “but what is X?” And the axioms would say, “X.” And you would say, “But what is X, as an ordinary positive integer?”
“No, no, no! Talk to the axioms.”
“Alright, is X greater or less than 10500,000?”
“Greater.” (The axioms aren’t stupid: they know that if they said “smaller”, then you could simply try every smaller number and verify that none of them encode a proof of PA’s inconsistency.)
“Alright then, what’s X+1?”
“Y.”
And so on. The axioms will keep cooking up fictitious numbers to satisfy your requests, and assuming that PA itself is consistent, you’ll never be able to trap them in an inconsistency. The point of the Completeness Theorem is that the whole infinite set of fictitious numbers the axioms cook up will constitute a model for PA—just not the usual model (i.e., the ordinary positive integers)! If we insist on talking about the usual model, then we switch from the domain of the Completeness Theorem to the domain of the Incompleteness Theorem.
Let’s say we are trying to prove statements within ZFC.
“ZFC can never prove this statement to be true”
...is one thing and...
“This proof checker can never prove this statement to be true”
...is another.
Neither can be proved by the specified proof checker—but the second statement can be proved by another, better proof checker—still working within ZFC—so it can be seen that it is true.
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”:
http://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem
You can make a Godel sentence for any supplied finite proof checker that essentially says: “This proof checker can never prove this statement to be true”. Sure enough, the proof checker won’t approve any proofs that the statement is correct—but the statement is true—and that can be proven.
Checking a proof in a recursively axiomatizable theory for correctness is decidable. The post topic programs only check proofs up to some length in, say, Peano arithmetic, which is recursively axiomatizable. Tarski’s undefinability theorem is about complete theories of arithmetic.
There is no such thing as a “complete theory of arithmetic”—see Godel’s incompleteness theorems.
The post says it is about “programs”—a fairly general class. Where is Peano arithmetic coming into the issue?
Please give up.
The above statement isn’t true. What Godel’s theorem says is that any effectively generatable theory which is strong enough to model PA is either incomplete or inconsistent. Effectively generatable for our purposes can be taken to mean that valid proofs in the system are enumerable and that there’s a primitive recursive procedure to determine whether a given proof is valid.
If one removes the effectively generatable condition then one can easily produce a complete, consistent system. Consider for example the following system: Consider some lexicographic ordering of well-formed statements in the language of PA, and let S(i) be the ith statement in this list. Let P(0) be PA, and generate P(n) by asking whether S(n) or ~S(n) is a theorem in P(n-1). If so, then set P(n) = P(n-1). If not, then let P(n) be P(n-1) with the additional axiom of S(n). Now, consider P(infinity) defined as the union of all P(n). This theory is complete and consistent but it is very much not effectively generatable since we can’t even recursively enumerate the system’s axioms.
It might help for you to take a model theory or logic course since there are a lot of subtle issues here that you seem to be missing.
I suppose there are complete inconsistent theories of arithmetic. However, here the discussion concerns whether a machine returns 1 - or not. Systems of math that are useless, or have infinitely many axioms and so can’t be implemented don’t really enter into the picture.
Tim, you’re making false statements. You’ve now misapplied both Godel’s theorem and Tarski’s theorem.You also seem to be under the impression that proof checking is not generally doable in an axiomatic system, which is also wrong. Let me suggest that you simply don’t have the background expertise to discuss these issues. These are subtle issues. Indeed, even your above reply runs into new issues (For example having infinitely many axioms doesn’t prevent a system of axioms from being effectively generatable. Indeed many well behaved axiomatic systems have axiom schema which do just this.) You may be running into a Dunning-Kruger type problem. I’m a professional mathematician (ok, a grad student but close enough for this purpose), and I find these issues difficult. Vladimir, I and others have pointed out what is wrong with your reasoning but you don’t seem to be following the explanations. Please take a logic course or read a textbook.
Seconded.
Re: “You also seem to be under the impression that proof checking is not generally doable in an axiomatic system, which is also wrong.”
You are claiming that every possible set of axioms allows for easy automation of proof checking?!?
If so, then we do have a genuine disagreement—and I think you are mistaken.
Not every possible set. All you need is a primitive recursive procedure to decide whether a given statement is an axiom, and primitive recursive procedures to check whether each rule of inference is correctly followed in going from one step to another.
Right: automated proof checking is not really “generally doable” in an axiomatic system—how hard it is depends entirely on the axiomatic system under discussion.
It is possible that I wasn’t clear enough (my phrasing could certainly use work). I was thinking of statements such as your remark that “An automated proof-checker can identify some correct proofs—but not all of them” whereas we generally don’t call something an automated proof checker unless it terminates on any proof and returns correctly if that’s a valid proof or not in the axiomatic system. Sometimes we insist that this be a primitively recursive process. Sometimes this is also generalizable in a natural way such that the proofchecker can do this given some specific oracle (there are results about how these sorts of things can behave if they have access to a Halting oracle for example. I don’t fully understand these except in vague generality.)
FWIW, I was thinking of unprovable truths, (wrt some chosen axioms) that are provable with stronger axioms. There, a proof checker based on a finite axiom set would return “false”, for true and provable statements.
Many statements aren’t simply “true”; if a statement isn’t logically valid, it’s only true in a specific theory, or about a specific structure. A given satisfiable non-valid statement is true about one structure, and false about another, true in one theory, false in another theory, independent in the third one.
Sure. In this problem, we at least have a specified problem domain—whether a machine will return “1” or “0″.
That’s irrelevant to a proof-checker. Proof-checkers reside in a specific axiomatic system. It doesn’t matter if there’s an axiomatic system that would give stronger results for the purpose that was under discussion, it just matters if there’s one of a given length in whatever formalism we want.
You keep talking with confidence about something you clearly don’t understand at all.
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!
The proof checker checks proofs within some formal theory. The Godel sentence for the checker is certainly true and provable by us, given the consistency of that formal theory. (If the theory were inconsistent, the checker would be able to prove any sentence.) But this doesn’t work as a proof within the theory! The theory cannot believe its own consistency (Godel’s second incompleteness theorem), so the checker cannot assume it when checking proofs. So your argument doesn’t actually give an example of a valid proof rejected by the checker.
I think you mean that there would be some proof (that checks) for any sentence.
Yes. Thanks.
Worse, it’s only “true” that a consistent theory is consistent in some unclear sense, because you can extend the theory with a statement that asserts inconsistency of the original theory, and the resulting theory will remain consistent.
What you’re saying is certainly true (onlookers, see pages 5-6 of this pdf for as especially clear explanation), but I like to think that you can’t actually exhibit a proof string that shows the inconsistency of PA. If you could, we’d all be screwed!
Proof in what theory, “can’t” by what definition of truth? In the extension of PA with inconsistency-of-PA axiom, it’s both provable and true that PA is inconsistent.
A proof in PA that 1+1=3 would suffice. Or, if you will, the Goedel number of this proof: an integer that satisfies some equations expressible in ordinary arithmetic. I agree that there’s something Platonic about the belief that a system of equations either has or doesn’t have an integer solution, but I’m not willing to give up that small degree of Platonism, I guess.
You would demand that particular proof, but why? PA+~Con(PA) doesn’t need such eccentricities. You already believe Con(PA), so you can’t start from ~Con(PA) as an axiom. Something in your mind makes that choice.
For those curious what Nesov is talking about:
-- Scott Aaronson
Let’s say we are trying to prove statements within ZFC.
“ZFC can never prove this statement to be true”
...is one thing and...
“This proof checker can never prove this statement to be true”
...is another.
Neither can be proved by the specified proof checker—but the second statement can be proved by another, better proof checker—still working within ZFC—so it can be seen that it is true.
“proved by a proof checker”—huh?
“Asserted”, “approved”—whatever.