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)|
|Through your library||Configure|
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 downloads4 ( #188,906 of 722,856 )
Recent downloads (6 months)1 ( #60,917 of 722,856 )
How can I increase my downloads?