FOM: Classical over Intuitionistic

[Ulrich Kohlenbach]

Shoenfield writes:
>      I am slightly puzzled by the statement:
>      >PA is conservative over HA for pi-0-2 sentneces.
>      I presume this depends on only allowing plus and times as non-
> logical constants.   If one allows Kleene's T-predicate, a counter-
> example is (forall x)(A(x) or not-A(x)) where A(x) is a sigma-0-1
> formula which defines a non-recursive set.
> 
> 

PA is Pi^0_2-conservative over HA even in the presence of arbitrary 
primitive recursive functions. The example above is only classically 
equivalent to a pi-0-2 sentence (the latter being obviously provable 
in HA since quantifier-free formulas are decidable in HA) but not 
intuitionistically. 

Ulrich Kohlenbach