2016/06/18 by Ken Akiba
Computer Science · Mathematics · #Absurdity #Algebra over a field #Calculus (dental) #Classical logic #Computability, Logic, AI Algorithms #Computer science #Denotational semantics #Dependent type #Discrete mathematics #Domain theory #Lambda calculus #Linguistics #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Logical equivalence #Mathematical proof #Mathematics #Natural deduction #Negation #Normalisation by evaluation #Operational semantics #Philosophy #Programming language #Pure mathematics #Rule of inference #Semantics (computer science) #Sequent #Sequent calculus #Simply typed lambda calculus #Type (biology) #Type theory #Typed lambda calculus #cs.LO
paper · pdf · doi:10.4204/eptcs.213.2
published as EPTCS 213, 2016, pp. 11-23 · In Proceedings CL&C 2016, arXiv:1606.05820
openalex publication_date 2016/06/18 · arxiv created 2016/06/21 · arxiv updated 2016/06/22 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
Classical (or Boolean) type theory is the type theory that allows the type inference σ → \bot) → \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.