A basic result in intuitionism is Pi-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.
A generalization of conservativity theorem for classical versus intuitionistic arithmetic
BERARDI, Stefano
2004-01-01
Abstract
A basic result in intuitionism is Pi-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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
