Reductio ad contradictionem: an algebraic perspective (Q295913)

Classical logic is two valued and querying a propositional knowledge base about a fact may result in the answers true or false (or no answer at all if no knowledge is available). Real knowledge bases are typically incomplete and may also be inconsistent. To deal explicitly with such states Belnap-Dunn logic has been developed, where in addition to the classical truth values true and false, there are truth values for both (true and false) and none (neither true nor false). Note, we are speaking here about the characterization of a knowledge base and not necessarily of reality. In this context, it is obviously unwanted to use the \textit{ex contradictione quodlibet} rule, since a single inconsistency of the knowledge base would allow to derive anything, even statements about facts which are completely unrelated and about which another part of the knowledge base is unambiguous. This would devalue the knowledge base. Still, proof by contradiction is a powerful proof tool and should not easily be abandoned. In this paper, Belnap-Dunn logic is extended by a negation \(\sim\) that allows for \textit{reductio ad contradictionem} (without going to \textit{ex contradictione quodlibet}), that is, to claim \(\sim p\) means that \(p\) leads to a contradiction. The main part of the paper is an algebraic study of the properties that characterize such an extension of Belnap-Dunn logic making use of de Morgan algebras and varieties of reductio algebras. Furthermore a sequent calculus for the extended logic is presented.