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