Provably recursive functions of constructive and relatively constructive theories

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


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



    Upload a copy of this work     Papers currently archived: 93,098

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Interpreting classical theories in constructive ones.Jeremy Avigad - 2000 - Journal of Symbolic Logic 65 (4):1785-1812.
Interpreting Classical Theories in Constructive Ones.Jeremy Avigad - 2000 - Journal of Symbolic Logic 65 (4):1785-1812.
Extracting Algorithms from Intuitionistic Proofs.Fernando Ferreira & António Marques - 1998 - Mathematical Logic Quarterly 44 (2):143-160.
Conservation Theorems on Semi-Classical Arithmetic.Makoto Fujiwara & Taishi Kurahashi - 2023 - Journal of Symbolic Logic 88 (4):1469-1496.
Preservation theorems for bounded formulas.Morteza Moniri - 2007 - Archive for Mathematical Logic 46 (1):9-14.
Two General Results on Intuitionistic Bounded Theories.Fernando Ferreira - 1999 - Mathematical Logic Quarterly 45 (3):399-407.


Added to PP

30 (#550,897)

6 months
11 (#272,000)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

No citations found.

Add more citations

References found in this work

Basic proof theory.A. S. Troelstra - 1996 - New York: Cambridge University Press. Edited by Helmut Schwichtenberg.
Constructivism in Mathematics: An Introduction.A. S. Troelstra & Dirk Van Dalen - 1988 - Amsterdam: North Holland. Edited by D. van Dalen.
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 13 references / Add more references