FOM: classical over intuitionistic

[Harvey Friedman]

Tenant 9:46PM 10/11/98 wrote (addressed to Simpson):

>For starters, there's the following improvement by Friedman on a result of
>G"odel:
>
>	PA is conservative over HA for all Pi^0_2 sentences.
>
>How about a full list of results of this flavor?

I am not the first to prove this. I think it is generally credited to Godel
via the Dialectica interpretation. I had a technique that gives a proof
about .01% as difficult, and also works for a very large variety of
systems. My technique proves

2nd order arithmetic is conservative over intuitionistic 2nd order
arithmetic for all pi^0_2 sentences

via a proof about .0001% as difficult as the one generally credited to C.
Spector, or Kreisel-Spector.

And for type theory and various set theories, conservativity for pi^0_2
sentences is properly credited to me via this technique. The technique is
presented and applied in

Classically and intuitionistically provably recursive functions, HIgher Set
Theory, Springer Lecture Notes, Vol. 669, 1978, 21-27.

Lately I have seen some other names associated with this "interpretation,"
which in my setup can be viewed as a very distilled form of exploding
Kripke model interpretation, but where Kripke models are not mentioned; it
all boils down to a trivial looking syntactic twist.