FOM: proof-theoretic ordinals (correction and follow up)

[Wilfried Buchholz]

On Mon, 13 Apr 1998 23:22:35 Steve Simpson wrote:

 > In my posting of 13 Apr 1998 10:59:01 I wrote:

 > > in at least some cases the ordinal notations were later replaced by
 > > direct translations or interpretations.  Wasn't this the case for
 > > classical and intuitionistic ID_{<omega}?  Please correct me if I'm
 > > wrong.

 > After consultation with Harvey Friedman, I think I was wrong about
 > this.  According to Harvey, we don't yet know how to reduce the
 > classical ID_2, ID_3, ..., ID_{<omega} to their intuitionistic
 > counterparts, except via ordinal notations.

Yes, we know how to reduce.......:
On pp.222-291 of [B,F,P,S] I have proved without using ordinal notations
that ID_\nu(classical) is conservative over ID_\nu(intuitionistic,strictly
positive) for negative arithmetic sentences. The corresponding result
for ID_{<lambda} (lambda a limit ordinal) has also been proved by Sieg
in Ch.III of [B,F,P,S].

( [B,F,P,S] Buchholz, Feferman, Pohlers, Sieg: Iterated Inductive Definitions
and Subsystems of Analysis: Recent Proof-Theoretical Studies. 
Springer LNM 897 (1981) )

-- Wilfried Buchholz


Name: Wilfried Buchholz
Position: Professor of Mathematics
Institution: Universit\"at M\"unchen
Research interest: proof theory, foundations of mathematics
More information: http://www.mathematik.uni-muenchen.de/~buchholz