Explicit analyses of proof/refutation interaction for constructible falsity and Heyting–Brouwer logic. (2nd October 2020) - Ferguson, Thomas Macaulay
Abstract: Nelson's logic of constructible falsity $N$ and Rauszer's Heyting–Brouwer logic $HB$ are well-known cases of extensions of intuitionistic logic $Int$ enriched with novel connectives. Wansing has suggested that Gödel's provability interpretation of $Int$ can be extended to these systems by pairing the category of formal proofs with a distinct category of formal refutations . In this paper, we extend the framework of Artemov's justification logic to provide explicit analyses of $N$ and $HB$ (and the dual-intuitionistic logic $DualInt$ ) that respect a distinction between proofs and refutations. The application distinguishes the categories by reinterpreting the agents of multiple-agent justification logic as devices that operate exclusively on one or the other category. The analyses reveal that differences between $N$ and $HB$ can be reduced to competing interaction principles characterizing the coordination between proofs and refutations. We conclude by reappraising some of the unusual features of $HB$ in light of the explicit analysis of $HB$ .