# Generating proof systems for
three-valued propositional logics

Vitor Greati (i) Universidade Federal do Rio Grande do Norte, Brazil and (ii)
University of Groningen, The Netherlands. Work supported by the FWF project
P33548. Giuseppe Greco Vrije Universiteit Amsterdam, The Netherlands. Sérgio
Marcelino SQIG - Instituto de Telecomunicações, Dep. Matemática - Instituto
Superior Técnico, Universidade de Lisboa, Portugal. Research funded by
FCT/MCTES through national funds and when applicable co-funded by EU under the
project UIDB/50008/2020. Alessandra Palmigiano (i) Vrije Universiteit
Amsterdam, The Netherlands and (ii) Department of Mathematics and Applied
Mathematics, University of Johannesburg, South Africa. The research of the
second and fourth author has been funded in part by the NWO grant
KIVI.2019.001. Umberto Rivieccio (i) Universidade Federal do Rio Grande do
Norte, Brazil and (ii) Universidad Nacional de Educación a Distancia, Spain.

###### Abstract

In general, providing an axiomatization for an arbitrary logic is a task that
may require some ingenuity. In the case of logics defined by a finite logical
matrix (three-valued logics being a particularly simple example), the
generation of suitable finite axiomatizations can be completely automatized,
essentially by expressing the matrix tables via inference rules. In this
chapter we illustrate how two formalisms, the _3-labelled calculi_ of Baaz,
Fermüller and Zach and the _multiple-conclusion (or Set-Set) Hilbert-style
calculi_ of Shoesmith and Smiley, may be uniformly employed to axiomatize
logics defined by a three-valued logical matrix. We discuss their main
properties (related to completeness, decidability and proof search) and make a
systematic comparison between both formalisms. We observe that either of the
following strategies are pursued: (i) expanding the _metalanguage_ of the
formalism (via labels or types) or (ii) generalizing the usual notion of
_subformula property_ (as done in recent work by C. Caleiro and S. Marcelino)
while remaining as close as possible to the original language of the logic. In
both cases, desirable requirements are to guarantee the decidability of the
associated symbolic procedure, as well as the possibility of an effective
proof search. The generating procedure common to both formalisms can be
described as follows: first (i) convert the matrix semantics into rule form
(we refer to this step as the _generating subprocedure_) and then (ii)
simplify the set of rules thus obtained, essentially relying on the defining
properties of any Tarskian consequence relation (we refer to this step as the
_streamlining subprocedure_). We illustrate through some examples that, if a
minimal expressiveness assumption is met (namely, if the matrix defining the
logic is _monadic_), then it is straightforward to define effective
translations guaranteeing the equivalence between the 3-labelled and the Set-
Set approach.

##  1 Introduction

Different types of logical calculi are better suited for different purposes.
As is well known, so-called _Gentzen-style_ (or _sequent_) _calculi_ are
commonly employed whenever we are interested in automatizing proof search. On
the other hand, so-called _natural deduction calculi_ are often taken as
benchmarks for deciding when two derivations amount to the same argument,
while _Hilbert-style calculi_ are a most useful tool in characterizing the
sets of formulas that are closed with respect to the derivability relation of
a given logic. In this chapter, we shall be concerned with automatizing proof
system generation, that is, with defining a _procedure for generating
decidable calculi_ for a large class of logics, namely all logics that can be
presented via a single finite-valued matrix and so, in particular, for three-
valued logics.

Before getting into further technical details, let us spend a few words on
what we mean by a _three-valued logic_ , as well as on the choice of the
particular logics considered in the present chapter. In the literature on
(non-classical) logics, a _finite-valued_ (propositional) logic is usually
taken to be a logic determined or defined by some finite structure, typically
a set whose elements are interpreted as truth values in some intuitive sense.
In turn, a _propositional logic_ is usually defined as a binary relation on
the set of formulas – inductively constructed from propositional variables by
means of a given set of propositional connectives – a relation that satisfies
the postulates laid out by A. Tarski [44, p. 31]; this is nowadays a standard
notion (though not the only existing one) in formal logic.

It has been shown that every propositional logic satisfying Tarski’s
postulates can be defined by means of a (possibly infinite) family of
(possibly infinite) _logical matrices_ [46]. It is thus fair to affirm that
logical matrices constitute a most general method (i.e. a standard
_semantics_) for introducing arbitrary (Tarskian) logics. From this
standpoint, finite-valued logics may be taken to be those logics that can be
defined by means of a _finite_ set of _finite_ logical matrices – one cannot,
without loss of generality, replace “finite set of finite matrices” by “a
single finite matrix” (see [16] for further discussion and counter-examples).
In this broad sense, _three-valued logics_ are thus those definable by some
finite set of three-element logical matrices (also in this case we cannot
replace “finite set” by “a single (three-element) matrix”). For technical
reasons, in the present chapter we shall narrow our focus to logics determined
by _a single matrix_. It is to these logics, as we shall illustrate through
plenty of examples, that the proof formalisms here considered apply more
straightforwardly111The techniques we present are not limited to the single
matrix case (regarding multiple conclusion calculi, see e.g. [14]). However,
in order to deal with arbitrary three-valued (or indeed, more generally,
finite-valued) logics, one needs more sophisticated tools (e.g. from the
theory of partial and non-deterministic matrices; cf. Section 7) that would
not fit well within the scope of the present contribution..

By the above considerations, we shall fix a three-element set, say
$\\{\mathbf{0},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\mathbf{1}\\}$, as our
standard space of truth values. A particular three-valued logic is then
determined by a choice of propositional connectives (each determined by the
corresponding truth table) together with a choice of one or more sets of
_designated_ truth values. All the non-trivial three-valued logics arise in
this way when combining the logics obtained by designating either a singleton
(say $\\{\mathbf{1}\\}$) or a two-element set (say
$\\{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\mathbf{1}\\}$).

Over an arbitrary propositional language, the number of three-valued truth
tables (and therefore of possible logics) obtainable in the above-described
way is obviously unbounded: in the present chapter we shall consider a few
examples chosen according to the criteria detailed below (see Section 3). We
shall introduce 3-labelled calculi [7] and Set-Set Hilbert-style calculi [42]
for a number of logics determined by a single three-valued matrix, as well as
what we call their _streamlined_ versions. We shall discuss their main
properties (completeness, decidability, effective proof search) and draw a
first systematic comparison of both formalisms.

Set-Set Hilbert-style calculi are a generalization of traditional Hilbert-
style calculi (introduced by Frege and popularized by Hilbert) in the sense
that their metalanguage is reduced to a minimum, and inference rules just
manipulate _sets of formulas_ that constitute consecutions of (that is, belong
to) the underlying logic. 3-labelled calculi, on the other hand, are not
Hilbert-style, for their language includes labels and rules manipulate _sets
of labelled formulas_ or, equivalently, _3-sequents_. The 3-labelled calculi
generated for three-valued logics, as we will see, can actually be seen as
generalizations of “multiple-conclusion sequent calculi” (see [33, Chapter
3]), insofar as the distinction between structural and logical rules is in
place, with zeroary rules being a generalized form of identity rules, cut
rules being a generalized form of (multi)cuts, and each connective being
associated with its own set of introduction rules.

We observe, however, that the core of the corresponding generating procedures
is essentially the same, and amounts to first (i) converting the matrix
semantics in rule form (we refer to this step as the _generating
subprocedure_) and then (ii) simplifying the set of rules thus obtained,
essentially relying on the defining properties of any Tarskian consequence
relation (we refer to this step as the _streamlining subprocedure_). The key
point where both generating subprocedures depart from each other has to do
with the specific properties of the output. In the case of 3-labelled calculi,
we can rely on labels corresponding to truth values, so turning matrices into
rule form is a quite straightforward process. In the case of Set-Set Hilbert-
style calculi, this additional information has to be conveyed in the logical
language, hence the need of _separators_ , which are logical formulas capable
of telling apart truth values pairwise in a sense that will be formally
specified in Section 5.1.

The chapter is organized as follows. In Section 2, we introduce basic notions
and terminology about algebras, languages, logics and logical matrices. In
Section 3, we provide an overview of the selected three-valued logics that
will be discussed in subsequent sections. We devote special attention to the
traditional Hilbert-style calculi available in the literature for such logics,
highlighting the fact that for some of them no finite calculus is currently
known (whilst Set-Set finite calculi are guaranteed to exist by [42]). In
Section 4, we introduce the formalism of 3-labelled calculi and associated
procedures for generating and streamlining analytic calculi for three-valued
logics. We do the same in Section 5 for the formalism of Set-Set Hilbert-style
calculi. Despite the fact that the generating subprocedure in the latter case
demands an expressiveness condition to be satisfied by the logical matrix at
hand, we will provide analytic finite axiomatizations for some non-
sufficiently expressive matrices in Subsection 5.2 (note that the result of
[42] just referred to does not mention analyticity). In Section 6 we compare
the generating procedures for 3-labelled calculi and Set-Set Hilbert-style
calculi, showing possibilities of translations from Set-Set to 3-labelled
rules and proofs. Finally, Section 7 closes the chapter with some concluding
remarks and suggestions for further research.

##  2 Preliminaries

A _(propositional) signature_ is a family
$\Sigma:=\\{\Sigma_{k}\\}_{k\in\omega}$, where each $\Sigma_{k}$ is a
collection of $k$-ary _connectives_ (we qualify a connective as _nullary_ when
$k=0$, as _unary_ when $k=1$, and as _binary_ when $k=2$). A signature is
finite when $\bigcup_{k\in\omega}\Sigma_{k}$ is finite. In this work, the
considered examples are in propositional signatures containing the unary
connectives $\neg,\circ,\bullet$ and $\Diamond$, and the binary connectives
$\land,\lor$ and $\to$. A _$\Sigma$ -algebra_ is a structure
$\mathbf{A}:=\langle A,{\cdot}_{\mathbf{A}}\rangle$, where $A$ is a non-empty
set called the _carrier_ or _universe_ of $\mathbf{A}$ and, for each
$\copyright\in\Sigma_{k}$ and $k\in\omega$,
${\copyright}_{\mathbf{A}}:A^{k}\to A$ is the _interpretation_ of $\copyright$
in $\mathbf{A}$. A $\Sigma$-algebra is _finite_ when both $\Sigma$ and its
carrier are finite. Given a denumerable set $P$ of _propositional variables_ ,
the absolutely free algebra over $\Sigma$ freely generated by $P$, or simply
the _(propositional) language_ over $\Sigma$ (generated by $P$), is denoted by
$\mathbf{L}_{\Sigma}(P)$, and its members are called _$\Sigma$ -formulas_. The
set of all subformulas of a given formula $\varphi\in L_{\Sigma}(P)$ will be
denoted by $\mathsf{subf}(\varphi)$, and the set of all propositional
variables occurring in $\varphi$ will be denoted by $\mathsf{props}(\varphi)$.
Given $\Phi\subseteq L_{\Sigma}(P)$, we let
${\Phi}^{\mathsf{c}}:=L_{\Sigma}(P){\setminus}\Phi$.

The collection of homomorphisms between two $\Sigma$-algebras $\mathbf{A}$ and
$\mathbf{B}$ is denoted by $\mathsf{Hom}(\mathbf{A},\mathbf{B})$. Furthermore,
the set of endomorphisms on $\mathbf{A}$ is denoted by
$\mathsf{End}(\mathbf{A})$ and each one of the members
$\sigma\in\mathsf{End}(\mathbf{L}_{\Sigma}(P))$ is called a _substitution_. In
case $p_{1},\ldots,p_{n}$ are the only propositional variables occurring in
$\varphi\in L_{\Sigma}(P)$, we say that $\varphi$ is $n$-ary and denote by
$\varphi_{\mathbf{A}}$ the $n$-ary operation on $A$ such that, for all
$a_{1},\ldots,a_{n}\in A$,
$\varphi_{\mathbf{A}}(a_{1},\ldots,a_{n})=h(\varphi)$, for an
$h\in\mathsf{Hom}(\mathbf{L}_{\Sigma}(P),\mathbf{A})$ with $h(p_{i})=a_{i}$
for each $1\leq i\leq n$. Instead of using “$n$-ary”, we may conveniently use
the word _unary_ , when $n=1$, and _binary_ , when $n=2$, as we do for
connectives. Also, if $\psi_{1},\ldots,\psi_{n}\in L_{\Sigma}(P)$, we let
$\varphi(\psi_{1},\ldots,\psi_{n})$ denote the formula
${\varphi}_{{\mathbf{L}_{\Sigma}(P)}}(\psi_{1},\ldots,\psi_{n})$. Moreover,
when $\Theta$ is a set of $n$-ary formulas, we let
$\Theta(\psi_{1},\ldots,\psi_{n}):=\\{\varphi(\psi_{1},\ldots,\psi_{n})\mid\varphi\in\Theta\\}$.

In what follows, we report the usual definitions of propositional logics as
consequence relations over a propositional language.

######  Definition 2.1.

A _(finitary)_ Set-Fmla _logic_ is a relation
$\vdash\,\subseteq\,\mathcal{P}(L_{\Sigma}(P))\times L_{\Sigma}(P)$ satisfying
the following ‘Tarski’ conditions [44, p. 31], for all
$\Phi,\Psi,\Pi,\\{\varphi,\psi\\}\subseteq L_{\Sigma}(P)$:

(R)eflexivity | $\Phi,\varphi\vdash\varphi$
---|---
(M)onotonicity |  if $\Phi\vdash\psi$, then $\Phi,\Psi\vdash\psi$
(T)ransitivity |  if $\Phi,\Pi\vdash\psi$ and $\Phi\vdash\gamma$ for each $\gamma\in\Pi$, then $\Phi\vdash\psi$
(S)tructurality |  if $\Phi\vdash\psi$ and $\sigma\in\mathsf{End}(\mathbf{L}_{\Sigma}(P))$, then $\sigma(\Phi)\vdash\sigma(\psi)$
(F)initariness |  if $\Phi\vdash\psi$, then $\Phi^{\prime}\vdash\psi$ for some finite $\Phi^{\prime}\subseteq\Phi$

######  Definition 2.2.

A _(finitary)_ Set-Set _logic_ is a relation
$\rhd\,\subseteq\,\mathcal{P}(L_{\Sigma}(P))\times\mathcal{P}(L_{\Sigma}(P))$
satisfying the following ‘Scott’ conditions [42], for all
$\Phi,\Phi^{\prime},\Psi,\Psi^{\prime}\subseteq L_{\Sigma}(P)$:

(O)verlap |  if $\Phi\cap\Psi\neq\varnothing$, then $\Phi\rhd\Psi$
---|---
(D)ilution |  $\Phi\rhd\Psi$, then $\Phi,\Phi^{\prime}\rhd\Psi,\Psi^{\prime}$
(C)ut for sets |  if $\Phi,\Pi\rhd{\Pi}^{\mathsf{c}},\Psi$ for all $\Pi\subseteq L_{\Sigma}(P)$, then $\Phi\rhd\Psi$
(S)tructurality |  if $\Phi\rhd\Psi$ and $\sigma\in\mathsf{End}(\mathbf{L}_{\Sigma}(P))$, then $\sigma(\Phi)\rhd\sigma(\Psi)$
(F)initariness |  if $\Phi\rhd\Psi$, then $\Phi^{\prime}\rhd\Psi^{\prime}$ for some finite $\Phi^{\prime}\subseteq\Phi$ and $\Psi^{\prime}\subseteq\Psi$

Every Set-Set logic $\rhd$ induces a Set-Fmla logic $\vdash_{\rhd}$ such that
$\Phi\vdash_{\rhd}\psi$ if, and only if, $\Phi\rhd\\{\psi\\}$. The complement
of a Set-Set logic $\rhd{}$ is denoted by $\blacktriangleright$.

A _(deterministic logical) $\Sigma$-matrix_ $\mathbb{M}$ is a structure
$\langle\mathbf{A},D\rangle$ where $\mathbf{A}$ is a $\Sigma$-algebra, the
universe $A$ is the set of _truth values of $\mathbb{M}$_, and the members of
$D\subseteq A$ are called _designated values_. We will write $\overline{D}$ to
refer to $A{\setminus{}}D$. A matrix is _finite_ when its underlying algebra
is finite. In this chapter, we will most of the time work with the set
$V_{3}:=\\{\mathbf{0},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\mathbf{1}\\}$ of
truth values. The mappings in
$\mathsf{Hom}(\mathbf{L}_{\Sigma}(P),\mathbf{A})$ are called _$\mathbb{M}$
-valuations_. Every $\Sigma$-matrix determines a Set-Set logic
$\rhd_{\mathbb{M}}$ such that $\Phi\rhd_{\mathbb{M}}\Psi$ iff
$h(\Phi)\cap\overline{D}\neq\varnothing$ or $h(\Psi)\cap D\neq\varnothing$ for
every $\mathbb{M}$-valuation $h$, as well as a Set-Fmla logic
$\vdash_{\mathbb{M}}$ with $\Phi\vdash_{\mathbb{M}}\psi$ iff
$\Phi\rhd_{\mathbb{M}}\\{\psi\\}$. Given a Set-Set logic $\rhd$ (resp. a Set-
Fmla logic $\vdash$), if $\rhd\;\subseteq\;\rhd_{\mathbb{M}}$ (resp.
$\vdash\;\subseteq\;\vdash_{\mathbb{M}}$), we shall say that $\mathbb{M}$ _is
a model of_ $\rhd$ (resp. $\vdash$), and if the converse also holds we shall
say that $\mathbb{M}$ _characterises_ $\rhd$ (resp. $\vdash$).

The pairs $(\Phi,\psi)\in\mathcal{P}(L_{\Sigma}(P))\times L_{\Sigma}(P)$
(resp.
$(\Phi,\Psi)\in\mathcal{P}(L_{\Sigma}(P))\times\mathcal{P}(L_{\Sigma}(P))$)
are called Set-Fmla _statements_ (resp. Set-Set _statements_), and we say that
such statements hold according to a Set-Fmla logic $\vdash$ (resp. a Set-Set
logic $\rhd$) when $\Phi\vdash\psi$ (resp. when $\Phi\rhd\Psi$). In what
follows, we use ‘H-calculus’ for “Hilbert-style calculus” and ‘H-rule’ for
“Hilbert-style rule of inference”. A _Set-Fmla H-calculus_ is a collection of
Set-Fmla statements $(\Phi,\psi)$, which, in this context, are called _Set-
Fmla H-rules_ and denoted by

