Archive for Mathematical Logic 49 (3):291-300 (2010)

Authors
Abstract
In this paper we prove conservation theorems for theories of classical first-order arithmetic over their intuitionistic version. We also prove generalized conservation results for intuitionistic theories when certain weak forms of the principle of excluded middle are added to them. Members of two families of subsystems of Heyting arithmetic and Buss-Harnik’s theories of intuitionistic bounded arithmetic are the intuitionistic theories we consider. For the first group, we use a method described by Leivant based on the negative translation combined with a variant of Friedman’s translation. For the second group, we use Avigad’s forcing method
Keywords Intuitionistic bounded arithmetic  Forcing  Friedman’s translation  Heyting arithmetic  The negative translation
Categories (categorize this paper)
DOI 10.1007/s00153-009-0172-0
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 53,688
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Basic Proof Theory.A. S. Troelstra - 2000 - Cambridge University Press.
Existence and Feasibility in Arithmetic.Rohit Parikh - 1971 - Journal of Symbolic Logic 36 (3):494-508.
Interpreting Classical Theories in Constructive Ones.Jeremy Avigad - 2000 - Journal of Symbolic Logic 65 (4):1785-1812.

View all 12 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Interpreting Classical Theories in Constructive Ones.Jeremy Avigad - 2000 - Journal of Symbolic Logic 65 (4):1785-1812.
Polynomially Bounded Recursive Realizability.Saeed Salehi - 2005 - Notre Dame Journal of Formal Logic 46 (4):407-417.
Preservation Theorems for Bounded Formulas.Morteza Moniri - 2007 - Archive for Mathematical Logic 46 (1):9-14.
A Realizability Interpretation for Classical Arithmetic.Jeremy Avigad - 2002 - Bulletin of Symbolic Logic 8 (3):439-440.
Closed Fragments of Provability Logics of Constructive Theories.Albert Visser - 2008 - Journal of Symbolic Logic 73 (3):1081-1096.
Models of Intuitionistic TT and N.Daniel Dzierzgowski - 1995 - Journal of Symbolic Logic 60 (2):640-653.
Forcing in Proof Theory.Jeremy Avigad - 2004 - Bulletin of Symbolic Logic 10 (3):305-333.
On Two Questions About Feasibly Constructive Arithmetic.Morteza Moniri - 2003 - Mathematical Logic Quarterly 49 (4):425.

Analytics

Added to PP index
2013-11-23

Total views
17 ( #568,144 of 2,349,541 )

Recent downloads (6 months)
1 ( #510,673 of 2,349,541 )

How can I increase my downloads?

Downloads

My notes