Back to Search
Start Over
A generalization of a conservativity theorem for classical versus intuitionistic arithmetic.
- Source :
-
Mathematical Logic Quarterly . Jan2004, Vol. 50 Issue 1, p41-46. 6p. - Publication Year :
- 2004
-
Abstract
- 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) [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 09425616
- Volume :
- 50
- Issue :
- 1
- Database :
- Academic Search Index
- Journal :
- Mathematical Logic Quarterly
- Publication Type :
- Academic Journal
- Accession number :
- 13727416
- Full Text :
- https://doi.org/10.1002/malq.200310074