$\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
25.44444pt\hbox{\vbox{\hbox{\hskip 3.0pt\hbox{\hskip 4.0pt\hbox{$\Phi$}\hskip
4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{{$$}\hskip 3.0pt}\hbox
to15.22223pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 3.0pt\hbox{\hskip
0.35416pt\hbox{\hbox{\hskip 4.0pt\hbox{$\psi$}\hskip
4.0pt}}}}}}\ignorespaces,$

being $\Phi$ the _antecedent_ (or _set of premises_) and $\psi$, the
_succedent_ (or _conclusion_) of the rule. H-rules with empty antecedents are
called _axioms_. As usual, given a Set-Fmla H-calculus $\mathcal{H}$, we say
that the Set-Fmla statement $(\Phi,\psi)$ is _provable_ in $\mathcal{H}$
whenever there is a finite sequence of formulas
$\varphi_{1},\ldots,\varphi_{n}$, where $\varphi_{n}=\psi$ and each
$\varphi_{i}$ is either a premise (that is, a formula in $\Phi$) or follows
from previous formulas in the sequence by an instance of a H-rule of
$\mathcal{H}$. The relation
$\vdash_{\mathcal{H}}\,\subseteq\,\mathcal{P}(L_{\Sigma}(P))\times
L_{\Sigma}(P)$ defined such that $\Phi\vdash_{\mathcal{H}}\psi$ if, and only
if, the statement $(\Phi,\psi)$ is provable in $\mathcal{H}$ is easily seen to
be a finitary Set-Fmla logic. In Section 5, we shall introduce Set-Set
H-calculi (based on [42]), which generalize Set-Fmla H-calculi by allowing for
sets of formulas to appear as succedents of the rules of inference.

##  3  Prominent three-valued logics

For the most part of this chapter, we shall be dealing with logics that have
an independent interest (i.e. not purely formal but also philosophical or
historical), having been introduced by renowned logicians with particular
applications or motivations in mind: this is for instance the case of the
time-honoured logical systems Ł3, G3 and K, which bear the names of J.
Łukasiewicz, K. Gödel and S. C. Kleene.

In Section 5.2, we shall also consider a few logics whose interest is mostly
theoretical, in that they will help us exemplify certain advantages or
difficulties related to the Set-Set approach: this will be, in particular, the
case of logics defined by non-monadic matrices, such as the implicative
fragment of Łukasiewicz logic.

A third criterion guiding our choice (partly overlapping with the first) has
been to include the three-valued logics that appear in other chapters of the
present book, in particular in the contributions by A. Avron & A. Zamansky [6]
and by F. Paoli & M. Pra Baldi [36].

Logic | $D$ |  Interpretations
---|---|---
Łukasiewicz (Ł3) | $\\{\mathbf{1}\\}$ |  $\land_{\mathsf{min}}$, $\lor_{\mathsf{max}}$, $\lnot_{\textbf{{\L${}_{3}$}}}$, $\to_{\textrm{{{\L${}_{3}$}}}}$
Logic of Paradox (LP) | $\\{\mathbf{1},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\\}$ |  $\land_{\mathsf{min}}$, $\lor_{\mathsf{max}}$, $\lnot_{\textbf{{\L${}_{3}$}}}$
Logic of Paradox with implication (LP→) | $\\{\mathbf{1},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\\}$ |  $\land_{\mathsf{min}}$, $\lor_{\mathsf{max}}$, $\lnot_{\textbf{{\L${}_{3}$}}}$, $\to_{\textbf{{LP}}}$
Bochvar-Kleene (BK) | $\\{\mathbf{1}\\}$ |  $\land_{\textbf{{BK}}}$, $\lor_{\textbf{{BK}}}$, $\lnot_{\textbf{{\L${}_{3}$}}}$, $\to_{\textbf{{BK}}}$
Paraconsistent Weak Kleene (PK) | $\\{\mathbf{1},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\\}$ |  $\land_{\textbf{{BK}}}$, $\lor_{\textbf{{BK}}}$, $\lnot_{\textbf{{\L${}_{3}$}}}$, $\to_{\textbf{{BK}}}$
Sette’s (S) | $\\{\mathbf{1},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\\}$ |  $\to_{\textbf{{S}}}$, $\lnot_{\textbf{{S}}}$
Sobociński (S3) | $\\{\mathbf{1},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\\}$ |  $\lnot_{\textbf{{\L${}_{3}$}}}$, $\to_{\textbf{{S3}}}$
Da Costa-D’Ottaviano’s (J3) | $\\{\mathbf{1},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\\}$ |  $\land_{\mathsf{min}}$, $\lor_{\mathsf{max}}$, $\lnot_{\textbf{{\L${}_{3}$}}}$, $\to_{\textbf{{J3}}}$, $\Diamond:=\lnot_{\textbf{{S}}}$
Gödel (G3) | $\\{\mathbf{1}\\}$ |  $\land_{\mathsf{min}}$, $\lor_{\mathsf{max}}$, $\lnot_{\textbf{{G3}}}$, $\to_{\textbf{{G3}}}$
Strong Kleene (K) | $\\{\mathbf{1}\\}$ |  $\land_{\mathsf{min}}$, $\lor_{\mathsf{max}}$, $\lnot_{\textbf{{\L${}_{3}$}}}$, $\to_{\textbf{{K}}}$
Post’s (P3) | $\\{\mathbf{1}\\}$ |  $\land_{\mathsf{min}},\lor_{\mathsf{max}},\lnot_{\textbf{{P3}}}$
L7 | $\\{\mathbf{1}\\}$ |  $\bullet_{7}$
L8 | $\\{\mathbf{1}\\}$ |  $\bullet_{8}$
Table 1: Summary of the three-valued logics considered in this chapter. Each
row refers to a logic, first informing its name, then the set $D\subseteq
V_{3}$ of designated truth values and the interpretations of the connectives
in the corresponding logical matrix, associated with the truth tables
presented in Figure 1.

$\land_{\mathsf{min}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{0}$ | $\mathbf{0}$ | $\mathbf{0}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$
$\mathbf{1}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$

$\lor_{\mathsf{max}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
$\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$

$\to_{\textrm{{{\L${}_{3}$}}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$ | $\mathbf{1}$
$\mathbf{1}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$

| $\lnot_{\textbf{{\L${}_{3}$}}}$
---|---
$\mathbf{0}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$
$\mathbf{1}$ | $\mathbf{0}$

$\to_{\textbf{{K}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
$\mathbf{1}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$

$\to_{\textbf{{LP}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
$\mathbf{1}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$

$\land_{\textbf{{BK}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{0}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$
$\mathbf{1}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$

$\lor_{\textbf{{BK}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$
$\mathbf{1}$ | $\mathbf{1}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$

$\to_{\textbf{{BK}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{1}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$
$\mathbf{1}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$

$\to_{\textbf{{S}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{0}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{0}$
$\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$

| $\lnot_{\textbf{{S}}}$
---|---
$\mathbf{0}$ | $\mathbf{0}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
$\mathbf{1}$ | $\mathbf{1}$

$\to_{\textbf{{S3}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
$\mathbf{1}$ | $\mathbf{0}$ | $\mathbf{0}$ | $\mathbf{1}$

$\to_{\textbf{{J3}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
$\mathbf{1}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$

$\to_{\textbf{{G3}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{0}$ | $\mathbf{1}$ | $\mathbf{1}$
$\mathbf{1}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$

| $\lnot_{\textbf{{G3}}}$
---|---
$\mathbf{0}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{0}$
$\mathbf{1}$ | $\mathbf{0}$

| $\lnot_{\textbf{{P3}}}$
---|---
$\mathbf{0}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{0}$
$\mathbf{1}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$

$\bullet_{7}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$
$\mathbf{1}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$ | $\mathbf{1}$

$\bullet_{8}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$ | $\mathbf{1}$ | $\mathbf{1}$
$\mathbf{1}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$ | $\mathbf{1}$

Figure 1: Three-valued interpretations for the connectives of the logics
listed in Table 1.

The three-valued logics of interest are all listed in Table 1. We provide
below a more detailed description of them, retrieving from the literature a
(not necessarily finite or analytic) Set-Fmla H-calculus, when available.

##### Łukasiewicz (Ł3).

The logic Ł3 was introduced more than a century ago (1920) by Jan Łukasiewicz,
in a short paper [48] written in Polish (for an English translation, see
[49]). Łukasiewicz’s intention was to challenge classical logic (which is
based on the Aristotelian principle of contradiction) by introducing a third
truth value meant to represent propositions that are neither false nor true
but only _possible_. Although there is nowadays consensus that Ł3 does not
successfully model the logic of possibility (this task having been taken over
by modal logic), Łukasiewicz’s proposal was later generalized to $n$-valued
logics (for each $n<\omega$) and even to an infinite-valued one, leading over
time to a huge research output in the area of mathematical logic (more
recently, in particular, in the mathematical fuzzy logic community: see e.g.
[28]).

Various inter-definabilities hold among the connectives of Łukasiewicz logics,
which in many presentations also include a _multiplicative disjunction_
($\oplus$) and a _multiplicative conjunction_ ($\odot$) given, in terms of our
primitive connectives, by $\varphi\oplus\psi:=\neg\varphi\to\psi$ and
$\varphi\odot\psi:=\neg(\varphi\to\neg\psi)$. Every logic in the Łukasiewicz
family can be presented in the language (first used by M. Wajsberg to
axiomatize the infinite-valued Łukasiewicz logic) having only the implication
$(\to)$ and the negation $(\neg)$ as primitive: one defines
$\varphi\lor\psi:=(\varphi\to\psi)\to\psi$ and, as in K below,
$\varphi\land\psi:=\neg(\neg\varphi\lor\neg\psi)$. The implication, in turn,
can be given by $\varphi\to\psi:=\neg\varphi\oplus\psi$ but is not definable
by the classical formula $\neg\varphi\lor\psi$ nor, indeed, by any formula
constructed from the remaining connectives chosen for our presentation
(conjunction, the disjunction and the negation).

The following is an adequate (sound and complete) calculus for Ł3, which can
be found in [4]:

$(\textbf{{\L${}_{3}$}}1)$ $\varphi\rightarrow(\psi\rightarrow\varphi)$
---
$(\textbf{{\L${}_{3}$}}2)$
$(\varphi\rightarrow\psi)\rightarrow((\psi\rightarrow\gamma)\rightarrow(\varphi\rightarrow\gamma))$
$(\textbf{{\L${}_{3}$}}3)$
$(\varphi\rightarrow(\psi\rightarrow\gamma))\rightarrow(\psi\rightarrow(\varphi\rightarrow\gamma))$
$(\textbf{{\L${}_{3}$}}4)$
$((\varphi\rightarrow\psi)\rightarrow\psi)\rightarrow((\psi\rightarrow\varphi)\rightarrow\varphi)$
$(\textbf{{\L${}_{3}$}}5)$
$((((\varphi\rightarrow\psi)\rightarrow\varphi)\rightarrow\varphi)\rightarrow(\psi\rightarrow\gamma))\rightarrow(\psi\rightarrow\gamma)$
$(\textbf{{\L${}_{3}$}}6)$ $\varphi\wedge\psi\rightarrow\varphi$
$(\textbf{{\L${}_{3}$}}7)$ $\varphi\wedge\psi\rightarrow\psi$
$(\textbf{{\L${}_{3}$}}8)$
$(\varphi\rightarrow\psi)\rightarrow((\varphi\rightarrow\gamma)\rightarrow(\varphi\rightarrow\psi\wedge\gamma))$
$(\textbf{{\L${}_{3}$}}9)$ $\varphi\rightarrow(\varphi\vee\psi)$
$(\textbf{{\L${}_{3}$}}10)$ $\psi\rightarrow(\varphi\vee\psi)$
$(\textbf{{\L${}_{3}$}}11)$
$(\varphi\rightarrow\gamma)\rightarrow((\psi\rightarrow\gamma)\rightarrow(\varphi\vee\psi\rightarrow\gamma))$
$(\textbf{{\L${}_{3}$}}12)$
$(\neg\psi\rightarrow\neg\varphi)\rightarrow(\varphi\rightarrow\psi)$
$\varphi\quad\varphi\rightarrow\psi$ $(\textbf{{\L${}_{3}$}}13)$ $\psi$

##### Strong Kleene (K).

In his book [30], the prominent mathematician S.C. Kleene introduced two
three-valued logics that nowadays bear his name. The first we consider (K) is
defined by the same truth tables as Ł3 as far as the connectives $\land,\lor$
and $\neg$ are concerned, whereas it differs in the implication (usually not
included in the primitive language), which may be given by
$\varphi\to\psi:=\neg\varphi\lor\psi$. Thus, formally, K is easily shown to
coincide with the $\\{\land,\lor,\neg\\}$-fragment of Ł3. The meaning Kleene
had in mind for the third value is, however, different from the Łukasiewicz
case, for $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ is now interpreted as
_undefined_ (rather than _possible_ , as in Ł3). Such an interpretation can be
justified within the theory of partial recursive functions, to which Kleene in
fact gave major contributions.

The notion of partial function generalizes that of ordinary function in that
the former may be undefined for some arguments, that is, we admit that no
output may be produced for certain inputs. Thus, for a given function $f$ on
integers and a given input $x$, we have three cases: either $f(x)=5$ or
$f(x)\neq 5$ or $f(x)$ is undefined; within K, a proposition corresponding to
the latter situation would be labelled by the truth value
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$. Notice also that the truth tables of
K reflect the following observation: even if the value of some atomic
proposition (say $p$) is undefined, we may still be able to assign a classical
value to a compound proposition (say $p\lor q$) in which $p$ appears, for it
suffices to know that $q$ is true. This reasoning also makes perfect sense
from a computational point of view: a program that computes the value of
$p\lor q$ may output the value $\mathbf{1}$ as soon as it successfully manages
to establish that (e.g.) $q$ has value $\mathbf{1}$, even if the computation
involving $p$ has not terminated yet.

A convenient way to axiomatize K (as well as LP considered further on) is to
start from a common weakening of both logics, namely four-valued Belnap-Dunn
logic, B. The latter (on which we shall say more in a little while) is
axiomatized by the following Set-Fmla H-calculus introduced in [41] (an almost
identical calculus was independently introduced in [25]):

$\varphi\wedge\psi$ ($\textbf{{K}}1$)  $\varphi$ |  $\varphi$ $\psi$ ($\textbf{{K}}3$)  $\varphi\wedge\psi$
---|---
$\varphi$ ($\textbf{{K}}4$)  $\varphi\vee\psi$ |  $\varphi\vee(\psi\vee\gamma)$ ($\textbf{{K}}6$)  $(\varphi\vee\psi)\vee\gamma$
$\varphi\vee(\psi{\wedge}\gamma)$ ($\textbf{{K}}7$)  $(\varphi\vee\psi)\wedge(\varphi\vee\gamma)$ |  $\varphi\vee\varphi$ ($\textbf{{K}}9$)  $\varphi$
$\varphi\vee\psi$ ($\textbf{{K}}10$)  $\neg\neg\varphi\vee\psi$ |  $(\neg\varphi\wedge\neg\psi)\vee\gamma$ ($\textbf{{K}}12$)  $\neg(\varphi\vee\psi)\vee\gamma$
$\neg(\varphi\vee\psi)\vee\gamma$ ($\textbf{{K}}13$)  $(\neg\varphi\wedge\neg\psi)\vee\gamma$ |  $\neg(\varphi\wedge\psi)\vee\gamma$ ($\textbf{{K}}15$)  $(\neg\varphi\vee\neg\psi)\vee\gamma$

As shown in [1], strong Kleene logic may be obtained by adding to the
preceding calculus the following rule:

$(\varphi\wedge\neg\varphi)\vee\psi$ ($\textbf{{K}}16$)  $\psi$ |  |
---|---|---

Notice that K does not have theorems, so it cannot be presented via a calculus
with closed assumptions (i.e. axioms).

##### Logic of Paradox (LP).

This logic was introduced (under the name _calculus of antinomies_) in the
1960s by F. G. Asenjo [3], but was studied in greater depth and made popular a
decade later by G. Priest, who also proposed the name we are adopting here:
_Logic of Paradox_. The intention of both authors was to develop a logical
framework that might allow one to handle logical paradoxes (also known as
_antinomies_) without trivializing the whole system, as happens in the
classical setting. Antinomies are propositions that, like the famous Russell’s
paradox, appear to be _both true and false_ at the same time. From the point
of view of a particular logic, we can say that an antinomy is a proposition
$p$ such that both $p$ and $\neg p$ assume a designated value. The logic
devised by Asenjo-Priest is therefore (a most prominent example of) a
_paraconsistent logic_ , i.e. one that rejects the following _ex
contradictione quodlibet_ rule:

$\varphi\wedge\neg\varphi$ ($\mathbf{ECQ}$)  $\psi$ |  |
---|---|---

Semantically, achieving such a behavior is easy: one may just adopt the same
truth tables as Kleene’s K while having
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ designated together with $\mathbf{1}$.
This simple strategy, while necessarily renouncing some derivations that hold
classically, allows LP to actually retain all the tautologies of classical
logic (see below).

As mentioned earlier, the Belnap-Dunn logic E is, formally, a weakening common
to LP and K. It may be interesting to mention that, in fact, the four-valued
matrix which defines E is obtained by simultaneously enlarging the set
$\\{\mathbf{0},\mathbf{1}\\}$ with two non-classical truth values: the former
(usually called n, for _neither_ true nor false) behaves as
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ does in K (n is a fixpoint of the
negation operator, but is not designated) and the latter (usually called b,
for _both_ true and false) behaves as $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$
does in LP (b is also a fixpoint of the negation operator but it is
designated).

As shown in [1, Thm. 3.4], LP can be axiomatized through the Set-Fmla
H-calculus extending E by the _exluded middle_ axiom:

$(\textbf{{LP}}1)$ $\varphi\lor\neg\varphi$
---

As mentioned earlier, the tautologies of LP are precisely the ones of
classical logic [39, Thm. III.8, p. 228], so classical logic and LP only
differ as far as proper inferences (that is, those with nonempty sets of
premises) are concerned.

##### Logic of Paradox with implication (LP→).

As in Kleene’s K, one can define within LP an implication connective by the
term $\neg\varphi\lor\psi$. Such an implication, however, will not enjoy the
Deduction Theorem, and indeed it will not even satisfy _modus ponens_ (adding
the latter rule to LP is already sufficient to regain classical logic). A
stronger result is shown in [2, Prop. 8]: no connective definable in LP can
possibly enjoy the Deduction Theorem. It is, however, possible to expand LP
with a new implication that enjoys the Deduction Theorem and still does not
force the resulting logic to become classical. This logic, which we shall
denote by LP→, seems to have been first considered in [9]. A Set-Fmla
H-calculus for LP→ may be obtained as follows. Let us start from the system
HBe from [4]:

$(\textbf{{LP}${}^{\rightarrow}{}$}1)$
$\varphi\rightarrow(\psi\rightarrow\varphi)$
---
$(\textbf{{LP}${}^{\rightarrow}{}$}2)$
$(\varphi\rightarrow(\psi\rightarrow\gamma))\rightarrow((\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\gamma))$
$(\textbf{{LP}${}^{\rightarrow}{}$}3)$
$((\varphi\rightarrow\psi)\rightarrow\varphi)\rightarrow\varphi$
$(\textbf{{LP}${}^{\rightarrow}{}$}4)$ $(\varphi\wedge\psi)\rightarrow\varphi$
$(\textbf{{LP}${}^{\rightarrow}{}$}5)$ $(\varphi\wedge\psi)\rightarrow\psi$
$(\textbf{{LP}${}^{\rightarrow}{}$}6)$
$\varphi\rightarrow(\psi\rightarrow(\varphi\wedge\psi))$
$(\textbf{{LP}${}^{\rightarrow}{}$}7)$ $\varphi\rightarrow(\varphi\vee\psi)$
$(\textbf{{LP}${}^{\rightarrow}{}$}8)$ $\psi\rightarrow(\varphi\vee\psi)$
$(\textbf{{LP}${}^{\rightarrow}{}$}9)$
$(\varphi\rightarrow\gamma)\rightarrow((\psi\rightarrow\gamma)\rightarrow((\varphi\vee\psi)\rightarrow\gamma))$
$(\textbf{{LP}${}^{\rightarrow}{}$}10)$
$\neg(\varphi\vee\psi)\leftrightarrow\neg\varphi\wedge\neg\psi$
$(\textbf{{LP}${}^{\rightarrow}{}$}11)$
$\neg(\varphi\wedge\psi)\leftrightarrow\neg\varphi\vee\neg\psi$
$(\textbf{{LP}${}^{\rightarrow}{}$}12)$
$\neg\neg\varphi\leftrightarrow\varphi$
$(\textbf{{LP}${}^{\rightarrow}{}$}13)$
$\neg(\varphi\rightarrow\psi)\leftrightarrow\varphi\wedge\neg\psi$
$\varphi\quad\varphi\rightarrow\psi$ $(\textbf{{LP}${}^{\rightarrow}{}$}14)$
$\psi$

The logic LP→ can be obtained from HBe by adding either of the following
axioms (see [4, Sec. 4], where LP→ is called Pac).

$(\textbf{{LP}${}^{\rightarrow}{}$}15)$ $\varphi\lor\neg\varphi$
---
$(\textbf{{LP}${}^{\rightarrow}{}$}16)$
$(\psi\to\varphi)\to((\psi\to\neg\varphi)\to\neg\psi)$

##### Paraconsistent Weak Kleene (PK).

This logic seems to have been considered already by S. Halldén in his 1949
monograph [29], and two decades later by A. Prior [40], but has only recently
been studied in depth (see e.g. [12], and also [19] which explores
applications to the theory of truth).

The connectives and truth tables of PK coincide with those of BK (see the next
subsection), and so does the interpretation of the middle value. Logical
consequence, however, is defined in PK in terms of preservation of non-falsity
rather than (as in BK) of preservation of truth. This choice leads to
designating $\\{\mathbf{1},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\\}$, which
entails (as we have seen with LP) that PK is indeed a paraconsistent logic. In
fact the valid formulas of PK coincide with those of LP which, as observed
earlier, are precisely the classical tautologies (see e.g. [12, p. 257]).
However, PK and LP differ in their derivations. To see this, let us recall
that PK can be axiomatized as follows. Take any complete Set-Fmla H-calculus
for classical logic (having _modus ponens_ as its only non-nullary rule) and,
while keeping all the axioms, replace _modus ponens_ by the following
restricted version (see [12, Prop. 4]):

$\varphi\quad\varphi\rightarrow\psi$ $(\textbf{{PK}}1)$ $\psi$ provided
$\mathsf{props}(\varphi)\subseteq\mathsf{props}(\psi)$.
---

This is in keeping with the observation that PK is the _left variable
inclusion companion_ of classical logic (in the sense of [11, pp. 49-50], to
which we refer for the relevant definitions and further details); likewise,
the logic BK dealt with in the sequel is the right variable inclusion
companion of classical logic.

Using the preceding characterization, one sees that PK validates, for
instance, the inference $\varphi\land\neg\varphi\vdash\varphi\land\psi$ which
is easily refutable in LP. On the other hand, LP satisfies all rules of the
Belnap-Dunn logic B, while it is easy to see that PK does not satisfy, for
instance, the rule ($\textbf{{K}}1$) shown earlier. Hence, LP and PK are, as
consequence relations, mutually incomparable.

As shown in [11, Example 26], PK can also be axiomatized via a Set-Fmla
H-calculus having no variable restriction on the applicability of rules; this
system, however, involves countably many rule schemata. The situation is thus
similar to the one of BK, and also in this case it is an open question whether
PK can be axiomatized by a finite H-calculus. And just like in that case the
divide between Set-Fmla and Set-Set is visible, after many decades we still do
not know if these logics are finitely axiomatizable in Set-Fmla but a finite
Set-Set analytic axiomatization (in the sense explained in Section 5) can
easily be obtained, see [17].

##### Bochvar-Kleene (BK).

This logic was introduced in 1937 by Bochvar [10], who had in mind potential
applications to the study of paradoxes, future contingent statements and
presuppositions (see e.g. [23] for a more recent computational interpretation
of BK). The third value is intended to represent nonsensical statements (or
corrupted data, in the interpretation given by Kleene for his equivalent
logic), and has an _infectious_ behaviour: any interaction of
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ with the other truth values delivers
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ itself.

It is worth clarifying that Bochvar’s original presentation of BK employs two
different propositional languages, an _external_ and an _internal_ one. We
shall here consider the logic of the internal language (shown in Figure 1),
which is functionally equivalent to Kleene’s system of ‘weak’ connectives
[30]. In Bochvar’s paper, the external connectives belong to a metalanguage
employed to assert or deny propositions which are built using the internal
language. Thus, for instance, according to the truth table of the internal
conjunction $\land_{\textbf{{BK}}}$, the value of a proposition such as
$\varphi\land\psi$ may be $\mathbf{1}$,
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ or $\mathbf{0}$. However, the value of
the metalinguistic affirmation of $\varphi\land\psi$ (this is denoted
$\vdash\varphi\land\psi$ by Bochvar) may only be classical, and it will be
$\mathbf{1}$ precisely when the value of $\varphi\land\psi$ is $\mathbf{1}$,
and $\mathbf{0}$ otherwise. The external conjunction of two propositions
$\varphi$ and $\psi$ is interpreted as the affirmation “$\vdash\varphi$ and
$\vdash\psi$ ”, which follows the usual Boolean truth tables. The semantics of
external disjunction, conjunction and implication is defined in a similar way.

Although we are here exclusively concerned with the internal connectives, the
preceding explanation was necessary to highlight the following fact: while
(finite) Set-Fmla H-calculi for BK presented in the external language (and
even for $n$-valued generalizations of BK: see [24]) are well known, the first
Set-Fmla H-calculus axiomatizing BK in the pure internal language is the one
displayed below, which includes countably many rule schemata. This
axiomatization was introduced in [13], in which BK is studied from an
algebraic perspective as the right variable inclusion companion of classical
logic (see also the chapter by Paoli & Pra Baldi [36] in this volume).

$\gamma\ast(\varphi\to\varphi)$ (BK1)  $\varphi\to\varphi$ |  $\gamma\ast(\varphi\to(\psi\to\varphi))$ (BK2)  $\varphi\to(\psi\to\varphi)$
---|---
$\gamma\ast(\varphi\to(\psi\to\delta)\to(\varphi\to\psi)\to(\varphi\to\delta))$ (BK3)  $\varphi\to(\psi\to\delta)\to(\varphi\to\psi)\to(\varphi\to\delta)$ |
$\gamma\ast((\neg\varphi\to\neg\psi)\to(\psi\to\varphi))$ (BK4)  $(\neg\varphi\to\neg\psi)\to(\psi\to\varphi)$ |  $\varphi\ast\psi,\varphi\to\psi$ (BK5)  $\psi$
$\varphi,\psi$ (BK6)  $\varphi\ast\psi$ |  $\varphi\ast\psi$ (BK7)  $\varphi$
$\varphi,\neg\varphi$ (BK8)  $\psi$ |  $\chi(\delta,\vec{z})$ (BK9)  $\chi(\epsilon,\vec{z})$ , for every $\delta\approx\epsilon\in\Theta$

where $\varphi\ast\psi:=\varphi\land(\varphi\lor\psi)$ and
$\Theta:=\\{\varphi\ast\varphi\approx\varphi,\varphi\ast(\psi\ast\gamma)\approx(\varphi\ast\psi)\ast\gamma,\varphi\ast(\psi\ast\gamma)\approx\varphi\ast(\gamma\ast\psi),\copyright(\varphi_{1},\ldots,\varphi_{k})\ast\psi\approx\copyright(\varphi_{1}\ast\psi,\ldots,\varphi_{k}\ast\psi),\psi\ast\copyright(\varphi_{1},\ldots,\varphi_{k})\approx\copyright(\psi\ast\varphi_{1},\ldots,\psi\ast\varphi_{k})\\}$.

As with PK, it is currently an open problem whether BK can or cannot be
axiomatized by a finite Set-Fmla H-calculus. In fact, BK and PK are both
examples that illustrate the gap that exists between the Set-Fmla and the Set-
Set approach to the axiomatization of logics.

Using the Set-Set formalism, it is easy to produce a finite axiomatization for
BK as a dual of the calculus for PK presented in the preceding section
obtained by reversing all rules and swapping all occurrences of $\land$ and
$\lor$. This result can be established thanks to a construction introduced in
[17], which allows one to update the matrix semantics of a given logic (by
adding infectious values), obtaining a semantics for its left and right
variable inclusion companions so as to preserve finite-valuedness. Under a
certain expressiveness requirement on the resulting matrix, this construction
can then be used (together with the results from [31, 14]) to obtain finite
analytic Set-Set axiomatizations for the variable inclusion companions of the
logic under consideration. In the case of BK, the claimed result then follows
from the fact that BK is the right variable inclusion companion of classical
logic [45, Thm. 4, p. 258].

##### Sobociński (S3)

This logic was introduced in 1952 by B. Sobociński [43] as an (admittedly
oversimplified) example of a logic possessing a “strict implication” analogous
to that of more widely-known (non-finitely valued) modal systems. The
propositional language of S3 consists just of the (Łukasiewicz) negation and
the above-mentioned implication, which does not coincide with any of the
implications of the other logics considered in the present chapter. Given the
mostly theoretical interest in S3, Sobociński does not propose an
interpretation for the truth values; from a formal point of view, however, S3
is closely related to relevance logics, and in particular to the one known as
R-Mingle (see [21]). In fact, as shown in [37], the set of tautologies of S3
coincides with those of the implication-negation fragment of R-Mingle.

The following Set-Fmla Hilbert-style axiomatization of S3 was presented in
[43] and further explored in [37]:

(S31)  $(\varphi\to\psi)\to((\psi\to\gamma)\to(\varphi\to\gamma))$
---
(S32)  $\varphi\to(\varphi\to(\psi\to\psi))$
(S33)  $(\varphi\to(\varphi\to\psi))\to(\varphi\to\psi)$
(S34)  $\varphi\to(\psi\to(\neg{\psi}\to\varphi))$
(S35)  $(\neg\varphi\to\neg\psi)\to(\psi\to\varphi)$
$\varphi\quad\varphi\to\psi$ (S36)  $\psi$

##### Da Costa and D’Ottaviano’s (J3).

This logic was proposed in 1970 by N. da Costa and I.M.L. D’Ottaviano [47] as
a formal solution to a question originally posed by Stanisław Jaśkowski (hence
the name J3), who is one of the earliest pioneers of paraconsistent logic
(together with N. da Costa himself). As in the case of LP, the middle value is
designated: this reflects the observation that J3 is also paraconsistent, in
that both a proposition and its negation may be assigned a designated value.
The authors of [47] give two possible interpretations for propositions that
are evaluated to the middle value: we can either regard them as _true_ (in
which case we have to admit, with G. Priest, that there may be “true
contradictions”) or as _provisionally true_. In the latter case it is assumed
that contradictions may exist within a theory at a certain stage of its
development, but that these will be hopefully eliminated later on. This
reasoning justifies the presence in J3 of a modal-like “possibility”
connective $\Diamond$ and its truth table: the logic is optimistic in that
$\Diamond\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}=\mathbf{1}$, that is to say,
the proposition “it is possible that $A$” is true (has value $\mathbf{1}$)
when $p$ is provisionally true ($\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$).

Taking the conjunction, the negation and $\Diamond$ as primitive, one defines
within J3 the remaining connectives as follows:

  * $\varphi\vee\psi:=\neg(\neg\varphi\wedge\neg\psi)$

  * $\varphi\rightarrow\psi:=\neg\Diamond\varphi\vee\psi$

  * $\varphi\leftrightarrow\psi:=(\varphi\rightarrow\psi)\wedge(\psi\rightarrow\varphi)$

  * $\circ\varphi:=\neg(\Diamond\varphi\wedge\Diamond\neg\varphi)$

As our notation suggests, the above-defined connective $\circ$ used in our
axiomatization is an example of what in paraconsistent logic is known as a
_consistency operator_ : this means that the value of $\circ\varphi$ is
designated (in which case, it must be $\mathbf{1}$) if and only if the value
of $\varphi$ is classical (see e.g. [18]).

It is easy to verify that, formally, all the connectives of J3 either coincide
with those of Ł3 (as in the case of $\land,\lor$ and $\neg$) or are definable
through them, for $\Diamond$ is itself definable in Ł3 by
$\Diamond\varphi:=\neg\varphi\to_{\textbf{{\L${}_{3}$}}}\varphi$. Conversely,
the Łukasiewicz implication (and hence all the connectives of Ł3) is definable
in J3 by:

$\varphi\to_{\textbf{{\L${}_{3}$}}}\psi:=(\Diamond\neg\varphi\lor\psi)\land(\neg\varphi\lor\Diamond\psi).$

This is shown in the MSc thesis of J. Marcos [32, p. 58], who must also be
credited for bringing this fact to our attention.

We may therefore affirm that the matrices defining Ł3 and J3 are equivalent up
to propositional language; however, the different choices of designated
elements determine two distinct logics. To see this, it suffices to observe
that Ł3 (alone) validates $\varphi\vdash\neg\Diamond\neg\varphi$ whereas
$\varphi\lor\neg\varphi$ is a tautology (only) in J3 (see e.g. [26, Example
3.20]).

A Set-Fmla H-calculus axiomatizing J3 was introduced in [22]:

$(\textbf{{J3}}1)$ $\varphi\rightarrow(\psi\rightarrow\varphi)$
---
$(\textbf{{J3}}2)$
$(\varphi\rightarrow(\psi\rightarrow\gamma))\rightarrow((\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\gamma))$
$(\textbf{{J3}}3)$
$((\varphi\rightarrow\psi)\rightarrow\varphi)\rightarrow\varphi$
$(\textbf{{J3}}4)$ $\neg\neg{\varphi}\leftrightarrow\varphi$
$(\textbf{{J3}}5)$ $\circ\varphi\leftrightarrow\circ\neg\varphi$
$(\textbf{{J3}}6)$
$\neg\Diamond\varphi\leftrightarrow(\neg\varphi\wedge\circ\varphi)$
$(\textbf{{J3}}7)$ $\circ(\Diamond\varphi)$
$(\textbf{{J3}}8)$
$((\neg(\varphi\wedge\psi)\wedge\circ(\varphi\wedge\psi))\wedge\psi)\rightarrow(\neg\varphi\wedge\circ\varphi)$
$(\textbf{{J3}}9)$
$(\neg\varphi\wedge\circ\varphi)\rightarrow(\neg(\varphi\wedge\psi)\wedge\circ(\varphi\wedge\psi))$
$(\textbf{{J3}}10)$
$((\varphi\wedge\psi)\wedge\circ(\varphi\wedge\psi))\leftrightarrow((\varphi\wedge\circ\varphi)\wedge(\psi\wedge\circ\psi))$
$\varphi\quad\varphi\rightarrow\psi$ $(\textbf{{J3}}11)$ $\psi$

##### Gödel (G3)

Like Łukasiewicz’s, Gödel logics form an infinite family of $n$-valued
propositional systems which are all extensions of a (unique) infinite-valued
common generalization today known as _Gödel-Dummett logic_. The origin of
these systems can indeed be traced back to K. Gödel [27], who introduced the
corresponding family of finite matrices as a means to prove that
intuitionistic logic is not finite-valued. Gödel-Dummett logic, the infinite-
valued member of the family, was first considered by M. Dummett [20], who
showed that it can be obtained as the axiomatic strengthening of
intuitionistic logic by the _prelinearity_ axiom $(\textbf{{G3}}1)$ shown
below. Each $n$-valued Gödel logic can be axiomatized by further adding to
Gödel-Dummett logic a single characteristic formula, which in the case of the
three-valued logic G3 is the axiom denoted $(\textbf{{G3}}2)$ below (see e.g.
[34, Thm. 6.9 and Lemma 6.10]).

$(\textbf{{G3}}1)$ $(\varphi\rightarrow\psi)\vee(\psi\rightarrow\varphi)$
---
$(\textbf{{G3}}2)$ $\varphi\vee(\varphi\rightarrow(\psi\vee\neg\psi))$

The logics in the Gödel family are mostly regarded (and have been extensively
studied) as _fuzzy logics_ , with intended application to reasoning with vague
predicates (see e.g. [28]). Accordingly, non-classical truth values such as
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ are interpreted as degrees of truth
intermediate between $\mathbf{0}$ (absolute falsity) and $\mathbf{1}$
(absolute truth). As axiomatic extensions of the intuitionistic propositional
calculus, all Gödel logics inherit the standard algebraic semantics of
intuitionistic logic, which is the class of Heyting algebras (aka relatively
pseudo-complemented lattices). G3 is no exception, and its truth tables are
determined by the algebraic counterparts of the propositional connectives: the
conjunction and disjunction (as in the case of Ł3, K etc.) are $\min$ and
$\max$, while the implication and negation correspond, respectively, to the
relative pseudo-complement and the pseudo-complement of Heyting algebras.

##### Post (P3)

The systems introduced by Emil Post in his seminal 1921 paper [38] are among
the earliest many-valued logics in the literature. The intended application
(to problems of representability of functions) is purely mathematical, so the
non-classical values do not come with an intended semantical interpretation.
Post uniformly defines an $n$-valued logic for each natural number $n$, and
establishes that each logic in this family is functionally complete and is
axiomatized by a finite Hilbert-style system. Given our focus on three-valued
logics, we shall here only consider the case where $n=3$. This logic shares
the conjunction and the disjunction with Ł3, but has a _cyclic_ negation that
we denote by $\lnot_{\textbf{{P3}}}$ (Figure 1). We will show in Example 5.26
that this negation and thus the whole logic has a simple finite (and analytic)
Set-Set axiomatization.

##### Logics L7 and L8.

These two systems were constructed _ad hoc_ to provide examples of three-
valued logics not axiomatizable by any finite Set-Fmla Hilbert-style calculus
[35, Lemma 3.3]. We will see, however, that there is a simple Set-Set analytic
axiomatization for L7, obtainable directly from the recipe we present in
Section 5. The logic L8, which lacks the expressiveness requirement for the
application of our recipe, is nevertheless finitely axiomatizable in Set-Set
by [42, Theorem 19.12].

##  4 The formalism of 3-labelled calculi

We begin by discussing what kinds of objects are manipulated by rules of
inference in 3-labelled calculi. A _3-labelled formula_ is an expression of
the form ‘$\nu\colon\varphi$’, where
$\nu\in\\{\mathbf{0},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\mathbf{1}\\}$ is a
_label_ and $\varphi$ is a formula. The _3-labelled calculi_ [7, 6] constitute
a family of proof systems whose rules of inference manipulate finite sets of
labelled formulas, usually referred to as _3-sequents_. Henceforth, we will
use the letters $X,Y$ and $Z$ to denote 3-sequents and write $X,Y$ to mean
$X\cup Y$. We may eliminate the truth values from the notation of a 3-sequent
$X$ by writing it as a triple of sets of formulas as follows:

$\Phi_{\mathbf{0}}\mid\Phi_{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}\mid\Phi_{\mathbf{1}},$

where each formula in $\Phi_{\nu}$ is labelled with $\nu$ in
$\\{\mathbf{0},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\mathbf{1}\\}$. We may
write $\Phi,\Psi$ and $\Gamma$ instead of $\Phi_{\mathbf{0}}$,
$\Phi_{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}$ and $\Phi_{\mathbf{1}}$,
respectively, in case there is no risk of confusion when writing rules and
derivations. The 3-labelled calculi of interest in this work are those
containing the structural rules of _identity_ , _weakening_ and _cut_ , which
do not depend on the connectives present in the language, as well as _logical
rules_ , which vary according to the language and describe the behaviour of
the connectives. We describe these rules in more detail below.

##### Identity

The only nullary (or _axiomatic_) rule:

Idφ $\varphi\mid\varphi\mid\varphi$

##### Weakening

We may derive from any 3-sequent another one by adding an arbitrary formula in
one of the three positions:

$\Phi\mid\Psi\mid\Gamma$ $W_{\mathbf{0}}$ $\Phi,\varphi\mid\Psi\mid\Gamma$ |  $\Phi\mid\Psi\mid\Gamma$ $W_{\mathbf{1}}$ $\Phi\mid\Psi\mid\Gamma,\varphi$
---|---

##### Cut

We may cut a formula whenever it appears in different positions in two given
3-sequents:

$\Phi,\varphi\mid\Psi\mid\Gamma$ $\Phi\mid\Psi,\varphi\mid\Gamma$
Cut${}_{\mathbf{0},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}$
$\Phi\mid\Psi\mid\Gamma$
---
$\Phi,\varphi\mid\Psi\mid\Gamma$ $\Phi\mid\Psi\mid\Gamma,\varphi$ Cut0,1
$\Phi\mid\Psi\mid\Gamma$
$\Phi\mid\Psi,\varphi\mid\Gamma$ $\Phi\mid\Psi\mid\Gamma,\varphi$
Cut${}_{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\mathbf{1}}$
$\Phi\mid\Psi\mid\Gamma$

##### Logical rules

Let $X_{1},\ldots,X_{m}$ be sets of 3-labelled formulas such that, for each
$\nu^{\prime}:\psi\in X_{i}$, we have
$\psi\in\\{\varphi_{1},\ldots,\varphi_{k}\\}\subseteq L_{\Sigma}(P)$. Also,
let $\copyright$ be a $k$-ary connective and $\nu\in V_{3}$. Then the
following is a logical rule:

$(\Phi\mid\Psi\mid\Gamma)[X_{1}]\quad\cdots\quad(\Phi\mid\Psi\mid\Gamma)[X_{m}]$
$(\Phi\mid\Psi\mid\Gamma)[\\{\nu:\copyright(\varphi_{1},\ldots,\varphi_{k})\\}]$

where the expression $(\Phi\mid\Psi\mid\Gamma)[Y]$ refers to the 3-sequent
resulting from adding the 3-labelled formulas in $Y$ to
$\Phi\mid\Psi\mid\Gamma$. The 3-labelled formula
$\nu:\copyright(\varphi_{1},\ldots,\varphi_{k})$ is called _the principal
formula_ of the rule, each $\varphi_{i}$, where $1\leq i\leq k$, is an
_auxiliary formula_ , the sets $\Phi,\Psi$ and $\Gamma$ are the _contexts_ of
the rule, and their formulas are called _side formulas_.

A _proof_ of a 3-labelled sequent $\Phi\mid\Psi\mid\Gamma$ in a 3-labelled
calculus is, as one could expect from the usual practice in sequent-style
calculi, a finite tree of 3-sequents rooted in $\Phi\mid\Psi\mid\Gamma$ built
using the rules of inference of the calculus, whose leaves result from an
application of an instance of a rule with an empty set of premises. See
Example 4.8 for a proof of a 3-sequent using a 3-labelled calculus for the
logic Ł3. A 3-labelled calculus, differently from what happens with Hilbert-
style systems, induce more than one logic, depending on the logical matrix we
intend to capture. Usually the algebra is fixed, and the different induced
logics vary with the choice of designated elements:

######  Definition 4.1.

Given a 3-labelled system $\mathsf{G}$ and a nonempty set $D\subseteq V_{3}$,
we associate a consequence relation $\rhd_{\mathsf{G}}^{D}$ to $\mathsf{G}$
and $D$ such that

$\displaystyle\Phi\rhd_{\mathsf{G}}^{D}\Psi\text{ if, and only if, }$
$\displaystyle\bigcup_{\nu\in
V_{3}{\setminus}D}\\{\nu:\varphi\mid\varphi\in\Phi\\}\,\cup\,\bigcup_{\nu\in
D}\\{\nu:\psi\mid\psi\in\Psi\\}\text{ is provable in $\mathsf{G}$}.$

In the three-valued case, we will usually deal with $D=\\{\mathbf{1}\\}$ and
$D=\\{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\mathbf{1}\\}$, for which cases
the above expression specializes to:

  * •

$\Phi\rhd_{\mathsf{G}}^{\\{\mathbf{1}\\}}\Psi\;\text{ if, and only if,
}\;\Phi\mid\Phi\mid\Psi\text{ is provable in $\mathsf{G}$}$, and

  * •

$\Phi\rhd_{\mathsf{G}}^{\\{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\mathbf{1}\\}}\Psi\;\text{
if, and only if, }\;\Phi\mid\Psi\mid\Psi\text{ is provable in $\mathsf{G}$}$.

Let $\mathbb{M}=\langle\mathbf{A},D\rangle$ be a three-valued logical matrix.
We say that a 3-labelled calculus $\mathsf{G}$ _axiomatizes_ $\mathbb{M}$ in
case $\rhd_{\mathbb{M}}\;=\;\rhd_{\mathsf{G}}^{D}$. An $\mathbb{M}$-valuation
$v$ _satisfies_ a 3-sequent $X$ in case $v(\varphi)=\nu$ for some 3-labelled
formula $\nu:\varphi\in X$. A 3-labelled rule _holds_ in $\mathbb{M}$ if for
no $\mathbb{M}$-valuation $v$ it is the case that the 3-sequent premises are
satisfied by $v$ while the conclusion 3-sequent is not satisfied by $v$. The
next lemma shows that we may use 3-labelled logical rules to give a proof-
theoretical characterization of each entry of the interpretations (truth
tables) of the connectives in $\mathbb{M}$.

######  Lemma 4.2.

A 3-labelled logical rule of the form

$(\Phi\mid\Psi\mid\Gamma)[\\{\nu_{1}:\varphi_{1}\\}]\quad\cdots\quad(\Phi\mid\Psi\mid\Gamma)[\\{\nu_{k}:\varphi_{k}\\}]$
$\copyright:\nu_{1},\ldots,\nu_{k},\nu$
$(\Phi\mid\Psi\mid\Gamma)[\\{\nu:\copyright(\varphi_{1},\ldots,\varphi_{k})\\}]$

holds in $\mathbb{M}:=\langle\mathbf{A},D\rangle$ if, and only if,
${\copyright}_{\mathbf{A}}(\nu_{1},\ldots,\nu_{k})=\nu$.

It is natural, then, to expect that, by inspecting the entries of the truth
tables of $\mathbb{M}$ and generating the corresponding rules according to the
previous result, we should get a 3-labelled axiomatization for $\mathbb{M}$.
The next result matches precisely this expectation, and gives more: the
resulting calculus is _cut-free_ and _analytic_ , that is, respectively, every
provable consecution has a proof where cuts are not employed and only
subformulas of the proved statement occur in the proof.

######  Theorem 4.3 ([7, 6]).

Let $\mathbb{M}=\langle\mathbf{A},D\rangle$ be a three-valued matrix whose
determined logic we denote by $\mathbf{L}$. Then the 3-labelled calculus
$\ell.{\mathbf{L}}$ whose logical rules are given by

$(\Phi\mid\Psi\mid\Gamma)[\,\nu_{1}:\varphi_{1}\,]\quad\cdots\quad(\Phi\mid\Psi\mid\Gamma)[\,\nu_{k}:\varphi_{k}\,]$
$\copyright:\nu_{1},\ldots,\nu_{k}$
$(\Phi\mid\Psi\mid\Gamma)[\copyright_{\mathbf{A}}(\nu_{1},\ldots,\nu_{k}):\copyright(\varphi_{1},\ldots,\varphi_{k})\,]$
,

for all $\nu_{1},\ldots,\nu_{k}\in V_{3}$, $\copyright\in\Sigma_{k}$ and
$k\in\omega$, axiomatizes $\mathbb{M}$, being, in addition, cut-free and
analytic.

In the following, in order to emphasize that the rules above are in a one-to-
one correspondence with matrix entries, we will write the rule names as
$\copyright^{\nu_{1}\nu_{2}}_{\nu}$ to identify the matrix entries for binary
connectives $\copyright$ (also for unary connectives, in which case there will
be no $\nu_{2}$), where the indices $\nu_{1}\nu_{2}$ refers to the list of
input values of the corresponding matrix entry (that govern the position of
the auxiliary formulas in the premise of a rule), and $\nu$ refers to the
corresponding output value in the matrix (which governs the position of the
principal formula in the conclusion of the rule). Moreover, we color the
output value in rules’ names to emphasize all rules sharing the same output
per each connective.

######  Example 4.4.

We illustrate below the case of $\ell.{\textbf{{\L${}_{3}$}}}$, beginning with
$\neg$. From the facts that
$\neg_{\textbf{{\L${}_{3}$}}}(\mathbf{1})=\mathbf{0}$,
$\neg_{\textbf{{\L${}_{3}$}}}(\nicefrac{{\mathbf{1}}}{{\mathbf{2}}})=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$
and $\neg_{\textbf{{\L${}_{3}$}}}(\mathbf{0})=\mathbf{1}$, we obtain,
respectively, the following 3-labelled rules:

$\Phi,\varphi\mid\Psi\mid\Gamma$ $\neg^{\mathbf{0}}_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}}$ $\Phi\mid\Psi\mid\Gamma,\neg\varphi$ |  $\Phi\mid\Psi\mid\Gamma,\varphi$ $\neg^{\mathbf{1}}_{\mathbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}}}$ $\Phi,\neg\varphi\mid\Psi\mid\Gamma$
---|---

For $\land$, we obtain:

$\Phi,\varphi\mid\Psi\mid\Gamma$ $\Phi,\psi\mid\Psi\mid\Gamma$ $\wedge^{\mathbf{0}\mathbf{0}}_{\mathbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}}}$ $\Phi,\varphi\wedge\psi\mid\Psi\mid\Gamma$ |  $\Phi,\varphi\mid\Psi\mid\Gamma$ $\Phi\mid\Psi,\psi\mid\Gamma$ $\wedge^{\mathbf{0}\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}_{\mathbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}}}$ $\Phi,\varphi\wedge\psi\mid\Psi\mid\Gamma$
---|---
$\Phi,\varphi\mid\Psi\mid\Gamma$ $\Phi\mid\Psi\mid\Gamma,\psi$ $\wedge^{\mathbf{0}\mathbf{1}}_{\mathbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}}}$ $\Phi,\varphi\wedge\psi\mid\Psi\mid\Gamma$ |  $\Phi\mid\Psi\mid\Gamma,\varphi$ $\Phi,\psi\mid\Psi\mid\Gamma$ $\wedge^{\mathbf{1}\mathbf{0}}_{\mathbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}}}$ $\Phi,\varphi\wedge\psi\mid\Psi\mid\Gamma$
$\Phi\mid\Psi\mid\Gamma,\varphi$ $\Phi\mid\Psi,\psi\mid\Gamma$ $\wedge^{\mathbf{1}\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}_{\mathbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\nicefrac{{1}}{{2}}}}}$ $\Phi\mid\Psi,\varphi\wedge\psi\mid\Gamma$ |  $\Phi\mid\Psi\mid\Gamma,\varphi$ $\Phi\mid\Psi\mid\Gamma,\psi$ $\wedge^{\mathbf{1}\mathbf{1}}_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}}$ $\Phi\mid\Psi\mid\Gamma,\varphi\wedge\psi$
$\Phi\mid\Psi,\varphi\mid\Gamma$ $\Phi,\psi\mid\Psi\mid\Gamma$ $\wedge^{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\mathbf{0}}_{\mathbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}}}$ $\Phi,\varphi\wedge\psi\mid\Psi\mid\Gamma$ |  $\Phi\mid\Psi,\varphi\mid\Gamma$ $\Phi\mid\Psi,\psi\mid\Gamma$ $\wedge^{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}_{\mathbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\nicefrac{{1}}{{2}}}}}$ $\Phi\mid\Psi,\varphi\wedge\psi\mid\Gamma$
$\Phi\mid\Psi,\varphi\mid\Gamma$ $\Phi\mid\Psi\mid\Gamma,\psi$ $\wedge^{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\mathbf{1}}_{\mathbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\nicefrac{{1}}{{2}}}}}$ $\Phi\mid\Psi,\varphi\wedge\psi\mid\Gamma$ |

