The Journal of Symbolic Logic

Research Article

A new “feasible” arithmetic

Stephen Bellantonia1  and Martin Hofmanna2 

a1 Department of Computer Science, University of Toronto, Toronto, Canada, E-mail:

a2 Laboratory for Foundations of Computer Science, University of Edinburgh, Edinburgh, Scotland, UK, E-mail:


A classical quantified modal logic is used to define a “feasible” arithmetic whose provably total functions are exactly the polynomial-time computable functions. Informally, one understands ⃞∝ as “∝ is feasibly demonstrable”.

differs from a system that is as powerful as Peano Arithmetic only by the restriction of induction to ontic (i.e., ⃞-free) formulas. Thus, 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 ⊢ ∝ a then ⊢ A ↔ ∝ for new symbol A.

(Received January 20 2000)

(Revised October 16 2000)


  Department of Computer Science, University of Toronto. The assistance of the Fields Institute for Research in Mathematical Sciences is gratefully acknowledged.

  Laboratory for Foundations of Computer Science, University of Edinburgh.