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 .