[FOM] Voevodsky

[Vaughan Pratt]

On 5/18/2011 12:01 AM, Robert Black wrote:
> Now what I take Voevodsky to be saying: we can coherently doubt the
> consistency of PA. This seems obviously true, since if it weren’t, the
> Hilbert programme for PA would have been incoherent. Further, although
> there are proofs of the consistency of PA, for each such proof we can
> doubt its cogency. (The examples Voevodsky considers are firstly the
> obvious proof that the axioms of PA are true and the proof rules
> preserve truth (formalized, this is the proof of Con(PA) in second-order
> arithmetic) where it is possible to doubt whether we really understand
> induction over arithmetically definable but non-recursive properties, or
> Gentzen-style proofs where it is possible to doubt whether the ordinals
> less than epsilon_0 (modulo some suitable notation) are really
> well-ordered. This seems to me correct. (I don’t mean I *do* doubt these
> things - I don’t - but one *can* coherently doubt them.) The consistency
> of PA is not absolutely indubitable.

You seem to be arguing that because there exists a questionable proof of 
consistency of PA (existence of a model), therefore all proofs of its 
consistency must be questionable.  That does not follow.  As others have 
pointed out here, surely Voevodsky has unquestioningly accepted much 
deeper proofs than Gentzen's proof of consistency of PA, so why should 
he single out this relatively straightforward argument as questionable?

> I’d be amazed if such a programme were to go through, and we need to be
> told exactly which sentences are truth-apt, and what their truth
> consists in, but is there any reason why it’s obviously silly?

Yes: because the consistency of PA is obvious to those who've bothered 
to read the proof.  It's a straightforward argument in the proof theory 
of PA.

As I wrote in my previous message, Voevodsky (and those supporting him) 
must be thinking of PA as a powerful system of logic beyond mortal 
comprehension.  It's not: there are relatively slowly growing recursive 
functions (relative to the recursive functions computer scientists like 
to come up with as examples of fast-growing functions) whose existence 
is obvious yet which cannot be proved to exist in PA, for the boring 
reason that they grow faster than *any* function whose existence is 
provable in PA.

Paris and Harrington were among the first to notice this limitation of 
PA, in 1975 when they proved independence of the Large Ramsey Theorem 
from PA.  More insightful however might be the following family of 
functions originating with Helmut Schwichtenberg, Definierbare 
Funktionen im λ-Kalkül mit Typen, Archiv für Mathematische. Logik und 
Grundlagenforschung, 17:113-114, 1975, with related versions due to Lob 
and Wainer even earlier (1970).  The version here is from Steve 
Fortune's 1979 Ph.D. thesis and can also be found in (even) more 
polished form on p.155 of Fortune et al, The Expressiveness of Simple 
and Second-Order Type Structures, JACM 30:1, 151-185 (Jan. 1983).

f_0(x) = x+1
f_{i+1}(x) = (f_i)^(x)(x)  (f_i applied x times to x)
f_k(x) = f_{k_x}(x) where k_x for x < ω is a suitably canonically 
defined sequence for which the limit ordinal k = lim_x k_x.

Hence f_1(x) = 2*x, f_2(x) = x*2^x, and so on.  f_ω can be viewed as 
essentially Ackermann's function.

Theorem 2.4.1 of the JACM article (acknowledging Schwichtenberg 1975 and 
(Lob and) Wainer 1970) states "Every function provably recursive in PA 
is majorized by [i.e. grows more slowly in the limit than] f_k for some 
k < ε_0.

Once you've picked your favorite sequence k_0, k_1, k_2, ..., k_i, ... 
(where i is always a natural number) with limit k for every limit 
ordinal k up to and including ε_0, and settled on a  program for 
computing the ordinal k_x from the ordinal k (presented in Cantor normal 
form) and the natural number x, you can now easily write a recursive 
program g(a,x) = f_a(x) taking an ordinal a <= ε_0 and a natural number x.

Since f_{ε_0} essentially diagonalizes over the functions named in the 
above theorem, it majorizes every function provably recursive in PA. 
Hence it is not itself such a function.

This might give people a better idea of just how weak PA really is.  If 
you can satisfy yourself that for any limit ordinal k up to and 
including ε_0 you can systematically find a sequence {k_x}, x < ω, of 
ordinals having that ordinal as its limit, then you can write a simple 
recursive program, as a function of ordinals up to ε_0 presented in 
Cantor normal form, that always halts but whose halting is not provable 
in PA.  Fortune et al offer one such way on p.155 of their article, but 
it's more fun coming up with your own.

Vaughan Pratt