[FOM] Advanced systems programming and the consistency of PA^{2}

[Robert Black]

>However, the construction uses mathematical induction only up to the 
>first uncountable ordinal (the same as the ordinal of Gentzen's cut 
>elimination proof for first order PA).

???????????? Surely Genzen's proof uses PRA plus transfinite 
induction up to epsilon_0, which is a hell of a long way short of the 
first uncountable ordinal. Or am I misunderstanding something?
-- 
Robert Black
Dept of Philosophy
University of Nottingham
Nottingham NG7 2RD

tel. 0115-951 5845
-------------- next part --------------
An HTML attachment was scrubbed...
URL: /pipermail/fom/attachments/20030615/0cc9ff93/attachment.html