On the Semantics of Classical Disjunction

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.