We leave to the reader the completion of this calculus for Ł3 in terms of the
rules for $\lor$ and $\to$.

The previous result is clearly a recipe to axiomatize three-valued matrices
via 3-labelled calculi. We call it the _(3-labelled) generating subprocedure_.
Notice that each logical rule introduces the 3-labelled formula
$\nu:\copyright(\varphi_{1},\ldots,\varphi_{n})$ in the conclusion, and the
auxiliary formulas are immediate subformulas of the principal formula
occurring exactly once, each of which in a different premise. Nonetheless,
providing an actual derivation is quite cumbersome. In the case of three-
valued logics, we will have $9$ logical introduction rules for each
connective, one for each entry of the concerned three-valued logical matrix.

A second calculus may be obtained from the previous one via what we we call
here a _streamlining sub-procedure_ — the result is called _streamlined
3-labelled calculi_. In this case, we are able to get, for instance, a
streamlined system with exactly three logical rules per each $k$-ary
connective $\copyright$, one for each $\nu\in V_{3}$, whose effect in a
derivation is the introduction of the 3-labelled formula
$\nu:\copyright(\varphi_{1},\ldots,\varphi_{k})$. A streamlined calculus
satisfying this property will be denoted here by $s\ell.{\mathbf{L}}$, where
$\mathbf{L}$ is the concerned three-valued logic. Again, the auxiliary
formulas in the premise of logical rules are immediate subformulas of the
principal formula, the number of premises is finite but not fixed, but, now,
the very same auxiliary formula could occur more than once and in different
sequent components. We provide below, for self-containment, the steps to
produce a streamlined calculus and point to the references where the
correctness of the simplification steps is proved.

