A machine-assisted view of paraconsistency

Abstract

For a newcomer, paraconsistent logics can be difficult to grasp. Even experts in logic can find the concept of paraconsistency to be suspicious or misguided, if not actually wrong. The problem is that although they usually have much in common with more familiar logics (such as intuitionistic or classical logic), paraconsistent logics necessarily disagree in other parts of the logical terrain which one might have thought were not up for debate. Thus, one's logical intuitions may need to be recalibrated to work skillfully with paraconsistency. To get started, one should clearly appreciate the possibility of paraconsistent logics and the genuineness of the distinctions to which paraconsistency points. For this purpose, one typically encounters matrices involving more than two truth values to characterize suitable consequence relations. In the eyes of a two-valued skeptic, such an approach might seem dubious. Even a non-skeptic might wonder if there's another way. To this end, to explore the basic notions of paraconsistent logic with the assistance of automated reasoning techniques. Such an approach has merit because by delegating some of the logical work to a machine, one's logical "biases" become externalized. The result is a new way to appreciate that the distinctions to which paraconsistent logic points are indeed genuine. Our approach can even suggest new questions and problems for the paraconsistent logic community.