An evaluation semantics for classical proofs

It is shown 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. The method turns out to be equivalent to H. Friedman´s (Lecture Notes in Mathematics, vol.699, p.21-28, 1978) proof by A -transition of the conservative extension of classical cover constructive arithmetic for II₂⁰ sentences. It is shown that Friedman´s result is a proof-theoretic version of a semantics-preserving CPS-translation from a nonfunctional programming language back to a functional programming language. A sound evaluation semantics for proofs in classical number theory (PA) of such sentences is presented as a modification of the standard semantics for proofs in constructive number theory (HA). The results soundly extend the proofs-as-programs paradigm to classical logics and to programs with the control operator, C