Denotations for Classical Proofs - Preliminary Results

This paper addresses the problem of extending the formulae-as-types principle to classical logic. More precisely, we introduce a typed lambda-calculus (-LK ) whose inhabited types are exactly the implicative tautologies of classical logic and whose type assignment system is a classical sequent calculus. Intuitively, the terms of -LK correspond to constructs that are highly non-deterministic. This intuition is made much more precise by providing a simple model where the terms of -LK are interpreted as non-empty sets of (interpretations of) untyped lambda-terms. We also consider the system (-LK + cut) and investigate the relation existing between cut elimination and reduction. Finally, we show how to extend our system in order to take conjunction, disjunction and negation into account.

• Type: Conference
• Year: 1992
• Where: LFCS
• Authors: Philippe de Groote
• Keywords: Artificial Intelligence, Classical Logic, Classical Sequent Calculus, Formulae-as-types Principle, LFCS 1992