On the Semantics of Classical Disjunction

Research output: Contribution to journalArticle

Authors

Colleges, School and Institutes

Abstract

The lambda mu -calculus provides a system of realizers for classical free (cf. natural) deduction in the absence of disjunction. We identify two forms of disjunction, one derived from Gentzen's sequent calculus LJ and one from LK, and develop the corresponding metatheory for lambda mu extended with disjunction. We describe a class of categorical models for the lambda mu -calculus with each of these disjunctions. Considering the calculus with LK-derived disjunction, lambda mu, we establish the standard metatheoretic properties and show that a class of continuations models of lambda mu can be elegantly extended to lambda mu nu. Comparing the two forms of disjunction, we show that any model which identifies them collapses to a trivial family of Boolean algebras. (C) 2001 Elsevier Science B.V. All rights reserved.

Details

Original languageEnglish
Pages (from-to)315-338
Number of pages24
JournalJournal of Pure and Applied Algebra
Volume159
Issue number2-3
Publication statusPublished - 24 May 2001