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)|
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.
Citations of this work BETA
Radical Anti-Realism, Wittgenstein and the Length of Proofs.Mathieu Marion - 2009 - Synthese 171 (3):419 - 432.
Similar books and articles
Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic.Jan Krajíček - 1997 - Journal of Symbolic Logic 62 (2):457-486.
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.
The Equivalence of the Disjunction and Existence Properties for Modal Arithmetic.Harvey Friedman & Michael Sheard - 1989 - Journal of Symbolic Logic 54 (4):1456-1459.
An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras.Martin Hofmann - 1997 - Bulletin of Symbolic Logic 3 (4):469-486.
Minimal Realizability of Intuitionistic Arithmetic and Elementary Analysis.Zlatan Damnjanovic - 1995 - Journal of Symbolic Logic 60 (4):1208-1241.
Added to index2009-01-28
Total downloads7 ( #521,215 of 2,163,617 )
Recent downloads (6 months)1 ( #348,037 of 2,163,617 )
How can I increase my downloads?