Browse Theses

In this thesis, we explore three aspects of the computational content of proofs. These are: a computational interpretation of the metatheory of intuitionistic propositional logic, an extension of this approach to intuitionistic predicate logic, and a computational interpretation of classical sequent proofs.

We begin with a study of the computational aspects of validity, provability, and completeness for intuitionistic propositional logic. We give a constructive proof of completeness of Kripke models for intuitionistic propositional calculus, such that the computational content of the proof is a form of the tableau algorithm. Since the evidence for provability we construct is actually a term in typed $\lambda$-calculus, we can interpret this result as a formal relationship between Kripke semantics and realizability semantics. We also show how a formal proof of the completeness theorem in Nuprl could be used to add the tableau decision procedure for provability to Nuprl's collection of proof techniques via reflection.

We then explore how these results could be generalized to the metatheory of intuitionistic predicate logic. To do this, we develop some machinery for representing infinite Kripke models in type theory using co-inductive types. Although provability in intuitionistic predicate logic is undecidable, we can still prove a constructive theorem in the metatheory which has computational content. We also show that using classical logic in part of the proof does not destroy the computational content of the proof.

Finally, we examine the computational aspects of classical sequent proofs. We show how the interpretation of nonlocal control operators as the computational content of classical axioms allows us to prove a completeness result for intuitionistic predicate logic with a depth-first-search tableau procedure as the computational content of the proof. Using the nonlocal control operator call/cc as the the computational interpretation of the classical axiom (($\varphi\to \perp )\to\varphi )\to\varphi$, we define a method for extracting programs from classical sequent proofs in propositional logic. We give a proof-theoretic account of continuations and their behaviour in this context, and prove a number of properties of the extraction.