Denotational Semantics of the Simplified Lambda-Mu Calculus and a New Deduction System of Classical Type Theory

Ken Akiba
(Virginia Commonwealth University)

Classical (or Boolean) type theory is the type theory that allows the type inference (σ \to \bot) \to \bot => σ (the type counterpart of double-negation elimination), where σ is any type and \bot is absurdity type. This paper first presents a denotational semantics for a simplified version of Parigot's lambda-mu calculus, a premier example of classical type theory. In this semantics the domain of each type is divided into infinitely many ranks and contains not only the usual members of the type at rank 0 but also their negative, conjunctive, and disjunctive shadows in the higher ranks, which form an infinitely nested Boolean structure. Absurdity type \bot is identified as the type of truth values. The paper then presents a new deduction system of classical type theory, a sequent calculus called the classical type system (CTS), which involves the standard logical operators such as negation, conjunction, and disjunction and thus reflects the discussed semantic structure in a more straightforward fashion.

In Ulrich Kohlenbach, Steffen van Bakel and Stefano Berardi: Proceedings Sixth International Workshop on Classical Logic and Computation (CL&C 2016), Porto, Portugal , 23th June 2016, Electronic Proceedings in Theoretical Computer Science 213, pp. 11–23.
Published: 19th June 2016.

ArXived at: https://dx.doi.org/10.4204/EPTCS.213.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org