A generalization of a conservativity theorem for classical versus intuitionistic arithmetic

✍ Scribed by Stefano Berardi

• Publisher: John Wiley and Sons
• Year: 2004
• Tongue: English
• Weight: 124 KB
• Volume: 50
• Category: Article
• ISSN: 0044-3050
• DOI: 10.1002/malq.200310074

✦ Synopsis

Abstract

A basic result in intuitionism is Π^0^~2~‐conservativity. Take any proof p in classical arithmetic of some Π^0^~2~‐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)