Automatic extraction of axiomatizations in terms of two-signed tableaux for finite-valued logics

Abstract

Classical Logic is bivalent in that it admits exactly two truth-values: the true and the false. Many-valued logics, in contrast, allow for the consideration of arbitrarily large classes of truth-values. To export the canonical notion of entailment to the realm of many-valuedness, the trick is to split any such class of truth-values into two classes by saying that some of these values are ‘designated’, and others are not. One might remark then that a shade of bivalence lurks in the distinction between the values that are designated and those that are not. It is known (cf. [2]) that this residual bivalence allows in fact for an alternative, and in many cases even constructively obtainable (cf. [1]), representation of many-valued logics interms of appropriate bivalent semantics. In this paper we will present a first concrete implementation of the method devised in [1] in order to obtain sound and complete classic-like tableau systems for a very comprehensive class of finite-valued logics. The algorithm is implemented in the functional programming language ML, and our program outputs a text file containing the corresponding theory to be processed by Isabelle, a flexible theorem-proving environment in which it is possible to check meta-results and theorems about the logics under scrutiny. The formulation of different many-valued logics under a common ground —two-signed tableau systems— makes it easier to compare properties of these logics and to appreciate the relations between them.