[FOM] Fwd: invitation to comment
Richard Heck
rgheck at brown.edu
Sun May 22 06:50:46 EDT 2011
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
More information about the FOM
mailing list