A new method for establishing conservativity of classical systems over their intuitionistic version
From MaRDI portal
Publication:4704759
DOI10.1017/S0960129599002844zbMath0935.03069MaRDI QIDQ4704759
Thierry Coquand, Martin Hofmann
Publication date: 25 November 1999
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Kripke models; Skolem functions; polynomial time computable; Bounded Arithmetic; fragments of intuitionistic arithmetic; subsystems of arithmetic
03D15: Complexity of computation (including implicit computational complexity)
03F30: First-order arithmetic and fragments
Related Items
The axiom of choice and combinatory logic, Forcing in Proof Theory, A complexity analysis of functional interpretations, Provably recursive functions of constructive and relatively constructive theories, The metamathematics of ergodic theory, Uniform Heyting arithmetic, Saturated models of universal theories, Remarks on applicative theories, Interpreting classical theories in constructive ones