Kamide is in America, Moisil and Leitgeb are in Australia
Satoru Niki, Hitoshi Omori
TL;DR
This work analyzes BD+ through two intuitionistic trajectories (American BDi and Australian HYPE), introducing star semantics to provide an Australian-first-order perspective and to relate BD+ to neighboring logics. It develops a N3-style predicate extension, QBDi3, with a robust semantics and axiomatization, and proves soundness and completeness via reductions to MH logic, alongside constructive properties derived from Aczel’s slash. The paper also compares BD+-based systems with related four-valued and connexive variants, clarifying how falsity conditions influence omniscience and double negation shift. Overall, it maps the landscape of BD+-based logics, offering precise translations and semantic tools to compare different negation plans and their consequences for intuitionistic and constructive reasoning.
Abstract
It is not uncommon for a logic to be invented multiple times, hinting at its robustness. This trend is followed also by the expansion BD+ of Belnap-Dunn logic by Boolean negation. Ending up in the same logic, however, does not mean that the semantic interpretations are always the same as well. In particular, different interpretations can bring us to different logics, once the basic setting is moved from a classical one to an intuitionistic one. For BD+, two such paths seem to have been taken; one (BDi) by N. Kamide along the so-called American plan, and another (HYPE) by G. Moisil and H. Leitgeb along the so-called Australian plan. The aim of this paper is to better understand this divergence. This task is approached mainly by (i) formulating a semantics for first-order BD+ that provides an Australian view of the system; (ii) showing connections of the less explored (first-order) BDi with neighbouring systems, including an intermediate logic and variants of Nelson's logics.