Denotations for Classical Proofs - Preliminary Results

13 years 1 months ago
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.
Philippe de Groote
Added 10 Aug 2010
Updated 10 Aug 2010
Type Conference
Year 1992
Where LFCS
Authors Philippe de Groote
Comments (0)