A new method for establishing conservativity of classical systems over their intuitionistic version
From MaRDI portal
Publication:4704759
DOI10.1017/S0960129599002844zbMath0935.03069OpenAlexW1986998737MaRDI QIDQ4704759
Martin Hofmann, Thierry Coquand
Publication date: 25 November 1999
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129599002844
Kripke modelsSkolem functionspolynomial time computableBounded Arithmeticfragments of intuitionistic arithmeticsubsystems of arithmetic
Complexity of computation (including implicit computational complexity) (03D15) First-order arithmetic and fragments (03F30)
Related Items (13)
A semantic approach to conservativity ⋮ A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC ⋮ Interpreting classical theories in constructive ones ⋮ The axiom of choice and combinatory logic ⋮ Provably recursive functions of constructive and relatively constructive theories ⋮ A complexity analysis of functional interpretations ⋮ Uniform Heyting arithmetic ⋮ Forcing in Proof Theory ⋮ The metamathematics of ergodic theory ⋮ MARKOV’S PRINCIPLE AND SUBSYSTEMS OF INTUITIONISTIC ANALYSIS ⋮ Remarks on applicative theories ⋮ Light Dialectica Program Extraction from a Classical Fibonacci Proof ⋮ Saturated models of universal theories
This page was built for publication: A new method for establishing conservativity of classical systems over their intuitionistic version
