Paper 5

Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant

Authors: Jørgen Villadsen and Anders Schlichtkrull

Volume 34 (2017)

Abstract

We present a formalization of a so-called paraconsistent logic that avoids the catastrophic explosiveness of inconsistency in classical logic. The paraconsistent logic has a countably innite number of nonclassical truth values. We show how to use the proof assistant Isabelle to formally prove theorems in the logic as well as meta-theorems about the logic. In particular, we formalize a meta-theorem that allows us to reduce the innite number of truth values to a nite number of truth values, for a given formula, and we use this result in a formalization of a small case study.