Fragments of Heyting arithmetic

Journal of Symbolic Logic 65 (3):1223-1240 (2000)
  Copy   BIBTEX

Abstract

We define classes Φnof formulae of first-order arithmetic with the following properties:(i) Everyφϵ Φnis classically equivalent to a Πn-formula (n≠ 1, Φ1:= Σ1).(ii)(iii)IΠnandiΦn(i.e., Heyting arithmetic with induction schema restricted to Φn-formulae) prove the same Π2-formulae.We further generalize a result by Visser and Wehmeier. namely that prenex induction within intuitionistic arithmetic is rather weak: After closing Φnboth under existential and universal quantification (we call these classes Θn) the corresponding theoriesiΘnstill prove the same Π2-formulae. In a second part we consideriΔ0plus collection-principles. We show that both the provably recursive functions and the provably total functions ofare polynomially bounded. Furthermore we show that the contrapositive of the collection-schema gives rise to instances of the law of excluded middle and hence.

Other Versions

reprint Burr, Wolfgang (2002) "Fragments of Heyting Arithmetic". Bulletin of Symbolic Logic 8(4):533-534

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 97,154

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

Fragments of Heyting arithmetic. [REVIEW]Lev Beklemishev - 2002 - Bulletin of Symbolic Logic 8 (4):533-533.
Polynomially Bounded Recursive Realizability.Saeed Salehi - 2005 - Notre Dame Journal of Formal Logic 46 (4):407-417.
An Independence Result on Weak Second Order Bounded Arithmetic.Satoru Kuroda - 2001 - Mathematical Logic Quarterly 47 (2):183-186.
A feasible theory for analysis.Fernando Ferreira - 1994 - Journal of Symbolic Logic 59 (3):1001-1011.

Analytics

Added to PP
2009-01-28

Downloads
32 (#560,846)

6 months
21 (#188,042)

Historical graph of downloads
How can I increase my downloads?