On the semantics of classical disjunction (Q5939825): Difference between revisions

The so-called \(\lambda \mu\)-calculus [\textit{M. Parigot},``\(\lambda\mu\)-calculus: an algorithmic interpretation of classical natural deduction'', Lecture Notes Comput. Sci. 624, 190-201 (1992; Zbl 0925.03092)] is an extension of lambda calculus, which (roughly) yields a semantics of proofs for classical logic in absence of disjunction. In \(\lambda\mu\), each type judgement has the form \(\Gamma\vdash t\in A,\Delta\), where \(\Gamma\) is a standard context and \(\Delta\) is a context containing types \textit indexed by labels \textrm \(\alpha,\beta,\ldots\), i.e. formulas of the form \(B^\alpha\), \(C^\beta\), etc. The basic idea is that each judgement of \(\lambda\mu\) has exactly one active formula on the right (the leftmost \(A\) typing \(t\)) and that there are suitable binding operators, \([-]\) and \(\mu\), for realizing the structural rules for the right side of the judgement. The present authors consider the problem of extending Parigot's system with disjunction. In particular, they identify two basic options: one given by the single-conclusioned \(\vee\)-introduction rule of the intuitionistic sequent calculus LJ, the other associated with the corresponding multiple-conclusioned \(\vee\)-rule of the classical Gentzen system LK. The first one gives rise to the calculus \(\lambda\mu\oplus\) and it roughly corresponds to adding sum types of the usual typed lambda calculus to \(\lambda\mu\). The LK-disjunction leads to the extension \(\lambda\mu\nu\) with two binding operators \(\nu\) and \(\langle-\rangle\). Roughly, \(\nu\) models the fact that introducing disjunction on the right promotes an indexed formula \(B^\alpha\) from the context to the active position; \(\langle-\rangle\) corresponds to disjunction elimination. The authors show that both systems are proof-theoretically well-behaved, i.e. they are confluent (any two reducts of a term have a common reduct) and strongly normalizing (all reduction sequences for any term terminate). The central result of the paper is a categorical semantics for \(\lambda\mu\) and its extensions \(\lambda\mu\oplus\) and \(\lambda\mu\nu\), for which soundness and completeness theorems hold. Technically, the difficulty is that the standard interpretation of intuitionistic logic into a bicartesian closed category cannot be extended to classical sequents, as adding classical involutive negation produces collapse to Boolean algebras and a trivial semantics of proofs. The solution adopted by the authors is to use fibrations (for the notion of fibered category, etc., cf. [\textit B. Jacobs, \textrm Categorical logic and type theory, Elsevier, Amsterdam (1999; Zbl 0911.03001)]\ as models of \(\lambda\mu\), with some additional structure in order to interpret the two extensions \(\lambda\mu\oplus\) and \(\lambda\mu\nu\). Following an idea of \textit{M. Hofmann} and \textit{T. Streicher} [``Continuation models are universal for the \(\lambda\mu\)-calculus'', LICS'97, IEEE Press, New York, 387-397 (1997)], the authors also show how to transform continuations (roughly structures modelling change of control during a computation) into \(\lambda\mu\nu\)-structures. In the final section, it is shown that, if \(P\) is a \(\lambda\mu\)-structure, which at the same time interprets \(\vee\) and \( \oplus\), and where the two operations are isomorphic (in each fibre), then each fibre of \(P\) collapses to a Boolean algebra. In logical terms, this means that a structure which identifies the two disjunctions, cannot provide non-trivial semantics of proofs. It is also shown that in every \(\lambda\mu\nu\)-structure we can separate De Morgan's isomorphisms: while \(\neg (A\wedge B)\cong (\neg A\vee \neg B)\) holds, it is not true in general that \(\neg(A\vee B)\cong (\neg A\wedge \neg B)\).