[FOM] Fwd: invitation to comment

[William Tait]

I have not been following completely this thread---it goes too fast for me. So forgive me if I am repeating points already posted. But I would like to make two of them about Vaughan's remark

On May 21, 2011, at 1:47 AM, Vaughan Pratt wrote:
>> From: Vladimir Voevodsky <vladimir at ias.edu>
>> Date: May 18, 2011 4:44:13 PM EDT
>> To put it very shortly I think that in-consistency of Peano arithmetic
>> as well as in-consistency of ZFC are open and very interesting problems
>> in mathematics. Consistency on the other hand is not an interesting
>> problem since it has been shown by Goedel to be impossible to proof.
> 
> This last sentence of Voevodsky makes very clear that he does not understand Goedel's second incompleteness theorem, which states only that the consistency of T cannot be proved *in T*.  That the consistency of PA cannot be proved in PA might mean something if PA were a powerful theory, but it is not.  As Martin pointed out, consistency of PA can be proved in PRA + ε_0.  The structure of ε_0 is well understood, and anyone claiming otherwise needs to show why.  Dismissing ε_0 with a wave of the hand as Voevodsky did is not mathematics, it is just handwaving based seemingly on a misunderstanding of Goedel's second incompleteness theorem.

1.  There is an ambiguity in speaking of establishing the consistency of PA. But first: most, although not all, people agree that we can express this syntactical property by means of a certain  arithmetic sentence Con_{PA}, obtained from the informal syntactical definition by coding the atomic symbols by numbers and coding finite sequences of numbers in some standard way by numbers. Anyway I am assuming that Con_{PA}, via this coding, really does express the consistency of PA. 

Vaughan points out that we can prove Con_{PA} in ordinary mathematics, for example using no more than PRA with the addition of a certain quantifier-free version of induction up to epsilon_0 (using some `standard' ordering of the natural numbers to represent the ordinals < epsilon_0).   But I think it unlikely that Voevodsky is unaware of this. 

The problem of proving the consistency of PA is not that of giving a 'mathematical' proof of Con_{PA} in the ordinary sense of a mathematical proof. As Poincare noted when Hilbert first introduced the problem of proving consistency of, say, PA in the early 20th century, a proof of consistency will inevitably involve proof by mathematical induction, and so there will be a circle. Only around 1922 did Hilbert (and Bernays) have a response to Poincare: The proof of consistency (and the applications of mathematical induction involved in it) will be in the context of a different kind of mathematics, finitist mathematics, based upon 'intuitive evidence', and which is itself immune to the demands of a consistency proof and thus avoid the circularity that Poincare attributed to the enterprise. 

In the event, Hilbert was wrong in two respects. First---and this is a consequence of Goedel2---in spite of Gödel's own initial doubts about this, it would seem that all of finitist mathematics is formalized in PA and so is insufficient to prove Con_{PA}. Second, however one is to understand the notion of 'intuition' involved, it is difficult (for me) to see why finitist mathematics, or even that part of it formalized in PRA (in case you don't think they are the same thing) is immune from the demand for a consistency proof. 

For this reason, I think that Voevodsky is right: whatever researches in proof theory or foundations of mathematics are to accomplish, the search for nontrivial consistency proofs is off the board. This may also be what Andrei Rodin meant when he wrote

> While for the in-consistency of PA and ZFC we may
> possibly have a sound *mathematical* argument (evidence) any attempted proof of
> the consistency of these systems will be not a mathematical proof proper but
> involve some further non-mathematical assumptions.
although I am not sure what he meant by "some further non-mathematical assumptions". 

It seems to me that we just have to live with the possibility of inconsistency of even the most basic parts of mathematics, say PRA. (A really mean god, to show his utter contempt for us, would arrange ['would have arranged'? Tenses are hard when speaking of gods] for the least proof of a contradiction to exist but to be too large in principle for us to process.)

2. Much as I admire Gentzen's proof theory, I do not think that he gave an adequate proof of Con_{PA}, even in the sense of an ordinary mathematical proof; for it assumes induction up to epsilon_0. He certainly intends that this principle is finitist (perhaps in some extended sense) and gives an 'intuitive' argument for why it should be admitted as such. But, like many other 'intuitive' arguments in the finitist literature, examination shows it to be just an incomplete proof in the ordinary sense, and one such that, when the details are filled in, is seen to involve non-finitist mathematics--- in Gentzen's case full PA.  

In any case, induction up to epsilon_0 is something that can be proved anda so should be   proved. And so a proof based upon it as an assumption is not a full proof.  Contrast this with induction and recursion up to omega, i.e. PRA: This is the starting point of arithmetic. To accept the notion of natural number IS to accept mathematicdal induction and finite iteration f^(n) of a function f: D---> D, for any given domain D (such as the domain of k-tuples of natural numbers). (Dedekind, of course, wasn't satisfied with this and so derived finite iteration and mathematical induction in (impredicative) second-order number theory.) 

So in this respect, Gödel's proof of Con_{PA} in the Dialectica paper  is superior to Gentzen's, for it begins with nothing more than the mere acceptance of the finite types based on the natural numbers. For once we simply admit these, the theory T is given: finite iteration applied to operations on domains D that are k-tuples of finite types is given.  

This way of understanding T is contrary to Gödel's own interpretation of the functions of higher types as 'reckonable functions'. (In spite of Gödel's efforts to show otherwise, this notion has a quantifier complexity that grows with the type.) Gödel's motivation was, at least in part, that he wanted equations between terms of higher type to express 'intensional' or 'definitional equality' and so be decidable---so that classical propositional logic applies. But this is inessential for the consistency proof.  Equations of higher types are to be understood in the usual way as extensional equalities. 

I have preached a longer sermon than I intended.

Bill Tait