Reductio ad contradictionem: An Algebraic Perspective

We introduce a novel expansion of the four-valued Belnap---Dunn logic by a unary operator representing reductio ad contradictionem and study its algebraic semantics. This expansion thus contains both the direct, non-inferential negation of the Belnap---Dunn logic and an inferential negation akin to the negation of Johansson's minimal logic. We formulate a sequent calculus for this logic and introduce the variety of reductio algebras as an algebraic semantics for this calculus. We then investigate some basic algebraic properties of this variety, in particular we show that it is locally finite and has EDPC. We identify the subdirectly irreducible algebras in this variety and describe the lattice of varieties of reductio algebras. In particular, we prove that this lattice contains an interval isomorphic to the lattice of classes of finite non-empty graphs with loops closed under surjective graph homomorphisms.