Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics

TL;DR

This paper develops methods to construct efficient, proof-theoretic tableau systems for finite-valued logics by translating them into bivalent semantics, enabling analytic and linear rule-based proof procedures with polynomial simulation of truth-tables.

Contribution

It introduces a novel framework for representing finite-valued logics via bivalent semantics and constructs uniform, cut-free, and cut-based tableau systems with enhanced proof strategies.

Findings

Standard tableaux can be polynomially simulated by linear rule tableaux.

The framework applies to many non-classical logics.

Proof procedures guarantee termination and are automatizable.

Abstract

The paper is a contribution both to the theoretical foundations and to the actual construction of efficient automatizable proof procedures for non-classical logics. We focus here on the case of finite-valued logics, and exhibit: (i) a mechanism for producing a classic-like description of them in terms of an effective variety of bivalent semantics; (ii) a mechanism for extracting, from the bivalent semantics so obtained, uniform (classically-labeled) cut-free standard analytic tableaux with possibly branching invertible rules and paired with proof strategies designed to guarantee termination of the associated proof procedure; (iii) a mechanism to also provide, for the same logics, uniform cut-based tableau systems with linear rules. The latter tableau systems are shown to be adequate even when restricted to analytic cuts, and they are also shown to polynomially simulate truth-tables, a feature that is not enjoyed by the former standard type of tableau systems (not even in the 2-valued case). The results are based on useful generalizations of the notions of analyticity and compositionality, and illustrate a theory that applies to many other classes of non-classical logics.