######  Definition 4.5.

The _streamlined version_ of a 3-labelled calculus is obtained applying the
following streamlining subprocedure (see [6] in the present book):

(P1)

If a rule $r$ is derivable from other rules without using cuts, then $r$ can
be deleted.

(P2)

If $r:=\frac{X}{Y}$ is a rule with $X$ a finite set of premises,
$r^{\prime}:=\frac{X^{\prime}}{Y}$ is sound, and $X^{\prime}\subset X$, then
$r$ can be replaced by $r^{\prime}$.

(P3)

Rules $r:=\frac{X_{1}\,\cdots\,X_{m}}{Y}$ and
$r^{\prime}:=\frac{X^{\prime}_{1}\cdots X^{\prime}_{n}}{Y}$ can be replaced by
$r^{\prime\prime}:=\frac{\\{X_{i}\cup X^{\prime}_{j}\\}}{T}$ with $1\leq i\leq
m$ and $1\leq j\leq n$, and vice-versa.

Here we just recall the following key result for the correctness of the steps
above refer the reader to [6] in this book for the proof:

######  Proposition 4.6.

If $\mathsf{G}^{\prime}$ and $\mathsf{G}$ are 3-labelled calculi and
$\mathsf{G}^{\prime}$ is obtained from $\mathsf{G}$ applying the streamlining
procedure in Definition 4.5, then:

  * •

$\mathsf{G}^{\prime}$ and $\mathsf{G}$ are equivalent (one derives the rules
of the other);

  * •

if $\mathsf{G}$ is sound and complete for a matrix $\mathbb{M}$, then so is
$\mathsf{G}^{\prime}$; and

  * •

if $\mathsf{G}$ admits cut-elimination, then so does $\mathsf{G}^{\prime}$.

######  Example 4.7.

The rules for $\land$ presented in Example 4.4 can be simplified using the
steps above, resulting in the following rules:

