FOM: Classical over Intuitionistic

[Harvey Friedman]

Shoenfield 11:38AM 10/15/98 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.

Here pi-0-2 means literally in the form (forall x1,...,xk in N)(therexists
y1,...,yp in N)(A(x1,...,xk,y1,...,yp)), where A is, say, a formula with
only bounded quantifiers, primitive recursive function symbols, and <,=.
Your counterexample is not of that form.

Because of MRDP (Hilbert's 10th), the counterexample you indicate can be
done with A(x) being of of the form (therexists y1,...,yp)(P(y1,...,yp) =
Q(y1,...,yp)), where P,Q are terms using only +,x, contrary to your
"presumption."