Kevin Brown saysSupposing we grant this "theorem." So what? This is only an issue if you somehow think that the lack of a complete proof engenders uncertainty. Why should it? Simply because the lack of a complete proof means that "it might be wrong"? But even if there *were* a "complete proof" it still "might be wrong." For your concept of a complete proof implies that ordinary proof is, by itself, insufficient to ensure certainty, and once you have raised this question mark, we can also raise the question mark over the notion of "complete proof." Namely, I can argue that a complete proof of consistency is "non-metacomplete" if it's carried out within a system whose consistency has not been metacompletely proven.
"Let us say a proof of the consistency of system X is "incomplete" if it's carried out within a system Y whose consistency has not been completely proven. Theorem: Every proof of the consistency of arithmetic is incomplete."
And in any case, on at least one reading of your "theorem," it isn't true. The consistency of ZFC is provable in ZFC + Con(ZFC), the consistency of ZFC + Con(ZFC) is provable in ZFC + Con(ZFC) + Con(ZFC+Con(ZFC)), etc., so the infinite hierarchy of such systems provides a complete proof of the consistency of ZFC. Or, just to press the point, there is actually a system which proves the consistency of *any* system: take any inconsistent system. This system even proves its *own* consistency. What more could you ask for?
The point is that you can raise doubts about *anything*; the appeal to the lack of an "absolute proof" (whatever that means) is essentially irrelevant, because even if there were an "absolute proof" you could still doubt it. On the other hand, asking for an ordinary proof is not unreasonable, not so much because ordinary proof confers absolute certainty, but because ordinary proof is what mathematicians are interested in. And there does exist an ordinary proof of the consistency of PA.
Kevin Brown saysAsk those logicians, or anybody else, whether they can prove that first-order logic is perfect. If you want to be a philosophical pedantic about it, it turns out that even this is impossible. But nobody argues that they think that first-order logic is fundamentally messed up. (If you are an intuitionist, then please stay quiet. :-)
"Ask those logicians if they can prove the consistency of those more general types of logic. (They can't.)"
Now if you think about it for a bit, there is no reasonable doubt that arithmetic is just fine. And if that does not satisfy you, then remember that the validity of ANY sort of reasoning, (including first order logic) depends on similar considerations. Nothing more, and nothing less.
Think about it. Do you really believe that there is a contradiction in the positive integers?
I suggested this to an email correspondent and he expressed utter incredulity, saying "You can't possibly believe that simple arithmetic could contain an inconsistency! How would you balance your check book?"
This is an interesting question. I actually balance my checkbook using a formal system called Quicken. Do I have a formal proof of the absolute consistency and correctness of Quicken? No. Is it conceivable that Quicken might contain an imperfection that could lead, in some circumstances, to an inconsistency? Certainly. But for many sci.mathematicians this situation must be a real paradox.
Suppose I balance my checkbook with a program called KevCash (so as not to sully the good name of Quicken), and suppose this program implements arithmetic perfectly - with one exception. The result of subtracting 5.555555 from 7.777777 is 2.222223. Now if B is my true balance then I should have the formal theorems
B = B + q ( (7.777777 - 5.555555) - 2.222222 )for EVERY value of q. Thus, in the formal system of KevCash I can prove that 1 = 2 = 3 = 4.23 = 89.23 = anything. Clearly the KevCash system has a consistency problem, because I can compute my balance to be anything I want just by manipulating the error produced by that one particular operation. ("So oft it chances in particular men...") But here is the fact that must seem paradoxical to most sci.math posters: thousands of people have used KevCash for years, and not a single error has appeared in the results. How can this be, given that KevCash is formally inconsistent?
The answer is that although KevCash is globally inconsistent, it possesses a high degree of local consistency. Travelling from any given premise (such as 5+7) DIRECTLY to the evaluation (e.g., 12), we are very unlikely to encounter the inconsistency. Of course, in a perfectly consistent system we could take ANY of the infinitely many paths from 5+7 to the evaluation and we would always arrive at the same result, which is clearly not true within KevCash (in which we could, by round-about formal manipulations, evaluate 5+7 to be -3511.1093, or any other value we wanted). Nevertheless, for almost all paths leading from a given premise to its evaluation, the result is the same.
Now consider our formal system of arithmetic. Many people seem agog at the suggestion that our formalization of arithmetic might possibly be inconsistent at some point. Clearly our arithmetic must possess a very high degree of local consistency, because otherwise we would have observed anomalies long before now. However, are we really justified in asserting that every one of the infinitely many paths from every premise to its evaluation gives the same result? As with the system KevCash, this question can't be answered simply by observing that our checkbooks usually seem to balance.
Moreover, the question cannot even be answered within any formal system that can be modelled by the natural numbers. It is evidently necessary to assume the validity of something like transfinite induction to prove the consistency of arithmetic. But how sure are we that a formal system that includes transfinite induction is totally consistent? (If, under the assumption of transfinite induction, we had found that arithmetic was NOT consistent, would we have abandoned arithmetic... or transfinite induction?) The only way we know how to prove this is by assuming still less self-evidently consistent procedures, and so on.
The points I'm trying to make are
"Many people seem agog at the suggestion that our formalization of arithmetic might possibly be inconsistent at some point."Gog, gog, gooo...
"However, are we really justified in asserting that EVERY one of the infinitely many paths from every premise to its evaluation gives the same result?"Heavens! You're right! God may be using a Pentium chip....