Cut--free sequent calculus and natural deduction for the tetravalent modal logic

TL;DR

This paper develops a cut-free sequent calculus and a natural deduction system for the tetravalent modal logic, enhancing proof-theoretic properties and providing tools for reasoning within this four-valued modal framework.

Contribution

It introduces a cut-elimination sequent calculus and a natural deduction system for tetravalent modal logic, improving proof-theoretic behavior and reasoning capabilities.

Findings

Original sequent calculus lacks cut-elimination.

A new sequent calculus with cut-elimination is constructed.

A sound and complete natural deduction system is presented.

Abstract

The {\em tetravalent modal logic} ($\cal TML$) is one of the two logics defined by Font and Rius (\cite{FR2}) (the other is the {\em normal tetravalent modal logic} ${\cal TML}^N$) in connection with Monteiro's tetravalent modal algebras. These logics are expansions of the well--known {\em Belnap--Dunn's four--valued logic} that combine a many-valued character (tetravalence) with a modal character. In fact, $\cal TML$ is the logic that preserve degrees of truth with respect to tetravalent modal algebras. As Font and Rius observed, the connection between the logic $\cal TML$ and the algebras is not so good as in ${\cal TML}^N$, but, as a compensation, it has a better proof-theoretic behavior, since it has a strongly adequate Gentzen calculus (see \cite{FR2}). In this work, we prove that the sequent calculus given by Font and Rius does not enjoy the cut--elimination property. Then, using a general method proposed by Avron, Ben-Naim and Konikowska (\cite{Avron02}), we provide a sequent calculus for $\cal TML$ with the cut--elimination property. Finally, inspired by the latter, we present a {\em natural deduction} system, sound and complete with respect to the tetravalent modal logic.