A semantic view of classical proofs: type-theoretic, categorical, and denotational characterizations

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 semantic theory of classical proofs based on a variant of Parigot´s λμ-calculus, 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?