"May I make a suggestion? Arithmetic's supposed inconsistency only can make sense in a completely formalized system. The problem may reside in the particular way of formalizing...in such a way that it presupposes no previous knowledge on the part of the reader while at the same time it is completely clear that it corresponds with what we call `arithmetic'.... Maybe these problems can be solved satisfactorily. But these solutions can have in them the seeds of contradictions that sneak up on you."Excellent suggestion. I agree completely. Nienhuys continued
"What would happen when a contradiction was found? I guess that the foundations-of-mathematics people would try to find a way to work around the problem."Yes, I agree. They would say "Ooppss, our formalization didn't quite correspond to TRUE arithmetic. Now, here's the final ultimate and absolutely true formalization... (I know we said this last time, but THIS time our formalization really IS perfect.)"
Jan Willem Nienhuys:Here you are positing the existence of a Platonic ideal "ARITHMETIC" that is eternal, perfect, and true, while acknowledging that any given formalization of this Platonic ideal may be flawed. The problem is that our formal proofs are based on a specific formalization of arithmetic, not on the ideal Platonic ARITHMETIC, so we are not justified in transferring our sublime confidence in the Platonic ideal onto our formal proofs.
"I think that what Ben Tilly meant was a contradiction in the positive integers that won't go away, no matter what formalization you use."
In effect your position is equivalent to saying that you are always right, because even if you are found to have said something wrong, that's not what you meant.
Then David Seal said
"...the contradiction still provides the proof you want of FLT within arithmetic. (And since FLT is a theorem about arithmetic, any proof of it must either be within arithmetic or within a system that includes arithmetic as a subsystem)."FLT is a theorem about the ideal of ARITHMETIC, prior to any particular formalization. (This is true both historically and conceptually.) The first step in attempting to prove it is to select a formal system within which to work. Of course, it's trivial to devise a formal system labeled "arithmetic" and then prove FLT within that system. For example, take PA+FLT. But the question is whether that system really represents ARITHMETIC, one requirement of which is consistency.
David Seal continued
Of course, if arithmetic *is* found to be self-contradictory, it's not just FLT that suddenly becomes uninteresting: an awful lot of other mathematics would suffer exactly the same fate...We don't know what, if any, parts of our present mathematics would be rendered uninteresting by the discovery of an inconsistency in our present formalization of arithmetic, because it would depend on the nature of the inconsistency and the steps taken to resolve it. Once the patched-up formalization was in place, we would re-evaluate all of our mathematics to see which, if any, proofs no longer work in the new improved "arithmetic". One would expect that almost all present theorems would survive. The theorems most likely to be in jeopardy would be the most elaborate, far-reaching, and "deep" results, because their proofs tax the resources of our present system the most.
Then Matthew Wiener quoted me saying "We have no meaningful
proof of the consistency of arithmetic", and replied
"The usual ZFC proof is quite meaningful, so far as I can tell."Let me be more explicit about the meaning of "meaningful". Consider the two well known theorems
The only kind of proof that would enhance our confidence in PA would be of the form
con(X) implies con(PA)where X is a system whose consistency is MORE self-evident than that of PA. (This is the key point.) For example, Hilbert hoped that with X = 1st Order Logic it would be possible to prove this theorem, thereby enhancing our confidence in the consistency of PA. That would have been a meaningful proof of the consistency of PA. However, it's now known that such a proof is impossible (unless you believe in the existence of a formal system that is more self-evidently consistent than PA but that cannot be modelled within the system of natural numbers).
Torkel Franzen said
It is not correct that "it's now known that such a proof is impossible" - for example, why should it be impossible to regard the theory of primitive recursive functionals as more evidently consistent than PA?Recall the entire sentence from which you are quoting:
"However, it's now known that such a proof is impossible (unless you believe in the existence of a formal system that is more self-evidently consistent than PA but that cannot be modelled within the system of natural numbers)."Since it's well known that both transfinite induction and the theory of primitive recursive functionals cannot be modelled within the system of natural numbers, my original statement clearly anticipated your comment above. I do not claim it would be impossible to regard such principles as more evidently consistent than PA; I simply observe that no one does, and for good reason. Each represents a non- finitistic extension of formal principles, which is precisely the source of uncertainty in the consistency of PA.
Here's a little thought experiment that sometimes helps people sort out their own heirarchy of faith: If, assuming the consistency of the theory of primitive recursive functionals, one could prove that PA is NOT consistent, would you be more inclined to abandon PA or the theory of primitive recursive functionals?
Torkel Franzen said
But doubts about the consistency of PA, if at all intelligible, must entail doubts about very many proofs in mathematics, and it seems a bit odd to harp on the particular (trivial) theorem "PA is consistent".When considering doubts about the consistency of PA, I see nothing odd about focusing on the theorem "PA is consistent". As to whether such doubts are intelligible, I will only comment that much of the most interesting and profound mathematics of this century has been concerned with just such doubts. As to the number of proofs that are cast into doubt by the possibility of inconsistency in PA, I've explained in other posts that the "perfect consistency or total gibberish" approach to formal systems evidently favored by residents of sci.math is not justified.
Torkel Franzen said
Hilbert was not looking for a theorem of the form "if FOL is consistent, PA is consistent" - after all, FOL is trivially consistent from practically any point of view...If you regard the consistency of FOL as absolute, then the antecedent clause "If con(FOL)" may be omitted from my statements without affecting their content. In fact, that is actually what I did in some earlier posts in which I described the goal of an absolute (as opposed to relative) finitistic proof of con(PA). However, Tim Chow commented that such a proof was not really absolute because it assumed the consistency of first-order logic. Like you, I don't personally worry much about con(FOL), but to accommodate Tim Chow's concern I decided to include the clause "If con(FOL)". Torkel Franzen said
- but for a "finitary" consistency proof for PA. His aim was not just to "increase our confidence" in the consistency of PA, but to show that the use of non-finitary methods is in principle eliminable in proofs of "real statements".Yes. It just so happened that Russell and Whitehead's FOL was a conveinent finitistic vehicle to use as an example. Of course, people sometimes raise the possibility of a finitistic system that cannot be modelled within the theory of natural numbers but, as Ernst Nagel remarked, "no one today appears to have a clear idea of what a finitistic proof would be like that is NOT capable of formulation within arithmetic".