Jan Willem Nienhuys wroteI can speak for neither Ben Tilly nor J.W. Nienhuys, but in my opinion, the position stated above, which is also mine, does not imply the belief in any Platonic ideal "ARITHMETIC". At least if we demand that our formalization should be powerful enough to allow proofs of non-trivial theorems."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.""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."
The most powerful, and the most dubious, of the arithmetical axioms is undoubtedly the Axiom (schema) of Induction. If a contradiction in Peano Arithmetics was discovered, this would probably depend on induction, so we must then at least weaken the Axiom of Induction. But Gvdel's Theorem can be derived even with a substantially weakened Axiom of Induction, and I believe that such a weakened axiom would then also lead to a contradiction, so it seems that we would have to throw away all induction.
But without induction, arithmetic would be rather meager. We could still prove theorems like 2+2=4 and (with a huge amount of work and paper) 4875*9522=46419750. But probably, we couldn't prove even the commutative law of addition. It seems that it would be very difficult to prove interesting general statements without induction. Therefore such a formal system wouldn't be very interesting, in my opinion.
My discussion contains a lot of opinions and guessings, but it doesn't presuppose any Platonic ideal ARITHMETIC.
So, let us hope that there is no contradiction in arithmetic. Okay, laymen, bankers, and others would survive, but us mathematicians?
I don't worry much about con(FOL), but to accommodate Tim Chow's concern I decided to include the clause "If con(FOL)".If the consistency of FOL is somehow a hypothetical matter, why should I assume that you or I make any sense whatever in our babbling?
...highly elaborate and lengthy chains of deduction in the far reaches of advanced number theory might need to be re-evaluated in the light of our patched-up formalization. I believe this was the point Ms vos Savant was laboring to make in her book on FLT.If so, it's an awfully trivial point, and hardly worth making. She might as well say "Everything we think might have an error in it because some demon somewhere is messing with our brains." Quite true. So what?
"PA can be modelled within ZF. It follows that con(ZF) implies con(PA)."More accurately, if follows that ZF implies Con(PA). [This] suggests yet again that you don't know beans about what you are talking about. A proof from ZF brings with it the supreme confidence that a century of working with ZF and beyond has given us.
Kevin Brown wrote:That seems to be your attitude. That, and/or zero comprehension of the issues involved.
Of course, it's perfectly acceptable to say "I'm simply not interested in the foundational issues of mathematics or in the meaning of consistency for formal systems".
PA can be modelled within ZF. It follows that con(ZF) implies con(PA).Ummm...actually it follows that ZF implies con(PA). I am actually not sure whether or not it is even true that con(ZF) implies con(PA). (Then again this is something that I have not thought about in a long time...)
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... This system even proves its *own* consistency.This hierarchy of systems possesses an interesting structure. For example, each system has a successor which is assumed to be a system, and distinct from any of the previous systems (i.e., no loops). And of course it's necessary to justify speaking of the completed infinite heirarchy, implying induction. The whole concept might almost be formalized as a set of axioms along the lines of:
(i) ZFC is a System.
(ii) For any System X, the successor X+con(X) is also a System.
(iii) ZFC is not the successor of a System.
(iv) If the successors of Systems X and Y are the same, then X and
Y are the same.
(v) If ZFC is in a set M, and if for every System X in M the
successor X+con(X) is in M, then M contains every System.
Now we're getting somewhere! If we can just prove this is consistent...By the way, here's an interesting quote from Ian Stewart's book "The Problems of Mathematics":
"Mathematical logicians study the relative consistency of different axiomatic theories in terms of consistency strength. One theory has greater consistency strength than another if its consistency implies the consistency of the other (and, in particular, if it can model the other). The central problem in mathematical logic is to determine the consistency strength in this ordering of any given piece of mathematics.One of the weakest systems is ordinary arithmetic, as formalized axiomatically by Giuseppe Peano... Analysis finds its place in a stronger theory, called second-order arithmetic. Still stronger theories arise when we axiomatize set theory itself. The standard version, Zermelo-Frankel Set Theory, is still quite weak, although the gap between it and analysis is large, in the sense that many mathematical results require MORE than ordinary analysis but LESS than the whole of ZF for their proofs."
The usual proof of the consistency of PA does *not* assume con(ZF).What does "the usual proof of the consistency of PA" mean? I am under the impression that Godel proved that the consistency of PA cannot be proved if PA is consistent.
But such a thing is not possible because, in contrast to the axioms for PA, the axioms of the First Order Predicate Language can be proved to be consistent w/r negation, and therefore absolutely consistent [e.g. Andrews, "An Introduction to Mathematical Logic and Type Theory", Th.2101].
I am citing the consistency of the FOPL as my basis for concluding *from* Godel's result to the effect that if PA is consistent then any proof of the sentence that expresses that hypothesis written out in that FOPL consisting of all sentences which are logical consequences of Peano's axioms can be converted into a proof of the opposite *that* if PA is consistent then no such proof is possible.
And I think I went on to conclude from this that we were therefore left with no alternative other than to simply assume that we can without fear of contradiction speak about infinite sets -- et voila, I am told that indeed such an assumption is among the axioms of ZF.
Thank you, Your Honor, I rest my case.