Paraconsistent logic, evidence, and justification
Lehman College - CUNY Graduate Center
In a forthcoming paper, Walter Carnielli and Abilio Rodriguez propose a Basic Logic of Evidence (BLE) whose natural deduction rules are thought of as preserving evidence instead of truth. BLE turns out to be equivalent to Nelson’s paraconsistent logic N4, resulting from adding strong negation to Intuitionistic logic without Intuitionistic negation. The Carnielli/Rodriguez understanding of evidence is informal. We provide a formal alternative, using justification logic. First we introduce a modal logic, KX4, in which box-X can be read as asserting there is implicit evidence for X, where we understand evidence to permit contradictions. We show BLE embeds into KX4 in the same way that Intuitionistic logic embeds into S4. Then we formulate a new justification logic, JX4, in which the implicit evidence motivating KX4 is made explicit. KX4 embeds into JX4 via a realization theorem. Thus BLE has both implicit and explicit evidence interpretations in a formal sense.
Lehman College Professor Melvin Fitting received the Herbrand Award of 2012 for his groundbreaking contributions to the field of automated theorem proving, which focuses on getting computer programs to prove logical and mathematical deductions.