An Evaluation Semantics for Classical Proofs
No Access Until
Permanent Link(s)
Collections
Other Titles
Author(s)
Abstract
We show how to interpret classical proofs as programs in a way that agrees with the well-known treatment of constructive proofs as programs and moreover extends it to give a computational meaning to proofs claiming the existence of a value satisfying a recursive predicate. Our method turns out to be equivalent to H. Friedman's proof by "A-translation" of the conservative extention of classical over constructive arithmetic for