$\Phi,\varphi,\psi\mid\Psi\mid\Gamma$
$\wedge_{\mathbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}}}$
$\Phi,\varphi\wedge\psi\mid\Psi\mid\Gamma$
---
$\Phi\mid\Psi,\varphi\mid\Gamma,\varphi\ \ \
\Phi\mid\Psi,\varphi,\psi\mid\Gamma\ \ \ \Phi\mid\Psi,\psi\mid\Gamma,\psi$
$\wedge_{\mathbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\nicefrac{{1}}{{2}}}}}$
$\Phi\mid\Psi,\varphi\wedge\psi\mid\Gamma$
$\Phi\mid\Psi\mid\Gamma,\varphi$ $\Phi\mid\Psi\mid\Gamma,\psi$
$\wedge_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}}$
$\Phi\mid\Psi\mid\Gamma,\varphi\wedge\psi$

Similarly, we may obtain one rule for each truth value introducing each of the
connectives $\lor$ and $\to$, resulting in the following rules:

$\Phi,\varphi\mid\Psi\mid\Gamma$ $\Phi,\psi\mid\Psi\mid\Gamma$
$\vee_{\mathbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}}}$
$\Phi,\varphi\vee\psi\mid\Psi\mid\Gamma$
---
$\Phi,\varphi\mid\Psi,\varphi\mid\Gamma\ \ \
\Phi\mid\Psi,\varphi,\psi\mid\Gamma\ \ \ \Phi,\psi\mid\Psi,\psi\mid\Gamma$
$\vee_{\mathbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\nicefrac{{1}}{{2}}}}}$
$\Phi\mid\Psi,\varphi\vee\psi\mid\Gamma$
$\Phi\mid\Psi\mid\Gamma,\varphi,\psi$
$\vee_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}}$
$\Phi\mid\Psi\mid\Gamma,\varphi\vee\psi$
$\Phi\mid\Psi\mid\Gamma,\varphi$ $\Phi,\psi\mid\Psi\mid\Gamma$
$\rightarrow_{\mathbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}}}$
$\Phi,\varphi\rightarrow\psi\mid\Psi\mid\Gamma$
$\Phi,\psi\mid\Psi\mid\Gamma,\varphi$ $\Phi\mid\Psi,\varphi,\psi\mid\Gamma$
$\rightarrow_{\mathbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\nicefrac{{1}}{{2}}}}}$
$\Phi\mid\Psi,\varphi\rightarrow\psi\mid\Gamma$
$\Phi,\varphi\mid\Psi,\varphi\mid\Gamma,\psi$
$\Phi,\varphi\mid\Psi,\psi\mid\Gamma,\psi$
$\rightarrow_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}}$
$\Phi\mid\Psi\mid\Gamma,\varphi\rightarrow\psi$

Taking these rules together with the rules for $\neg$ in Example 4.4 gives us
a 3-labelled calculus for Ł3 that we call $s\ell.{\textbf{{\L${}_{3}$}}}$.

######  Example 4.8.

Let us prove that $\varphi\to(\psi\to\varphi)$ is a tautology (that is,
receives a designated value under every valuation) of Ł3. Since
$s\ell.{\textbf{{\L${}_{3}$}}}$ is complete for this logic, we just need to
derive the 3-sequent
$\varnothing\mid\varnothing\mid\varphi\to(\psi\to\varphi)$ in
$s\ell.{\textbf{{\L${}_{3}$}}}$ (recall Definition 4.1 and the fact that the
set of designated values of the logical matrix for Ł3 is $\\{\mathbf{1}\\}$).
Notice that we use $W^{\ast}$ to mean a sequence of applications of weakening
rules.

Idφ $\varphi\mid\varphi\mid\varphi$ $W^{\ast}$
$\varphi,\psi\mid\varphi,\psi\mid\varphi$ Idφ $\varphi\mid\varphi\mid\varphi$
$W$ $\varphi,\psi\mid\varphi\mid\varphi$
$\rightarrow_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}}$
$\varphi\mid\varphi\mid\psi\to\varphi$ $\mathcal{D}_{1}$ $\mathcal{D}_{2}$
$\rightarrow_{\mathbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\nicefrac{{1}}{{2}}}}}$
$\varphi\mid\psi\to\varphi\mid\psi\to\varphi$
$\rightarrow_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}}$
$\varnothing\mid\varnothing\mid\varphi\to(\psi\to\varphi)$

where $\mathcal{D}_{1}$ and $\mathcal{D}_{2}$ are the following subtrees:

Idφ $\varphi\mid\varphi\mid\varphi$ $W^{\ast}$ $\varphi,\psi\mid\psi,\varphi\mid\varphi$ Idφ $\varphi\mid\varphi\mid\varphi$ $W^{\ast}$ $\varphi,\psi\mid\psi,\varphi\mid\varphi$ $\rightarrow_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}}$ $\varphi\mid\psi,\varphi\mid\psi\to\varphi$ |  Idψ $\psi\mid\psi\mid\psi$ $W^{\ast}$ $\varphi,\psi\mid\psi\mid\varphi,\psi$ Idφ $\varphi\mid\varphi\mid\varphi$ $W^{\ast}$ $\varphi,\psi\mid\varphi\mid\psi,\varphi$ $\rightarrow_{\mathbf{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}}}$ $\varphi\mid\varnothing\mid\psi,\psi\to\varphi$
---|---

We should emphasize that different streamlined calculi may be obtained
depending on how and to which extent the simplification steps outlined above
are applied. The algorithm presented in Theorem 4.3 was implemented in the
system MultiLog [8], which can be used by anyone for producing a streamlined
3-labelled calculus $s\ell.{\mathbf{L}}$ — that is, one with one rule per each
truth value and each connective ($3c$ rules, for $c$ connectives) — given a
three-valued logical matrix for $\mathbf{L}$ as input.

##  5 Multiple-conclusion Hilbert-style calculi

In this section, we are interested in providing finite and analytic multiple-
conclusion (or Set-Set) Hilbert-style axiomatizations for three-valued logical
matrices. As we shall detail in a moment, this proof formalism generalizes
traditional Hilbert-style calculi in allowing sets of formulas in the
conclusion of the rules of inference. Putting aside the trivial cases, we will
focus on two tasks: first, on specifying a general method for axiomatizing any
three-valued matrix that satisfies a criterion of sufficient expressiveness
called _monadicity_ ; and, second, on axiomatizing some specific three-valued
matrices that do not meet such criterion. The result proved in [42, Theorem
19.12] guarantees that every finite logical matrix (in particular, three-
valued matrices) has an adequate (sound and complete) finite Set-Set
axiomatization, but finding one for the non-monadic matrices can be a rather
involved task, as we will see. In [31], the recipe for the monadic case was
generalized to deal with non-determinism and the resulting finite calculi were
shown to satisfy a generalized subformula property, yielding what we call
_$\Theta$ -analiticity_, a fact that had remained unnoticed for many decades.

We begin by giving the formal definitions related to the proof formalism of
Set-Set calculi together with some examples.

######  Definition 5.1.

A _Set-Set inference rule_ $\mathsf{r}$ is a pair
$(\Phi,\Psi)\in\mathcal{P}(L_{\Sigma}(P))\times\mathcal{P}(L_{\Sigma}(P))$
that we denote by $\frac{\Phi}{\Psi}$, where $\Phi$ is the _antecedent_ and
$\Psi$ is _succedent_ of $\mathsf{r}$. If $\sigma$ is a substitution, then
$\mathsf{r}^{\sigma}:=\frac{\sigma(\Phi)}{\sigma(\Psi)}$ is said to be an
_instance_ of $\mathsf{r}$. A _subrule_ of $\mathsf{r}$ is a rule
$\frac{\Phi^{\prime}}{\Psi^{\prime}}$ with $\Phi^{\prime}\subseteq\Phi$ and
$\Psi^{\prime}\subseteq\Psi$. An inference rule is _finitary_ when its
antecedent and succedent are finite. A _Set-Set calculus_ $\mathsf{R}$ is a
collection of Set-Set inference rules.

######  Example 5.2.

Consider the calculus $\mathsf{R}^{\to\neg}_{\textbf{{S3}}}$ consisting of the
following rules of inference:

$\displaystyle\frac{p}{\neg\neg
p}\mathsf{r}^{\lnot_{\textbf{{S3}}}}_{1}\quad\frac{\neg\neg
p}{p}\mathsf{r}^{\lnot_{\textbf{{S3}}}}_{2}\quad\frac{}{p,\neg
p}\mathsf{r}^{\lnot_{\textbf{{S3}}}}_{3}$ $\displaystyle\frac{\neg p,q}{p\to
q}\mathsf{r}^{\to_{\textbf{{S3}}}}_{1}\quad\frac{p,\neg q}{\neg(p\to
q)}\mathsf{r}^{\to_{\textbf{{S3}}}}_{2}\quad\frac{p\to q,\neg q}{\neg
p}\mathsf{r}^{\to_{\textbf{{S3}}}}_{3}$ $\displaystyle\frac{\neg(p\to
q)}{p}\mathsf{r}^{\to_{\textbf{{S3}}}}_{4}\quad\frac{\neg(p\to q)}{\neg
q}\mathsf{r}^{\to_{\textbf{{S3}}}}_{5}\quad\frac{p,p\to
q}{q}\mathsf{r}^{\to_{\textbf{{S3}}}}_{6}$

Notice that what distinguishes $\mathsf{R}^{\to\neg}_{\textbf{{S3}}}$ from a
standard Hilbert-style calculus is the last rule, whose succedent is a two-
formula set. This calculus, according to the recipe we are about to present,
is an axiomatization (see Definition 5.11) of the $\\{\to,\neg\\}$-fragment of
the logic S3.

As mentioned in Section 3, the logics BK and PK are not known to be finitely
axiomatizable by means of a Set-Fmla H-calculus. The next couple of examples
show that this matter is much simpler in the Set-Set formalism, as these
logics fall in the scope of the axiomatization recipe we will provide in a
moment.

######  Example 5.3.

Consider the Set-Set calculus $\mathsf{R}_{\textbf{{BK}}}$ consisting of the
following rules of inference:

$\displaystyle\frac{p}{\neg\neg
p}\mathsf{r}^{\lnot_{\textbf{{BK}}}}_{1}\quad\;\frac{\neg\neg
p}{p}\mathsf{r}^{\lnot_{\textbf{{BK}}}}_{2}\quad\;\frac{p,\neg
p}{}\mathsf{r}^{\lnot_{\textbf{{BK}}}}_{3}$ $\displaystyle\frac{p,q}{p\land
q}\mathsf{r}^{\land_{\textbf{{BK}}}}_{1}\quad\frac{p\land
q}{p}\mathsf{r}^{\land_{\textbf{{BK}}}}_{2}\quad\frac{p\land
q}{q}\mathsf{r}^{\land_{\textbf{{BK}}}}_{3}\quad\frac{\neg p,\neg
q}{\neg(p\land q)}\mathsf{r}^{\land_{\textbf{{BK}}}}_{4}$
$\displaystyle\frac{\neg(p\land q)}{p,\neg
p}\mathsf{r}^{\land_{\textbf{{BK}}}}_{5}\quad\frac{\neg(p\land q)}{q,\neg
q}\mathsf{r}^{\land_{\textbf{{BK}}}}_{6}\quad\frac{p,\neg q}{\neg(p\land
q)}\mathsf{r}^{\land_{\textbf{{BK}}}}_{7}\quad\frac{\neg p,q}{\neg(p\land
q)}\mathsf{r}^{\land_{\textbf{{BK}}}}_{8}$ $\displaystyle\frac{\neg p,\neg
q}{p\to q}\mathsf{r}^{\to_{\textbf{{BK}}}}_{1}\quad\frac{\neg p,q}{p\to
q}\mathsf{r}^{\to_{\textbf{{BK}}}}_{2}\quad\frac{p,q}{p\to
q}\mathsf{r}^{\to_{\textbf{{BK}}}}_{3}\quad\frac{p,\neg q}{\neg(p\to
q)}\mathsf{r}^{\to_{\textbf{{BK}}}}_{4}$ $\displaystyle\frac{p\to q}{\neg
p,p}\mathsf{r}^{\to_{\textbf{{BK}}}}_{5}\quad\frac{\neg(p\to q)}{\neg
q}\mathsf{r}^{\to_{\textbf{{BK}}}}_{6}\quad\frac{p\to q}{\neg
q,q}\mathsf{r}^{\to_{\textbf{{BK}}}}_{7}\quad\frac{\neg(p\to
q)}{p}\mathsf{r}^{\to_{\textbf{{BK}}}}_{8}\quad\frac{p\to
q,p}{q}\mathsf{r}^{\to_{\textbf{{BK}}}}_{9}$ $\displaystyle\frac{\neg p,\neg
q}{\neg(p\lor q)}\mathsf{r}^{\lor_{\textbf{{BK}}}}_{1}\quad\frac{\neg(p\lor
q)}{\neg p}\mathsf{r}^{\lor_{\textbf{{BK}}}}_{2}\quad\frac{p\lor q}{\neg
p,p}\mathsf{r}^{\lor_{\textbf{{BK}}}}_{3}\quad\frac{\neg(p\lor q)}{\neg
q}\mathsf{r}^{\lor_{\textbf{{BK}}}}_{4}$ $\displaystyle\frac{p\lor q}{\neg
q,q}\mathsf{r}^{\lor_{\textbf{{BK}}}}_{5}\quad\frac{\neg p,q}{p\lor
q}\mathsf{r}^{\lor_{\textbf{{BK}}}}_{6}\quad\frac{p,\neg q}{p\lor
q}\mathsf{r}^{\lor_{\textbf{{BK}}}}_{7}\quad\frac{p,q}{p\lor
q}\mathsf{r}^{\lor_{\textbf{{BK}}}}_{8}\quad\frac{p\lor
q}{p,q}\mathsf{r}^{\lor_{\textbf{{BK}}}}_{9}$

This calculus axiomatizes the logic BK, according to the procedure we describe
in Subsection 5.1. In rule $\mathsf{r}^{\lnot_{\textbf{{BK}}}}_{3}$, we
observe that Set-Set rules may have an empty succedent. As we will see in the
next definition, the effect of an application of a rule with this property is
the discontinuation of a derivation branch. We should emphasize that the empty
succedent in a rule is not replaceable by the version of the same rule having
a single fresh propositional variable in the succedent (for instance, using
the rule $\frac{\neg p,p}{q}$ instead of $\frac{\neg p,p}{}$ in the present
example). Such modification would prevent the derivation of valid statements
with empty succedents, leading thus to a different Set-Set logic.

######  Example 5.4.

Call $\mathsf{R}_{\textbf{{PK}}}$ the Set-Set calculus given by:

  * •

all rules $\mathsf{r}^{\lnot_{\textbf{{BK}}}}_{i}$ from the previous example
turned upside down;

  * •

all rules $\mathsf{r}^{\land_{\textbf{{BK}}}}_{i}$ and
$\mathsf{r}^{\lor_{\textbf{{BK}}}}_{j}$ from the previous example turned
upside down, with $\lor$ in place of $\land$ (and vice-versa); and

  * •

the following rules governing $\to$:

$\displaystyle\frac{\neg p}{p\to
q}\mathsf{r}^{\to_{\textbf{{PK}}}}_{1}\quad\frac{q}{p\to
q}\mathsf{r}^{\to_{\textbf{{PK}}}}_{2}\quad\frac{}{p,p\to
q}\mathsf{r}^{\to_{\textbf{{PK}}}}_{3}\quad\frac{p,\neg p}{\neg(p\to
q)}\mathsf{r}^{\to_{\textbf{{PK}}}}_{4}$ $\displaystyle\frac{q,\neg
q}{\neg(p\to q)}\mathsf{r}^{\to_{\textbf{{PK}}}}_{5}\quad\frac{p}{\neg(p\to
q),q}\mathsf{r}^{\to_{\textbf{{PK}}}}_{6}\quad\frac{\neg(p\to q)}{\neg p,\neg
q}\mathsf{r}^{\to_{\textbf{{PK}}}}_{7}\quad\frac{p\to q}{\neg
p,q}\mathsf{r}^{\to_{\textbf{{PK}}}}_{8}$ $\displaystyle\frac{\neg(p\to
q)}{p,\neg q}\mathsf{r}^{\to_{\textbf{{PK}}}}_{9}\quad\frac{\neg(p\to
q)}{p,q}\mathsf{r}^{\to_{\textbf{{PK}}}}_{10}$

By the recipe in Subsection 5.1, this is a Set-Set axiomatization for PK.

We now show how the notions of Hilbert-style derivation and proof are
generalized in order to deal with the novelty of allowing for sets of formulas
in the succedent of a rule of inference.

######  Definition 5.5.

An _$\mathsf{R}$ -derivation_ is a rooted directed tree $\mathsf{t}$ such that
every node is labelled with sets of formulas or with a discontinuation symbol
$\star$, and in which every non-leaf node (that is, a node with child nodes)
$\mathsf{n}$ in $\mathsf{t}$ is an _expansion of $\mathsf{n}$ by a rule
instance_ $\mathsf{r}^{\sigma}$ of $\mathsf{R}$. This means that the
antecedent of $\mathsf{r}^{\sigma}$ is contained in the label of $n$ and that
$n$ has exactly one child node for each formula $\psi$ in the succedent of
$\mathsf{r}^{\sigma}$, which is, in turn, labelled with the same formulas as
those of $\mathsf{n}$ plus $\psi$. In case $\mathsf{r}^{\sigma}$ has an empty
succedent, then $\mathsf{n}$ has a single child node labelled with $\star$.
Figure 2 illustrates how derivations using only finitary inference rules are
graphically represented. We denote by $\mathsf{lab}^{\mathsf{t}}(\mathsf{n})$
the label of the node $\mathsf{n}$ in the tree $\mathsf{t}$.

$\Phi$

$\Phi$$\frac{\sigma(\Gamma)}{\varnothing}$$\star$

$\Phi$$\frac{\sigma(\Gamma)}{\sigma(\psi_{1}),\sigma(\psi_{2}),\ldots,\sigma(\psi_{n})}$$\sigma(\psi_{1})$$\cdots$$\sigma(\psi_{2})$$\cdots$$\ldots$$\sigma(\psi_{n})$$\cdots$

Figure 2: Graphical representation of $\mathsf{R}$–derivations using finitary
inference rules, in the form of a leaf node, a discontinued node and an
expanded node, respectively.

In Figure 2, the dashed edges and blank circles represent other nodes and
edges that may exist in the derivation. Notice that, in the case of expanded
nodes, we omit the formulas inherited from the parent node, exhibiting only
the ones introduced by the applied rule of inference. Also, we have written
the rule instance of the rule being applied in the second and third trees, but
in practice only the name of the rule of inference will be written for
simplicity. In these cases, we emphasize that a precondition for the
application of the rule instance is that $\sigma(\Gamma)\subseteq\Phi$ (that
is, the premises of the rule being applied are satisfied).

######  Definition 5.6.

