Hostname: page-component-745bb68f8f-cphqk Total loading time: 0 Render date: 2025-02-11T05:56:14.206Z Has data issue: false hasContentIssue false
  • English
  • Français

A new method for establishing conservativity of classical systems over their intuitionistic version

Published online by Cambridge University Press:  01 August 1999

THIERRY COQUAND  and
MARTIN HOFMANN
THIERRY COQUAND
Affiliation:
Chalmers University, Computer Science, S41296 Göteborg, Sweden. E-mail: coquand@cs.chalmers.se
MARTIN HOFMANN
Affiliation:
Laboratory for Foundations of Computer Science, The King's Buildings, Mayfield Road, Edinburgh EH9 3JZ. E-mail: mxh@dcs.ed.ac.uk
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We use a syntactical notion of Kripke models to obtain interpretations of subsystems of arithmetic in their intuitionistic counterparts. This yields, in particular, a new proof of Buss' result that the Skolem functions of Bounded Arithmetic are polynomial time computable.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 9 , Issue 4 , August 1999 , pp. 323 - 333
Copyright
© 1999 Cambridge University Press