Logic in Computer Science (LICS 1996)

Paper: A semantic view of classical proofs: type-theoretic, categorical, and denotational characterizations (at LICS 1996)

Authors: C.-H. Luke Ong

Abstract

Classical logic is one of the best examples of a mathematical theory that is truly useful to computer science. Hardware and software engineers apply the theory routinely. Yet from a foundational standpoint, there are aspects of classical logic that are problematic. Unlike intuitionistic logic, classical logic is often held to be non-constructive, and so, is said to admit no proof semantics. To draw an analogy in the proofs- as-programs paradigm, it is as if we understand well the theory of manipulation between equivalent specifications (which we do), but have comparatively little foundational insight of the process of transforming one program to another that implements the same specification. This extended abstract outlines a {\em semantic} theory of classical proofs based on a variant of Parigot's $\lambda\mu$-calculus \cite{Par92}, but presented here as a type theory. After reviewing the conceptual problems in the area and the potential benefits of such a theory, we sketch the key steps of our approach in terms of the questions that we have sought to answer: - Syntax: How should one circumscribe a coherent system of classical proofs? Is there a satisfactory Curry-Howard style representation theory? - Categorical characterization: What is the ``boolean algebra'' of classical propositional proofs (as opposed to validity)? What manner of categories characterizes classical proofs the same way that cartesian closed categories capture intuitionistic propositional proofs? - Complete denotational models: Are there good intensional game models of classical logic canonical for the circumscribed proofs? We give an overview of an approach to understand classical propositional proofs based on a Curry-Howard style, type- theoretic presentation of a variant of Parigot's $\lambda\mu$-calculus. The intrinsic notion of equality between proofs is consistent, decidable, congruent, and compatible with cut. We give a categorical characterization of $\lambdamu$, and construct a game model that satisfies a completeness property.

BibTeX

  @InProceedings{Ong-Asemanticviewofclas,
    author = 	 {C.-H. Luke Ong},
    title = 	 {A semantic view of classical proofs: type-theoretic, categorical, and denotational characterizations},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {230-241},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }