10.
A basic result in intuitionism is Π
02‐conservativity. Take any proof
p in classical arithmetic of some Π
02‐statement (some arithmetical statement ?
x.?
y.
P(
x, y), with
P decidable). Then we may effectively turn
p in some intuitionistic proof of the same statement. In a previous paper [1], we generalized this result: any classical proof
p of an arithmetical statement ?
x.?
y.
P(
x, y), with
P of degree
k, may be effectively turned into some proof of the same statement, using Excluded Middle only over degree
k formulas. When
k = 0, we get the original conservativity result as particular case. This result was a by‐product of a semantical construction. J. Avigad of Carnegie Mellon University, found a short, direct syntactical derivation of the same result, using H. Friedman's
A‐translation. His proof is included here with his permission. (© 2003 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)
相似文献