Skip to main content
PRL Project

An Evaluation Semantics for Classical Proofs

by Chetan Murthy

Proceedings of Sixth IEEE Symposium on Logic in Computer Science

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 $\Pi^{0}_{2}$ sentences. We show that Friedman's result is a proof-theoretic version of a semantics-preserving CPS-translation from a nonfunctional programming language (with the "control" (C, a relative of call/cc) operator) back to a functional programming language. We present a sound evaluation semantics for proofs in classical number theory (PA) of such sentences, as a modification the standard semantics for proofs in constructive number theory (HA). Our results soundly extend the proofs-as-programs paradigm to classical logics and to programs with C.

bibTex ref: Mur91

cite link