Aspects of the Computational Content of Proofs

Other Titles

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 λ-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 \cc\ as the the computational interpretation of the classical axiom 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.

Journal / Series
Volume & Issue
Date Issued
Cornell University
computer science; technical report
Effective Date
Expiration Date
Union Local
Number of Workers
Committee Chair
Committee Co-Chair
Committee Member
Degree Discipline
Degree Name
Degree Level
Related Version
Related DOI
Related To
Related Part
Based on Related Item
Has Other Format(s)
Part of Related Item
Related To
Related Publication(s)
Link(s) to Related Publication(s)
Link(s) to Reference(s)
Previously Published As
Government Document
Other Identifiers
Rights URI
technical report
Accessibility Feature
Accessibility Hazard
Accessibility Summary
Link(s) to Catalog Record