2017/08/19 by Harley Eades, Eades, Harley, Gianluigi Bellin +1
Computer Science · #03B70 #18C50 #68Q55 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1708.05896
openalex publication_date 2017/08/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
One leading question with respect to Bi-intuitionistic logic (BINT) is, what does BINT look like across the three arcs -- logic, typed λ-calculi, and category theory -- of the Curry-Howard-Lambek correspondence? Categorically, BINT can be seen as a mixing of two worlds: the first being intuitionistic logic (IL), which is modeled by a cartesian closed category, and the second being the dual to intuitionistic logic called cointuitionistic logic (coIL), which is modeled by a cocartesian coclosed category. Crolard showed that combining these two categories into the same category results in it degenerating to a poset. However, this degeneration does not occur when both logics are linear. We propose that IL and coIL need to be separated, and then mixed in a controlled way using the modalities from linear logic. This separation can be ultimately achieved by an adjoint formalization of bi-intuitionistic logic. This formalization consists of three worlds instead of two: the first is intuitionistic logic, the second is linear bi-intuitionistic (Bi-ILL), and the third is cointuitionistic logic. They are then related via two adjunctions. The adjunction between IL and ILL is known as a Linear/Non-linear model (LNL model) of ILL, and is due to Benton. However, the dual to LNL models which would amount to the adjunction between coILL and coIL has yet to appear in the literature. In this paper we fill this gap by studying the dual to LNL models which we call dual LNL models. We show that dual LNL models correspond to dual linear categories, the dual to Bierman's linear categories proposed by Bellin. Then we give the definition of bi-LNL models by combining our model with LNL models to obtain a new model of bi-intuitionistic logic. Finally, we give a corresponding sequent calculus, natural deduction, and term assignment for dual LNL models.