AbstractThe tetravalent modal logic ($${\mathcal {TML}}$$
TML
) is one of the two logics defined by Font and Rius (J Symb Log 65(2):481–518, 2000) (the other is the normal tetravalent modal logic$${{\mathcal {TML}}}^N$$
TML
N
) in connection with Monteiro’s tetravalent modal algebras. These logics are expansions of the well-known Belnap–Dunn’s four-valued logic that combine a many-valued character (tetravalence) with a modal character. In fact, $${\mathcal {TML}}$$
TML
is the logic that preserves degrees of truth with respect to tetravalent modal algebras. As Font and Rius observed, the connection between the logic $${\mathcal {TML}}$$
TML
and the algebras is not so good as in $${{\mathcal {TML}}}^N$$
TML
N
, but, as a compensation, it has a better proof-theoretic behavior, since it has a strongly adequate Gentzen calculus (see Font and Rius in J Symb Log 65(2):481–518, 2000). 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 et al. (Log Univ 1:41–69, 2006), we provide a sequent calculus for $${\mathcal {TML}}$$
TML
with the cut-elimination property. Finally, inspired by the latter, we present a natural deduction system, sound and complete with respect to the tetravalent modal logic.