Given $\Delta\subseteq L_{\Sigma}(P)$, a node $\mathsf{n}$ of an
$\mathsf{R}$-derivation $\mathsf{t}$ is said to be _$\Delta$ -closed_ when
$\mathsf{lab}^{\mathsf{t}}(\mathsf{n})\cap\Delta\neq\varnothing$ or when
$\mathsf{n}$ is labelled with $\star$. If all leaf nodes of $\mathsf{t}$ are
$\Delta$-closed, then $\mathsf{t}$ is said to be $\Delta$-closed.

######  Definition 5.7.

An _$\mathsf{R}$ -proof_ of a statement $(\Phi,\Psi)$ is a $\Psi$-closed
$\mathsf{R}$-derivation whose root is labelled with a subset of $\Phi$.

The notion of Set-Set calculus succeeds in capturing the notion of Set-Set
logics, as the following result states:

######  Proposition 5.8.

A Set-Set calculus $\mathsf{R}$ induces a Set-Set logic $\rhd_{\mathsf{R}}$
such that $\Phi\rhd_{\mathsf{R}}\Psi$ if, and only if, there is an
$\mathsf{R}$-proof of $(\Phi,\Psi)$. This is the smallest logic (according to
$\subseteq$) containing the rules of inference of $\mathsf{R}$.

###### Proof.

See [42, Theorem 1]. ∎

######  Example 5.9.

We provide below an $\mathsf{R}^{\to\neg}_{\textbf{{S3}}}$-proof and an
$\mathsf{R}^{\land\neg}_{\textbf{{BK}}}$-proof witnessing, respectively, that
$\neg p,q,r\rhd_{\mathsf{R}^{\to\neg}_{\textbf{{S3}}}}(q\to p)\to(s\to r),p\to
s$ and $\neg(p\land q),p\rhd_{\mathsf{R}^{\land\neg}_{\textbf{{BK}}}}\neg q$.

$\neg p,q,r$$\mathsf{r}^{\lnot_{\textbf{{\nullfont
S3}}}}_{3}$$s$$\mathsf{r}^{\to_{\textbf{{\nullfont S3}}}}_{1}$$p\to s$$\neg
s$$\mathsf{r}^{\to_{\textbf{{\nullfont S3}}}}_{2}$$\neg(q\to
p)$$\mathsf{r}^{\to_{\textbf{{\nullfont S3}}}}_{1}$$s\to
r$$\mathsf{r}^{\to_{\textbf{{\nullfont S3}}}}_{1}$$(q\to p)\to(s\to r)$

$\neg(p\land q),p$$\mathsf{r}^{\land_{\textbf{{\nullfont
BK}}}}_{6}$$q$$\mathsf{r}^{\land_{\textbf{{\nullfont BK}}}}_{1}$$p\land
q$$\mathsf{r}^{\lnot_{\textbf{{\nullfont BK}}}}_{3}$$\star$$\neg q$

Knowing in advance that the subformulas of a statement of interest are enough
for providing a proof of the statement is an important feature of a calculus,
usually referred to as _analyticity_ , which was already observed in the
3-labelled systems introduced in the previous section. The next definition
introduces a broader notion of analyticity, called _$\Theta$ -analyticity_,
where $\Theta\subseteq L_{\Sigma}(\\{p\\})$ — that is, a set of unary
formulas. The main idea is to allow for not only subformulas of a statement to
appear in an analytic proof, but also formulas resulting from substitutions of
those subformulas over the formulas in $\Theta$. For example, if
$\Theta=\\{r,\neg r\\}$ , a $\Theta$-analytic proof witnessing that $\neg p$
follows from $\neg(p\land q)$ would use only formulas in $\\{p,q,\neg p,\neg
q,\neg\neg p,p\land q,\neg(p\land q),\neg\neg(p\land q)\\}$. We formalize the
notion of $\Theta$-analyticity below.

######  Definition 5.10.

Let $\Theta\subseteq L_{\Sigma}(\\{p\\})$ and $\mathsf{R}$ be a Set-Set
calculus. We say that an $\mathsf{R}$-proof $\mathsf{t}$ of $(\Phi,\Psi)$ is
_$\Theta$ -analytic_ in case only formulas in
$\mathsf{subf}^{\Theta}(\Phi\cup\Psi):=\mathsf{subf}(\Phi\cup\Psi)\cup\\{\sigma(\varphi)\mid\varphi\in\Theta,\sigma:P\to\mathsf{subf}(\Phi\cup\Psi)\\}$
appear in the labels of the nodes of $\mathsf{t}$. We write, in this case,
that $\Phi\rhd_{\mathsf{R}}^{\Theta}\Psi$. When we have
$\Phi\rhd_{\mathsf{R}}^{\Theta}\Psi$ whenever $\Phi\rhd_{\mathsf{R}}\Psi$
(notice that the converse always hold), then $\mathsf{R}$ is said to be
_$\Theta$ -analytic_.

Observe that, in case $\Theta=\varnothing$ or $\Theta=\\{p\\}$, we obtain the
standard notion of analyticity, according to which only the subformulas of the
statement are enough to produce a proof of that very statement in case such
proof exists.

As explained in [31], finite and finitary $\Theta$-analytic calculi are
associated to a proof-search algorithm and a countermodel-search algorithm,
and consequently to a decision procedure for the corresponding Set-Set logics.
Briefly put, if we want to know whether $\Phi\;\rhd_{\mathsf{R}}\;\Psi$, where
$\mathsf{R}$ is a finite and finitary $\Theta$-analytic Set-Set calculus,
obtaining a proof when the answer is positive and a (symbolic) countermodel
otherwise, we may attempt to build a derivation in the following way: start
from a single node labelled with $\Phi$ and search for a rule instance of
$\mathsf{R}$ not used in the same branch with formulas in the set
$\mathsf{subf}^{\Theta}(\Phi\cup\Psi)$ whose premises are in $\Phi$. If there
is one, expand that node by creating a child node labelled with
$\Phi\cup\\{\psi\\}$ for each formula $\psi$ in the succedent of the chosen
rule instance and repeat this step for each new node. In case it fails in
finding a rule instance for applying to some node, we may conclude that no
proof exists, and from each non-$\Psi$-closed branch we may extract a
countermodel. In case every branch eventually gets $\Psi$-closed, the
resulting tree is a proof of the desired statement. This procedure is
exponential-time in the size of the statement of interest in general and, when
$\mathsf{R}$ is Set-Fmla (all inference rules have a single formula in the
succedent), the running-time is polynomial.

######  Definition 5.11.

Let $\mathbb{M}$ be a logical matrix and $\mathsf{R}$ be a multiple conclusion
calculus. Then $\mathsf{R}$ is _sound_ for $\mathbb{M}$ when
$\rhd_{\mathsf{R}}\subseteq\rhd_{\mathbb{M}}$ and it is _complete_ for
$\mathbb{M}$ when the converse holds. When $\mathsf{R}$ is sound and complete
for $\mathbb{M}$, we say that $\mathsf{R}$ is _adequate for_ or _axiomatizes_
$\mathbb{M}$.

######  Example 5.12.

The trivial three-valued matrices $\mathbb{M}$ are those having as sets of
designated values either $\varnothing$ or
$\\{\mathbf{0},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\mathbf{1}\\}$. It is not
hard to see that, in the first case, the calculus containing the single rule
$\frac{p}{\varnothing}$ axiomatizes $\mathbb{M}$; likewise, in the second
case, the rule $\frac{\varnothing}{p}$ is enough. Note that, in the case of
3-labelled calculi, the calculus $\mathsf{G}_{\mathsf{triv}}$ having only the
rules of Identity and Weakening can be easily seen to axiomatize the trivial
matrices (refer to Definition 4.1 for the definitions of the consequence
relations in these cases).

In view of Example 5.12, from now on we shall only consider matrices with
either one or two designated values. We may reduce even more the
configurations to be considered by noticing that a phenomenon observable in
Example 5.12 occurs in general: if
$\mathbb{M}_{1}:=\langle\mathbf{A},D_{1}\rangle$ and
$\mathbb{M}_{2}:=\langle\mathbf{A},{A}{\setminus}{D_{1}}\rangle$, then
$\Phi\rhd_{\mathbb{M}_{1}}\Psi$ iff $\Psi\rhd_{\mathbb{M}_{2}}\Phi$, thus an
axiomatization for $\mathbb{M}_{1}$ can be readily turned into (or used as) an
axiomatization for $\mathbb{M}_{2}$. Indeed, the procedure described in the
sequel will deliver a calculus for $\mathbb{M}_{1}$ from which a calculus for
$\mathbb{M}_{2}$ may be produced by simply turning the inference rules of the
former upside down. In view of this duality, in the three-valued setting we
will first restrict our attention only to matrices having a single designated
value, and will then discuss how to extend the approach to the other cases.

###  5.1 Axiomatizing three-valued matrices: the monadic case

We say that $\mathbb{M}:=\langle\mathbf{A},D\rangle$ is _monadic_ whenever
there is a unary formula $\mathrm{S}(p)\in L_{\Sigma}(\\{p\\})$, sometimes
called a _separator_ , for each pair of truth values $x,y\in A$, such that
$\mathrm{S}_{\mathbf{A}}(x)\in D$ and
$\mathrm{S}_{\mathbf{A}}(y)\in{A}{\setminus}{D}$ or vice-versa. Throughout
this section, we fix a three-valued matrix
$\mathbb{M}:=\langle\mathbf{A},D\rangle$ with $A:=\\{d,u_{1},u_{2}\\}$ and
$D:=\\{d\\}$. Notice that the propositional variable $p$ separates $d$ from
$u_{1}$ and $u_{2}$, so monadicity in this situation requires just the
existence of a separator $\mathrm{S}$ for the non-designated values $u_{1}$
and $u_{2}$. Granted the existence of this separator, then, for each
$x\in\\{u_{1},u_{2}\\}$, let $(\Omega_{x}(p),\mho_{x}(p))$ be a quasi-
partition (that is, a partition allowing for empty components) of
$\\{p,\mathrm{S}(p)\\}$ such that $\psi\in\Omega_{x}(p)$ iff
$\psi_{\mathbf{A}}(x)\in D$ and $\psi\in\mho_{x}(p)$ iff
$\psi_{\mathbf{A}}(x)\in{A}{\setminus}{D}$; in addition, set
$\Omega_{d}(p):=\\{p\\}$ and $\mho_{d}(p):=\varnothing$. It suffices then to
consider only two possible configurations for each $\Omega_{x}(p)$ and
$\mho_{x}(p)$, depending on whether $\mathrm{S}_{\mathbf{A}}(u_{1})\in D$ and
$\mathrm{S}_{\mathbf{A}}(u_{2})\in{A}{\setminus}{D}$, or vice-versa, which we
present in tabular form below:

$x$ | $\Omega_{x}(p)$ | $\mho_{x}(p)$
---|---|---
$d$ | $\\{p\\}$ | $\varnothing$
$u_{1}$ | $\\{\mathrm{S}(p)\\}$ | $\\{p\\}$
$u_{2}$ | $\varnothing$ | $\\{p,\mathrm{S}(p)\\}$

$x$ | $\Omega_{x}(p)$ | $\mho_{x}(p)$
---|---|---
$d$ | $\\{p\\}$ | $\varnothing$
$u_{1}$ | $\varnothing$ | $\\{p,\mathrm{S}(p)\\}$
$u_{2}$ | $\\{\mathrm{S}(p)\\}$ | $\\{p\\}$

Table 2: The configuration at the left applies when
$\mathrm{S}_{\mathbf{A}}(u_{1})\in D$ and
$\mathrm{S}_{\mathbf{A}}(u_{2})\in{A}{\setminus}{D}$, while the one at the
right applies when $\mathrm{S}_{\mathbf{A}}(u_{2})\in D$ and
$\mathrm{S}_{\mathbf{A}}(u_{1})\in{A}{\setminus}{D}$.

In any case, the following lemma, which is a particular case of the general
result given in [31], guarantees that the separators uniquely characterizes
each truth value:

######  Lemma 5.13.

For all $\mathbb{M}$-valuation $v$, $x\in A$ and $\varphi\in L_{\Sigma}(P)$,

$v(\varphi)=x\text{ if{f} }v(\Omega_{x}(\varphi))\subseteq\\{d\\}\text{ and
}v(\mho_{x}(\varphi))\subseteq\\{u_{1},u_{2}\\}.$

###### Proof.

The left-to-right direction easily follows from the definitions of
$\Omega_{x}(p)$ and $\mho_{x}(p)$. For the converse, suppose that
$v(\varphi)=y\neq x$. Assume that $\mathrm{U}\in L_{\Sigma}(\\{p\\})$
separates $x$ and $y$, with $\mathrm{U}(p)\in\Omega_{x}(p)$. Then
$v(\mathrm{U}(\varphi))=\mathrm{U}_{\mathbf{A}}(v(\varphi))=\mathrm{U}_{\mathbf{A}}(y)\in\\{u_{1},u_{2}\\}$,
hence $v(\Omega_{x}(\varphi))\not\subseteq\\{d\\}$. The case when
$\mathrm{U}(p)\in\mho_{x}(p)$ is analogous. ∎

######  Example 5.14.

Clearly, in a three-valued $\Sigma$-matrix $\langle
V_{3},\\{\mathbf{1}\\}\rangle$, when there is $\neg\in\Sigma_{1}$ interpreted
either as $\lnot_{\textbf{{\L${}_{3}$}}}$ or $\lnot_{\textbf{{G3}}}$, $\neg p$
is a separator for $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ and $\mathbf{0}$,
since
$\lnot_{\textbf{{\L${}_{3}$}}}(\nicefrac{{\mathbf{1}}}{{\mathbf{2}}})={\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}\notin\\{\mathbf{1}\\}$
and $\lnot_{\textbf{{\L${}_{3}$}}}(\mathbf{0})=\mathbf{1}\in\\{\mathbf{1}\\}$.

Below we provide discriminators applicable to some of the prominent logics
presented in Section 3.

$\lnot_{\textbf{{\L${}_{3}$}}}$
---
$x$ | $\Omega_{x}^{\\{\mathbf{1}\\}}(p)$ | $\mho_{x}^{\\{\mathbf{1}\\}}(p)$
$\mathbf{0}$ | $\neg p$ | $p$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\varnothing$ | $p,\neg p$
$\mathbf{1}$ | $p$ | $\varnothing$

$\lnot_{\textbf{{\L${}_{3}$}}}$
---
$x$ | $\Omega_{x}^{\\{\mathbf{1},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\\}}(p)$ | $\mho_{x}^{\\{\mathbf{1},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\\}}(p)$
$\mathbf{0}$ | $\varnothing$ | $p$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $p,\neg p$ | $\varnothing$
$\mathbf{1}$ | $p$ | $\neg p$

Table 3: Discriminators for matrices with $\lnot_{\textbf{{\L${}_{3}$}}}$.
$\lnot_{\textbf{{G3}}}$
---
$x$ | $\Omega_{x}^{\\{\mathbf{1}\\}}(p)$ | $\mho_{x}^{\\{\mathbf{1}\\}}(p)$
$\mathbf{0}$ | $\neg p$ | $p$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\varnothing$ | $p,\neg p$
$\mathbf{1}$ | $p$ | $\varnothing$
Table 4: Discriminator for matrices with $\lnot_{\textbf{{G3}}}$.

The next example shows that non-monadicity is not hard to witness: a slight
change in the matrix of G3 would do. In Subsection 5.2, we will see other
examples of non-monadic matrices, as well as Set-Set axiomatizations for them.

######  Example 5.15.

The matrix resulting from the one of G3 by replacing the set of designated
values by $\\{\mathbf{1},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\\}$ is not
monadic. One can see this by producing by composition all the unary operators
on $V_{3}$ using the connectives of G3, and noticing that none of them can
separate $\mathbf{1}$ from $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$. Actually,
a shorter path for such conclusion is by noticing that this matrix is not even
reduced, hence it cannot be monadic [42].

From now on, let $\Theta:=\\{p,\mathrm{S}(p)\\}$ and assume, without loss of
generality, that the leftmost configuration presented in Table 2 defines a
discriminator for $\mathbb{M}$. We now define a recipe to generate a finite
$\Theta$-analytical Set-Set calculus for $\mathbb{M}$.

######  Definition 5.16.

Define $\mathsf{R}_{\mathbb{M}}$ as the Set-Set calculus containing, for each
$k\in\omega$, $\copyright\in\Sigma^{k}$ and $x_{1},\ldots,x_{k}\in A$, the
following rule schemas:

$\displaystyle\mathsf{r}_{\copyright,x_{1},\ldots,x_{k},T_{y}}:=\frac{\bigcup_{i=1}^{k}\Omega_{x_{i}}(p_{i})}{\bigcup_{i=1}^{k}\mho_{x_{i}}(p_{i}),T_{y}(\copyright(p_{1},\ldots,p_{k}))},$
$\displaystyle\text{ for each }T_{y}\in\Omega_{y}(p),and$
$\displaystyle\mathsf{r}_{\copyright,x_{1},\ldots,x_{k},F_{y}}:=\frac{\bigcup_{i=1}^{k}\Omega_{x_{i}}(p_{i}),F_{y}(\copyright(p_{1},\ldots,p_{k}))}{\bigcup_{i=1}^{k}\mho_{x_{i}}(p_{i})},$
$\displaystyle\text{ for each }F_{y}\in\mho_{y}(p),$ $\displaystyle\text{where
}y:=\copyright_{\mathbf{A}}(x_{1},\ldots,x_{k}).$

######  Theorem 5.17.

$\mathsf{R}_{\mathbb{M}}$ is sound with respect to $\mathbb{M}$, that is,
$\rhd_{\mathsf{R}_{\mathbb{M}}}\subseteq\rhd_{\mathbb{M}}$.

###### Proof.

Let $\copyright\in\Sigma^{k}$, $x_{1},\ldots,x_{k}\in A$ and
$y:={\copyright}_{\mathbf{A}}(x_{1},\ldots,x_{k})$. Suppose that $v$ is an
$\mathbb{M}$-valuation such that
$v(\bigcup_{i=1}^{k}\Omega_{x_{i}}(p_{i}))\subseteq\\{d\\}$ and
$v(\bigcup_{i=1}^{k}\mho_{x_{i}}(p_{i}))\subseteq\\{u_{1},u_{2}\\}$ (notice
that a purported counter-model for any of the schemas in Definition 5.16 must
show this behaviour). Then, by Lemma 5.13, we have $v(p_{i})=x_{i}$ for all
$1\leq i\leq k$. Now, looking at a schema of the form
$\mathsf{r}_{\copyright,x_{1},\ldots,x_{k},T_{y}}$, with
$y:={\copyright}_{\mathbf{A}}(x_{1},\ldots,x_{k})$, a counter-model for it
would have $v(T_{y}(\copyright(p_{1},\ldots,p_{k})))\in\\{u_{1},u_{2}\\}$, but
then, by Lemma 5.13 again, this would mean that
$v(\copyright(p_{1},\ldots,p_{k}))\neq y$, contradicting our hypothesis. The
same reasoning may be applied to the schemas of the form
$\mathsf{r}_{\copyright,x_{1},\ldots,x_{k},F_{y}}$. ∎

