Premium
A generalization of a conservativity theorem for classical versus intuitionistic arithmetic
Author(s) -
Berardi Stefano
Publication year - 2004
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200310074
Subject(s) - statement (logic) , mathematics , arithmetic function , intuitionism , decidability , generalization , degree (music) , intuitionistic logic , discrete mathematics , arithmetic , linear logic , mathematical analysis , physics , geometry , acoustics , political science , law
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)