Functional interpretations of feasibly constructive arithmetic

Annals of Pure and Applied Logic 63 (2):103-200 (1993)
  Copy   BIBTEX


A notion of feasible function of finite type based on the typed lambda calculus is introduced which generalizes the familiar type 1 polynomial-time functions. An intuitionistic theory IPVω is presented for reasoning about these functions. Interpretations for IPVω are developed both in the style of Kreisel's modified realizability and Gödel's Dialectica interpretation. Applications include alternative proofs for Buss's results concerning the classical first-order system S12 and its intuitionistic counterpart IS12 as well as proofs of some of Buss's conjectures concerning IS12, and a proof that IS12 cannot prove that extended Frege systems are not polynomially bounded



    Upload a copy of this work     Papers currently archived: 89,685

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

On two questions about feasibly constructive arithmetic.Morteza Moniri - 2003 - Mathematical Logic Quarterly 49 (4):425.
Unifying Functional Interpretations.Paulo Oliva - 2006 - Notre Dame Journal of Formal Logic 47 (2):263-290.
On interpretations of bounded arithmetic and bounded set theory.Richard Pettigrew - 2009 - Notre Dame Journal of Formal Logic 50 (2):141-152.
Predicative arithmetic.Edward Nelson - 1986 - Princeton, N.J.: Princeton University Press.
Closed fragments of provability logics of constructive theories.Albert Visser - 2008 - Journal of Symbolic Logic 73 (3):1081-1096.
Predicate Logics of Constructive Arithmetical Theories.Albert Visser - 2006 - Journal of Symbolic Logic 71 (4):1311 - 1326.
Kant’s Theory of Arithmetic: A Constructive Approach? [REVIEW]Kristina Engelhard & Peter Mittelstaedt - 2008 - Journal for General Philosophy of Science / Zeitschrift für Allgemeine Wissenschaftstheorie 39 (2):245 - 271.


Added to PP

17 (#734,021)

6 months
4 (#313,042)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Alasdair Urquhart
University of Toronto, St. George Campus

Citations of this work

Interpreting classical theories in constructive ones.Jeremy Avigad - 2000 - Journal of Symbolic Logic 65 (4):1785-1812.
Saturated models of universal theories.Jeremy Avigad - 2002 - Annals of Pure and Applied Logic 118 (3):219-234.
Bounded arithmetic for NC, ALogTIME, L and NL.P. Clote & G. Takeuti - 1992 - Annals of Pure and Applied Logic 56 (1-3):73-117.

View all 29 citations / Add more citations