For what follows, recall that we denote the complement of a Set-Set logic
$\rhd{}$ by $\blacktriangleright$.

######  Lemma 5.18.

Let $\Pi\subseteq L_{\Sigma}(P)$ such that
$\Pi\blacktriangleright_{\mathsf{R}_{\mathbb{M}}}^{\Theta}{\Pi}^{\mathsf{c}}$.
Then there is an $\mathbb{M}$-valuation $v$ such that $v(\Pi)\subseteq\\{d\\}$
and $v({\Pi}^{\mathsf{c}})\subseteq\\{u_{1},u_{2}\\}$.

###### Proof.

Consider the mapping $v^{\prime}:P\to A$ such that

$v^{\prime}(p):=\begin{cases}d&p\in\Pi\\\
u_{1}&p\not\in\Pi,\mathrm{S}(p)\not\in\Pi\\\
u_{2}&p\not\in\Pi,\mathrm{S}(p)\in\Pi\\\ \end{cases}$

We will prove by induction on the structure of formulas that the extension $v$
of $v^{\prime}$ to the full language is such that $P(\varphi):=``v(\varphi)=x$
iff $\Omega_{x}(\varphi)\subseteq\Pi$ and
$\mho_{x}(\varphi)\subseteq{\Pi}^{\mathsf{c}}$” for all $\varphi\in
L_{\Sigma}(P)$. As a consequence, since $\Omega_{d}(p)=\\{p\\}$ and
$\mho_{d}(p)=\varnothing$, we will have that $v(\varphi)=d$ iff
$\varphi\in\Pi$, proving the present lemma. Proceeding with the induction,
then, the base case is obvious from the definition of $v^{\prime}$. In the
inductive step, let $\varphi:=\copyright(\psi_{1},\ldots,\psi_{k})$, for a
$\copyright\in\Sigma^{k}$, and assume that $P(\psi_{i})$ holds for all $1\leq
i\leq k$. From the left to the right, suppose that
$v(\copyright(\psi_{1},\ldots,\psi_{k}))=x$, hence
${\copyright}_{\mathbf{A}}(v(\psi_{1}),\ldots,v(\psi_{k}))=x$, and call
$x_{i}:=v(\psi_{i})$. By the induction hypothesis, we have that
$\Omega_{x_{i}}(\psi_{i})\subseteq\Pi$ and
$\mho_{x_{i}}(\psi_{i})\subseteq{\Pi}^{\mathsf{c}}$, and, by (the
contrapositive of) monotonicity of $\rhd_{\mathsf{R}_{\mathbb{M}}}^{\Theta}$,
we have
$\bigcup_{i}\Omega_{x_{i}}(\psi_{i})\blacktriangleright_{\mathsf{R}_{\mathbb{M}}}^{\Theta}\bigcup_{i}\mho_{x_{i}}(\psi_{i})$.
Assume, by contradiction, that $\gamma\in\Omega_{x}(\varphi)\setminus\Pi$,
thus
$\bigcup_{i}\Omega_{x_{i}}(\psi_{i})\blacktriangleright_{\mathsf{R}_{\mathbb{M}}}^{\Theta}\bigcup_{i}\mho_{x_{i}}(\psi_{i}),\gamma$,
but this goes against the rule
$\mathsf{r}_{\copyright,x_{1},\ldots,x_{k},\gamma_{x}}$ present in
$\mathsf{R}_{\mathbb{M}}$. A similar argument applies when we assume that
$\gamma\in\mho_{x}(\varphi)\setminus{\Pi}^{\mathsf{c}}$. The other direction
easily follows by monotonicity of $\rhd_{\mathsf{R}_{\mathbb{M}}}^{\Theta}$
again and Lemma 5.13. ∎

######  Theorem 5.19.

$\mathsf{R}_{\mathbb{M}}$ is a finite $\\{p,\mathrm{S}(p)\\}$-analytical
axiomatization for $\mathbb{M}$.

###### Proof.

Finiteness of $\mathsf{R}_{\mathbb{M}}$ is obvious since $\mathbb{M}$ is a
finite logical matrix. Soundness follows by Theorem 5.17 and the fact that
$\rhd_{\mathsf{R}_{\mathbb{M}}}^{\Theta}\subseteq\rhd_{\mathsf{R}_{\mathbb{M}}}$.
It remains to prove completeness, i.e., that
$\rhd_{\mathbb{M}}\subseteq\rhd_{\mathsf{R}_{\mathbb{M}}}^{\Theta}$. Suppose
that $\Phi\blacktriangleright_{\mathsf{R}_{\mathbb{M}}}^{\Theta}\Psi$, then,
by cut for sets, there is $\Pi\subseteq L_{\Sigma}(P)$ such that
$\Pi,\Phi\blacktriangleright_{\mathsf{R}_{\mathbb{M}}}^{\Theta}\Psi,{\Pi}^{\mathsf{c}}$.
Then Lemma 5.18 applies and the provided $\mathbb{M}$-valuation makes
$v(\Phi)\subseteq\\{d\\}$ and $v(\Psi)\subseteq\\{u_{1},u_{2}\\}$, as desired.
∎

It is worth emphasizing the modularity of the proposed approach: each
connective is axiomatized by its own set of rule schemas, thus axiomatizing a
matrix expanded with new connectives is a matter of adding new rule schemas
corresponding to the new connectives. The examples to be presented in a moment
will show that Definition 5.16 may deliver redundant and complex rule schemas.
This fact motivates the next result, which introduces some streamlining steps
that highly simplify the generated axiomatization. The proof uses, in essence,
the properties of Set-Set logics. In what follows, we say that a rule schema
is a _dilution_ of another when the former can be obtained from the latter by
adding formulas in the antecedent or in the succedent (recall property (D) in
Definition 2.2). In that case, we may also say that the latter is a
_subschema_ of the former. In what follows, denote by
$\mathsf{fmlas}(\mathsf{t})$ the set of formulas appearing in the
$\mathsf{R}$-derivation $\mathsf{t}$.

######  Theorem 5.20.

Let $\mathsf{R}$ be a $\Theta$-analytical calculus for a matrix $\mathbb{M}$
and consider the following streamlining subprocedure:

(S1)

Remove all instances of overlap.

(S2)

Remove all rule schemas that are dilutions of other rule schemas in
$\mathsf{R}$.

(S3)

Replace occurrences of pairs of rule schemas $\frac{\Phi,\varphi}{\Psi}$ and
$\frac{\Phi}{\Psi,\varphi}$ by $\frac{\Phi}{\Psi}$.

(S4)

Replace a rule of inference by one of its subrules that is derivable using the
rules of the calculus.

(S5)

Remove a rule of inference $\mathsf{r}:=\frac{\Phi}{\Psi}$ that has a proof
$\mathsf{t}$ using the others rules of $\mathsf{R}$, such that, for all
$\Gamma\subseteq L_{\Sigma}(P)$ and all $\sigma:P\to\mathsf{subf}(\Gamma)$, if
$\sigma(\Phi),\sigma(\Psi)\subseteq\mathsf{subf}^{\Theta}(\Gamma)$, then
$\sigma(\mathsf{fmlas}(\mathsf{t}))\subseteq\mathsf{subf}^{\Theta}(\Gamma)$.

Then (S1), (S2), (S3), (S4) and (S5) preserve adequacy for $\mathbb{M}$ and
$\Theta$-analyticity.

In order to use a terminology that is closer to that used in 3-labelled
calculi, if $\mathbf{L}$ is determined by $\mathbb{M}$, then we will sometimes
denote $\mathsf{R}_{\mathbb{M}}$ by $mc.{\mathbf{L}}$ and the streamlined
version of this calculus by $smc.{\mathbf{L}}$. We now exemplify the
axiomatization procedure and the streamlining procedures just described,
producing Set-Set axiomatizations for the monadic matrices among those three-
valued matrices introduced in the beginning of the present work. Assume that
$d=\mathbf{1}$, $u_{1}=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ and
$u_{2}=\mathbf{0}$ for the next examples.

######  Example 5.21.

Consider the three-valued matrix with $\\{\mathbf{1}\\}$ as the set of
designated values over a signature containing only $\neg$, interpreted as
$\lnot_{\textbf{{\L${}_{3}$}}}$. Notice that the configuration at the left of
Table 3 applies in this case. According to Definition 5.16, then, the
following rule schemas axiomatize $\neg$ in this matrix:

$\displaystyle\mathsf{r}_{\neg,\mathbf{1},\neg p}=\frac{p}{\neg\neg
p}\quad\mathsf{r}_{\neg,\mathbf{1},p}=\frac{p,\neg
p}{}\quad\mathsf{r}_{\neg,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},p}=\frac{\neg
p}{p,\neg p}\quad\mathsf{r}_{\neg,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\neg
p}=\frac{\neg\neg p}{p,\neg p}\quad\mathsf{r}_{\neg,\mathbf{0},p}=\frac{\neg
p}{p,\neg p}$

By Theorem 5.20, we may remove schemas
$\mathsf{r}_{\neg,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},p}$ and
$\mathsf{r}_{\neg,\mathbf{0},p}$ as they are instances of overlap, as well as
replace $\mathsf{r}_{\neg,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\neg p}$ with
$\frac{\neg\neg p}{p}$, as the latter is a subschema of the former easily
derivable from $\mathsf{r}_{\neg,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\neg
p}$ itself and $\mathsf{r}_{\neg,\mathbf{1},p}$. The simplified axiomatization
for $\lnot_{\textbf{{\L${}_{3}$}}}$, then, contains the following rule
schemas:

$\displaystyle\frac{p}{\neg\neg
p}\mathsf{r}^{\lnot_{\textbf{{\L${}_{3}$}}}}_{1}\quad\frac{\neg\neg
p}{p}\mathsf{r}^{\lnot_{\textbf{{\L${}_{3}$}}}}_{2}\quad\frac{p,\neg
p}{}\mathsf{r}^{\lnot_{\textbf{{\L${}_{3}$}}}}_{3}$

######  Example 5.22.

Now consider the matrix of Example 5.21 expanded with connectives $\land$ and
$\lor$, interpreted respectively as $\land_{\mathsf{min}}$ and
$\lor_{\mathsf{max}}$. Let us axiomatize $\land$ in detail. By employing
Definition 5.16, we produce the following rule schemas:

$\displaystyle\mathsf{r}_{\land,\mathbf{1},\mathbf{1},p}=\frac{p,q}{p\land
q}\quad\mathsf{r}_{\land,\mathbf{1},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},p}=\frac{p,p\land
q}{q,\neg
q}\quad\mathsf{r}_{\land,\mathbf{1},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\neg
p}=\frac{p,\neg(p\land q)}{q,\neg q}$
$\displaystyle\mathsf{r}_{\land,\mathbf{1},\mathbf{0},p}=\frac{p,\neg q,p\land
q}{q}\quad\mathsf{r}_{\land,\mathbf{1},\mathbf{0},\neg p}=\frac{p,\neg
q}{q,\neg(p\land
q)}\quad\mathsf{r}_{\land,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\mathbf{1},p}=\frac{q,p\land
q}{p,\neg p}$
$\displaystyle\mathsf{r}_{\land,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\mathbf{1},\neg
p}=\frac{q,\neg(p\land q)}{p,\neg
p}\quad\mathsf{r}_{\land,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},p}=\frac{p\land
q}{p,\neg p,q,\neg
q}\quad\mathsf{r}_{\land,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\neg
p}=\frac{\neg(p\land q)}{p,\neg p,q,\neg q}$
$\displaystyle\mathsf{r}_{\land,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\mathbf{0},p}=\frac{\neg
q,p\land q}{p,\neg
p,q}\quad\mathsf{r}_{\land,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\mathbf{0},\neg
p}=\frac{\neg q}{p,\neg p,q,\neg(p\land
q)}\quad\mathsf{r}_{\land,\mathbf{0},\mathbf{1},\neg p}=\frac{\neg
p,q}{p,\neg(p\land q)}$
$\displaystyle\mathsf{r}_{\land,\mathbf{0},\mathbf{1},p}=\frac{\neg p,q,p\land
q}{p}\quad\mathsf{r}_{\land,\mathbf{0},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\neg
p}=\frac{\neg p}{p,q,\neg q,\neg(p\land
q)}\quad\mathsf{r}_{\land,\mathbf{0},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},p}=\frac{\neg
p,p\land q}{p,q,\neg q}$
$\displaystyle\mathsf{r}_{\land,\mathbf{0},\mathbf{0},\neg p}=\frac{\neg
p,\neg q}{p,q,\neg(p\land
q)}\quad\mathsf{r}_{\land,\mathbf{0},\mathbf{0},p}=\frac{\neg p,\neg q,p\land
q}{p,q}$

Over these schemas, we apply Theorem 5.20 to obtain a much shorter version of
this calculus:

$\displaystyle\frac{p,q}{p\land
q}\mathsf{r}^{\land_{\mathsf{min}}}_{1}\quad\frac{p\land
q}{p}\mathsf{r}^{\land_{\mathsf{min}}}_{2}\quad\frac{p\land
q}{q}\mathsf{r}^{\land_{\mathsf{min}}}_{3}\quad\frac{\neg(p\land q)}{\neg
p,\neg q}\mathsf{r}^{\land_{\mathsf{min}}}_{4}\quad\frac{\neg p}{\neg(p\land
q)}\mathsf{r}^{\land_{\mathsf{min}}}_{5}\quad\frac{\neg q}{\neg(p\land
q)}\mathsf{r}^{\land_{\mathsf{min}}}_{6}$

We may then follow the same procedure for axiomatizing $\lor$, and the result
will be:

$\displaystyle\frac{p}{p\lor
q}\mathsf{r}^{\lor_{\mathsf{max}}}_{1}\quad\frac{q}{p\lor
q}\mathsf{r}^{\lor_{\mathsf{max}}}_{2}\quad\frac{p\lor
q}{p,q}\mathsf{r}^{\lor_{\mathsf{max}}}_{3}\quad\frac{\neg p,\neg
q}{\neg(p\lor q)}\mathsf{r}^{\lor_{\mathsf{max}}}_{4}\quad\frac{\neg(p\lor
q)}{\neg p}\mathsf{r}^{\lor_{\mathsf{max}}}_{5}\quad\frac{\neg(p\lor q)}{\neg
q}\mathsf{r}^{\lor_{\mathsf{max}}}_{6}$

With axiomatizations of $\lnot_{\textbf{{\L${}_{3}$}}}$,
$\land_{\mathsf{min}}$ and $\lor_{\mathsf{max}}$ in hand, it is straighforward
now to produce a calculus for the logics Ł3 and K: we just need to axiomatize
$\to_{\textrm{{{\L${}_{3}$}}}}$ and $\to_{\textbf{{K}}}$, which we do more
briefly in the next example.

######  Example 5.23.

According to Definition 5.16 and the streamlining procedures proposed in
Theorem 5.20, $\to_{\textrm{{{\L${}_{3}$}}}}$ is axiomatized by the following
rule schemas:

$\displaystyle\frac{\neg p}{p\to
q}\mathsf{r}^{\to_{\textrm{{{\L${}_{3}$}}}}}_{1}\;\frac{q}{p\to
q}\mathsf{r}^{\to_{\textrm{{{\L${}_{3}$}}}}}_{2}\;\frac{}{p\to q,\neg
q,p}\mathsf{r}^{\to_{\textrm{{{\L${}_{3}$}}}}}_{3}\;\frac{\neg q,p}{\neg(p\to
q)}\mathsf{r}^{\to_{\textrm{{{\L${}_{3}$}}}}}_{4}$ $\displaystyle\frac{p\to
q,\neg q}{\neg
p}\mathsf{r}^{\to_{\textrm{{{\L${}_{3}$}}}}}_{5}\;\frac{\neg(p\to q)}{\neg
q}\mathsf{r}^{\to_{\textrm{{{\L${}_{3}$}}}}}_{6}\;\frac{\neg(p\to
q)}{p}\mathsf{r}^{\to_{\textrm{{{\L${}_{3}$}}}}}_{7}\;\frac{p,p\to
q}{q}\mathsf{r}^{\to_{\textrm{{{\L${}_{3}$}}}}}_{8}$

In turn, $\to_{\textbf{{K}}}$ is axiomatized by:

$\displaystyle\frac{\neg p}{p\to
q}\mathsf{r}^{\to_{\textbf{{K}}}}_{1}\;\frac{q}{p\to
q}\mathsf{r}^{\to_{\textbf{{K}}}}_{2}\;\frac{\neg q,p}{\neg(p\to
q)}\mathsf{r}^{\to_{\textbf{{K}}}}_{3}\;\frac{p\to q}{\neg
p,q}\mathsf{r}^{\to_{\textbf{{K}}}}_{4}\;\frac{\neg(p\to q)}{\neg
q}\mathsf{r}^{\to_{\textbf{{K}}}}_{5}\;\frac{\neg(p\to
q)}{p}\mathsf{r}^{\to_{\textbf{{K}}}}_{6}$

Notice that, in this case, instead of $\neg p$, we could have used $p\to p$ to
separate the values $\mathbf{0}$ and $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$,
since $\mathbf{0}\to_{\textbf{{K}}}\mathbf{0}=\mathbf{1}$ is designated and
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\to_{\textbf{{K}}}\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$
is non-designated. The produced rules, after simplification, would be the
following:

$\displaystyle\frac{q\to q,p}{(p\to q)\to(p\to q)}\quad\frac{p\to q}{p\to
p,q}\quad\frac{q}{p\to q}$ $\displaystyle\frac{(p\to q)\to(p\to q)}{p\to
q,q\to q}\quad\frac{(p\to q)\to(p\to q)}{p\to q,p}\frac{p\to p}{p\to
q,p}\quad\frac{p\to q,p}{q}$

######  Example 5.24.

Consider now $\lnot_{\textbf{{G3}}}$, which changes the output under
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ to $\mathbf{0}$ when compared with
$\lnot_{\textbf{{\L${}_{3}$}}}$. Definition 5.16 produces the following rules
schemas:

