Paper: An evaluation semantics for classical proofs (at LICS 1991)

Authors: Chetan R. Murthy

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₂⁰ 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

BibTeX

  @InProceedings{Murthy-Anevaluationsemanti,
    author = 	 {Chetan R. Murthy},
    title = 	 {An evaluation semantics for classical proofs},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)},
    year =	 {1991},
    month =	 {July}, 
    pages =      {96--107},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }