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 $\textsf{N}$ and Rauszer's Heyting–Brouwer logic $\textsf{HB}$ are well-known cases of extensions of intuitionistic logic $\textsf{Int}$ enriched with novel connectives. Wansing has suggested that Gödel's provability interpretation of $\textsf{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 $\textsf{N}$ and $\textsf{HB}$ (and the dual-intuitionistic logic $\textsf{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 $\textsf{N}$ and $\textsf{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 $\textsf{HB}$ in light of the explicit analysis of $\textsf{HB}$ .