2 search results - page 1 / 1 » Relating Classical Realizability and Negative Translation fo... |
TLCA
2009
Springer
14 years 1 months ago
2009
Springer
Friedman showed how to turn a classical proof of a Σ0 1 formula into an intuitionistic proof of the same formula, thus giving an effective method to extract witnesses from classi...
CORR
2011
Springer
13 years 2 months ago
2011
Springer
Abstract. We show how to extract existential witnesses from classical proofs using Krivine’s classical realizability—where classical proofs are interpreted as λ-terms with the...