On the semantics of classical disjunction

The λμ-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 λμ extended with disjunction. We describe a class of categorical models for the λμ-calculus with each of these disjunctions. Considering the calculus with LK-derived disjunction, λμν, we establish the standard metatheoretic properties and show that a class of continuations models of λμ can be elegantly extended to λμν. Comparing the two forms of disjunction, we show that any model which identifies them collapses to a trivial family of Boolean algebras.