A new "feasible" arithmetic

Journal of Symbolic Logic 67 (1):104-116 (2002)
Abstract
A classical quantified modal logic is used to define a "feasible" arithmetic A 1 2 whose provably total functions are exactly the polynomial-time computable functions. Informally, one understands $\Box\alpha$ as "α is feasibly demonstrable". A 1 2 differs from a system A 2 that is as powerful as Peano Arithmetic only by the restriction of induction to ontic (i.e., $\Box$ -free) formulas. Thus, A 1 2 is defined without any reference to bounding terms, and admitting induction over formulas having arbitrarily many alternations of unbounded quantifiers. The system also uses only a very small set of initial functions. To obtain the characterization, one extends the Curry-Howard isomorphism to include modal operations. This leads to a realizability translation based on recent results in higher-type ramified recursion. The fact that induction formulas are not restricted in their logical complexity, allows one to use the Friedman A translation directly. The development also leads us to propose a new Frege rule, the "Modal Extension" rule: if $\vdash \alpha$ then $\vdash A \leftrightarrow \alpha$ a for new symbol A
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2178/jsl/1190150032
Options
 Save to my reading list
Follow the author(s)
Edit this record
My bibliography
Export citation
Find it on Scholar
Mark as duplicate
Request removal from index
Revision history
Download options
Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 30,169
Through your library
References found in this work BETA
The Realm of Primitive Recursion.Harold Simmons - 1988 - Archive for Mathematical Logic 27 (2):177-188.
Safe Recursion with Higher Types and BCK-Algebra.Martin Hofmann - 2000 - Annals of Pure and Applied Logic 104 (1-3):113-166.

Add more references

Citations of this work BETA
Tiering as a Recursion Technique.Harold Simmons - 2005 - Bulletin of Symbolic Logic 11 (3):321-350.

Add more citations

Similar books and articles
Interpretability Over Peano Arithmetic.Claes Strannegård - 1999 - Journal of Symbolic Logic 64 (4):1407-1425.
The Interpretability Logic of Peano Arithmetic.Alessandro Berarducci - 1990 - Journal of Symbolic Logic 55 (3):1059-1089.
A Feasible Theory for Analysis.Fernando Ferreira - 1994 - Journal of Symbolic Logic 59 (3):1001-1011.
On the Complexity of Models of Arithmetic.Kenneth McAloon - 1982 - Journal of Symbolic Logic 47 (2):403-415.
Fragments of Heyting Arithmetic.Wolfgang Burr - 2000 - Journal of Symbolic Logic 65 (3):1223-1240.
Elementary Realizability.Zlatan Damnjanovic - 1997 - Journal of Philosophical Logic 26 (3):311-339.
Added to PP index
2009-01-28

Total downloads
7 ( #534,342 of 2,191,918 )

Recent downloads (6 months)
1 ( #288,547 of 2,191,918 )

How can I increase my downloads?

Monthly downloads
My notes
Sign in to use this feature