David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
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)|
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
No references found.
Citations of this work BETA
Mathieu Marion (2009). Radical Anti-Realism, Wittgenstein and the Length of Proofs. Synthese 171 (3):419 - 432.
Similar books and articles
Jan Krajíček (1997). Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic. Journal of Symbolic Logic 62 (2):457-486.
Claes Strannegård (1999). Interpretability Over Peano Arithmetic. Journal of Symbolic Logic 64 (4):1407-1425.
Alessandro Berarducci (1990). The Interpretability Logic of Peano Arithmetic. Journal of Symbolic Logic 55 (3):1059-1089.
Fernando Ferreira (1994). A Feasible Theory for Analysis. Journal of Symbolic Logic 59 (3):1001-1011.
Kenneth McAloon (1982). On the Complexity of Models of Arithmetic. Journal of Symbolic Logic 47 (2):403-415.
Harvey Friedman & Michael Sheard (1989). The Equivalence of the Disjunction and Existence Properties for Modal Arithmetic. Journal of Symbolic Logic 54 (4):1456-1459.
Martin Hofmann (1997). An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras. Bulletin of Symbolic Logic 3 (4):469-486.
Wolfgang Burr (2000). Fragments of Heyting Arithmetic. Journal of Symbolic Logic 65 (3):1223-1240.
Zlatan Damnjanovic (1997). Elementary Realizability. Journal of Philosophical Logic 26 (3):311-339.
Zlatan Damnjanovic (1995). Minimal Realizability of Intuitionistic Arithmetic and Elementary Analysis. Journal of Symbolic Logic 60 (4):1208-1241.
Added to index2009-01-28
Total downloads5 ( #264,986 of 1,692,502 )
Recent downloads (6 months)1 ( #181,267 of 1,692,502 )
How can I increase my downloads?