Denotations for Classical Proofs - Preliminary-results
P. Degroote · 1992
This paper addresses the problem of extending the formulae-as-types principle to classical logic. More precisely, we introduce a typed lambda-calculus (lambda-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 lambda-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 lambda-LK--> are interpreted as non-empty sets of (interpretations of) untyped lambda-terms. We also consider the system (lambda-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.