[FOM] Hilbert and conservativeness

[Robert Black]

Hilbert did eventually come to the recognition that a consistency 
proof would bring conservativeness for what we would call pi_1 
sentences (without making any assumptions about the completeness of 
finitary reasoning beyond calculations with particular numbers), but 
I don't think there's a really clear statement of the point until his 
1928 Hamburg lecture 'Die Grundlagen der Mathematik'. There he takes 
the 'Fermat proposition' and argues that if we had a proof of it in 
an 'ideal' system for which we had a finitary consistency proof then 
we could convert this proof into a finitary proof of FLT.

In my rough and ready translation:

But the consistency proof at the same time offers a general method of 
transforming proofs for general propositions of the type of say the 
Fermat proposition which are conducted with the aid of the epsilon 
function into finitary proofs.
Assume, for example, that we had found a proof of the Fermat theorem 
with the aid of the logical epsilon function. From it one could then 
in the following way make a finitary proof.
Suppose we had numerals p, a, b, c (p>2) which satisfied the Fermat 
equation  aŽ^p+b^p=c^p. Then we could get this as a provable formula 
by bringing the agreement of the numerals aŽ^p+b^p and c^p into the 
form of a proof. On the other hand by our assumption we have a proof 
for the formula
(Z(x) & Z(y) & Z(z) & Z(w) & (w>2)) -> (xŽ^w+y^w‚z^w), from which by 
instantiation and modus ponens we get aŽ^p+b^p‚c^p. Thus both 
aŽ^p+b^p=c^p and aŽ^p+b^p‚c^p would be provable. But this cannot, as 
the finitary consistency proof shows, be the case.

[For e-mail purposes I have expressed Hilbert's distinction between 
Fraktur variables for numerals and italic variables in the 
infinitistic formal system by using a,b,c,p for the former and 
x,y,z,w for the latter]

Craig Smorynski in his entertaining but alas not easily obtainable 
'HILBERT'S PROGRAMME' remarks (p.64) that 'It was just this 
breakthrough that transformed Hilbert's programme into Hilbert's 
Programme and gave rise to the myth that, all along, Hilbert had 
known what he was doing'.

Robert

>At several places Hilbert notes that a finitistic consistency proof for
>'ideal' mathematics implies that 'ideal' mathematics is conservative
>over finitistic mathematics w.r.t. finitistically meaningful ('real')
>statements.
>
>What I'm wondering is how Hilbert knew this. Did he note, as we might
>do today, that if T_1 |- Cons(T_2) then every Pi_1 sentence provable in
>T_2 is provable in T_1 (provided the theories meet the relevant
>conditions); or did he simply believe that finitistic mathematics is
>complete and hence any consistent theory extending it is conservative?
>
>Aatu Koskensilta (aatu.koskensilta at xortec.fi)
>
>"Wovon man nicht sprechen kann, daruber muss man schweigen"
>   - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
>
>_______________________________________________
>FOM mailing list
>FOM at cs.nyu.edu
>http://www.cs.nyu.edu/mailman/listinfo/fom