An evaluation semantics for classical proofs

Abstract

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/sub 2//sup 0/ 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.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>