FOM: Classical over Intuitionistic
Ulrich Kohlenbach
kohlenb at daimi.au.dk
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
intuitionistically.
Ulrich Kohlenbach
More information about the FOM
mailing list