Binary Sequent Calculi for Truth-invariance Entailment of Finite Many-valued Logics

TL;DR

This paper introduces a novel binary sequent calculus and Kripke-like semantics for finite many-valued logics, providing soundness and completeness without relying on traditional matrix-based entailment.

Contribution

It develops a new binary sequent calculus and semantics for finite many-valued logics, transforming them into positive 2-valued multi-modal logic with a unique algebraic and Kripke-style framework.

Findings

Established sound and complete Kripke-like semantics.

Developed a binary sequent calculus for finite many-valued logics.

Connected many-valued logic to positive 2-valued multi-modal logic.

Abstract

In this paper we consider the class of truth-functional many-valued logics with a finite set of truth-values. The main result of this paper is the development of a new \emph{binary} sequent calculi (each sequent is a pair of formulae) for many valued logic with a finite set of truth values, and of Kripke-like semantics for it that is both sound and complete. We did not use the logic entailment based on matrix with a strict subset of designated truth values, but a different new kind of semantics based on the generalization of the classic 2-valued truth-invariance entailment. In order to define this non-matrix based sequent calculi, we transform many-valued logic into positive 2-valued multi-modal logic with classic conjunction, disjunction and finite set of modal connectives. In this algebraic framework we define an uniquely determined axiom system, by extending the classic 2-valued distributive lattice logic (DLL) by a new set of sequent axioms for many-valued logic connectives. Dually, in an autoreferential Kripke-style framework we obtain a uniquely determined frame, where each possible world is an equivalence class of Lindenbaum algebra for a many-valued logic as well, represented by a truth value.