[FOM] Hilbert and conservativeness
Robert Black
Mongre at gmx.de
Mon Aug 29 05:52:40 EDT 2005
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
More information about the FOM
mailing list