FOM: Classical over Intuitionistic

Ulrich Kohlenbach kohlenb at
Thu Oct 15 14:27:16 EDT 1998

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 

Ulrich Kohlenbach

More information about the FOM mailing list