$\displaystyle\mathsf{r}_{\neg,\mathbf{1},\neg p}=\frac{p}{\neg\neg
p}\;\mathsf{r}_{\neg,\mathbf{1},p}=\frac{p,\neg
p}{}\;\mathsf{r}_{\neg,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},p}=\frac{\neg
p}{p,\neg p}\;\mathsf{r}_{\neg,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\neg
p}=\frac{}{p,\neg p,\neg\neg p}\;\mathsf{r}_{\neg,\mathbf{0},p}=\frac{\neg
p}{p,\neg p}$

Notice that $\mathsf{r}_{\neg,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},p}$ and
$\mathsf{r}_{\neg,\mathbf{0},p}$ may be removed as they are instances of
overlap. Also, $\frac{}{\neg p,\neg\neg p}$ is derivable from the other rules,
so we may use it instead of
$\mathsf{r}_{\neg,\nicefrac{{\mathbf{1}}}{{\mathbf{2}}},\neg p}$. Finally, in
this new calculus, we may derive $\mathsf{r}_{\neg,\mathbf{1},\neg p}$, so it
can be removed. The final axiomatization for $\lnot_{\textbf{{G3}}}$ is then

$\displaystyle\frac{p,\neg
p}{}\mathsf{r}^{\lnot_{\textbf{{G3}}}}_{1}\quad\frac{}{\neg p,\neg\neg
p}\mathsf{r}^{\lnot_{\textbf{{G3}}}}_{2}$

We have seen many examples of axiomatizations for three-valued logical
matrices having a single designated value. Now we indicate how to extend our
approach to matrices with two designated values. Let
$\mathbb{M}_{1}=\langle\\{d,u_{1},u_{2}\\},\\{u_{1},u_{2}\\}\rangle$. We may
obtain a matrix $\mathbb{M}_{2}$ with a single designated value from
$\mathbb{M}_{1}$ by simply taking the set $\\{d\\}$ as designated:
$\mathbb{M}_{2}=\langle\\{d,u_{1},u_{2}\\},\\{d\\}\rangle$. We know then that,
if $\mathbb{M}_{2}$ is monadic, there are quasi-partitions
$(\Omega_{x}^{2}(p),\mho_{x}^{2}(p))$ for each $x$ and that
$v(\varphi)=x\text{ if{f} }v(\Omega_{x}^{2}(\varphi))\subseteq\\{d\\}\text{
and }v(\mho_{x}^{2}(\varphi))\subseteq\\{u_{1},u_{2}\\}$, from which, by
Definition 5.16, we obtain an adequate $\\{p,\mathrm{S}(p)\\}$-analytic
calculus $\mathsf{R}_{2}$ for $\mathbb{M}_{2}$. If we take
$(\Omega_{x}^{1}(p),\mho_{x}^{1}(p))$ for each $x$ such that
$\Omega_{x}^{1}(p):=\mho_{x}^{2}(p)$ and $\mho_{x}^{1}(p):=\Omega_{x}^{2}(p)$,
then $v(\varphi)=x\text{ if{f}
}v(\Omega_{x}^{1}(\varphi))\subseteq\\{u_{1},u_{2}\\}\text{ and
}v(\mho_{x}^{1}(\varphi))\subseteq\\{d\\}$, thus we have separators for
$\mathbb{M}_{1}$. We may use them in Definition 5.16 to build a
$\\{p,\mathrm{S}(p)\\}$-analytical calculus $\mathsf{R}_{1}$ which can be
easily proved to be sound and complete with respect to $\mathbb{M}_{1}$ by
simply adapting the proofs of Lemma 5.18 and Theorem 5.19. But we can easily
see that the schemas in $\mathsf{R}_{1}$ are just the schemas in
$\mathsf{R}_{2}$ turned upside down, and this is how our approach simply
extends to the case of two designated values.

######  Example 5.25.

Consider the three-valued matrix for the Logic of Paradox (LP), which has the
same signature and interpretation structure as the logic K, but, instead of
having $\\{\mathbf{1}\\}$ as set of designated values, it has
$\\{\mathbf{1},\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\\}$. According to what we
have presented above, we may produce an axiomatization for the matrix with the
same interpretations but with set of designated values being
$\\{\mathbf{0}\\}$, following Definition 5.16 and Theorem 5.20, and then
simply turn the rules upside down to axiomatize LP.

######  Example 5.26.

Post’s logic P3 is axiomatized by the rules for $\land$ and $\lor$ in Ł3 (see
Example 5.22) together with the following rules for $\neg$, again produced
using the described procedure and simplifications:

$\frac{}{\neg\neg p,\neg
p,p}\mathsf{r}^{\lnot_{\textbf{{P3}}}}_{1}\qquad\frac{\neg\neg
p,p}{}\mathsf{r}^{\lnot_{\textbf{{P3}}}}_{2}\qquad\frac{\neg
p,p}{}\mathsf{r}^{\lnot_{\textbf{{P3}}}}_{3}$

######  Remark 5.27.

The recipe we have described and exemplified throughout this section is a
simplification of the general method for axiomatizing finite monadic matrices
given in [42], which was recently generalized to finite monadic partial non-
deterministic logical matrices in [14].

###  5.2 Axiomatization of non-monadic matrices

As we have been insisting on, non-monadic deterministic logical matrices can
always be axiomatized in Set-Set [42, Theorem 19.12] using the original
language, although not via our recipe. There is no known algorithm for this
general case. By employing separators with contexts [42, Section 19.5] in an
ad hoc manner, however, we managed to show Set-Set $\Theta$-analytic
axiomatizations — now allowing $\Theta$ to contain formulas of arities other
than 1, for instance $p\lor q$ and $p\to q$ — for fragments of some of the
logics presented in Section 3. We present them in the sequel.

######  Remark 5.28.

We should mention that our recipe for monadic matrices can always be applied
to non-monadic matrices provided that the object language is extended with
connectives guaranteeing the separation of all truth values. The resulting
matrix is then monadic and the logic is a conservative extension of the
original logic [31].

####  5.2.1 Disjunctive fragment of Bochvar-Kleene’s logic

Let $\rhd_{\textbf{{BK}}}^{\lor}$ be the Set-Set logic determined by the
three-valued logical matrix $\mathbb{M}_{\textbf{{BK}}}^{\lor}$ whose
signature contains only $\lor$, interpreted as $\lor_{\textbf{{BK}}}$ in this
case — the truth table of which we repeat below for convenience — and whose
set of designated values is $\\{\mathbf{1}\\}$. The reader can easily verify
that this matrix is not monadic by using the fact that the sets
$\\{\mathbf{0}\\}$ and $\\{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}\\}$ are both
closed under $\lor_{\textbf{{BK}}}$. Although our previous recipe does not
apply in this scenario, we are still able to provide an analytic
axiomatization for this matrix.

$\lor_{\textbf{{BK}}}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
---|---|---|---
$\mathbf{0}$ | $\mathbf{0}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$
$\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$
$\mathbf{1}$ | $\mathbf{1}$ | $\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ | $\mathbf{1}$

######  Definition 5.29.

Let $\mathsf{R}^{\lor}_{\textbf{{BK}}}$ be the Set-Set calculus whose rule
schemas are the following:

$\displaystyle\frac{p\lor
q}{p,q}\mathsf{r}^{\lor,1}_{\textbf{{BK}}}\quad\frac{p,q}{p\lor
q}\mathsf{r}^{\lor,2}_{\textbf{{BK}}}$ $\displaystyle\frac{p_{1}\lor
q_{1},p_{2}}{p_{1}\lor
p_{2}}\mathsf{r}^{\lor,3}_{\textbf{{BK}}}\quad\frac{p_{2}\lor
q_{1},p_{1}}{p_{1}\lor
p_{2}}\mathsf{r}^{\lor,4}_{\textbf{{BK}}}\quad\frac{p_{1}\lor
p_{2},q_{1}}{p_{2}\lor q_{1}}\mathsf{r}^{\lor,5}_{\textbf{{BK}}}$
$\displaystyle\frac{p_{1}\lor q_{1},p_{2}\lor q_{1}}{(p_{1}\lor p_{2})\lor
q_{1},p_{1}}\mathsf{r}^{\lor,6}_{\textbf{{BK}}}\quad\frac{(p_{1}\lor
p_{2})\lor q_{1},q_{1}}{p_{1}\lor
q_{1}}\mathsf{r}^{\lor,7}_{\textbf{{BK}}}\quad\frac{(p_{1}\lor p_{2})\lor
q_{1},q_{1}}{p_{2}\lor q_{1}}\mathsf{r}^{\lor,8}_{\textbf{{BK}}}$

######  Theorem 5.30.

$\mathsf{R}^{\lor}_{\textbf{{BK}}}$ is sound for
$\mathbb{M}_{\textbf{{BK}}}^{\lor}$.

###### Proof.

This is routine. ∎

######  Lemma 5.31.

Some derivable rules:

$\frac{p_{1}\lor p_{2},q_{1}}{p_{1}\lor
q_{1}}\mathsf{r}^{\lor,9}_{\textbf{{BK}}}\\\ \quad\frac{p_{1}\lor
p_{2}}{p_{2}\lor p_{1}}\mathsf{r}^{\lor,10}_{\textbf{{BK}}}\\\ $

######  Theorem 5.32.

$\mathsf{R}^{\lor}_{\textbf{{BK}}}$ is complete for
$\mathbb{M}_{\textbf{{BK}}}^{\lor}$ and $\\{p\lor q\\}$-analytic.

###### Proof.

Let $\Theta:=\\{p\lor q\\}$. Suppose that
$\Phi\blacktriangleright_{\mathsf{R}^{\lor}_{\textbf{{BK}}}}^{\Theta}\Psi$,
then, by cut for sets, there is $\Pi\subseteq L_{\Sigma}(P)$ such that
$\Pi\blacktriangleright_{\mathsf{R}^{\lor}_{\textbf{{BK}}}}^{\Theta}{\Pi}^{\mathsf{c}}$,
with $\Phi\subseteq\Pi$ and $\Psi\subseteq{\Pi}^{\mathsf{c}}$. Let
$S:=\mathsf{subf}(\Phi\cup\Psi)\cup\\{\varphi\lor\psi\mid\varphi,\psi\in\mathsf{subf}(\Phi\cup\Psi)\\}$.
Then $T\blacktriangleright_{\mathsf{R}^{\lor}_{\textbf{{BK}}}}^{\Theta}F$ for
some partition $(T,F)$ of $S$, with $\Phi\subseteq T$ and $\Psi\subseteq F$.
We consider two cases, defining for each of them a mapping
$v:\mathsf{subf}(\Phi\cup\Psi)\to V_{3}$ and proving that
$v(\varphi\lor\psi)=v(\varphi)\lor_{\textbf{{BK}}}v(\psi)$:

  * •

(a): for all $\varphi,\psi$, if $\varphi\in T\cap\mathsf{subf}(\Phi\cup\Psi)$
and $\psi\in F\cap\mathsf{subf}(\Phi\cup\Psi)$, then $\varphi\lor\psi\in T$.
Let $v:\mathsf{subf}(\Phi\cup\Psi)\to V_{3}$ such that

$v(\varphi):=\begin{cases}\mathbf{1}&\text{ if }\varphi\in T\\\
\mathbf{0}&\text{ if }\varphi\in F\\\ \end{cases}$

    * –

if $v(\varphi\lor\psi)=\mathbf{1}$, then, by
$(\mathsf{r}^{\lor,1}_{\textbf{{BK}}})$, either $v(\varphi)=\mathbf{1}$ or
$v(\psi)=\mathbf{1}$, and we are done, as the range of $v$ is
$\\{\mathbf{1},\mathbf{0}\\}$;

    * –

if $v(\varphi)=\mathbf{1}$, in case $v(\psi)=\mathbf{1}$, use
$(\mathsf{r}^{\lor,2}_{\textbf{{BK}}})$, and in case $v(\psi)=\mathbf{0}$, use
the assumption (a). The argument is analogous for $v(\psi)=\mathbf{1}$, with
the help of $(\mathsf{r}^{\lor,10}_{\textbf{{BK}}})$;

    * –

if $v(\varphi\lor\psi)=\mathbf{0}$, use the contrapositive of (a), which gives
us that either $\varphi\in F$ or $\psi\in T$. We want to conclude
$\varphi,\psi\in F$ and for that it is enough to show $\psi\in F$. Assume that
$\psi\in T$ and consider two subcases: either $\varphi\in T$ or $\varphi\in
F$. The first case is absurd by $(\mathsf{r}^{\lor,2}_{\textbf{{BK}}})$. The
second case produces, by (a), $\psi\lor\varphi\in T$, but then by
$(\mathsf{r}^{\lor,10}_{\textbf{{BK}}})$ we have $\varphi\lor\psi\in T$,
absurd again. Thus $\psi\in F$ and we are done.

    * –

if $v(\varphi)=\mathbf{0}$ and $v(\psi)=\mathbf{0}$, by
$(\mathsf{r}^{\lor,1}_{\textbf{{BK}}})$ we have $\varphi\lor\psi\in F$.

  * •

for some $\psi_{\mathbf{1}}\in T\cap\mathsf{subf}(\Phi\cup\Psi)$ and
$\psi_{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}\in
F\cap\mathsf{subf}(\Phi\cup\Psi)$, we have
$\psi_{\mathbf{1}}\lor\psi_{\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}}\in F$. Let
$v:\mathsf{subf}(\Phi\cup\Psi)\to V_{3}$ such that

$v(\varphi):=\begin{cases}\mathbf{1}&\text{ if }\varphi\in T\\\
\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}&\text{ if
}\varphi,\varphi\lor\psi_{\mathbf{1}}\in F\\\ \mathbf{0}&\text{ if }\varphi\in
F,\varphi\lor\psi_{\mathbf{1}}\in T\\\ \end{cases}$

    * –

if $v(\varphi\lor\psi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$, then
$\varphi\lor\psi,(\varphi\lor\psi)\lor\psi_{\mathbf{1}}\in F$. By
$(\mathsf{r}^{\lor,1}_{\textbf{{BK}}})$, either $\varphi\in F$ or $\psi\in F$.
In the first case, by $(\mathsf{r}^{\lor,6}_{\textbf{{BK}}})$, we have
$\varphi\lor\psi_{\mathbf{1}}\in F$ or $\psi\lor\psi_{\mathbf{1}}\in F$. The
former entails that $v(\varphi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$, while
the latter, by $(\mathsf{r}^{\lor,5}_{\textbf{{BK}}})$, gives that
$\psi\lor\psi\in F$, which, by rule $(\mathsf{r}^{\lor,1}_{\textbf{{BK}}})$,
gives $\psi\in F$, and thus $v(\psi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$.
In the second case, with $\psi\in F$, by rule
$(\mathsf{r}^{\lor,3}_{\textbf{{BK}}})$, $\varphi\lor\psi_{\mathbf{1}}\in F$.
As $\psi_{\mathbf{1}}\in T$, by rule $(\mathsf{r}^{\lor,2}_{\textbf{{BK}}})$
we have $\varphi\in F$, and then
$v(\varphi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$, as desired;

    * –

if $v(\varphi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$, then
$\varphi,\varphi\lor\psi_{\mathbf{1}}\in F$, and, by rule
$(\mathsf{r}^{\lor,9}_{\textbf{{BK}}})$, we have $\varphi\lor\psi\in F$;
hence, by rule $(\mathsf{r}^{\lor,7}_{\textbf{{BK}}})$, we obtain
$(\varphi\lor\psi)\lor\psi_{\mathbf{1}}\in F$, thus
$v(\varphi\lor\psi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$. The case
$v(\psi)=\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ is analogous, using rules
$(\mathsf{r}^{\lor,5}_{\textbf{{BK}}})$ and
$(\mathsf{r}^{\lor,8}_{\textbf{{BK}}})$ instead;

    * –

if $v(\varphi\lor\psi)=\mathbf{0}$, then $\varphi\lor\psi\in F$ and
$(\varphi\lor\psi)\lor\psi_{\mathbf{1}}\in T$. By
$(\mathsf{r}^{\lor,7}_{\textbf{{BK}}})$ and
$(\mathsf{r}^{\lor,8}_{\textbf{{BK}}})$, $\varphi\lor\psi_{\mathbf{1}}\in T$
and $\psi\lor\psi_{\mathbf{1}}\in T$ respectively. By
$(\mathsf{r}^{\lor,3}_{\textbf{{BK}}})$ and
$(\mathsf{r}^{\lor,4}_{\textbf{{BK}}})$, then, we have $v(\psi)=\mathbf{0}$
and $v(\varphi)=\mathbf{0}$, as desired;

    * –

if $v(\varphi)=\mathbf{0}$ and $v(\psi)=\mathbf{0}$, then $\varphi,\psi\in F$
and $\varphi\lor\psi_{\mathbf{1}},\psi\lor\psi_{\mathbf{1}}\in T$. By
$(\mathsf{r}^{\lor,1}_{\textbf{{BK}}})$, we have $\varphi\lor\psi\in F$, and,
by $(\mathsf{r}^{\lor,6}_{\textbf{{BK}}})$, we get
$(\varphi\lor\psi)\lor\psi_{\mathbf{1}}\in T$, entailing that
$v(\varphi\lor\psi)=\mathbf{0}$;

    * –

if $v(\varphi\lor\psi)=\mathbf{1}$, by $(\mathsf{r}^{\lor,9}_{\textbf{{BK}}})$
and $(\mathsf{r}^{\lor,5}_{\textbf{{BK}}})$, we have
$\varphi\lor\psi_{\mathbf{1}}\in F$ and $\psi\lor\psi_{\mathbf{1}}\in F$, thus
$v(\varphi)\neq\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ and
$v(\psi)\neq\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$. Then, by
$(\mathsf{r}^{\lor,1}_{\textbf{{BK}}})$, we have $\varphi\in T$ or $\psi\in
T$, and hence, in either case,
$v(\varphi\lor\psi)=v(\varphi)\lor_{\textbf{{BK}}}v(\psi)$;

    * –

if $v(\varphi)=\mathbf{1}$ and
$v(\psi)\neq\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$, we have $\varphi\in T$ and
either $\psi\in T$ or $\psi\lor\psi_{\mathbf{1}}\in F$. In the first case, by
$(\mathsf{r}^{\lor,2}_{\textbf{{BK}}})$, we get $\varphi\lor\psi\in T$, and,
in the second, by $(\mathsf{r}^{\lor,4}_{\textbf{{BK}}})$, we have also
$\varphi\lor\psi\in T$, and we are done. The case $v(\psi)=\mathbf{1}$ and
$v(\varphi)\neq\nicefrac{{\mathbf{1}}}{{\mathbf{2}}}$ is analogous.

∎

####  5.2.2 Implicative fragment of Łukaziewicz’s logic