[FOM] Fwd: invitation to comment

[Richard Heck]

On 05/21/2011 02: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.
>
I won't assert it outright, but I think Timothy Chow's suggestion about 
what is going on here is worth considering, namely, that Voevodsky means 
something other by "proof" than what we would normally assume: that he 
is worried that any proof of Con(PA) must, in some epistemic and not 
purely mathematical sense be circular, in the sense that such a proof 
could carry no weight for someone worried about whether PA is actually 
consistent. So we might well have a proof, in one sense, but not one 
that satisfies.

Perhaps (perhaps!) one way to elaborate this concern is to note the 
following:

FACT. Let T be a recursive set of axioms, and suppose S containing Q 
proves Con(T). Then, if T is inconsistent, so is S.

If T is inconsistent, then of course S is *false*, but what is claimed 
is stronger. And obvious. Since S contains Q, it is \Sigma_1 complete, 
and so proves Bew_T(t, "0=1") for some term t. But S also proves 
\neg\exists x(Bew_T(x, "0=1")), so S is inconsistent.

That said, I think it would be difficult to argue that Gentzen's proof 
is circular in this sort of sense. And I'll mention one more thing. It 
is also common to dismiss the Tarskian proof of Con(PA) on the ground 
that it requires that we assume PA. This is false. If we start with 
I\Sigma_1, add a truth theory for the language of arithmetic, and extend 
the induction axioms to permit semantic vocabulary, the result proves 
Con(PA). We do not in any sense need to assume that all axioms of PA are 
true. That too is something we prove.

Richard Heck