A new "feasible" arithmetic

Journal of Symbolic Logic 67 (1):104-116 (2002)
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
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history Request removal from index
Download options
PhilPapers Archive

Upload a copy of this paper     Check publisher's policy on self-archival     Papers currently archived: 23,651
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
Harold Simmons (1988). The Realm of Primitive Recursion. Archive for Mathematical Logic 27 (2):177-188.
Martin Hofmann (2000). Safe Recursion with Higher Types and BCK-Algebra. Annals of Pure and Applied Logic 104 (1-3):113-166.

Add more references

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

Add more citations

Similar books and articles

Monthly downloads

Added to index


Total downloads

7 ( #499,540 of 1,902,847 )

Recent downloads (6 months)

1 ( #446,006 of 1,902,847 )

How can I increase my downloads?

My notes
Sign in to use this feature

Start a new thread
There  are no threads in this forum
Nothing in this forum yet.