Denotations for Classical Proofs - Preliminary-results
(1992) Lecture Notes in Computer Science — Vol. 620, p. 105-116 (1992)
Files
No attached file found for this publication.
Details
- Authors
- Abstract
- 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.
- Affiliations
Citations
Degroote, P. (1992). Denotations for Classical Proofs - Preliminary-results. Lecture Notes in Computer Science, 620, 105-116. https://hdl.handle.net/2078.5/79960 (Original work published 1992)