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

Martín Figallo

(Departamento de Matemática. Universidad Nacional del Sur. Bahía Blanca,
Argentina)

###### Abstract

The tetravalent modal logic ($\cal TML$) is one of the two logics defined by
Font and Rius ([13]) (the other is the normal tetravalent modal logic ${\cal
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, $\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 [13]). 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 ([4]), we provide a sequent calculus for $\cal 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.

##  1 Introduction

The class TMA of tetravalent modal algebras was first considered by Antonio
Monteiro (1978), and mainly studied by I. Loureiro, A.V. Figallo, A. Ziliani
and P. Landini. Later on, J.M. Font and M. Rius were interested in the logics
arising from the algebraic and lattice–theoretical aspects of these algebras.
From Monteiro’s point of view, in the future these algebras would give rise to
a four-valued modal logic with significant applications in Computer Science
(see [13]). Although such applications have not yet been developed, the two
logics considered in [13] are modal expansions of Belnap-Dunn’s four-valued
logic, a logical system that is well–known for the many applications it has
found in several fields. In these logics, the four non-classical epistemic
values emerge: 1 (true and not false), 0 (false and not true), n (neither true
nor false) and b (both true and false). We may think of them as the four
possible ways in which an atomic sentence $P$ can belong to the present state
of information : we were told that (1) $P$ is true (and were not told that $P$
is false); (2) $P$ is false (and were not told that $P$ is true); (3) $P$ is
both true and false (perhaps from different sources, or in different instants
of time); (4) we were not told anything about the truth value of $P$. In this
interpretation, it makes sense to consider a modal-like unary operator
$\square$ of epistemic character, such that for any sentence $P$, the sentence
$\square P$ would mean “the available information confirms that $P$ is true”.
It is clear that in this setting the sentence $\square P$ can only be true in
the case where we have some information saying that $P$ is true and we have no
information saying that $P$ is false, while it is simply false in all other
cases (i.e., lack of information or at least some information saying that $P$
is false, disregarding whether at the same time some other information says
that $P$ is true); that is, on the set $\\{0,{\bf n},{\bf b},1\\}$ of
epistemic values this operator must be defined as $\square 1=1$ and
$\square{\bf n}=\square{\bf b}=\square 0=0$ . This is exactly the algebra that
generates the variety of TMAs.

In [13], Font and Rius studied two logics related to TMAs. One of them is
obtained by following the usual “preserving truth” scheme, taking $\\{1\\}$ as
designated set, that is, $\psi$ follows from $\psi_{1},\dots,\psi_{n}$ in this
logic when every interpretation that sends all the $\psi_{i}$ to $1$ also
sends $\psi$ to $1$. The other logic, denoted by ${\cal TML}$ (the logic we
are interested in), is defined by using the preserving degrees of truth
scheme, that is, $\psi$ follows from $\psi_{1},\dots,\psi_{n}$ when every
interpretation that assigns to $\psi$ a value that is greater or equal than
the value it assigns to the conjunction of the $\psi_{i}$’s. These authors
proved that ${\cal TML}$ is not algebraizable in the sense of Blok and
Pigozzi, but it is finitely equivalential and protoalgebraic. However, they
confirm that its algebraic counterpart is also the class of TMAs: but the
connection between the logic and the algebras is not so good as in the first
logic. As a compensation, this logic has a better proof-theoretic behavior,
since it has a strongly adequate Gentzen calculus (Theorems 3.6 and 3.19 of
[13]).

In [13], it was proved that $\cal TML$ can be characterized as a matrix logic
in terms of two logical matrices, but later, in [9], it was proved that $\cal
TML$ can be determined by a single logical matrix. Besides, taking profit of
the contrapositive implication introduced by A. V. Figallo and P. Landini
([11]), a sound and complete Hilbert-style calculus for this logic was
presented. Finally, the paraconsistent character of $\cal TML$ was also
studied from the point of view of the _Logics of Formal Inconsistency_ ,
introduced by W. Carnielli and J. Marcos in [8] and afterward developed in
[7].

##  2 Preliminaries

Recall that, a De Morgan algebra is a structure $\langle
A,\wedge,\vee,\neg,0\rangle$ such that $\langle A,\wedge,\vee,0\rangle$ is a
bounded distributive lattice and $\neg$ is a De Morgan negation, i.e., an
involution that additionally satisfies De Morgan’s laws: for every $a,b\in A$

$\neg\neg a=a$ $\neg(a\vee b)=\neg a\wedge\neg b.$

A tetravalent modal algebra (TMA) is an algebra $\mathbb{A}=\langle
A,\wedge,\vee,\neg,\square,0\rangle$ of type $(2,2,1,1,0)$ such that its non-
modal reduct $\langle A,\wedge,\vee,\neg,0\rangle$ is a De Morgan algebra and
the unary operation $\square$ satisfies, for all $a\in A$, the two following
axioms:

$\square a\wedge\neg a=0,$ $\neg\square a\wedge a=\neg a\wedge a.$

Every TMA $\mathbb{A}$ has a top element $1$ which is defined as $\neg 0$.
These algebras were studied mainly by I. Loureiro ([14]), and also by A. V.
Figallo, P. Landini ([11]) and A. Ziliani, at the suggestion of the late A.
Monteiro (see [13]). The class of all tetravalent modal algebras constitute a
variety which is denoted by TMA. Let $M_{4}=\\{0,{\bf n},{\bf b},1\\}$ and
consider the lattice given by the following Hasse diagram

$1$$\bf n$$\bf b$$0$

This is a well-known lattice and it is called ${\bf L4}$ (See [1], pg. 516.)
Then, TMA is generated by the above four–element lattice enriched with two
unary operators $\neg$ and $\square$ given by $\neg{\bf n}={\bf n}$, $\neg{\bf
b}={\bf b}$, $\neg 0=1$ and $\neg 1=0$ and the unary operator $\square$ is
defined as: $\square{\bf n}=\square{\bf b}=\square 0=0$ and $\square 1=1$ (see
[13]). This tetravalent modal algebra, denoted by $\mathfrak{M}_{4m}$, has two
prime filters, namely, $F_{\tiny\mbox{\bf n}}=\\{{\bf n},1\\}$ and
$F_{\tiny\mbox{\bf b}}=\\{{\bf b},1\\}$. As we said, $\mathfrak{M}_{4m}$
generates the variety ${\bf TMA}$, i.e., an equation holds in every TMA iff it
holds in $\mathfrak{M}_{4m}$.

###### Lemma 2.1

(See [13]) In every TMA $\mathbb{A}$ and for all $a,b\in A$ the following
hold:
(i) $\neg\square a\vee a=1$, (viii) $\square\square a=\square a$, (ii)
$\square a\vee\neg a=a\vee\neg a$, (ix) $\square(a\wedge b)=\square
a\wedge\square b$, (iii) $\square a\vee\neg\square a=1$, (x)
$\square(a\vee\square b)=\square a\vee\square b$, (iv) $\square
a\wedge\neg\square a=0$, (xi) $\square\neg\square a=\neg\square a$ (v)
$\square a\leq a$, (xii) $a\wedge\square\neg a=0$, (vi) $\square 1=1$, (xiii)
$\square(\square a\wedge\square b)=\square a\wedge\square b$ (vii) $\square
0=0$, (xiv) $\square(\square a\vee\square b)=\square a\vee\square b$

The next proposition will be needed in what follows.

###### Proposition 2.2

Let $\mathbb{A}$ be a TMA. If $x\leq y\vee z$ and $x\wedge\neg z\leq y$, then
$x\leq y\vee\square z$, for every $x,y,z\in A$.

Proof.  It is a routine task to check that the assertion holds in
$\mathfrak{M}_{4m}$. The fact that $\mathfrak{M}_{4m}$ generates the variety
${\bf TMA}$ completes the proof. $\boldsymbol{\blacksquare}$

Let $\mathscr{L}=\\{\vee,\wedge,\neg,\square\\}$ be a propositional language.
From now on, we shall denote by $\mathfrak{Fm}=\langle
Fm,\wedge,\vee,\neg,\square,\bot\rangle$ the absolutely free algebra of type
(2,2,1,1,0) generated by some denumerable set of variables. We denote by $Fm$
the set of sentential formulas, and we shall refer to them by lowercase Greek
letters $\alpha,\beta,\gamma,\dots$ and so on; and we shall denote finite sets
of formulas by uppercase Greek letters $\Gamma,\Delta,$ etc.

###### Definition 2.3

The tetravalent modal logic ${\cal TML}$ defined over $\mathfrak{Fm}$ is the
propositional logic $\langle Fm,\models_{{\cal TML}}\rangle$ given as follows:
for every finite set $\Gamma\cup\\{\alpha\\}\subseteq Fm$,
$\Gamma\models_{\cal TML}\alpha$ if and only if, for every $\mathbb{A}\in{\bf
TMA}$ and for every $h\in Hom(\mathfrak{Fm},\mathbb{A})$,
$\bigwedge\\{h(\gamma)\ :\ \gamma\in\Gamma\\}\leq h(\alpha)$. In particular,
$\emptyset\models_{\cal TML}\alpha$ if and only if $h(\alpha)=1$ for every
$\mathbb{A}\in{\bf TMA}$ and for every $h\in Hom(\mathfrak{Fm},\mathbb{A})$.

###### Remark 2.4

Observe that, if $h\in Hom(\mathfrak{Fm},\mathbb{A})$ for any
$\mathbb{A}\in{\bf TMA}$, we have that $h(\bot)=0$. This follows from the fact
that $\bot$ is the $0$-ary operation in $\mathfrak{Fm}$, $0$ is the $0$-ary
operation in $\mathbb{A}$ and the definition of homomorphism (in the sense of
universal algebra).

Let ${\cal M}=\langle{\cal T},{\cal D},{\cal O}\rangle$ be a logical matrix
for $\mathscr{L}$, that is, ${\cal T}$ is a finite, non-empty set of truth
values, ${\cal D}$ is a non-empty proper subset of ${\cal T}$, and ${\cal O}$
includes a $k$-ary function $\hat{f}:{\cal T}^{k}\to{\cal T}$ for each $k$-ary
connective $f\in\mathscr{L}$. Recall that, a valuation in ${\cal M}$ is a
function $v:Fm\to{\cal T}$ such that

$v(f(\psi_{1},\dots,\psi_{k}))=\hat{f}(v(\psi_{1}),\dots,v(\psi_{k}))$

for each $k$-ary connective $f$ and all $\psi_{1},\dots,\psi_{k}\in Fm$. A
formula $\alpha\in Fm$ is satisfied by a given valuation $v$, in symbols
$v\models\alpha$, if $v(\alpha)\in{\cal D}$. Let $\Gamma,\Delta\subseteq Fm$.
We say that the $\Delta$ is consequence of $\Gamma$, denoted
$\Gamma\models_{\cal M}\Delta$, iff for every valuation $v$ in ${\cal M}$,
either $v$ does not satisfy some formula in $\Gamma$ or $v$ satisfies some
formula in $\Delta$.
J. M. Font and M. Rius proved in [13] that the tetravalent modal logic $\cal
TML$ is a matrix logic defined in terms of two logical matrices. But later, M.
E. Coniglio and M. Figallo proved in [9] that $\cal TML$ can be characterized
as a matrix logic in terms of a single logical matrix. Indeed, let ${\cal
M}_{4}=\langle{\cal T},{\cal D},{\cal O}\rangle$ be the matrix where the set
of truth values is ${\cal T}=\\{0,{\bf n},{\bf b},1\\}$, the set of designated
values is ${\cal D}=\\{{\bf b},1\\}$ and ${\cal
O}=\\{\tilde{\vee},\tilde{\wedge},\tilde{\neg},\tilde{\square}\\}$ where
$\tilde{\vee},\tilde{\wedge}:{\cal T}^{2}\to{\cal T}$ and
$\tilde{\neg},\tilde{\square}:{\cal T}\to{\cal T}$ are defined as
$x\tilde{\vee}y=\mathop{\rm Sup}\nolimits\\{x,y\\}$,
$x\tilde{\wedge}y=\mathop{\rm Inf}\nolimits\\{x,y\\}$ (here we are assuming
that the elements of ${\cal T}$ are ordered as in the lattice $M_{4}$).

$x$ | $\tilde{\neg}x$ | $\tilde{\square}x$
---|---|---
0 | 1 | 0
n | n | 0
b | b | 0
1 | 0 | 1

then,

###### Proposition 2.5

([9]) $\cal TML$ is sound and complete w.r.t. ${\cal M}_{4}$.

Therefore, given $\Gamma$ and $\Delta$ sets of formulas, $\Delta$ is
consequence of $\Gamma$ in ${\cal TML}$, denoted $\Gamma\models_{\cal
TML}\Delta$, iff for every valuation $v$ in ${\cal M}_{4}$, either $v$ does
not satisfy some formula in $\Gamma$ or $v$ satisfies some formula in
$\Delta$. If $\Delta$ is a set with exactly one element, we recover the
consequence relation given in Definition 2.3.

In order to characterize $\cal TML$ syntactically, that is, by means of a
deductive system, J. M. Font and M. Rius introduced in [13] the sequent
calculus $\mathfrak{G}$. The sequent calculus $\mathfrak{G}$ is
single–conclusion, that is, it deals with sequents of the form
$\Delta\Rightarrow\alpha$ such that $\Delta\cup\\{\alpha\\}$ is a finite
subset of $Fm$. The axioms and rules of $\mathfrak{G}$ are the following:

Axioms

$\mbox{(Structural axiom) \, }\displaystyle{\alpha\Rightarrow\alpha}\hskip
56.9055pt\mbox{(Modal axiom) \, }{\Rightarrow\alpha\vee\neg\square\alpha}$

Structural rules

$\mbox{(Weakening) \,
}\displaystyle\frac{\Delta\Rightarrow\alpha}{\Delta,\beta\Rightarrow\alpha}\hskip
56.9055pt\mbox{(Cut) \, }\displaystyle\frac{\Delta\Rightarrow\alpha\hskip
14.22636pt\Delta,\alpha\Rightarrow\beta}{\Delta\Rightarrow\beta}$

Logic rules

$\mbox{($\wedge\Rightarrow$) \,
}\displaystyle\frac{\Delta,\alpha,\beta\Rightarrow\gamma}{\Delta,\alpha\wedge\beta\Rightarrow\gamma}\hskip
56.9055pt\mbox{($\Rightarrow\wedge$) \,
}\displaystyle\frac{\Delta\Rightarrow\alpha\hskip
14.22636pt\Delta\Rightarrow\beta}{\Delta\Rightarrow\alpha\wedge\beta}$

$\mbox{($\vee\Rightarrow$) \,
}\displaystyle\frac{\Delta,\alpha\Rightarrow\gamma\hskip
14.22636pt\Delta,\beta\Rightarrow\gamma}{\Delta,\alpha\vee\beta\Rightarrow\gamma}$

$\mbox{($\Rightarrow\vee$)${}_{1}$ \,
}\displaystyle\frac{\Delta\Rightarrow\alpha}{\Delta\Rightarrow\alpha\vee\beta}\hskip
56.9055pt\mbox{($\Rightarrow\vee$)${}_{2}$ \,
}\displaystyle\frac{\Delta\Rightarrow\beta}{\Delta\Rightarrow\alpha\vee\beta}$

$\mbox{($\neg$) \,
}\displaystyle\frac{\alpha\Rightarrow\beta}{\neg\beta\Rightarrow\neg\alpha}\hskip
56.9055pt\mbox{($\bot$)
\,}\frac{\Delta\Rightarrow\bot}{\Delta\Rightarrow\alpha}$

$\mbox{($\neg\neg\Rightarrow$) \,
}\displaystyle\frac{\Delta,\alpha\Rightarrow\beta}{\Delta,\neg\neg\alpha\Rightarrow\beta}\hskip
56.9055pt\mbox{($\Rightarrow\neg\neg$)}\,\frac{\Delta\Rightarrow\alpha}{\Delta\Rightarrow\neg\neg\alpha}$

$\mbox{($\square\Rightarrow$) \,
}\displaystyle\frac{\Delta,\alpha,\neg\alpha\Rightarrow\beta}{\Delta,\alpha,\neg\square\alpha\Rightarrow\beta}\hskip
56.9055pt\mbox{($\Rightarrow\square$)}\,\frac{\Delta\Rightarrow\alpha\wedge\neg\alpha}{\Delta\Rightarrow\alpha\wedge\neg\square\alpha}$

The notion of derivation in the sequent calculus $\mathfrak{G}$ is the usual.
Besides, for every finite set $\Gamma\cup\\{\varphi\\}\subseteq Fm$, we write
$\Gamma\vdash_{\mathfrak{G}}\varphi$ iff the sequent
$\Gamma\Rightarrow\varphi$ has a derivation in $\mathfrak{G}$. We say that the
sequent $\Gamma\Rightarrow\varphi$ is provable iff there exists a derivation
for it in $\mathfrak{G}$.
J. M. Font and M. Rius proved in [13] that $\mathfrak{G}$ is sound and
complete with respect to the tetravalent modal logic $\cal TML$.

###### Theorem 2.6

(Soundness and Completeness, [13]) For every finite set
$\Gamma\cup\\{\alpha\\}\subseteq Fm$,

$\Gamma\models_{\cal TML}\alpha\ \ \textrm{ if and only if}\ \
\Gamma\vdash_{\mathfrak{G}}\alpha.$

Moreover,

###### Proposition 2.7

([13]) An arbitrary equation $\psi\approx\varphi$ holds in every TMA iff
$\psi\dashv\vdash_{\mathfrak{G}}\varphi$ (that is,
$\psi\vdash_{\mathfrak{G}}\varphi$ and $\varphi\vdash_{\mathfrak{G}}\psi$).

As a consequence of it we have that:

###### Corollary 2.8

([13])

  * (i)

The equation $\psi\approx 1$ holds in every TMA iff
$\vdash_{\mathfrak{G}}\psi$.

  * (ii)

For any $\psi,\varphi\in Fm$, $\psi\vdash_{\mathfrak{G}}\varphi$ iff
$h(\psi)\leq h(\varphi)$ for every $h\in Hom(\mathfrak{Fm},\mathbb{A})$, for
every $\mathbb{A}\in{\bf TMA}$.

##  3 $\mathfrak{G}$ does not admit a cut–elimination theorem

Corollary 2.8 is a powerful tool to determine whether a given sequent of
$\mathfrak{G}$ is provable or not. For instance,

###### Proposition 3.1

In $\mathfrak{G}$ we have that the sequent
$\neg\square\alpha\Rightarrow\alpha$ is provable iff the sequent
$\Rightarrow\alpha$ is provable.

Proof.  Indeed, suppose that the sequent $\neg\square\alpha\Rightarrow\alpha$
is provable in $\mathfrak{G}$. Then, $h(\neg\square\alpha)\leq h(\alpha)$, for
all $h\in Hom(\mathfrak{Fm},\mathfrak{M}_{4m})$. But, considering all the
cases, we must have that $h(\neg\square\alpha)=0$ and $h(\alpha)=1$, for all
$h$, and therefore the sequent $\Rightarrow\alpha$ is provable in
$\mathfrak{G}$. The converse is straightforward. $\boldsymbol{\blacksquare}$

Recall that a rule of inference is admissible in a formal system if the set of
theorems of the system is closed under the rule; and a rule is said to be
derivable in the same formal system if its conclusion can be derived from its
premises using the other rules of the system.

A well–known rule for readers familiar with modal logic is the Rule of
Necessitation, which states that if $\varphi$ is a theorem, so is
$\square\varphi$. Formally,

$\mbox{(Nec) \,}\frac{\Rightarrow\varphi}{\Rightarrow\square\varphi}$

Then, we have that:

###### Lemma 3.2

The Rule of Necessitation is admissible in $\mathfrak{G}$.

Proof.  From Corollary 2.8 and considering the algebra $\mathfrak{M}_{4m}$.
$\boldsymbol{\blacksquare}$

From the above lemma, we can obtain a proof of
$\Rightarrow\square(\alpha\vee\neg\square\alpha)$ in $\mathfrak{G}$, for any
$\alpha\in Fm$. Let $\Pi$ be a proof of
$\Rightarrow\square(\alpha\vee\neg\square\alpha)$ and let ($r$) be the last
rule application in $\Pi$. Clearly, $\Pi$ make use of more than one rule since
$\square(\alpha\vee\neg\square\alpha)$ is not an axiom. Then, we have the
following two cases:

Case 1: $\Pi$ is of the form $\cdot$ $\cdot$ $\cdot$
$\Gamma\Rightarrow\varphi$ (r)
$\Rightarrow\square(\alpha\vee\neg\square\alpha)$ Case 2: $\Pi$ is of the form
$\cdot$ $\cdot$ $\cdot$
$\Gamma_{1}\Rightarrow\varphi_{1}\,\,\,\,\Gamma_{2}\Rightarrow\varphi_{2}$ (r)
$\Rightarrow\square(\alpha\vee\neg\square\alpha)$

In case 1, ($r$) has just one premise, and therefore it can be: ($\bot$),
weakening, ($\wedge\Rightarrow$), ($\vee\Rightarrow$), ($\Rightarrow\vee$),
($\neg$), ($\neg\neg\Rightarrow$), ($\Rightarrow\neg\neg$),
($\square\Rightarrow$) or ($\Rightarrow\square$). In the case of ($\bot$), the
only possibility is having $\Gamma=\emptyset$. But this would imply that the
sequent $\Rightarrow\bot$ is provable, which contradicts the soundness of
$\mathfrak{G}$. Thus, this case is discarded. On the other hand, none of the
other rules above has the structure of ($r$), so they are also discarded.
Therefore, $\pi$ is of the form depicted in Case 2. Then, ($r$) must be one of
the following: the cut rule, ($\Rightarrow\wedge$) or ($\vee\Rightarrow$). It
is clear that ($r$) cannot be ($\Rightarrow\wedge$) nor ($\vee\Rightarrow$).
Consequently, ($r$) must be the cut rule.

We have just proved, therefore, the following assertion.

###### Proposition 3.3

Every proof of $\Rightarrow\square(\alpha\vee\neg\square\alpha)$ in
$\mathfrak{G}$ uses the cut rule.

Moreover, we have that:

###### Lemma 3.4

For every $\varphi\in Fm$ such that $\Rightarrow\varphi$ is provable in
$\mathfrak{G}$, we have that $\Rightarrow\square\varphi$ is provable in
$\mathfrak{G}$; and every proof of $\Rightarrow\square\varphi$ in
$\mathfrak{G}$ makes use of the cut rule.

Consequently,

###### Theorem 3.5

$\mathfrak{G}$ does not admit cut–elimination.

##  4 The general method of Avron, Ben-Naim and Konikowska

In [3], A. Avron and B. Konikowska use the Rasiowa-Sikorski decomposition
methodology to get sound and complete proof systems employing $n$-sequents for
all propositional logics based on non-deterministic matrices. Later, these
same authors jointly with J. Ben-Naim ([4]) presented a general method to
transform a given sound and complete $n$-sequent proof system into an
equivalent sound and complete system of ordinary two-sided sequents (for
languages satisfying a certain minimal expressiveness condition). In this
section we shall recall both methods considering ordinary (deterministic)
matrices.

In what follows, $\mathscr{L}$ is a propositional language and let (in this
section) $\mathfrak{Fm}$ be the absolutely free algebra over $\mathscr{L}$
generated by some denumerable set of variables, with underlying set (of
formulas) $Fm$. Let ${\cal M}=\langle{\cal T},{\cal D},{\cal O}\rangle$ be a
logical matrix for $\mathscr{L}$. As we said, a valuation $v$ in ${\cal M}$
satisfies a given formula $\alpha$ if $v(\alpha)\in{\cal D}$. A sequent
$\Gamma\Rightarrow\Delta$ is satisfied by the valuation $v$, in symbols
$v\models\,\Gamma\Rightarrow\Delta$, if either $v$ does not satisfy some
formula in $\Gamma$ or $v$ satisfies some formula in $\Delta$. A sequent is
valid if it is satisfied by all valuations.

Now, suppose that ${\cal T}=\\{t_{0},\dots,t_{n-1}\\}$, where $n\geq 2$, and
${\cal D}=\\{t_{d},\dots,t_{n-1}\\}$, where $1\leq d\leq n-1$.

###### Definition 4.1

(see [3]) An $n$–sequent over $\mathscr{L}$ is an expression

$\Gamma_{0}\mid\dots\mid\Gamma_{n-1}$

where, for each $i$, $\Gamma_{i}$ is a finite set of formulas. A valuation $v$
satisfies the $n$–sequent $\Gamma_{0}\mid\dots\mid\Gamma_{n-1}$ iff there
exists $i$, $0\leq i\leq n-1$ and $\psi\in\Gamma_{i}$ such that
$v(\psi)=t_{i}$. An $n$–sequent is valid if it is satisfied by every valuation
$v$.

Note that, a valuation $v$ satisfies an ordinary sequent
$\Gamma\Rightarrow\Delta$ iff $v$ satisfies the $n$–sequent
$\Gamma_{1}\mid\dots\mid\Gamma_{n-1}$ where $\Gamma_{i}=\Gamma$ for all $0\leq
i\leq d-1$ and $\Gamma_{j}=\Delta$ for all $d\leq j\leq n-1$ .

An alternative presentation of $n$-sequents is by means of sets of signed
formulas. A signed formula over the language $\mathscr{L}$ and ${\cal T}$, is
an expression of the form

$t_{i}:\psi$

where $t_{i}\in{\cal T}$ and $\psi\in Fm$. A valuation $v$ satisfies the
signed formula $t_{i}:\psi$ iff $v(\psi)=t_{i}$. If ${\cal U}\subseteq{\cal
T}$ and $\Gamma\subseteq Fm$, we denote by ${\cal U}:\Gamma$ the set

${\cal U}:\Gamma=\\{t:\alpha\mid t\in{\cal U},\alpha\in\Gamma\\}$

If ${\cal U}=\\{t\\}$, we write $t:\Gamma$ instead of $\\{t\\}:\Gamma$. A
valuation satisfies the set of signed formulas ${\cal U}:\Gamma$ if it
satisfies some signed formula of ${\cal U}:\Gamma$; and we say that ${\cal
U}:\Gamma$ is valid if it is satisfied by every valuation $v\in{\cal V}$. It
is clear that, the $n$–sequent $\Gamma_{0}\mid\dots\mid\Gamma_{n-1}$ is valid
iff the set of signed formulas $\bigcup\limits_{i=0}^{n-1}t_{i}:\Gamma_{i}$ is
valid.

A. Avron and B. Konikowska developed in [3] a generic $n$-sequent system for
any logic based on an $n$-valued matrix. Consider the $n$-valued matrix ${\cal
M}=\langle{\cal T},{\cal D},{\cal O}\rangle$ and let $SF_{\cal M}$ the system
defined as follows: for $\Omega$ and $\Omega^{\prime}$ sets of signed formulas

  * •

Axioms: ${\cal T}:\alpha$

  * •

Structural rules:  Weakening:

$\displaystyle\frac{\Omega}{\Omega^{\prime}}\hskip 8.5359pt\mbox{ in case
}\hskip 5.69046pt\Omega\subseteq\Omega^{\prime}$

  * •

Logical rules:  for each $k$-ary connective $f$ and every
$(a_{1},\dots,a_{k})\in{\cal T}^{k}$

$\displaystyle\frac{\Omega,a_{1}:\alpha_{1}\,\,\dots\,\,\Omega,a_{k}:\alpha_{k}}{\Omega,\hat{f}(a_{1},\dots,a_{k}):f(\alpha_{1},\dots,\alpha_{k})}$

###### Theorem 4.2

([3]) The system $SF_{\cal M}$ is sound and complete w.r.t. the matrix ${\cal
M}$

Let $Fm_{p}$ be the set of all formulas of $Fm$ that have $p$ as their only
propositional variable, i.e., $Fm_{p}=\\{\alpha\in Fm:Var(\alpha)=\\{p\\}\\}$.
Let ${\cal M}=\langle{\cal T},{\cal D},{\cal O}\rangle$ be a logical matrix
and denote by ${\cal N}$ the set ${\cal T}\setminus{\cal D}$.

###### Definition 4.3

([4]) The language $\mathscr{L}$ is sufficiently expressive for ${\cal M}$ iff
for any $i$, $0\leq i\leq n-1$ there exist natural numbers $l_{i},m_{i}$ and
formulas $\alpha_{j}^{i},\beta_{k}^{i}\in Fm_{p}$, for $1\leq j\leq l_{i}$ and
$1\leq k\leq m_{i}$ such that for any valuation $v$, the following conditions
hold:
(i) $\alpha_{1}^{i}=p$ if $t_{i}\in{\cal N}$ and $\beta_{1}^{i}=p$ if
$t_{i}\in{\cal D}$,
(ii) For $\varphi\in Fm$ and $t_{i}\in{\cal T}$

$v(\varphi)=t_{i}\,\Leftrightarrow\
v(\alpha_{1}^{i}[p/\varphi]),\dots,v(\alpha_{l_{i}}^{i}[p/\varphi])\in{\cal
N}\,and\,v(\beta_{1}^{i}[p/\varphi]),\dots,v(\alpha_{m_{i}}^{i}[p/\varphi])\in{\cal
D}$

where $\alpha_{j}^{i}[p/\varphi]$ ($\beta_{k}^{i}[p/\varphi]$) is the formula
obtained by the substitution of $p$ by $\varphi$ in $\alpha_{j}^{i}$
($\beta_{k}^{i}$).

Note that, as it is mentioned in [4], condition (i) above is not really
limiting, since given $\alpha_{j}^{i},\beta_{k}^{i}$ satisfying (ii), we can
simply add to them the necessary formula $p$ without violating (ii). Condition
(i) will only be used for a backward translation from ordinary sequents to
$n$-sequents, and will be disregarded otherwise.

If $\Gamma$ is a set of formulas and $\alpha\in Fm_{p}$, we denote by
$\alpha[p/\Gamma]$ the set

$\alpha[\Gamma]=\\{\alpha[p/\gamma]\mid\gamma\in\Gamma\\}$

The method is based on replacing each $n$-sequent by a semantically equivalent
set of two-sided sequents.

Let $\mathscr{L}$ be a sufficiently expressive language and for $0\leq i\leq
n-1$ let $l_{i}$, $m_{i}$, $\alpha_{j}^{i}$ and $\beta_{k}^{i}$ as in
Definition 4.3. Consider the $n$–sequent
$\Sigma=\Gamma_{0}\mid\dots\mid\Gamma_{n-1}$ over $\mathscr{L}$. A partition
$\pi$ of the $n$–sequent $\Sigma$ is a tuple $\pi=(\pi_{0},\dots,\pi_{n-1})$
such that, for every $i$, $\pi_{i}$ is a partition of the set $\Gamma_{i}$ of
the form:

$\pi_{i}=\\{\Gamma^{\prime}_{ij}\mid 1\leq j\leq
l_{i}\\}\cup\\{\Gamma^{\prime\prime}_{ik}\mid 1\leq k\leq m_{i}\\}$

Note that $\pi_{i}$ is not a partition in the usual sense, since its
components are allowed to be empty. Besides, observe that the number of sets
in this partition is exactly the number of formulas corresponding to $i$ in
Definition 4.3.

Then, given a partition $\pi$ of the $n$-sequent $\Sigma$, we define the two-
sided sequent $\Sigma_{\pi}$ determined by $\Sigma$ and the partition $\pi$,
as follows:

$\bigcup\limits_{j=0}^{l_{0}}\alpha_{j}^{0}[\Gamma^{\prime}_{0j}],\dots,\bigcup\limits_{j=n-1}^{l_{n-1}}\alpha_{j}^{n-1}[\Gamma^{\prime}_{(n-1)j}]\,\Rightarrow\,\bigcup\limits_{k=0}^{m_{0}}\beta_{k}^{0}[\Gamma^{\prime\prime}_{0k}],\dots,\bigcup\limits_{k=n-1}^{m_{n-1}}\beta_{k}^{n-1}[\Gamma^{\prime\prime}_{(n-1)k}]$

Let $\Pi$ be the set of all partitions of the $n$–sequent $\Sigma$. Then, the
set $TWO(\Sigma)$ is defined as follows:

$TWO(\Sigma)=\\{\Sigma_{\pi}\mid\pi\in\Pi\\}$

###### Theorem 4.4

([4]) Let $\Sigma$ be an $n$–sequent over $\mathscr{L}$ and $v$ a valuation.
Then, $v$ satisfies $\Sigma$ iff $v$ satisfies $\Sigma^{\prime}$, for every
$\Sigma^{\prime}\in TWO(\Sigma)$.

###### Definition 4.5

([4]) Let ${\cal C}$ be an $n$–sequent calculus over $\mathscr{L}$. Then, let
$TWO({\cal C})$ the (ordinary) sequent calculus over $\mathscr{L}$ given by:

  * Axioms: $TWO(A)$, for all axiom $A$ of $\cal C$,

  * Inference rules: $\displaystyle\frac{TWO(S)}{\Sigma^{\prime}}$, where $S$ is a finite set of $n$-sequents, $R$ is one $n$-sequent such that $\displaystyle\frac{S}{R}$ is a rule in $\cal C$ and $\Sigma^{\prime}\in TWO(R)$.

Then,

###### Theorem 4.6

([4]) If an $n$–sequent $\Sigma$ is provable in $\cal C$, then each two-sided
sequent $\Sigma^{\prime}\in TWO(\Sigma)$ is provable in $TWO({\cal C})$.

###### Theorem 4.7

([4]) Let $\mathscr{L}$ be a sufficiently expressive language for ${\cal M}$,
and let $\cal C$ be a sound and complete sequent calculus w.r.t $\cal M$.
Then, $TWO({\cal C})$ is sound and complete w.r.t. ${\cal M}$.

The analogue of the cut rule for ordinary sequents is the following
generalized cut rule for sets of signed formulas:

$\displaystyle\frac{\Omega\cup\\{i:\alpha\,|\,i\in I\\}\hskip
14.22636pt\Omega\cup\\{j:\alpha\,|\,j\in J\\}}{\Omega}\hskip 14.22636pt\mbox{
for }I,J\subseteq{\cal V},I\cap J=\emptyset$

###### Theorem 4.8

([4]) Under the conditions of Theorem 4.7, the cut rule is admissible in
$TWO({\cal C})$. In particular, if $\cal C$ is obtained by the method of [3],
then the cut rule is admissible in $TWO({\cal C})$.

As it was observed in [4], the $n$-sequent calculi obtained using the above
general method are hardly optimal (the same is true for the two-sided
calculi). We can use the three general streamlining principles from [3] to
reduce the calculi to a more compact form. The three streamlining principles
are: Principle 1: deleting a derivable rule, Principle 2: simplifying a rule
by replacing it with one with weaker premises, and Principle 3: combining two
context–free rules with the same conclusion into one. Recall that a rule $R$
is context-free if whenever $\frac{\phi_{1}\dots\phi_{n}}{\Sigma}$ is a valid
application of $R$, and $\Sigma^{\prime}$ is a set of signed formulas, then
$\frac{\phi_{1}\cup\Sigma^{\prime}\dots\phi_{n}\cup\Sigma^{\prime}}{\Sigma\cup\Sigma^{\prime}}$
is also a valid application of $R$. A rule $R$ of an ordinary two–sided
sequent calculus is a context–free if
$\displaystyle\frac{\Gamma_{1}\Rightarrow\Delta_{1},\dots,\Gamma_{k}\Rightarrow\Delta_{k}}{\Gamma\Rightarrow\Delta}$
is a valid application of $R$, then
$\displaystyle\frac{\Gamma_{1},\Gamma^{\prime}\Rightarrow\Delta_{1},\Delta^{\prime},\dots,\Gamma_{k},\Gamma^{\prime}\Rightarrow\Delta_{k},\Delta^{\prime}}{\Gamma,\Gamma^{\prime}\Rightarrow\Delta,\Delta^{\prime}}$
is also a valid application of $R$, where $\Gamma^{\prime}$ and
$\Delta^{\prime}$ are finite sets of formulas.
Of these three, the first and the third decrease the number of rules, while
the second simplifies a rule by decreasing the number of its premises.

It is worth mentioning that applying Principles 1–3 preserves the cut-
elimination property since cut-elimination is obtained via the completeness
result and the principles are designed to retain completeness.

##  5 Cut–free sequent calculus for ${\cal TML}$

Now, we shall use the method exhibited in Section 4 to develop a $4$-sequent
calculus for $\cal TML$. In this case, we shall use its alternative
presentation provided by sets of $4$-signed formulas.

Let ${\cal SF}_{4}$ be $4$-sequent calculus given by: for $\alpha,\beta\in
Fm$, $\Omega$ and $\Omega^{\prime}$ arbitrary sets of signed formulas

Axioms: $\\{0:\alpha,{\bf n}:\alpha,{\bf b}:\alpha,n:\alpha\\}$.

Structural rules: Weakening.

$\displaystyle\frac{\Omega}{\Omega^{\prime}}\hskip 8.5359pt\mbox{ in case
}\hskip 5.69046pt\Omega\subseteq\Omega^{\prime}$

Logical rules: for $i,j\in M_{4}$

$\mbox{($\vee_{ij}$) \, }\displaystyle\frac{\Omega,i:\alpha\hskip
28.45274pt\Omega,j:\beta}{\Omega,\mathop{\rm
Sup}\nolimits\\{i,j\\}:\alpha\vee\beta}\hskip 71.13188pt\mbox{($\wedge_{ij}$)
\, }\displaystyle\frac{\Omega,i:\alpha\hskip
28.45274pt\Omega,j:\beta}{\Omega,\mathop{\rm
Inf}\nolimits\\{i,j\\}:\alpha\wedge\beta}$

$\mbox{($\neg_{0}$) \,
}\displaystyle\frac{\Omega,0:\alpha}{\Omega,1:\neg\alpha}\hskip
28.45274pt\mbox{($\neg_{\bf n}$) \, }\displaystyle\frac{\Omega,{\bf
n}:\alpha}{\Omega,{\bf n}:\neg\alpha}\hskip 28.45274pt\mbox{($\neg_{\bf b}$)
\, }\displaystyle\frac{\Omega,{\bf b}:\alpha}{\Omega,{\bf b}:\neg\alpha}\hskip
28.45274pt\mbox{($\neg_{1}$) \,
}\displaystyle\frac{\Omega,1:\alpha}{\Omega,0:\neg\alpha}$

$\mbox{($\square_{i}$) \,
}\displaystyle\frac{\Omega,i:\alpha}{\Omega,0:\square\alpha},\mbox{ for
}i\not=1\hskip 42.67912pt\mbox{($\square_{1}$) \,
}\displaystyle\frac{\Omega,1:\alpha}{\Omega,1:\square\alpha}$

In rules ($\vee_{ij}$) (and (($\wedge_{ij}$)), the supremum (infimum) is taken
on the lattice $M_{4}$. Besides, observe that the system ${\cal SF}_{4}$ has
forty logical rules and it is not optimal. However, in this step we are not
going to use the principles mentioned in Section 4 to reduce ${\cal SF}_{4}$.

###### Proposition 5.1

  *   * (i)

${\cal SF}_{4}$ is sound and complete w.r.t. the matrix ${\cal M}_{4}$,

  * (ii)

the cut rule is admissible in ${\cal SF}_{4}$.

Proof.  From Theorem 4.2. $\boldsymbol{\blacksquare}$

Now, we shall apply the method described in Section 4 to translate ${\cal
SF}_{4}$ to an ordinary two-sided sequent calculus.

###### Proposition 5.2

The language $\mathscr{L}$ is sufficiently expressive for the semantics
determined by the matrix ${\cal M}_{4}$.

Proof.  Let $v:Fm\to M_{4}$ be a valuation and let $\alpha\in Fm$ an arbitrary
formula, then we have that

$v(\alpha)=0\,\Longleftrightarrow\,v(\alpha)\in{\cal N}\mbox{ and
}v(\neg\alpha)\in{\cal D}$ $v(\alpha)={\bf
n}\,\Longleftrightarrow\,v(\alpha)\in{\cal N}\mbox{ and }v(\neg\alpha)\in{\cal
N}$ $v(\alpha)={\bf b}\,\Longleftrightarrow\,v(\alpha)\in{\cal D}\mbox{ and
}v(\neg\alpha)\in{\cal D}$
$v(\alpha)=1\,\Longleftrightarrow\,v(\alpha)\in{\cal D}\mbox{ and
}v(\neg\alpha)\in{\cal N}$

where ${\cal N}=M_{4}\setminus{\cal D}=\\{0,{\bf n}\\}$.
$\boldsymbol{\blacksquare}$

According to Theorem 4.7, to transform ${\cal SF}_{4}$ to an ordinary one, we
have to replace every axiom $A$ with the equivalent set of ordinary sequents
$TWO(A)$. In terms of $4$-sequents, the only axiom of ${\cal SF}_{4}$ has the
form

$\alpha\mid\alpha\mid\alpha\mid\alpha$

and it yields the following ordinary two-sided sequents

$\alpha,\neg\alpha\Rightarrow\alpha\hskip
28.45274pt\alpha,\neg\alpha\Rightarrow\neg\alpha\hskip
28.45274pt\alpha\Rightarrow\neg\alpha,\alpha\hskip
28.45274pt\alpha,\neg\alpha\Rightarrow\neg\alpha,\alpha\hskip
28.45274pt\neg\alpha\Rightarrow\neg\alpha,\alpha$

All of them can be derived from $\alpha\Rightarrow\alpha$ (or from an instance
of it) by the use of weakening.
Now, let us focus on rules ($\vee_{ij}$), $i,j\in M_{4}$. First observe that,
if $\varphi\in Fm$ then

$TWO(\varphi\mid\hskip 8.5359pt\mid\hskip 8.5359pt\mid\hskip
8.5359pt)=\\{\varphi\Rightarrow\,,\Rightarrow\neg\varphi\\}$ $TWO(\hskip
8.5359pt\mid\varphi\mid\hskip 8.5359pt\mid\hskip
8.5359pt)=\\{\varphi\Rightarrow\,,\neg\varphi\Rightarrow\\}$ $TWO(\hskip
8.5359pt\mid\hskip 8.5359pt\mid\varphi\mid\hskip
8.5359pt)=\\{\Rightarrow\varphi\,,\Rightarrow\neg\varphi\\}$ $TWO(\hskip
8.5359pt\mid\hskip 8.5359pt\mid\hskip
8.5359pt\mid\varphi)=\\{\neg\varphi\Rightarrow\,,\Rightarrow\varphi\\}$

So, after removing the contexts for brevity, the rules ($\vee_{ij}$)’s are
translated to the following thirty-two two-sided sequent rules:

($\vee$)10 | $\displaystyle\frac{\Rightarrow\alpha\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\beta\Rightarrow\hskip 8.5359pt\Rightarrow\neg\beta}{\Rightarrow\alpha\vee\beta\mbox{ \, ; \, }\neg(\alpha\vee\beta)\Rightarrow}$ | ($\vee$)1n | $\displaystyle\frac{\Rightarrow\alpha\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\beta\Rightarrow\hskip 8.5359pt\neg\beta\Rightarrow}{\Rightarrow\alpha\vee\beta\mbox{ \, ; \, }\neg(\alpha\vee\beta)\Rightarrow}$
---|---|---|---
($\vee$)1b | $\displaystyle\frac{\Rightarrow\alpha\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\Rightarrow\beta\hskip 8.5359pt\Rightarrow\neg\beta}{\Rightarrow\alpha\vee\beta\mbox{ \, ; \, }\neg(\alpha\vee\beta)\Rightarrow}$ | ($\vee$)11 | $\displaystyle\frac{\Rightarrow\alpha\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\Rightarrow\beta\hskip 8.5359pt\neg\beta\Rightarrow}{\Rightarrow\alpha\vee\beta\mbox{ \, ; \, }\neg(\alpha\vee\beta)\Rightarrow}$
($\vee$)b0 | $\displaystyle\frac{\Rightarrow\alpha\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\beta\Rightarrow\hskip 8.5359pt\Rightarrow\neg\beta}{\Rightarrow\alpha\vee\beta\mbox{ \, ; \, }\Rightarrow\neg(\alpha\vee\beta)}$ | ($\vee$)bn | $\displaystyle\frac{\Rightarrow\alpha\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\beta\Rightarrow\hskip 8.5359pt\neg\beta\Rightarrow}{\Rightarrow\alpha\vee\beta\mbox{ \, ; \, }\neg(\alpha\vee\beta)\Rightarrow}$
($\vee$)bb | $\displaystyle\frac{\Rightarrow\alpha\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\Rightarrow\beta\hskip 8.5359pt\Rightarrow\neg\beta}{\Rightarrow\alpha\vee\beta\mbox{ \, ; \, }\Rightarrow\neg(\alpha\vee\beta)}$ | ($\vee$)b1 | $\displaystyle\frac{\Rightarrow\alpha\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\Rightarrow\beta\hskip 8.5359pt\neg\beta\Rightarrow}{\Rightarrow\alpha\vee\beta\mbox{ \, ; \, }\neg(\alpha\vee\beta)\Rightarrow}$

($\vee$)n0 | $\displaystyle\frac{\alpha\Rightarrow\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\beta\Rightarrow\hskip 8.5359pt\Rightarrow\neg\beta}{\alpha\vee\beta\Rightarrow\mbox{ \, ; \, }\neg(\alpha\vee\beta)\Rightarrow}$ | ($\vee$)nn | $\displaystyle\frac{\alpha\Rightarrow\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\beta\Rightarrow\hskip 8.5359pt\neg\beta\Rightarrow}{\alpha\vee\beta\Rightarrow\mbox{ \, ; \, }\neg(\alpha\vee\beta)\Rightarrow}$
---|---|---|---
($\vee$)nb | $\displaystyle\frac{\alpha\Rightarrow\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\Rightarrow\beta\hskip 8.5359pt\Rightarrow\neg\beta}{\Rightarrow\alpha\vee\beta\mbox{ \, ; \, }\neg(\alpha\vee\beta)\Rightarrow}$ | ($\vee$)n1 | $\displaystyle\frac{\alpha\Rightarrow\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\Rightarrow\beta\hskip 8.5359pt\neg\beta\Rightarrow}{\Rightarrow\alpha\vee\beta\mbox{ \, ; \, }\neg(\alpha\vee\beta)\Rightarrow}$
($\vee$)00 | $\displaystyle\frac{\alpha\Rightarrow\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\beta\Rightarrow\hskip 8.5359pt\Rightarrow\neg\beta}{\alpha\vee\beta\Rightarrow\mbox{ \, ; \, }\Rightarrow\neg(\alpha\vee\beta)}$ | ($\vee$)0n | $\displaystyle\frac{\alpha\Rightarrow\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\beta\Rightarrow\hskip 8.5359pt\neg\beta\Rightarrow}{\alpha\vee\beta\Rightarrow\mbox{ \, ; \, }\neg(\alpha\vee\beta)\Rightarrow}$
($\vee$)0b | $\displaystyle\frac{\alpha\Rightarrow\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\Rightarrow\beta\hskip 8.5359pt\Rightarrow\neg\beta}{\Rightarrow\alpha\vee\beta\mbox{ \, ; \, }\Rightarrow\neg(\alpha\vee\beta)}$ | ($\vee$)01 | $\displaystyle\frac{\alpha\Rightarrow\hskip 8.5359pt\neg\alpha\Rightarrow\hskip 8.5359pt\Rightarrow\beta\hskip 8.5359pt\neg\beta\Rightarrow}{\Rightarrow\alpha\vee\beta\mbox{ \, ; \, }\neg(\alpha\vee\beta)\Rightarrow}$

In the above list we use an informal notation by separating the alternate
conclusion sequents with semicolons. At this point, we shall follow the three
principles mentioned in the above section in order to reduce the number of
rules. Our main tool for this job will be the next proposition.

###### Proposition 5.3

Let $\mathfrak{SC}$ a sequent calculus in which the cut rule is admissible,
let $S$ be a set of sequents and $\Sigma$ be a sequent such that
$\displaystyle\frac{S\cup\\{\Gamma\Rightarrow\Delta,\varphi\\}}{\Sigma}$ and
$\displaystyle\frac{S\cup\\{\Gamma,\varphi\Rightarrow\Delta\\}}{\Sigma}$ are
two context-free rules of $\mathfrak{SC}$. Then,
$\displaystyle\frac{S}{\Sigma}$ is derivable in $\mathfrak{SC}$.

Proof.  From the fact that the rules are context-free and using the cut rule.
$\boldsymbol{\blacksquare}$
Then, from ($\vee$)10, ($\vee$)1n and Proposition 5.3 we get
$\displaystyle\frac{\Rightarrow\alpha\hskip
8.5359pt\neg\alpha\Rightarrow\hskip
8.5359pt\beta\Rightarrow}{\Rightarrow\alpha\vee\beta\mid\neg(\alpha\vee\beta)\Rightarrow}$.
From ($\vee$)1b, ($\vee$)11 and Proposition 5.3 we get
$\displaystyle\frac{\Rightarrow\alpha\hskip
8.5359pt\neg\alpha\Rightarrow\hskip
8.5359pt\Rightarrow\beta}{\Rightarrow\alpha\vee\beta\mid\neg(\alpha\vee\beta)\Rightarrow}$.
From these rules and Proposition 5.3 we obtain (1)
$\displaystyle\frac{\Rightarrow\alpha\hskip
8.5359pt\neg\alpha\Rightarrow}{\Rightarrow\alpha\vee\beta}$ and (1’)
$\displaystyle\frac{\Rightarrow\alpha\hskip
8.5359pt\neg\alpha\Rightarrow}{\neg(\alpha\vee\beta)\Rightarrow}$.
Analogously, from ($\vee$)b0, ($\vee$)bn, ($\vee$)bb, ($\vee$)b1 we obtain
(2) $\displaystyle\frac{\Rightarrow\alpha\hskip
8.5359pt\Rightarrow\neg\alpha}{\Rightarrow\alpha\vee\beta}$. Finally, from
(1), (2) and Proposition 5.3 we get that

$\displaystyle\frac{\Rightarrow\alpha}{\Rightarrow\alpha\vee\beta}$ (3)

is derivable. On the other hand, following an analogous reasoning we can prove
that

$\displaystyle\frac{\Rightarrow\beta}{\Rightarrow\alpha\vee\beta}$ (4)

is derivable. Then, after combining rules (3) and (4) and restoring the
context we get the rule

$\mbox{($\Rightarrow\vee$)
}\displaystyle\frac{\Gamma\Rightarrow\Delta,\alpha,\beta}{\Gamma\Rightarrow\Delta,\alpha\vee\beta}$

From ($\vee$)n0, ($\vee$)nn, ($\vee$)nb and ($\vee$)n1 we obtain (5)
$\displaystyle\frac{\Rightarrow\alpha\hskip
8.5359pt\neg\alpha\Rightarrow}{\Rightarrow\alpha\vee\beta}$; then using (1’)
and restoring the context we get (5)
$\displaystyle\frac{\Gamma,\neg\alpha\Rightarrow\Delta}{\Gamma,\neg(\alpha\vee\beta)\Rightarrow\Delta}$.
In a similar way, it can be proved that (6)
$\displaystyle\frac{\Gamma,\neg\beta\Rightarrow\Delta}{\Gamma,\neg(\alpha\vee\beta)\Rightarrow\Delta}$
is derivable. Then, combining (5) and (6) and restoring the context we get

$\mbox{($\neg\vee\Rightarrow$)
}\displaystyle\frac{\Gamma,\neg\alpha,\neg\beta\Rightarrow\Delta}{\Gamma,\neg(\alpha\vee\beta)\Rightarrow\Delta}$

From ($\vee$)n0, ($\vee$)nn, ($\vee$)00 and ($\vee$)0n and restoring context
we obtain the rule

$\mbox{($\vee\Rightarrow$)
}\displaystyle\frac{\Gamma,\alpha\Rightarrow\Delta\hskip
14.22636pt\Gamma,\beta\Rightarrow\Delta}{\Gamma,\alpha\vee\beta\Rightarrow\Delta}$

and, from ($\vee$)00, ($\vee$)0b, ($\vee$)b0 and ($\vee$)bb we get

$\mbox{($\Rightarrow\neg\vee$)
}\displaystyle\frac{\Gamma\Rightarrow\Delta,\neg\alpha\hskip
14.22636pt\Gamma\Rightarrow\Delta,\neg\beta}{\Gamma\Rightarrow\Delta,\neg(\alpha\vee\beta)}$

In the same way, we obtain the following rules for the connective $\wedge$:

$\mbox{($\wedge\Rightarrow$) \,
}\displaystyle\frac{\Gamma,\alpha,\beta\Rightarrow\Delta}{\Gamma,\alpha\wedge\beta\Rightarrow\Delta}\hskip
56.9055pt\mbox{($\Rightarrow\wedge$) \,
}\displaystyle\frac{\Gamma\Rightarrow\Delta,\alpha\hskip
14.22636pt\Gamma\Rightarrow\Delta,\beta}{\Gamma\Rightarrow\Delta,\alpha\wedge\beta}$

$\mbox{($\neg\wedge\Rightarrow$) \,
}\displaystyle\frac{\Gamma,\neg\alpha\Rightarrow\Delta\hskip
14.22636pt\Gamma,\neg\beta\Rightarrow\Delta}{\Gamma,\neg(\alpha\wedge\beta)\Rightarrow\Delta}\hskip
42.67912pt\mbox{($\Rightarrow\neg\wedge$) \,
}\displaystyle\frac{\Gamma\Rightarrow\Delta,\neg\alpha,\neg\beta}{\Gamma\Rightarrow\Delta,\neg(\alpha\wedge\beta)}$

On the other hand, rules ($\neg$)i with $i\in M_{4}$ are translated to (after
eliminating the trivial rules)

($\neg$)0 | $\displaystyle\frac{\alpha\Rightarrow\hskip 8.5359pt\Rightarrow\neg\alpha}{\neg\neg\alpha\Rightarrow}$ | ($\neg$)n | $\displaystyle\frac{\alpha\Rightarrow\hskip 8.5359pt\neg\alpha\Rightarrow}{\neg\neg\alpha\Rightarrow}$
---|---|---|---
($\neg$)b | $\displaystyle\frac{\Rightarrow\alpha\hskip 8.5359pt\Rightarrow\neg\alpha}{\Rightarrow\neg\neg\alpha}$ | ($\neg$)1 | $\displaystyle\frac{\Rightarrow\alpha\hskip 8.5359pt\neg\alpha\Rightarrow}{\Rightarrow\neg\neg\alpha}$

From ($\neg$)0, ($\neg$)n and Proposition 5.3 on the one hand; and ($\neg$)b,
($\neg$)1 and Proposition 5.3 on the other, we obtain

$\mbox{($\neg\neg\Rightarrow$) \,
}\displaystyle\frac{\Gamma,\alpha\Rightarrow\Delta}{\Gamma,\neg\neg\alpha\Rightarrow\Delta}\hskip
42.67912pt\mbox{($\Rightarrow\neg\neg$) \,
}\displaystyle\frac{\Gamma\Rightarrow\Delta,\alpha}{\Gamma\Rightarrow\Delta,\neg\neg\alpha}$

Finally, rules ($\square$)i are translated to

($\square$)0 | $\displaystyle\frac{\alpha\Rightarrow\hskip 8.5359pt\Rightarrow\neg\alpha}{\square\alpha\Rightarrow\mbox{ \, ; \, }\Rightarrow\neg\square\alpha}$ | ($\square$)n | $\displaystyle\frac{\alpha\Rightarrow\hskip 8.5359pt\neg\alpha\Rightarrow}{\square\alpha\Rightarrow\mbox{ \, ; \, }\Rightarrow\neg\square\alpha}$
---|---|---|---
($\square$)b | $\displaystyle\frac{\Rightarrow\alpha\hskip 8.5359pt\Rightarrow\neg\alpha}{\square\alpha\Rightarrow\mbox{ \, ; \, }\Rightarrow\neg\square\alpha}$ | ($\square$)1 | $\displaystyle\frac{\Rightarrow\alpha\hskip 8.5359pt\neg\alpha\Rightarrow}{\Rightarrow\square\alpha\mbox{ \, ; \, }\neg\square\alpha\Rightarrow}$

and, from these rules and Proposition 5.3, we obtain

$\mbox{($\square\Rightarrow$)${}_{1}$ \,
}\displaystyle\frac{\Gamma,\alpha\Rightarrow\Delta}{\Gamma,\square\alpha\Rightarrow\Delta}\hskip
39.83368pt\mbox{($\square\Rightarrow$)${}_{1}$ \,
}\displaystyle\frac{\Gamma\Rightarrow\Delta,\neg\alpha}{\Gamma,\square\alpha\Rightarrow\Delta}\hskip
39.83368pt\displaystyle\mbox{($\Rightarrow\square$) \,
}\frac{\Gamma\Rightarrow\Delta,\alpha\hskip
8.5359pt\Gamma,\neg\alpha\Rightarrow\Delta}{\Gamma\Rightarrow\Delta,\square\alpha}$
$\mbox{($\neg\square\Rightarrow$) \,
}\displaystyle\frac{\Gamma\Rightarrow\Delta,\alpha\hskip
8.5359pt\Gamma,\neg\alpha\Rightarrow\Delta}{\Gamma,\neg\square\alpha\Rightarrow\Delta}\hskip
28.45274pt\mbox{($\Rightarrow\neg\square$)${}_{1}$ \,
}\displaystyle\frac{\Gamma,\alpha\Rightarrow\Delta}{\Gamma\Rightarrow\Delta,\neg\square\alpha}\hskip
25.6073pt\mbox{($\Rightarrow\neg\square$)${}_{2}$ \,
}\displaystyle\frac{\Gamma\Rightarrow\Delta,\neg\alpha}{\Gamma\Rightarrow\Delta,\neg\square\alpha}$

###### Definition 5.4

Let ${\bf SC}_{\cal TML}$ be the sequent calculus given by the axiom
$\alpha\Rightarrow\alpha$ the structural rules of cut and left and right
weakening

$\mbox{\rm($w\Rightarrow$) \,
}\displaystyle\frac{\Gamma\Rightarrow\Delta}{\Gamma,\alpha\Rightarrow\Delta}\hskip
42.67912pt\mbox{\rm($\Rightarrow w$) \,
}\displaystyle\frac{\Gamma\Rightarrow\Delta}{\Gamma\Rightarrow\Delta,\alpha}$

and the logical rules ($\vee\Rightarrow$), ($\Rightarrow\vee$),
($\neg\vee\Rightarrow$), ($\Rightarrow\neg\vee$), ($\wedge\Rightarrow$),
($\Rightarrow\wedge$), ($\neg\wedge\Rightarrow$), ($\Rightarrow\neg\wedge$),
($\neg\neg\Rightarrow$), ($\Rightarrow\neg\neg$), ($\square\Rightarrow$)i,
($\Rightarrow\square$), ($\neg\square\Rightarrow$),
($\Rightarrow\neg\square$)i $i=1,2$.

We shall write $\Gamma\Leftrightarrow\Delta$ to indicate that both the
sequents $\Gamma\Rightarrow\Delta$ and $\Delta\Rightarrow\Gamma$ are provable.
Then, it is not difficult to verify that
$\alpha\wedge\neg\alpha\Leftrightarrow\alpha\wedge\neg\square\alpha$, for
every formula $\alpha$. Besides, the modal axiom
$\Rightarrow\alpha\vee\neg\square\alpha$ of $\mathfrak{G}$ is derivable in
${\bf SC}_{\cal TML}$. Indeed,

$\alpha\Rightarrow\alpha$ ($\Rightarrow\neg\square$)1
$\Rightarrow\alpha,\neg\square\alpha$ ($\Rightarrow\vee$)
$\Rightarrow\alpha\vee\neg\square\alpha$

Moreover, the sequent $\Rightarrow\square(\alpha\vee\neg\square\alpha)$ is
derivable in ${\bf SC}_{\cal TML}$ without the cut rule:

$\alpha\Rightarrow\alpha$ ($\Rightarrow\neg\square$)1
$\Rightarrow\alpha,\neg\square\alpha$ ($\Rightarrow\vee$)
$\Rightarrow\alpha\vee\neg\square\alpha$ $\neg\alpha\Rightarrow\neg\alpha$
($\square\Rightarrow$)1 $\neg\alpha,\square\alpha\Rightarrow$
($\neg\neg\Rightarrow$) $\neg\alpha,\neg\neg\square\alpha\Rightarrow$
($\neg\vee\Rightarrow$) $\neg(\alpha\vee\neg\square\alpha)\Rightarrow$
($\Rightarrow\square$) $\Rightarrow\square(\alpha\vee\neg\square\alpha)$

###### Remark 5.5

In Font and Rius’ system $\mathfrak{G}$ , the propositional constant $\bot$ is
used. By following Avron, Ben-Naim and Konikowska’s method, we obtained a
system in which $\bot$ does not appear. However, it is easy to check that the
sequent $\neg\alpha\wedge\square\alpha\Rightarrow$ is provable in ${\bf
SC}_{\cal TML}$, for any formula $\alpha$. Then, if we denote by $\bot$ the
formula $\neg\alpha\wedge\square\alpha$, for any formula $\alpha$, we have
that the rule $(\bot)$ of $\mathfrak{G}$ is derivable in ${\bf SC}_{\cal
TML}$.

###### Theorem 5.6

  *   * (i)

${\bf SC}_{\cal TML}$ is sound and complete w.r.t. ${\cal M}_{4}$.

  * (ii)

The cut rule is admissible in ${\bf SC}_{\cal TML}$,

Proof.  The system ${\bf SC}_{\cal TML}$ was constructed according to the
method displayed in Section 4. $\boldsymbol{\blacksquare}$

###### Corollary 5.7

${\bf SC}_{\cal TML}$ is a cut-free sequent calculus that provides a
syntactical counterpart for $\cal TML$.

##  6 Some applications of the cut elimination theorem

In this section, we shall use the cut-free system ${\bf SC}_{\cal TML}$ to
show independent proofs of some (known) interesting properties of the logic
${\cal TML}$. In what follows $\Gamma$, $\Delta$ are sets of formulas and
$\alpha$, $\beta$, $\psi$ are formulas.
In the first place, we shall present a new independent proof of Proposition
2.5. To do this, we need the following technical result.

###### Proposition 6.1

If $\vdash_{{\bf SC}_{\cal TML}}\Gamma\Rightarrow\Delta$ then, for every
$\mathbb{A}\in{\bf TMA}$ and for every $h\in Hom(\mathfrak{Fm},\mathbb{A})$,
$\bigwedge_{\gamma\in\Gamma}h(\gamma)\leq\bigvee_{\delta\in\Delta}h(\delta)$.

Proof.  Suppose that $\vdash_{{\bf SC}_{\cal TML}}\Gamma\Rightarrow\Delta$ and
let $\cal P$ be a cut–free proof of the sequent $\Gamma\Rightarrow\Delta$ in
${\bf SC}_{\cal TML}$. Let $\mathbb{A}\in{\bf TMA}$ and let $h\in
Hom(\mathfrak{Fm},\mathbb{A})$. We use induction on the number $n$ of
inferences in $\cal P$. If $n=0$ the proposition is obviously valid. (I.H.)
Suppose that the proposition holds for $n<k$, $k>0$. Let $n=k$ and let $(r)$
be the last inference in $\cal P$. Ir $(r)$ is the right/left weakening rule,
the proposition holds since $\mathbb{A}$ is, in particular, a lattice. If
$(r)$ is one of the rules ($\vee\Rightarrow$), ($\Rightarrow\vee$),
($\neg\vee\Rightarrow$), ($\Rightarrow\neg\vee$), ($\wedge\Rightarrow$),
($\Rightarrow\wedge$), ($\neg\wedge\Rightarrow$), ($\Rightarrow\neg\wedge$),
($\neg\neg\Rightarrow$), ($\Rightarrow\neg\neg$), the proposition holds since
$\mathbb{A}$ is, in particular, a De Morgan algebra. Finally, if $(r)$ is one
of the rules , ($\square\Rightarrow$)i, ($\Rightarrow\square$),
($\neg\square\Rightarrow$), ($\Rightarrow\neg\square$)i $i=1,2$ then the
proposition holds since $\mathbb{A}$ is a tetravalent modal algebra. For
instance, suppose that $(r)$ is $(\Rightarrow\square)$ and the last inference
of $\cal P$ is $\displaystyle\frac{\Gamma\Rightarrow\Delta,\alpha\hskip
14.22636pt\Gamma,\neg\alpha\Rightarrow\Delta}{\Gamma\Rightarrow\Delta,\square\alpha}$.
By (I.H.), we have (1)
$\bigwedge_{\gamma\in\Gamma}h(\gamma)\leq\bigvee_{\delta\in\Delta}h(\delta)\vee
h(\alpha)$ and (2) $\bigwedge_{\gamma\in\Gamma}h(\gamma)\wedge
h(\neg\alpha)\leq\bigvee_{\delta\in\Delta}h(\delta)$. Then, from (1), (2) and
Proposition 2.2 we have
$\bigwedge_{\gamma\in\Gamma}h(\gamma)\leq\bigvee_{\delta\in\Delta}h(\delta)\vee
h(\square\alpha)$. $\boldsymbol{\blacksquare}$

###### Proposition 6.2

The following conditions are equivalent.

  * (i)

$\Gamma\models_{\cal TML}\psi$ ,

  * (ii)

$\Gamma\models_{{\cal M}_{4}}\psi$.

Proof.  (i) imples (ii): immediate.
(ii) implies (i): It is consequence of Theorem 5.6 (i) and Proposition 6.1.
$\boldsymbol{\blacksquare}$

Next, we shall prove that the rule ($\neg$) of Font and Rius’ system is
addmissible in ${\bf SC}_{\cal TML}$. Let $X$ a set of formulas, we shall
denote by $\neg X$ the set $\neg X=\\{\neg\gamma:\gamma\in X\\}$.

###### Theorem 6.3

If $\vdash_{{\bf SC}_{\cal TML}}\Gamma\Rightarrow\Delta$, then $\vdash_{{\bf
SC}_{\cal TML}}\neg\Delta\Rightarrow\neg\Gamma$.

Proof.  Suppose that $\vdash_{{\bf SC}_{\cal TML}}\Gamma\Rightarrow\Delta$ and
let $\cal P$ a cut–free proof of the sequent $\Gamma\Rightarrow\Delta$. We use
induction on the number $n$ of inferences in ${\cal P}$. If $n=0$, then
$\Gamma\Rightarrow\Delta$ is $\alpha\Rightarrow\alpha$, for some $\alpha$, and
$\neg\Delta\Rightarrow\neg\Gamma$ is $\neg\alpha\Rightarrow\neg\alpha$ which
is provable in ${\bf SC}_{\cal TML}$. (I.H.) Suppose that the lemma holds for
$n<k$, with $k>0$. Let $n=k$ and let $(r)$ be the last inference in $\cal P$.
If $(r)$ is left weakening, then the last inference of $\cal P$ is
$\displaystyle\frac{\Gamma\Rightarrow\Delta}{\Gamma,\alpha\Rightarrow\Delta}$.
By (I.H.), $\neg\Delta\Rightarrow\neg\Gamma$ is provable in ${\bf SC}_{\cal
TML}$ and using right weakening we have $\vdash_{{\bf SC}_{\cal
TML}}\neg\Delta\Rightarrow\neg\Gamma,\neg\alpha$. If $(r)$ is an instance of
the right weakening the treatment is analogous.
Suppose now that $(r)$ is (an instance of) a logic rule. If $(r)$ is
$(\Rightarrow\vee)$ and the last inference of $\cal P$ is
$\displaystyle\frac{\Gamma\Rightarrow\Delta,\alpha,\beta}{\Gamma\Rightarrow\Delta,\alpha\vee\beta}$.
By (I.H.), $\neg\alpha,\neg\beta,\neg\Delta\Rightarrow\neg\Gamma$ is provable,
and using $(\neg\vee\Rightarrow)$ we have that
$\neg(\alpha\vee\beta),\neg\Delta\Rightarrow\neg\Gamma$ is provable. The cases
where $(r)$ is one of the rules $(\vee\Rightarrow)$, $(\Rightarrow\neg\vee)$,
$(\neg\vee\Rightarrow)$, $(\Rightarrow\wedge)$ $(\wedge\Rightarrow)$,
$(\Rightarrow\neg\wedge)$, $(\neg\wedge\Rightarrow)$ are left to the reader.
If $(r)$ is $(\Rightarrow\neg\neg)$ and the last inference of $\cal P$ is
$\displaystyle\frac{\Gamma\Rightarrow\Delta,\alpha}{\Gamma\Rightarrow\Delta,\neg\neg\alpha}$.
By (I.H.), $\neg\alpha,\neg\Delta\Rightarrow\neg\Gamma$ is provable in ${\bf
SC}_{\cal TML}$ and using $(\neg\neg\Rightarrow)$ we have that
$\neg\neg\neg\alpha,\neg\Delta\Rightarrow\neg\Gamma$ is provable. If $(r)$ is
$(\neg\neg\Rightarrow)$ the proof is analogous.
If $(r)$ is $(\square\Rightarrow)_{1}$ and the last inference of $\cal P$ is
$\displaystyle\frac{\Gamma,\alpha\Rightarrow\Delta}{\Gamma,\square\alpha\Rightarrow\Delta}$.
By (I.H.), we have that $\neg\Delta\Rightarrow\neg\Gamma,\neg\alpha$ is
provable in ${\bf SC}_{\cal TML}$. Then, using $(\Rightarrow\neg\square)_{2}$
we have that $\neg\Delta\Rightarrow\neg\Gamma,\neg\square\alpha$ is provable.
If $(r)$ is $(\square\Rightarrow)_{2}$ and the last inference of $\cal P$ is
$\displaystyle\frac{\Gamma\Rightarrow\Delta,\neg\alpha}{\Gamma,\square\alpha\Rightarrow\Delta}$.
By (I.H.), we have that $\neg\Delta,\neg\neg\alpha\Rightarrow\neg\Gamma$ is
provable in ${\bf SC}_{\cal TML}$ and using left weakening we have (1)
$\vdash_{{\bf SC}_{\cal
TML}}\alpha,\neg\Delta,\neg\neg\alpha\Rightarrow\neg\Gamma$. On the other
hand, one can easily check that $\vdash_{{\bf SC}_{\cal
TML}}\alpha\Rightarrow\neg\neg\alpha$ and by means of (right/left)
weakening(s) we have (2) $\vdash_{{\bf SC}_{\cal
TML}}\alpha,\neg\Delta\Rightarrow\neg\neg\alpha,\neg\Gamma$. From (1), (2) and
the cut rule, we have $\vdash_{{\bf SC}_{\cal
TML}}\alpha,\neg\Delta\Rightarrow\neg\Gamma$ (the cut rule is admissible in
${\bf SC}_{\cal TML}$). Then, using $(\Rightarrow\neg\square)_{1}$ we have
$\vdash_{{\bf SC}_{\cal
TML}}\neg\Delta\Rightarrow\neg\Gamma,\neg\square\alpha$.
If $(r)$ is $(\Rightarrow\square)$ and the last inference of $\cal P$ is
$\displaystyle\frac{\Gamma\Rightarrow\Delta,\alpha\hskip
14.22636pt\Gamma,\neg\alpha\Rightarrow\Delta}{\Gamma\Rightarrow\Delta,\square\alpha}$.
By (I.H.) we have that (3) $\vdash_{{\bf SC}_{\cal
TML}}\neg\alpha,\neg\Delta\Rightarrow\neg\Gamma$ and (4) $\vdash_{{\bf
SC}_{\cal TML}}\neg\Delta\Rightarrow\neg\neg\alpha,\neg\Gamma$. From (4) and a
similar reasoning to the above, we have that (5) $\vdash_{{\bf SC}_{\cal
TML}}\neg\Delta\Rightarrow\alpha,\neg\Gamma$. From (3), (5) and
$(\neg\square\Rightarrow)$ we get $\vdash_{{\bf SC}_{\cal
TML}}\neg\Delta,\neg\square\alpha\Rightarrow\neg\Gamma$.
The cases where $(r)$ is one of the rules $(\Rightarrow\neg\square)_{1}$,
$(\Rightarrow\neg\square)_{2}$ and $(\neg\square\Rightarrow)$ are treated
similarly. $\boldsymbol{\blacksquare}$

###### Corollary 6.4

$(\neg)$ is admissible in ${\bf SC}_{\cal TML}$.

Finally,

###### Theorem 6.5

$\vdash_{\cal TML}\square\psi$ iff $\vdash_{\cal TML}\psi$.

Proof. ($\Longrightarrow$) Suppose that $\vdash_{\cal TML}\square\psi$. By
Theorem 5.6, Proposition 2.5 we know that the sequent $\Rightarrow\square\psi$
has a cut-free proof $\cal P$ in ${\bf SC}_{\cal TML}$. Let $(r)$ be the last
inference of $\cal P$. By inspecting the rules of ${\bf SC}_{\cal TML}$ we may
assert that $(r)$ has to be an instance of the rule ($\Rightarrow\square$).
So, $(r)$ is $\displaystyle\frac{\Rightarrow\psi\hskip
14.22636pt\neg\psi\Rightarrow}{\Rightarrow\square\psi}$ and clearly the
sequent $\Rightarrow\psi$ is provable in ${\bf SC}_{\cal TML}$. Therefore
$\vdash_{\cal TML}\psi$.
($\Longleftarrow$) Suppose that $\vdash_{\cal TML}\psi$. By Theorem 5.6 (i),
we have: (1) $\Rightarrow\psi$ is provable in ${\bf SC}_{\cal TML}$. From (1)
and Theorem 6.3, we have that: (2) $\neg\psi\Rightarrow$ is also provable in
${\bf SC}_{\cal TML}$. From (1), (2) and the rule ($\Rightarrow\square)$, we
may assert that $\Rightarrow\square\psi$ is provable in ${\bf SC}_{\cal TML}$.
Therefore, $\vdash_{\cal TML}\square\psi$. $\boldsymbol{\blacksquare}$

##  7 Natural deduction for ${\cal TML}$

In this section, we shall present a natural deduction system for ${\cal TML}$.
We take our inspiration from the construction made before. In particular, it
threw some light on how the connective $\square$ behaves. We think that this
system shows an interesting example of a rule (different from the usual ones),
namely the introduction rule of the connective $\square$, that needs to
produce a discharge of hypothesis; and this is related to the intrinsic
meaning of the connective.
The proof system ${\bf ND}_{\cal TML}$ will be defined following the
notational conventions given in [15].

###### Definition 7.1

Deductions in ${\bf ND}_{\cal TML}$ are inductively defined as follows:
Basis: The proof tree with a single occurrence of an assumption $\phi$ with a
marker is a deduction with conclusion $\phi$ from open assumption $\phi$ .
Inductive step: Let ${\cal D}$, ${\cal D}_{1}$ ,${\cal D}_{2}$,${\cal D}_{3}$
be deductions. Then, they can be extended by one of the following rules below.
The classes [$\neg\phi$]u, [$\neg\psi$]v, [$\phi$]u , [$\psi$]v below contain
open assumptions of the deductions of the premises of the final inference, but
are closed in the whole deduction.

MA (modal axioma) $\phi\vee\neg\square\phi$

${\cal D}_{1}$ $\phi$ ${\cal D}_{2}$ $\psi$ $\wedge$I $\phi\wedge\psi$ ${\cal
D}$ $\phi\wedge\psi$ $\wedge$E1 $\phi$ ${\cal D}$ $\phi\wedge\psi$ $\wedge$E2
$\psi$

${\cal D}$ $\neg\phi$ $\neg\wedge$I1 $\neg(\phi\wedge\psi)$ ${\cal D}$
$\neg\psi$ $\neg\wedge$I2 $\neg(\phi\wedge\psi)$ ${\cal D}_{1}$
$\neg(\phi\wedge\psi)$ [$\neg\phi$]u ${\cal D}_{2}$ $\chi$ [$\neg\psi$]v
${\cal D}_{3}$ $\chi$ $\neg\wedge$E,$u$,$v$ $\chi$

${\cal D}$ $\phi$ $\vee$I1 $\phi\vee\psi$ ${\cal D}$ $\psi$ $\vee$I2
$\phi\vee\psi$ ${\cal D}_{1}$ $\phi\vee\psi$ [$\phi$]u ${\cal D}_{2}$ $\chi$
[$\psi$]v ${\cal D}_{3}$ $\chi$ $\vee$E,$u$,$v$ $\chi$

${\cal D}_{1}$ $\neg\phi$ ${\cal D}_{2}$ $\neg\psi$ $\neg\vee$I
$\neg(\phi\vee\psi)$ ${\cal D}$ $\neg(\phi\vee\psi)$ $\neg\vee$E1 $\neg\phi$
${\cal D}$ $\neg(\phi\vee\psi)$ $\neg\vee$E2 $\neg\psi$

${\cal D}$ $\phi$ $\neg\neg$I $\neg\neg\phi$ ${\cal D}$ $\neg\neg\phi$
$\neg\neg$E $\phi$

${\cal D}_{1}$ $\psi\vee\phi$ [$\neg\phi$]u ${\cal D}_{2}$ $\psi$
$\square$I∗,$u$ $\psi\vee\square\phi$ ${\cal D}$ $\square\phi$ $\square$E
$\phi$

${\cal D}$ $\neg\phi$ $\neg\square$I $\neg\square\phi$ ${\cal D}_{1}$
$\neg\square\phi$ ${\cal D}_{2}$ $\phi$ $\neg\square$E $\neg\phi$

${\cal D}$ $\neg\phi\wedge\square\phi$ $\bot$I $\bot$ ${\cal D}$ $\bot$
$\bot$E $\alpha$

###### Remark 7.2

If we take $\psi$ as $\bot$ in $\square$I∗ we get

${\cal D}_{1}$ $\phi$ [$\neg\phi$]u ${\cal D}_{2}$ $\bot$ $\square$I,$u$
$\square\phi$

Formally, $\square$I is derivable in ${\bf ND}_{\cal TML}$. The intuition
behind this rule is the following:“if we have a deduction for $\alpha$ and
$\neg\alpha$ is not provable, then we have a deduction for $\square\alpha$”.

As usual, by application of the rule $\neg\wedge$E a new proof-tree is formed
from ${\cal D}$, ${\cal D}_{1}$, and ${\cal D}_{2}$ by adding at the bottom
the conclusion $\chi$ while closing the sets [$\neg\phi$]u and [$\neg\psi$]u
of open assumptions marked by $u$ and $v$, respectively. Idem for the rules
$\wedge$E and $\square$I. Note that we have introduced the symbol $\bot$, it
behaves here as an arbitrary unprovable propositional constant.
Let $\Gamma\cup\\{\alpha\\}\subseteq Fm$. We say that the conclusion $\alpha$
is derivable from a set $\Gamma$ of premises, noted $\Gamma\vdash\alpha$, if
and only if there is a deduction in ${\bf ND}_{\cal TML}$ of $\alpha$ from
$\Gamma$.

###### Theorem 7.3

(Soundness and Completeness) Let $\Gamma,\Delta\subseteq Fm$, $\Gamma$ finite.
The following conditions are equivalent:

  * (i)

the sequent $\Gamma\Rightarrow\Delta$ is derivable in ${\bf SC}_{\cal TML}$,

  * (ii)

there is a deduction of the disjunction of the sentences in $\Delta$ from
$\Gamma$ in ${\bf ND}_{\cal TML}$.

Proof.  (i) implies (ii): Suppose that the sequent $\Gamma\Rightarrow\Delta$
is derivable in ${\bf SC}_{\cal TML}$, that is, there is a formal proof $\cal
P$ of $\Gamma\Rightarrow\Delta$ in ${\bf SC}_{\cal TML}$ which does not use
the cut rule. We shall show that there is a deduction of the disjunction of
the formulas in $\Delta$ (denoted by $\bigvee\Delta$) from $\Gamma$ in ${\bf
ND}_{\cal TML}$, using induction on the number $n$ of rule applications in
$\cal P$, $n\geq 0$.
If $n=0$, then $\Gamma\Rightarrow\Delta$ is $\alpha\Rightarrow\alpha$ and it
is clear that $\alpha\vdash\alpha$. Now, (I.H.) suppose that “(i) implies
(ii)” holds for $n<k$, with $k>0$.
Let $n=k$, that is $\cal P$ is a derivation in ${\bf SC}_{\cal TML}$ with last
rule (r) of the form

$\Gamma_{1}\Rightarrow\Delta_{1}$ $\ddots$ $\dots$ $\vdots$
$\Gamma_{t}\Rightarrow\Delta_{t}$ $\ddots$ ($r$) $\Gamma\Rightarrow\Delta$

If (r) is left weakening, then the last rule of $\cal P$ has the form
$\displaystyle{\rm(r)}\frac{\Gamma^{\prime}\Rightarrow\Delta}{\Gamma^{\prime},\beta\Rightarrow\Delta}$.
By (I.H.), there exists a deduction $\cal D$ of $\Delta$ from
$\Gamma^{\prime}$, then

$\cal D$ $\bigvee\Delta$ $\beta$ $\wedge$I $\bigvee\Delta\wedge\beta$
$\wedge$E1 $\bigvee\Delta$

is a deduction of $\bigvee\Delta$ from $\Gamma^{\prime}\cup\\{\beta\\}$. If
(r) is right weakening, then (r) has the form
$\displaystyle{\rm(r)}\frac{\Gamma\Rightarrow\Delta^{\prime}}{\Gamma\Rightarrow\Delta^{\prime},\beta}$,
then by (I.H.) there is a deduction $\cal D$ of $\bigvee\Delta^{\prime}$ from
$\Gamma$.

$\cal D$ $\bigvee\Delta^{\prime}$ $\vee$I1 $\bigvee\Delta^{\prime}\vee\beta$

Now, suppose that (r) is a logical rule, we shall prove it just for
($\Rightarrow\vee$), ($\vee\Rightarrow$), ($\Rightarrow\neg\vee$),
($\neg\vee\Rightarrow$). If (r) is ($\vee\Rightarrow$), then we may assume
that the last inference of $\cal P$ has the form
$\displaystyle\mbox{($\Rightarrow\vee$)}\frac{\Gamma\Rightarrow\Delta^{\prime},\alpha,\beta}{\Gamma\Rightarrow\Delta^{\prime},\alpha\vee\beta}$.
Then, by (I.H.) we have a deduction $\cal D$ of
$\bigvee\Delta^{\prime}\vee\alpha\vee\beta$ from $\Gamma$ and the proof is
complete.
If (r) is ($\vee\Rightarrow$) and last inference of $\cal P$ has the from
$\displaystyle\mbox{($\vee\Rightarrow$)}\frac{\Gamma,\gamma_{1}\Rightarrow\Delta\hskip
14.22636pt\Gamma,\gamma_{2}\Rightarrow\Delta}{\Gamma,\gamma_{1}\vee\gamma_{2}\Rightarrow\Delta}$,
then by (I.H.) there are deductions ${\cal D}_{i}$ , $i=1,2$, of $\alpha$ from
$\Gamma\cup\\{\gamma_{i}\\}$. Then, the following

$\gamma_{1}\vee\gamma_{2}$ [$\gamma_{1}$]${}^{u_{1}}$ ${\cal D}_{1}$
$\bigvee\Delta$ [$\gamma_{2}$]${}^{u_{2}}$ ${\cal D}_{2}$ $\bigvee\Delta$
$\vee$E,$u_{1}$,$u_{2}$ $\bigvee\Delta$

is a deduction of $\bigvee\Delta$ from
$\Gamma\cup\\{\gamma_{1}\vee\gamma_{2}\\}$. Note that in this last deduction
we have made every assumption $\gamma_{i}$ in ${\cal D}_{i}$ an open
assumption with label $u_{i}$.
If (r) is ($\neg\vee\Rightarrow$) then we may assume that the last instance of
${\cal P}$ has the form
$\displaystyle\mbox{($\neg\vee\Rightarrow$)}\frac{\Gamma,\neg\gamma_{1}\Rightarrow\Delta}{\Gamma,\neg(\gamma_{1}\vee\gamma_{2})\Rightarrow\Delta}$.
By (I.H.), there is a deduction ${\cal D}$ of $\alpha$ from
$\Gamma\cup\\{\gamma_{1}\\}$ and the following

$\neg(\gamma_{1}\vee\gamma_{2})$ $\neg\vee$E1 $\neg\gamma_{1}$ ${\cal D}$
$\bigvee\Delta$

is a deduction of $\alpha$ from
$\Gamma\cup\\{\neg(\gamma_{1}\vee\gamma_{2})\\}$. If (r) is
($\Rightarrow\neg\vee$) we proceed analogously.
For (r) being any of the rules ($\square\Rightarrow$)i,
($\Rightarrow\square$), ($\neg\square\Rightarrow$),
($\Rightarrow\neg\square$)i $i=1,2$, we present the next table showing the
deduction corresponding to the premise(s) of (r) and the deduction
corresponding to the consequence of (r).

Rule (r) | Upper sequent(s)’s | Lower sequent’s
---|---|---
| deduction(s) | deduction
|  |
$\Gamma,\gamma\Rightarrow\Delta$ ($\square\Rightarrow$)1 $\Gamma,\square\gamma\Rightarrow\Delta$ |  $\gamma$ $\cal D$ $\bigvee\Delta$ |  $\square\gamma$ $\square$E $\gamma$ $\cal D$ $\bigvee\Delta$
|  |
$\Gamma\Rightarrow\Delta,\neg\gamma$ ($\square\Rightarrow$)2 $\Gamma,\square\gamma\Rightarrow\Delta$ |  $\cal D$ $\bigvee\Delta\vee\neg\gamma$ |  $\cal D$ $\bigvee\Delta\vee\neg\gamma$ $[\bigvee\Delta]_{u}$ $\bigvee\Delta$ $[\neg\gamma]_{u}$ $\square\gamma$ $\wedge$I $\neg\gamma\wedge\square\gamma$ $\bot$I $\bot$ $\bot$E $\bigvee\Delta$ $\vee$E, $u$, $v$ $\bigvee\Delta$
|  |
$\Gamma\Rightarrow\Delta,\gamma$ $\Gamma,\neg\gamma\Rightarrow\Delta$ ($\Rightarrow\square$) $\Gamma\Rightarrow\Delta,\square\gamma$ |  ${\cal D}_{1}$ $\bigvee\Delta\vee\gamma$ $\neg\gamma$ ${\cal D}_{2}$ $\bigvee\Delta$ |  ${\cal D}_{1}$ $\bigvee\Delta\vee\gamma$ $\neg\gamma^{u}$ ${\cal D}_{2}$ $\bigvee\Delta$ $\square$I∗,$u$ $\bigvee\Delta\vee\square\gamma$
|  |
$\Gamma\Rightarrow\Delta,\gamma$ $\Gamma,\neg\gamma\Rightarrow\Delta$ ($\neg\square\Rightarrow$) $\Gamma,\neg\square\gamma\Rightarrow\Delta$ |  ${\cal D}_{1}$ $\bigvee\Delta\vee\gamma$ $\neg\gamma$ ${\cal D}_{2}$ $\bigvee\Delta$ |  ${\cal D}_{1}$ $\bigvee\Delta\vee\gamma$ $[\neg\gamma]^{u}$ ${\cal D}_{2}$ $\bigvee\Delta$ $\square$I,$u$ $\bigvee\Delta\vee\square\gamma$ $\neg\square\gamma$ $\vee$I2 $\bigvee\Delta\vee\neg\square\gamma$ $\wedge$I $(\bigvee\Delta\vee\square\gamma)\wedge(\bigvee\Delta\vee\neg\square\gamma)$ 111$(\gamma\vee\alpha)\wedge(\gamma\vee\beta)\dashv\vdash\gamma\vee(\alpha\wedge\beta)$ $\bigvee\Delta\vee(\square\gamma\wedge\neg\square\gamma)$ 222 $\alpha\vee(\square\gamma\wedge\neg\square\gamma)\dashv\vdash\alpha\vee\bot$ $\bigvee\Delta\vee\bot$ $\bigvee\Delta$
|  |
$\Gamma,\gamma\Rightarrow\Delta$ ($\Rightarrow\neg\square$)1 $\Gamma\Rightarrow\Delta,\neg\square\gamma$ |  $\gamma$ $\cal D$ $\bigvee\Delta$ |  (MA) $\gamma\vee\neg\square\gamma$ $\gamma^{v}$ $\cal D$ $\bigvee\Delta$ $\bigvee\Delta\vee\neg\square\gamma$ $\neg\square\gamma^{u}$ $\bigvee\Delta\vee\neg\square\gamma$ $\vee$E,$u$,$v$ $\bigvee\Delta\vee\neg\square\gamma$
|  |
$\Gamma\Rightarrow\Delta,\neg\gamma$ ($\Rightarrow\neg\square$)2 $\Gamma\Rightarrow\Delta,\neg\square\gamma$ |  $\cal D$ $\bigvee\Delta\vee\neg\gamma$ |  $\cal D$ $\bigvee\Delta\vee\neg\gamma$ $\bigvee\Delta^{u}$ $\bigvee\Delta\vee\neg\square\gamma$ $\neg\gamma^{v}$ $\neg\square$I $\neg\square\gamma$ $\bigvee\Delta\vee\neg\square\gamma$ $\vee$E,$u$,$v$ $\bigvee\Delta\vee\neg\square\gamma$

(ii) implies (i): Let $\cal D$ be a deduction of the disjunction of the
sentences in $\Delta$ from $\Gamma$ in ${\bf ND}_{\cal TML}$. As before, we
use induction on the number $n$ of rule instances in the deduction $\cal D$.
If $r=0$ the proof is trivial. (I.H.) Suppose that “(ii) implies (i)” holds
for $n<k$, $k>0$; and let $(r)$ the last rule instance in $\cal D$. If $(r)$
is one of the introduction/elimination rule of $\wedge$I, $\wedge$E,
$\neg\wedge$I, $\neg\wedge$E, $\vee$I, $\vee$E , $\neg\vee$I, $\neg\vee$E,
$\neg\neg$I and $\neg\neg$E; the proof is immediate since these rules are just
translations of the corresponding rules of ${\bf SC}_{\cal TML}$. Suppose that
$(r)$ is $\square$I∗, then $\cal D$ is

${\cal D}_{1}$ $\psi\vee\phi$ [$\neg\phi$]u ${\cal D}_{2}$ $\psi$
$\square$I∗,$u$ $\psi\vee\square\phi$

Then, by (I.H), we have that the sequents $\Gamma_{1}\Rightarrow\psi\vee\phi$
and $\Gamma_{2},\neg\phi\Rightarrow\psi$ are provable in ${\bf SC}_{\cal
TML}$, where $\Gamma_{1}\cup\Gamma_{2}=\Gamma$. By using weakening(s) and the
cut rule we obtain $\Gamma\Rightarrow\psi,\phi$ and
$\Gamma\neg\phi\Rightarrow\psi$ are provable. Then, using
($\square\Rightarrow$), we have that $\vdash_{{\bf SC}_{\cal
TML}}\Gamma\Rightarrow\psi,\square\phi$. If $(r)$ is $\square$E, then $\cal D$
is

${\cal D}$ $\square\phi$ $\square$E $\phi$

By (I.H.), we have $\vdash_{{\bf SC}_{\cal TML}}\Gamma\Rightarrow\square\phi$.
From the fact that $\vdash_{{\bf SC}_{\cal TML}}\square\phi\Rightarrow\phi$
and the cut rule the proof is completed. If $(r)$ is $\neg\square$I, then
$\cal D$ is

${\cal D}$ $\neg\phi$ $\neg\square$I $\neg\square\phi$

By (I.H.), we have $\vdash_{{\bf SC}_{\cal TML}}\Gamma\Rightarrow\neg\phi$. By
Theorem 6.3, $\vdash_{{\bf SC}_{\cal TML}}\neg\neg\phi\Rightarrow\neg\Gamma$
and from $\vdash_{{\bf SC}_{\cal TML}}\phi\Rightarrow\neg\neg\phi$ and the cut
rule, we have $\vdash_{{\bf SC}_{\cal TML}}\phi\Rightarrow\neg\Gamma$. Using
($\square\Rightarrow)$ we obtain $\vdash_{{\bf SC}_{\cal
TML}}\square\phi\Rightarrow\neg\Gamma$ and by Theorem 6.3 $\vdash_{{\bf
SC}_{\cal TML}}\neg\neg\Gamma\Rightarrow\neg\square\phi$. Finally, from
$\vdash_{{\bf SC}_{\cal TML}}\Gamma\Rightarrow\neg\neg\Gamma$ and cut(s) (and
weakening(s) if necessary) we obtain $\vdash_{{\bf SC}_{\cal
TML}}\Gamma\Rightarrow\neg\square\phi$. If $(r)$ is $\neg\square$E, then $\cal
D$ is

${\cal D}_{1}$ $\neg\square\phi$ ${\cal D}_{2}$ $\phi$ $\neg\square$E
$\neg\phi$

By (I.H) and using weakening(s) we have that the sequents
$\Gamma\Rightarrow\neg\square\phi$ and $\Gamma\Rightarrow\phi$ are provable in
${\bf SC}_{\cal TML}$. Using ($\Rightarrow\wedge$), we obtain $\vdash_{{\bf
SC}_{\cal TML}}\Gamma\Rightarrow\phi\wedge\neg\square\phi$ and since
$\phi\wedge\neg\square\phi\Leftrightarrow\phi\wedge\neg\phi$ and the cut rule
we obtain $\vdash_{{\bf SC}_{\cal TML}}\Gamma\Rightarrow\phi\wedge\neg\phi$.
Finally, taking into account that $\vdash_{{\bf SC}_{\cal
TML}}\phi\wedge\neg\phi\Rightarrow\neg\phi$ we have $\vdash_{{\bf SC}_{\cal
TML}}\Gamma\Rightarrow\neg\phi$.
The cases in which $(r)$ is $\bot$I or $\bot$E are immediate (see Remark 5.5).
$\boldsymbol{\blacksquare}$

Since our natural deduction system is strongly inspired by the cut-free
sequent calculus ${\bf SC}_{\cal TML}$, one can likely expect normalization to
hold for ${\bf SC}_{\cal TML}$.

##  8 Conclusions

In the present paper we focused on the proof-theoretic aspects of the
tetravalent modal logic ${\cal TML}$. In the first place, we showed that the
strongly adequate Gentzen calculus given by Font and Rius for ${\cal TML}$
does not enjoy the cut–elimination property. Then, by applying a method due to
Avron, Ben-Naim and Konikowska, we developed a sequent calculus for $\cal TML$
with the cut–elimination property. This allowed us to provide new independent
proof of some known interesting properties of ${\cal TML}$. Finally, strongly
inspired by this cut–free sequent calculus, we presented a natural deduction
system, sound and complete with respect to the ${\cal TML}$.

Despite the fact that ${\cal TML}$ was originally defined as the logic that
preserves degrees of truth w.r.t. tetravalent modal algebras, we could use
Avron, Ben-Naim and Konikowska’s method; and this is because ${\cal TML}$ is
also a matrix logic. An interesting task to be done is to extend this method
to logics to logics that preserves degrees of truth w.r.t. some ordered
structure but which do not have a matrix semantics.

##  9 Acknowledgments

I would like to thank the anonymous referees for their extremely careful
reading, helpful suggestions and constructive comments on this paper.

## References

  * [1] Anderson, A. R. and Belnap N. D. (with contributions by thirteen others), Entailment: the logic of relevance and necessity, volume II, (1992) Princeton University Press.
  * [2] Avron, A.. Non-deterministic semantics for logics with a consistency operator. Journal of Approximate Reasoning, 45, 271–287, (2007).
  * [3] Avron, A. and Konikowska, B., Multi-valued Calculi for Logics Based on Non-determinism, Proceedings COS’04 (Challenge of Semantics Workshop), Vienna 2004, Journal of Interest Group in Pure and Applied Logic, 2005 (10), 365–387.
  * [4] Avron, A., Ben-Naim, J. and Konikowska, B., Cut-free ordinary sequent calculi for logics having generalzed finite–valued semantics. Logica Universalis, 1, 41–69, 2006.
  * [5] Arieli, O. and Avron, A., The value of the four values. Artificial Intelligence v. 102, n. 1 (1998), pp. 97–141.
  * [6] Belnap, N., How computers should think. In: Contemporary Aspects of Philosophy (Editor: G. Ryle). Oriol Press, pp. 30–56, 1976.
  * [7] Carnielli, W.A., Coniglio, M.E. and Marcos, J., Logics of Formal Inconsistency. In: Handbook of Philosophical Logic, vol. 14, pp. 15-107. Eds.: D. Gabbay; F. Guenthner. Springer, 2007.
  * [8] Carnielli, W.A. and Marcos, J., A taxonomy of C-systems. In W. A. Carnielli, M. E. Coniglio, and I. M. L. D’Ottaviano, editors, Paraconsistency — The logical way to the inconsistent, volume 228 of Lecture Notes in Pure and Applied Mathematics, pp. 1–94. Marcel Dekker, New York, 2002.
  * [9] Coniglio, M.E. and Figallo, M., Hilbert-style Presentations of Two Logics Associated to Tetravalent Modal Algebras , Studia Logica, nro. 3, vol. 102 (2014), 525–539.
  * [10] Da Costa, N.C.A., Calculs propositionnel pour les systèmes formels inconsistants. Comptes Rendus de l’Académie de Sciences de Paris, série A, vol. 257(1963), 3790–3792.
  * [11] Figallo, A.V. and Landini, P., On generalized I-algebras and 4-valued modal algebras. Reports on Mathematical Logic 29 (1995), 3–18.
  * [12] Font, J.M. and Rius, M., A four-valued modal logic arising from Monteiro’s last algebras. In Proc. 20th Int. Symp. Multiple-Valued Logic (Charlotte, 1990), The IEEE Computer Society Press, 85–92, 1991.
  * [13] Font, J.M. and Rius, M., An abstract algebraic logic approach to tetravalent modal logics. J. Symbolic Logic v. 65, n. 2 (2000), 481–518.
  * [14] Loureiro, I., Algebras modais tetravalentes, Ph. D. Thesis, Faculdade de Ciências de Lisboa, 1983.
  * [15] Troelstra, A. S. and Schwichtenberg, H., Basic Proof System. Cambridge, UK: Cambridge University Press (1996).