# Syntax and Consequence Relation — A Categorical Perspective

Lingyuan Ye  Tsinghua University<EMAIL_ADDRESS>
##  1\. Introduction

On the proof-theoretic side, logic, roughly speaking, is mainly about the
grammar of the language (syntax), and reasoning on this language (consequence
relations). On the model-theoretic side, we further provides mathematical
structures that evaluates the language (semantic models).

Among these, syntax is perhaps the easiest part. What one usually does to
specify the syntax is to first fix a set of variables $X$, which almost always
is chosen to be a countably infinite set, and then define the set of well-
formed formulas $\mathrm{Fml}$ with variables being in $X$. Here in this paper
we will confine ourselves to only consider language of algebraic nature. This
means that our signature for the language would be algebraic, and the only
formula-forming rules would be application of function symbols. Syntax in
richer context with variable bindings could become much less trivial.111See
[7] for example for an extensive study of a very rich syntax theory in a
first-order setting.

The more interesting part of logic in our setting is how to reason with the
given language, and how we provide the semantics. For the proof-theoretic
side, the inferential structure on the specified language is formally
described by _consequence relation_. There are different forms of consequence
relations appearing in the literature, depending on your specific proof
systems, but almost all the examples can be generally viewed as some _binary
relations_ between the sets $\mathrm{Fml}$, $\mathbf{P}(\mathrm{Fml})$,
$\mathbf{P}(\mathrm{Fml}\times\mathrm{Fml})$, or possibly some other sets
constructed from the syntactical data. Here $\mathbf{P}(Y)$ denotes the power
set of $Y$. In every concrete scenario, a consequence relation is always
recursively generated from a set of inference rules, which means that they are
consequence relations that possess some _finitary_ nature.

Tarski is arguably one of the very first logicians to initiate the abstract
study of the structure of general consequence relations. In his paper [16] he
describes consequence relations in terms of _closure operators_ on a power set
of some set. In further developments of abstract consequence relations, and in
the majority of concrete logical systems, the consequence relations are
required to be _structural_ , i.e. they should be invariant under substitution
of variables. Structural consequence relations have been used by Blok and
Pigozzi in [2] to study the _algebraisation_ of logics; various refined
treatment and generalisations of this work has been provided by Block and
Jónsson [1], and by Galatos and Tsinakis [5]. They provides natural links from
the syntactic side to the semantic side.

For usual logics of algebraic signature, including propositional logics and
all kinds of modal logics, a semantic model can be viewed abstractly as a
structure that provides _valuation_ of syntactic data. A truth table or a
modal evaluation frame are structures that determine whether a propositional
or modal formula is _true_ or _false_ , or has value 1 or 0, or even not
necessarily 2-valued. The recursive nature of the the usual truth clauses when
defining such a valuation in particular shows furthermore that the valuation
function should _preserve tha algebraic structure_ of the syntax, i.e. they
should be an algebraic homomorphism with respect to the signature of the
syntax.

All of these aspects will be studied in this paper, but with a complete
reformulation and conceptual generalisation using the language of category
theory. The reasons we feel such an approach is needed are manyfold. Though
the study of modern logic has proven to be quite successful, the current
framework described above is somewhat frustrating in several aspects. This
starts from the very beginning of the way of describing the syntax. There are
no good criteria _a priori_ that determines the choice of the fixed set of
variables.222I should comment here that the truth of this sentence should be
conditional, depending on one’s perspective of what logic is. In more
philosophical or metamathematical contexts, especially when certain logic
systems are used to provide the foundation of mathematics, we cannot build the
logic system with very strong mathematical axioms. There the choice of the set
of variables, though not completely determined, are at least confined by our
epistemic and computational ability. Here is this paper we will never consider
such a foundational view point towards logic. What we will give is a
_mathematical study_ of logic, where the mathematics we use are possible
grounded by some other (meta)logical systems serving as the foundation. There
is indeed, I believe, a common feeling among experts that such a choice is not
particularly important, but there is no explicit explanation or systematic
formulation of why the obtained results are independent from such a choice.
Fixing a set of variables also requires extra work when we further develop the
formulation of consequence relations. The description of structurality, or
invariance under substitution of variables, is yet another level of complexity
we have to add into our framework. In [5] for example, where they provide a
more general framework of consequence relations, structurality is modelled
using the language of modules over a residuated lattices and invariance under
its actions. Furthermore, it seems to the author that in the literature there
lacks sufficient formulation of general principles in defining the semantics.

As indicated in the title, our approach towards logic, even in the basic level
of describing the syntax, is _categorical_ , or _functorial_ , which very
nicely fixes the fore mentioned drawbacks. We have two main conceptual
advantage in taking up this approach. On the pure syntactic level, a
functorial formuation fixes the fore mentioned drawbacks of a unnatural choice
of a fixed set of variables. Functoriality means that we are going to describe
the construction of syntax as a _functor_ $\mathbf{F}$ that outputs the set of
well-formed formulas $\mathbf{F}X$ as the underlying set of variables $X$
varies. This is a very natural move from the author’s perspective, since the
usual way of specifying the syntax of a logic very naturally gives us a
functor. This functorial approach towards the syntax is studied in Section 2.

The more important reason that we provide a functorial formulation of syntax
using $\mathbf{F}$ is that substitution of variables are automatically
described by the action of $\mathbf{F}$ on maps. This means that the functor
$\mathbf{F}$ describes the construction of syntactic data, as well as the
substitutional structure, within a single integrated package. We will then
apply it to further study abstract consequence relations, where structurality
is now built in, and general semantics. There we will state and show our other
general perspective towards logic: consequence relations and semantics are
general ways to construct _quotients_ of structures. The details will be more
specifically given in later section. As we will see, our approach provides a
very clean and conceptual understanding of the nature of logic (viewed as a
branch of mathematics), and extends and generalises various existing results,
concerning consequence relations and algebraisation, algebraic semantics,
etc., that already established in the literatures, as well as derives several
new ones.

This is the second draft of a longer text, which we will progressively release
new versions, including additions, revisions and updates. We assume the
readers to be familiar with basic categorical notions, including categories,
functors, natural transformations, adjunctions, limits and colimits, etc..

######  Notation.

To avoid notation clashes, in this paper we will use $\fatsemi$ to denote
function (morphisms) composition, and we will reserve the symbol $\circ$ for
the monoidal product on the category of endo-functors given by functor
composition. We will also often omit it if there’s no confusion. And unlike
the usual order for function composition, $f\fatsemi g$ will denote post-
compose $g$ with $f$, i.e. $f\fatsemi g=g\circ f$ in the usual notation for
function composition. For representable functors, we will use $\mathsf{y}^{X}$
to denote the Hom-functor $\mathbf{Set}(X,-)$ on $\mathbf{Set}$ (or any other
arbitrary category $\mathcal{C}$). In particular, we will use
$\mathsf{y}\cong\mathsf{y}^{1}$ to denote the identify endo-functor, with 1
denotes the singleton set. The functor category from $\mathcal{C}$ to
$\mathcal{D}$ will be denoted as $[\mathcal{C},\mathcal{D}]$. Given any binary
relation $R$ on a set $X$, we use $xRy$ to denote $(x,y)\in R$.

##  2\. Syntactic Monad

In this paper, we will mainly focus on logic over algebraic (propositional)
signatures. The syntax over such a signature is quite simple, since it does
not involve variable binding. The syntax of such logics can then be studied
from a universal algebra point of view, using the language of monads and
algebras of monads.

Let a signature $\Sigma$ be a set of connectives, together with a map
$\mathsf{ar}:\Sigma\to\omega$ assigning to each connective its arity. We
identify a connective $\star$ that has arity zero as a (propositional)
constant. For example, in the usual syntax of propositional logic both $\top$
and $\bot$ are propositional constants. The signature here may contain the
usual propositional connectives, including $\top,\bot,\wedge,\vee,\neg,\to$
and others, or modal operators $\operatorname{\triangledown}$ of arity larger
than zero as well. Hence, such a setting at least encompass all standard
(multi-)modal logics. For any set of variables $X$, the set of well-defined
formulas ($\Sigma$-terms) over $X$ are usually defined recursively as follows,

$\varphi:\equiv x\in X\mid\star(\varphi_{1},\cdots,\varphi_{n})$

where $\star$ ranges over connectives in $\Sigma$, and $n$ is the arity of
$\star$. We denote this set of well-formed formulas as $\mathbf{F}X$. If a
formula $\varphi$ can be constructed in the above sense, viz.
$\varphi\in\mathbf{F}X$, then it only contains variables in the set $X$.

The above description of syntax actually extends to an endo-functor on
$\mathbf{Set}$

$\mathbf{F}:\mathbf{Set}\to\mathbf{Set}.$

For any function $f:X\to Y$, we think of it as specifying variable
substitution, taking $x\in X$ into $f(x)\in Y$. The function $\mathbf{F}f$
then sends each formula $\varphi$ in $\mathbf{F}X$ into a formula in
$\mathbf{F}Y$, by _simultaneously substituting_ every $x\in X$ in $\varphi$
into $f(x)$. We will also write $\varphi^{f}$, the substitution of $\varphi$
along $f$, to denote $\mathbf{F}f(\varphi)$. For a subset $\Phi$ of
$\mathbf{F}X$, we write $\Phi^{f}$ to denote the set
$\operatorname{\\{}\varphi^{f}\mid\varphi\in\Phi\operatorname{\\}}$ as well.
The fact that the functor $\mathbf{F}$ acts on morphisms models substitution
is very important to our categorical approach of logic.

######  Remark 2.1.

Our functorial approach here subsumes the usual formulation of substitution in
the literature. Usually in other literatures, where we only describe the
syntax as a set $\mathrm{Fml}$ based on a fixed set of variables $X$,
substitution is modelled by action of a monoid $M$ on $\mathrm{Fml}$. From our
functorial perspective, the set of formulas $\mathrm{Fml}$ is simply the set
$\mathbf{F}X$ for the chosen variable set $X$. The monoid that describes
substitution is actually isomorphic to the monoid of endo-functions on $X$

$M\cong\mathbf{Set}(X,X).$

The monoid structure on $\mathbf{Set}(X,X)$ is given by composition of
functions. The functor $\mathbf{F}$ then describes the action of this monoid
on our set of formulas simply as follows: For any given
$\sigma\in\mathbf{Set}(X,X)$ and any $\varphi\in\mathbf{F}X$,

$\sigma\cdot\varphi=\mathbf{F}\sigma(\varphi)=\varphi^{\sigma}.$

The fact that $\mathbf{F}$ is a functor ensures this is a well-defined action
of a monoid

$\varphi^{\operatorname{id}_{X}}=\mathbf{F}\operatorname{id}_{X}(\varphi)=\operatorname{id}_{\mathbf{F}X}(\varphi)=\varphi,$
$\varphi^{\sigma\fatsemi\tau}=(\mathbf{F}\sigma\fatsemi\mathbf{F}\tau)(\varphi)=(\varphi^{\sigma})^{\tau}.$

Hence, the usual formulation of substitution on the syntactical level is
subsumed in our functorial description. ∎

The crucial observation is that $\mathbf{F}$ further has a monad structure
that, as we will show in Lemma 2.3 below, describes the $\Sigma$-term algebras
associated to the syntax. Such a result belongs to a much more general
connection between algebras and monads, a description of which can be found in
[8].333Be careful that in [8], the notion of algebraic theory is slightly
different than usual; it is formulated in the representation-invariant
categorical notion of theories, viz. Lawvere theories. See the reference there
for more information.

A monad on $\mathbf{Set}$ is a triple $(\mathbf{T},\eta,\mu)$, where
$\mathbf{T}$ is an endo-functor on $\mathbf{Set}$, and $\eta,\mu$ are natural
transformations of the following type,

$\eta:\mathsf{y}\to\mathbf{T},\quad\mu:\mathbf{T}\mathbf{T}\to\mathbf{T},$

Recall that we use $\mathsf{y}$ to denote the identity functor. They are
required to make the following diagrammes commute,

${\mathbf{T}}$${\mathbf{T}\mathbf{T}}$${\mathbf{T}}$${\mathbf{T}}$$\scriptstyle{\eta\circ\operatorname{id}_{\mathbf{T}}}$$\scriptstyle{\mu}$$\scriptstyle{\operatorname{id}_{\mathbf{T}}\circ\eta}$
${\mathbf{T}\mathbf{T}\mathbf{T}}$${\mathbf{T}\mathbf{T}}$${\mathbf{T}\mathbf{T}}$${\mathbf{T}}$$\scriptstyle{\mu\circ\operatorname{id}_{\mathbf{T}}}$$\scriptstyle{\operatorname{id}_{\mathbf{T}}\circ\mu}$$\scriptstyle{\mu}$$\scriptstyle{\mu}$

The left, right triangle and the square are called the left, right unit law
and associativity law, respectively. Equivalently, let
$([\mathbf{Set},\mathbf{Set}],\circ,\mathsf{y})$ be the monoidal category of
endo-functors on $\mathbf{Set}$ with the monoidal product given by functor
composition; then a monad on $\mathbf{Set}$ is precisely an _internal monoid_
in this monoidal category.444Given a monoidal category
$(\mathcal{C},\otimes,I)$, an internal monoid is an object $x$ equipped with
two maps $u:I\to x$, $m:x\otimes x\to x$, which are further required to
satisfy the usual unit and associativity laws expressed in equations between
composites of functions. In particular, an internal monoid in
$(\mathbf{Set},\times,1)$ is simply a monoid in the usual sense. See [13,
Section III.6] for a very brief account of internal groups, which are internal
monoid equipped with an additional inverse map; see [4] for a much more
detailed discussion of internal algebras in a category. The above diagrammes
precisely express that $\eta$ is a two-sided unit of $\mu$ and $\mu$ is
associative. We refer the readers to [13, Chapter VI] for a more detailed
description.

Explicitly, we have the following morphisms in $[\mathbf{Set},\mathbf{Set}]$

$\eta_{\mathbf{F}}:\mathsf{y}\to\mathbf{F},\
\mu_{\mathbf{F}}:\mathbf{F}\mathbf{F}\to\mathbf{F}.$

For any set $X$, we have the component of the unit

$\eta_{\mathbf{F},X}:X\to\mathbf{F}X.$

It is given by the inclusion $X\hookrightarrow\mathbf{F}(X)$, since in our
description of syntax we have defined that every variable (element) in $X$ is
a well-formed formula. To avoid confusion, when we want to consider $x\in X$
as a formula in $\mathbf{F}X$ we will always write $\eta_{\mathbf{F},X}(x)$
explicitly. We also have the component of multiplication

$\mu_{\mathbf{F},X}:\mathbf{F}\mathbf{F}X\to\mathbf{F}X.$

The elements in $\mathbf{F}\mathbf{F}X$ are formulas constructed from the set
of variables being the set of formulas $\mathbf{F}X$ over $X$, which can be
naturally viewed as formulas over $X$ itself. Formally, we can inductively
define $\mu_{\mathbf{F},X}$ as follows: Let $\varphi$ ranges over
$\mathbf{F}X$ and $\psi_{j}$ ranges over $\mathbf{F}\mathbf{F}X$, then we have

$\displaystyle\mu_{\mathbf{F},X}(\eta_{\mathbf{F},\mathbf{F}X}(\varphi))$
$\displaystyle:=\varphi,$
$\displaystyle\mu_{\mathbf{F},X}(\star_{i}(\psi_{1},\cdots,\psi_{n_{i}}))$
$\displaystyle:=\star(\mu_{\mathbf{F},X}(\psi_{1}),\cdots,\mu_{\mathbf{F},X}(\psi_{n})),$

for any $\star$ in $\Sigma$ of arity $n$. It is easy to check the naturality
for both $\eta_{\mathbf{F}}$ and $\mu_{\mathbf{F}}$.

######  Lemma 2.2.

$(\mathbf{F},\eta_{\mathbf{F}},\mu_{\mathbf{F}})$ is a monad.

When no confusion would arise, we usually use the functor part to denote the
whole monad structure. We call $\mathbf{F}$ the _syntactic monad_.

Monads have algebras. Given the monad $\mathbf{F}$, there is an induced
category of algebras $\mathbf{Set}^{\mathbf{F}}$ of $\mathbf{F}$, whose
objects are maps of the form $\alpha:\mathbf{F}X\to X$, where $X$ is called
the _carrier_ of $\alpha$, that further makes the following diagrammes
commute,

${X}$${\mathbf{F}X}$${X}$$\scriptstyle{\eta_{\mathbf{F},X}}$$\scriptstyle{\alpha}$
${\mathbf{F}\mathbf{F}X}$${\mathbf{F}X}$${\mathbf{F}X}$${X}$$\scriptstyle{\mathbf{F}\alpha}$$\scriptstyle{\mu_{\mathbf{F},X}}$$\scriptstyle{\alpha}$$\scriptstyle{\alpha}$

We will use $\alpha$, as well as its carrier $X$ when there no confusion would
arise, to denote an $\mathbf{F}$-algebra. A morphism between two algebras
$\alpha:\mathbf{F}X\to X$ and $\beta:\mathbf{F}Y\to Y$ is a function $f:X\to
Y$ that makes the following diagramme commute,

${\mathbf{F}X}$${\mathbf{F}Y}$${X}$${Y}$$\scriptstyle{\mathbf{F}f}$$\scriptstyle{\alpha}$$\scriptstyle{\beta}$$\scriptstyle{f}$

For example, for any set $X$ the multiplication
$\mu_{\mathbf{F},X}:\mathbf{F}\mathbf{F}X\to\mathbf{F}X$ is actually an
$\mathbf{F}$-algebra. It makes the corresponding diagrammes commute due to
unit and associative laws of monad. This extends to an adjunction

$\mathsf{F}:\mathbf{Set}\rightleftarrows\mathbf{Set}^{\mathbf{F}}:U_{\mathbf{F}},$

where $\mathbf{F}$ is the induced monad of this adjunction. $U_{\mathbf{F}}$
is the forgetful functor sending each $\mathbf{F}$-algebra to its carrier.
Such an adjunction in particular means that the $\mathbf{F}$-algebra structure
$\mu_{\mathbf{F},X}$ on $\mathbf{F}X$ is the _free $\mathbf{F}$-algebra_ on
$X$. Again, see [13, Chapter. VI] for a more detailed description of algebras
of a monad.

In the usual terminology of logic literatures, $\mathbf{F}$-algebras are
precisely the term algebras for the given signature $\Sigma$, as we will show
below. A $\Sigma$-algebra is a set $X$ equipped with operations
$\star^{X}:X^{n}\to X$, for any $\star\in\Sigma$ that $\mathsf{ar}(\star)=n$.
When $n=0$ we identify $X^{0}$ as a singleton set $1$. A $\Sigma$-algebra
morphism between two $\Sigma$-algebras is a map $f:X\to Y$ that preserves
these operations, i.e. for any $\star\in\Sigma$ we have

$f(\star^{X}(x_{1},\cdots,x_{n}))=\star^{Y}(f(x_{1}),\cdots,f(x_{n})).$

There is then an evident category of $\Sigma$-algebras, which we denote as
$\Sigma\text{-}\mathrm{Alg}$. The following result is a consequence of a much
more general correspondence between monads and algebraic theories.

######  Lemma 2.3.

The category $\mathbf{Set}^{\mathbf{F}}$ and $\Sigma\text{-}\mathrm{Alg}$ are
equivalent (isomorphic).

###### Proof Sketch.

We only describes how $\mathbf{F}$-algebras and $\Sigma$-algebras corresponds
bijectively to each other. Given a $\Sigma$-algebra $X$, we can easily
construct an $\mathbf{F}$-algebra

$\gamma:\mathbf{F}X\to X,$

by defining inductively as follows

$\displaystyle\gamma(\eta_{\mathbf{F},X}(x))$ $\displaystyle:=x,$
$\displaystyle\gamma(\star(\varphi_{1},\cdots,\varphi_{n}))$
$\displaystyle:=\star^{X}(\gamma(\varphi_{1}),\cdots,\gamma(\varphi_{n})),$

for any $\star\in\Sigma$. One can then prove inductively that

$\eta_{\mathbf{F},X}\fatsemi\gamma=\operatorname{id}_{X},\quad\mu_{\mathbf{F},X}\fatsemi\gamma=\mathbf{F}\gamma\fatsemi\gamma,$

which means $\gamma$ is in fact an $\mathbf{F}$-algebra.

On the other hand, given an $\mathbf{F}$-algebra $\alpha:\mathbf{F}X\to X$ we
associate it with a $\Sigma$-algebra structure. For any $\star\in\Sigma$ with
$\mathsf{ar}(\star)=n$, we can simply define

$\star^{X}_{\alpha}(x_{1},\cdots,x_{n}):=\alpha(\star(\eta_{\mathbf{F},X}(x_{1}),\cdots,\eta_{\mathbf{F},X}(x_{n}))).$

A further inductive proof shows that the above two processes are mutually
inverse of each other, and under this bijective correspondence the notions of
$\mathbf{F}$-algebra and $\Sigma$-algebra homomorphisms coincide. ∎

######  Remark 2.4.

Lemma 2.3 actually implies that $\mathbf{F}$ is a _free monad_ , by the fact
that there is another description of $\Sigma$-algebras using a polynomial
functor. A polynomial functor is defined to be a functor in
$[\mathbf{Set},\mathbf{Set}]$ which is naturally isomorphic to a coproduct of
representable functors. See [6] for an introduction. Let
$H:\mathbf{Set}\to\mathbf{Set}$ be the following functor

$H=\sum_{\star\in\Sigma}\mathsf{y}^{\mathsf{ar}(\star)}.$

where $\sum$ denotes the coproducts (disjoint unions). By definition $H$ is a
polynomial functor, and it sends every set $X$ to the set
$\sum_{\star\in\Sigma}X^{\mathsf{ar}(\star)}$. There is a similar notion of
algebras for an arbitrary endo-functor on $\mathbf{Set}$, not only just for
monads: An $H$-algebra is simply a set map $\gamma:HX\to X$ satisfying no
further conditions, and there is an evident notion of morphisms between
$H$-algebras. Hence, we have a category of $H$-algebras, which we denote as
$H\text{-}\mathrm{Alg}$. In this case, an $H$-algebra on $X$ is a function

$\sum_{\star\in\Sigma}X^{\mathsf{ar}(\star)}\to X,$

which is equivalent to give for every $\star\in\Sigma$ an operation $X^{n}\to
X$ where $n=\mathsf{ar}(\star)$. This means the notion of $\Sigma$-algebras is
the same as $H$-algebras, and we then have yet a further equivalence
(isomorphism)

$\mathbf{Set}^{\mathbf{F}}\cong H\text{-}\mathrm{Alg}.$

Such an equivalence in particular shows that $\mathbf{F}$ is the _free monad_
on the polynomial functor $H$, which implies that $\mathbf{F}$ itself is a
polynomial monad, i.e. the functor $\mathbf{F}$ is also a polynomial functor
such that the unit and multiplication of its monad structure are all
cartesian. See [12] for a detailed technical background on free monads and
related conceptions. We will come back to this point in later sections. Such
an observation makes it possible to further pursue a purely abstract
description of syntactic monads based on free monads over a polynomial
functor. We leave this for future works. ∎

We end this section by discussing finite products of $\mathbf{F}$. In later
sections, besides mere formulas, we will also be interested in pairs of
formulas, or more generally a sequent of some type. We can model these in our
categorical framework by taking products of $\mathbf{F}$ in
$[\mathbf{Set},\mathbf{Set}]$. Now limits and colimits in a functor category
like $[\mathbf{Set},\mathbf{Set}]$ are taken component-wise; see [3, Chapter.
2.15] on limits and colimits in a functor category. This in particular means
that for the product $\mathbf{F}^{n}$ in $[\mathbf{Set},\mathbf{Set}]$ and for
any set $X$, we have

$\mathbf{F}^{n}(X)=(\mathbf{F}X)^{n}.$

Now the action of $\mathbf{F}$ on functions is also component-wise. For a
tuple $(\varphi_{1},\cdots,\varphi_{n})\in\mathbf{F}^{n}X$, we have

$(\varphi_{1},\cdots,\varphi_{n})^{f}=\mathbf{F}^{n}f(\varphi_{1},\cdots,\varphi_{n})=(\mathbf{F}f\varphi_{1},\cdots,\mathbf{F}f\varphi_{n})=(\varphi_{1}^{f},\cdots,\varphi_{n}^{f}).$

This shows that $\mathbf{F}^{n}$ models point-wise substitution for tuples of
formulas, which is exactly what we want.

All the above results have shown us that the syntactic monad $\mathbf{F}$
indeed contains all the relevant information about the syntax: As far as the
single functor $\mathbf{F}$ goes, the set $\mathbf{F}X$ gives out the set of
well-formed formulas constructed from the variable set $X$ for the given
signature $\Sigma$, and the functor $\mathbf{F}$ acting on set maps $f:X\to Y$
models uniform substitution. This also works nicely if we consider products of
$\mathbf{F}$. The monad structure on $\mathbf{F}$ further contains all the
information about $\Sigma$-algebras. Lemma 2.3, together with the free
$\mathbf{F}$-algebra functor $\mathsf{F}$, establishes the familiar fact that
$\mathbf{F}X$ is the free $\Sigma$-algebra on the generating set $X$.

##  3\. Abstract Consequence Relations

The syntactic monad $\mathbf{F}$ describes, by its name, the syntax of our
logic, which is only establishing the ground work for the more important part
of logic, viz. inferential and reasoning structures and semantic relations. In
this section, we will focus on the proof-theoretic side of the story.

Reasoning in logic is usually represented abstractly in the form of
consequence relations. From a non-categorical setting, with a fixed set of
variables $X$ and hence a fixed set of formulas $\mathrm{Fml}$, a consequence
relation can be defined on various sets constructed from $\mathrm{Fml}$,
depending on the style of the inference system. An _asymmetric_ consequence
relation is usually considered as a binary relation
$\operatorname{\vdash}\subseteq\mathbf{P}\mathrm{Fml}\times\mathrm{Fml}$. A
_symmetric_ consequence relation is a binary relation
$\operatorname{\vdash}\subseteq\mathbf{P}\mathrm{Fml}\times\mathbf{P}\mathrm{Fml}$.
It is well known that asymmetric and symmetric consequence relations are
equivalent, and hence we will only consider symmetric ones in the remainder.
Consequence relations on other sets are also studied. To provide an algebraic
perspective towards logics and study their algebraisations we also want to
consider consequence relations defined on pairs of formulas
$\mathrm{Eq}=\mathrm{Fml}\times\mathrm{Fml}$, viz.
$\operatorname{\vdash}\subseteq\mathbf{P}\mathrm{Eq}\times\mathbf{P}\mathrm{Eq}$.
More generally, we may consider consequence relations defined on sequents. A
sequent of type $(n,m)$ with $n,m\in\omega$ is usually denoted as

$\varphi_{1},\cdots,\varphi_{n}\Mapsto\psi_{1},\cdots,\psi_{m}.$

In particular, a formula can be identified with a $(0,1)$-sequent, and a pair
of formulas can be identified as a $(1,1)$-sequent. The set of all
$(m,n)$-sequents $\mathrm{Seq}_{n,m}$ is simply given by
$\mathrm{Fml}^{n}\times\mathrm{Fml}^{m}\cong\mathrm{Fml}^{n+m}$. Hence
basically, we want to consider consequence relations defined on finite
products of $\mathrm{Fml}$ in general.

In [5], Galatos and Tsinakis have generalised consequence relations to
arbitrary complete lattices, which leads to a very nice mathematical theory of
consequence relations. In this section we will follow such a spirit to give a
mathematically rigorous theory of consequence relations, but with several
changes of perspective.

Firstly, a categorical mind set has taught us that in most of the mathematical
context we should put objects, as well as corresponding _maps between objects_
, into consideration. From our point of view, the theory of abstract
consequence relations is much more naturally related to _suplattices_ , rather
than complete lattices. A suplattice by definition is a complete join-semi
lattice, viz. a poset that has arbitrary joins. It is well-known that every
suplattice is automatically complete, hence object-wise complete lattices and
suplattices are the same thing.555A proof can be found in [10, p. 27].
However, a morphism between suplattices is only required to preserves
arbitrary joins, rather than all meets and all joins. This makes
$\mathbf{SupL}$, the category of suplattices, have very different categorical
property than $\mathbf{CompL}$, the category of complete lattices.666One way
to see their difference is that suplattices are _algebraic_ over
$\mathbf{Set}$. In later sections we will describe that $\mathbf{SupL}$ is
equivalent to the category of $\mathbf{P}$-algebras, where $\mathbf{P}$ is the
covariant power set monad. In particular, this implies that all free-
suplattice-constructions exists in $\mathbf{Set}$, due to the free suplattice
functor $\mathsf{P}$ induced by $\mathbf{P}$. However, complete lattices are
_not_ algebraic over $\mathbf{Set}$. The free complete lattices on $n>2$
generators does not exists (or must form a proper class); see [10, p. 31] for
a proof.

Using the language of suplattices, we can see much more clearly that
consequence relations in logic are natural ways to construct _quotients_ , as
we’ve mentioned briefly in Section 1. Furthermore, the category
$\mathbf{SupL}$ is very closely connected to the covariant power functor
$\mathbf{P}$. As we will show later, there is a monad structure on
$\mathbf{P}$, and the category $\mathbf{Set}^{\mathbf{P}}$ of
$\mathbf{P}$-algebras is the same as suplattices. This naturally establishes
sets including $\mathbf{P}\mathrm{Fml},\mathbf{P}\mathrm{Eq}$, or more
generally $\mathbf{P}\mathrm{Seq}_{n,m}$, where consequence relations are
usually built on, as typical examples of free suplattices. We will see more of
such connections in the future part of this section.

Secondly, continuing to follow the philosophy of the previous section, we want
the description of substitution and structurality of consequence relations to
be directly built within our framework. In [5], besides using complete
lattices to define abstract consequence relations, it further describes
substitution as some module structures — complete lattices with an action of a
residuated lattice modelling substitution — which is another level of
complexity we prefer not to have. In the following texts, we will again
directly adopt a functorial approach to express structurality. These
considerations have led to the following formulation.

We first give a brief introduction to suplattices, in particular morphisms
between suplattices. By the adjoint functor theorem, a monotone map
$f^{*}:P\to Q$ between two suplattice is a suplattice morphism, i.e. it
preserves arbitrary joins, if and only if there is another monotone map
$f_{*}:Q\to P$ such that $f^{*}$ is left adjoint to $f_{*}$

$f^{*}:P\rightleftarrows Q:f_{*};$

it means for any $x\in P,y\in Q$ we have

$f^{*}(x)\leq y\Leftrightarrow x\leq f_{*}(y).$

When $f^{*}$ is a suplattice morphism, $f_{*}$ can be explicitly described by
the following formula

$f_{*}(y)=\bigvee\operatorname{\\{}x\in P\mid f^{*}(x)\leq
y\operatorname{\\}}.$

Similarly, we can express the left adjoint using the right adjoint

$f^{*}(x)=\bigwedge\operatorname{\\{}y\in Q\mid f_{*}(y)\geq
x\operatorname{\\}}.$

We leave for the readers to check that $f^{*},f_{*}$ indeed form an adjunction
in both cases. This means that to show a monotone function is a suplattice
morphism, it suffices to find a right adjoint. The right adjoint $f_{*}$ in
general will _not_ be a suplattice morphism; it preserves arbitrary meets but
not joins by general category theory. However, when $f^{*}$ is an isomorphism,
$f_{*}$ will simply be the inverse of $f^{*}$ and both $f^{*}$ and $f_{*}$
will preserve arbitrary joins and meets.

Notice that for a left adjoint $f^{*}$, it is injective if and only if it is
an order embedding, viz. $x\leq y\Leftrightarrow f^{*}(x)\leq f^{*}(y)$. The
same holds for a right adjoint. The following lemma shows that the right and
left adjoint are closely connected.

######  Lemma 3.1.

Given a morphism between suplattices $f^{*}:P\to Q$, it is surjective (resp.
injective) if and only its right adjoint $f_{*}$ is injective (resp.
surjective).

###### Proof.

We only show $f^{*}$ being surjective (resp. injective) implies $f_{*}$ being
injective (resp. surjective). The other way around is similar and we leave for
the readers to check.

Suppose $f^{*}$ is surjective, since for any $y\in Q$ there exists some $x$
that $f^{*}(x)=y$, it follows that

$f_{*}(y)=\bigvee\operatorname{\\{}x\in P\mid f^{*}(x)\leq
y\operatorname{\\}}=\bigvee_{f^{*}(x)=y}x.$

We then further have

$f^{*}f_{*}(y)=\bigvee_{f^{*}(x)=y}f^{*}(x)=y.$

This means $f_{*}$ must be injective. On the other hand, suppose $f^{*}$ is
injective. For any $x,y\in P$, $x\leq y\Leftrightarrow f^{*}(x)\leq f^{*}(y)$.
By the adjunction this further implies that

$y\leq f_{*}f^{*}(x)\Leftrightarrow f^{*}(y)\leq f^{*}(x)\Leftrightarrow y\leq
x.$

Hence, $f_{*}f^{*}(x)=x$, which shows that $f_{*}$ must be surjective. ∎

We refer the readers to [11, Chapter. I] for a more complete formulation of
the categorical properties of the category $\mathbf{SupL}$.

To work our step up to a fully functorial approach of abstract consequence
relations, we first reformulate some of the results presented in [5] using
suplattices. As we will show below, Lemma 3.2 is a strong evidence that
considering suplattices is far more natural than considering complete
lattices, and it gives us a first instance of our general philosophy that
consequence relations are general ways to construct _quotients_ of structures.

The following definition of consequence relation on a single suplattice is
adapted from [5]. We define an abstract consequence relation on a suplattice
$P$ to be a _preorder_ $\operatorname{\vdash}$ on $P$, such that
$\operatorname{\vdash}\supseteq\operatorname{\geq}$, and for any $x\in P$

$x\operatorname{\vdash}\bigvee\operatorname{\\{}y\in P\mid x\vdash
y\operatorname{\\}}.$

We say _$x$ implies $y$_ if $x\operatorname{\vdash}y$ in $P$.

Another useful notion is that of a _closure operator_ , which corresponds to
Tarski’s original approach to abstract consequence relations in [16]. A
closure operator $j$ on a suplattice $P$ is a _monotone_ function $j:P\to P$
which is _extensive_ , viz. $j(x)\geq x$ for any $x$, and _idempotent_ , viz.
$jj(x)=j(x)$ for any $x$.

Finally, we present what we mean by a _quotient_ of a suplattice. A quotient
of $P$ is a surjective suplattice homomorphism $e^{*}:P\twoheadrightarrow Q$,
considered _up to isomorphism_. In other words, a quotient strictly speaking
is an equivalence class of surjections out of $P$ in the category
$\mathbf{SupL}$. Two surjections $e^{*}_{1}:P\twoheadrightarrow
Q_{1},e^{*}_{2}:P\twoheadrightarrow Q_{2}$ are considered equivalent if and
only if there is an isomorphism $Q_{1}\cong Q_{2}$ between suplattices making
the following diagramme commute,

${P}$${Q_{1}}$${Q_{2}}$$\scriptstyle{e_{2}^{*}}$$\scriptstyle{e_{1}^{*}}$$\scriptstyle{\cong}$

In the remaining texts we will loosely speak of a surjection as a quotient,
but silently assuming any two isomorphic surjections in the above sense
represent the same quotient.

From our knowledge the following lemma, which states that consequence
relations and closure operators on a suplattice are the same as quotients, is
at least folklore, if not well-known. The piece that consequence relations and
closure operators on a suplattice corresponds bijectively is implicit in [5].
The fact that closure operators and quotients are the same is perhaps known to
the experts for a much longer period — a proof can be found in [11, Section
I.4]; a similar result for frames, left exact versions of suplattices, is also
established in [10, Section II.2]. For the convenience of the readers we
collect the pieces together and prove the following lemma.

######  Lemma 3.2.

Consequence relations, closure operators, and quotients of a suplattice
bijectively correspond to each other.

###### Proof.

(1): We first show that consequence relations and closure operators on $P$ are
bijectively correspondent. Given a closure operator $j$, we define
$\operatorname{\vdash}_{j}$ to be

$x\operatorname{\vdash}_{j}y\Leftrightarrow y\leq j(x).$

It is a preorder:

$x\leq j(x)\Rightarrow x\operatorname{\vdash}_{j}x;$
$x\operatorname{\vdash}_{j}y,y\operatorname{\vdash}_{j}z\Rightarrow z\leq
j(y)\leq jj(x)=j(x)\Rightarrow x\operatorname{\vdash}_{j}z.$

It contains $\geq$:

$y\leq x\Rightarrow y\leq x\leq j(x)\Rightarrow x\operatorname{\vdash}_{j}y.$

We also have

$x\operatorname{\vdash}_{j}\bigvee_{x\operatorname{\vdash}_{j}y}y\Leftrightarrow\bigvee_{x\operatorname{\vdash}_{j}y}y\leq
j(x)\Leftrightarrow(x\operatorname{\vdash}_{j}y\Rightarrow y\leq j(x)),$

Hence, $\operatorname{\vdash}_{j}$ is a well-defined consequence relation. On
the other hand, given a consequence relation $\operatorname{\vdash}$, we
define a closure operator $\gamma$ to be the following,

$\gamma(x)=\bigvee_{x\operatorname{\vdash}y}y.$

It is obviously increasing because $\operatorname{\vdash}$ is reflexive. For
monotonicity, suppose $x\leq z$ and thus $z\operatorname{\vdash}x$. Given any
$y$ that $x\operatorname{\vdash}y$, by transitivity we have
$z\operatorname{\vdash}y$ as well, which implies

$\gamma(x)=\bigvee_{x\operatorname{\vdash}y}y\leq\bigvee_{z\operatorname{\vdash}w}w=\gamma(z).$

Finally, to prove idempotence of $\gamma$ we show that

$x\operatorname{\vdash}z\Leftrightarrow\gamma(x)\operatorname{\vdash}z.$

The left to right direction is trivial, since $\gamma(x)\geq x$ thus
$\gamma(x)\operatorname{\vdash}x$. For the other direction we only need to
observe that by definition $x\operatorname{\vdash}\gamma(x)$. Thus, we have

$\gamma(\gamma(x))=\bigvee_{\gamma(x)\operatorname{\vdash}y}y=\bigvee_{x\operatorname{\vdash}y}y=\gamma(x).$

Hence, $\gamma$ is a closure operator. Finally, it is easy to see that these
operations are inverse to each other, since we have

$x\operatorname{\vdash}_{\gamma}z\Leftrightarrow
z\leq\bigvee_{x\operatorname{\vdash}y}y\Leftrightarrow
x\operatorname{\vdash}z,$

and also

$\gamma_{j}(x)=\bigvee_{x\operatorname{\vdash}_{j}y}y=\bigvee_{y\leq
j(x)}y=j(x).$

(2): Next, we show that quotients of suplattices are in bijective
correspondence to closure operators on $P$. Given a quotient

$e^{*}:P\twoheadrightarrow Q,$

we define $e:P\to P$ to be the following map

$e(x)=e_{*}e^{*}(x).$

From Lemma 3.1 we know that for any $y\in Q$

$e^{*}e_{*}(y)=y.$

This in particular implies that $e$ is a closure operator. On the other hand,
given a closure operator, we defined a quotient

$j^{*}:P\twoheadrightarrow P_{j},$

where $P_{j}$ is the set of fixed-points of $j$, or equivalently the image of
$P$ under $j$, and

$j^{*}(x)=j(x).$

By definition, $j^{*}$ is surjective. The right adjoint $j_{*}$ can simply
taken to be the inclusion

$j_{*}:P_{j}\hookrightarrow P.$

They are indeed adjoint because for any $y\in P_{j}$, $j(x)\leq y$ implies
$x\leq y$, and $x\leq y$ implies $j(x)\leq j(y)=y$, thus a closure operator
indeed gives us a quotient. We show that these two operations are inverse to
each other. It is obvious that the closure operator induced by the quotient
$j^{*}$ is simply $j$. It remains to show that given a quotient
$e^{*}:P\twoheadrightarrow Q$, we must have $Q\cong P_{e}$. Observe the right
adjoint $e_{*}:Q\to P$ actually restricts to a map

$e_{*}:Q\to P_{e}.$

This is because for any $q\in Q$

$ee_{*}(q)=e_{*}e^{*}e_{*}(q)=e_{*}(q).$

This restricted morphism is surjective, because for any $x\in P_{e}$ we have

$x=e^{*}e_{*}(x).$

By Lemma 3.1 we also know $e_{*}$ is injective. $e_{*}:Q\to P$ is a right
adjoint thus preserves meets; meets in $P_{e}$ are calculated the same as in
$P$; hence the restricted map $e_{*}:Q\to P_{e}$ is indeed an isomorphism
between posets, which in particular shows that $Q$ is isomorphic to $P_{e}$ as
a suplattice. ∎

In the light of the above correspondence, given a quotient
$j^{*}:P\twoheadrightarrow P_{j}$ that corresponds to the closure operator $j$
and consequence relation $\operatorname{\vdash}$ on $P$, we call elements in
$P_{j}$ as _closed theories_ , or simply say it is _closed_ , and also call
the quotient suplattice $P_{j}$ _the lattice of closed theories_. For any
$x\in P$, its _closure_ is given by $j(x)=\bigvee_{x\operatorname{\vdash}y}y$,
and every element implies its closure. This in particular shows that

$w\in P\text{ is closed }\text{ iff }\forall y\in P,\
w\operatorname{\vdash}y\Rightarrow y\leq w.$

In the below adjunction

$j^{*}:P\rightleftarrows P_{j}:j_{*},$

$j^{*}$ is surjective and $j_{*}$ is an inclusion between posets. Since
$j^{*}$ is a left adjoint thus preserves joins, it follows that joins in
$P_{j}$ are computed as the closure of joins in $P$. Since $j_{*}$ is a poset-
embedding and preserves arbitrary meets, $P_{j}$ must then be closed under
arbitrary meets in $P$, and meets in $P_{j}$ are computed exactly the same as
in $P$.

######  Example 3.3.

Let’s apply the above very useful lemma to a concrete example where we
describe the image-factorisation of suplattices. As we will see later, the
category $\mathbf{SupL}$ is _algebraic_ over $\mathbf{Set}$, i.e. there is a
monad such that $\mathbf{SupL}$ is the category of algebras of this monad. In
particular, this implies that we have image-factorisation in $\mathbf{SupL}$.
We only need to observe that the construction of a closure operator induced by
a surjection in the previous proof actually extends to arbitrary suplattice
morphisms.

Given any suplattice morphism

$e^{*}:P\to Q,$

the map $x\mapsto e_{*}e^{*}(x)$ is indeed a closure operator. It is obviously
monotone. $x\leq e_{*}e^{*}(x)$ simply because $e_{*}$ is right adjoint to
$e^{*}$ and $e^{*}(x)\leq e^{*}(x)$. It is idempotent by noticing the
following computation:

$\displaystyle e^{*}e_{*}e^{*}(x)$
$\displaystyle=e^{*}\left(\bigvee\operatorname{\\{}y\in P\mid e^{*}(y)\leq
e^{*}(x)\operatorname{\\}}\right)$
$\displaystyle=\bigvee\operatorname{\\{}e^{*}(y)\mid e^{*}(y)\leq
e^{*}(x)\operatorname{\\}}$ $\displaystyle=e^{*}(x)$

Let us denote this closure operator by $\epsilon$. We then have a
factorisation of $e$ as follows,

${P}$${Q}$${P_{\epsilon}}$$\scriptstyle{e^{*}}$$\scriptstyle{\epsilon^{*}}$$\scriptstyle{e^{*}_{\epsilon}}$

The map $e^{*}_{\epsilon}$ sends any $x\in P_{\epsilon}$ to $e^{*}(x)$; in
other words, it is the map $e^{*}$ restricted to $P_{\epsilon}$. The above
diagramme indeed commutes

$e_{\epsilon}^{*}\epsilon^{*}(x)=e^{*}e_{*}e^{*}(x)=e^{*}(x).$

The right adjoint of $e^{*}_{\epsilon}$ is given by
$y\mapsto\epsilon^{*}e_{*}(y)=e_{*}e^{*}e_{*}(y)$, and we have

$x\leq e_{*}e^{*}e_{*}(y)\Leftrightarrow e^{*}(x)\leq e^{*}e_{*}(y).$

By the adjunction we know that $e^{*}e_{*}(y)\leq y$, hence $x\leq
e_{*}e^{*}e_{*}(y)\Rightarrow e_{\epsilon}^{*}(x)\leq y$. On the other hand,
suppose $e^{*}(x)\leq y$ for $x\in P_{\epsilon},y\in Q$. We further note

$\displaystyle e^{*}(x)=e^{*}e_{*}e^{*}(x)\leq y$ $\displaystyle\Rightarrow
e_{*}e^{*}(x)\leq e_{*}(y)$ $\displaystyle\Rightarrow
e^{*}e_{*}e^{*}(x)=e^{*}(x)\leq e^{*}e_{*}(y)$ $\displaystyle\Rightarrow x\leq
e_{*}e^{*}e_{*}(y).$

This proves that $y\mapsto e_{*}e^{*}e_{*}(y)$ is indeed the right adjoint of
$e_{\epsilon}^{*}$. Hence, the above is indeed a commuting diagramme in
$\mathbf{SupL}$. Finally, to show the above diagramme consists of the image-
factorisation of $e^{*}$ we only need to observe that $e^{*}_{\epsilon}$ is
injective. For any $x\in P_{\epsilon}$ we know that

$e_{*}e^{*}(x)=x.$

This in particular shows that $e^{*}_{\epsilon}$, which is $e^{*}$ restricted
to $P_{\epsilon}$, must be injective. Thus, $P_{\epsilon}$ is indeed the image
of $e^{*}$, and the above diagramme depicts the image-factorisation. ∎

The above is the whole story of how consequence relations relates to closure
operators and quotients of suplattices. To further study _structural_
consequence relations, viz. consequence relations that are invariant under
substitution, it is not sufficient to study an isolated suplattice. Inspired
by how we have given a functorial treatment of syntax with built in
substitutional structure, we extend our framework to further study consequence
relations based on a pure functorial setting. Explicitly, we now consider
functors of the form

$\mathcal{A}:\mathbf{Set}\to\mathbf{SupL}.$

For any set map $f:X\to Y$, $\mathcal{A}$ induces a suplattice morphism

$\mathcal{A}f:\mathcal{A}X\to\mathcal{A}Y.$

This functorial dependence are used to model the abstract _point-wise
substitution_ , as we will see more clearly later when we discuss concrete
examples.

Let us first observe one very important functor of this type. As mentioned
before, suplattices actually have a very close connection with the covariant
power set functor $\mathbf{P}$.777The power set construction can be extended
to a functor in both covariant and contravariant ways. The former is an endo-
functor on $\mathbf{Set}$, while the latter is a functor from
$\mathbf{Set}^{\operatorname{op}}$ to $\mathbf{Set}$. In this paper we will
exclusively consider the covariant case. This naturally relates to our
functorial approach to the usual examples of consequence relations in concrete
logical systems, since as we’ve already seen the usual consequence relations
are almost always defined on the power set of some sets related to the set of
formulas.

The power set functor $\mathbf{P}$ sends each set $X$ to its power set
$\mathbf{P}X$, and every function $f:X\to Y$ to a function
$\mathbf{P}f:\mathbf{P}X\to\mathbf{P}Y$, which takes each subset $S$ of $X$ to
the image $f(S)$ in $Y$. The crucial point is that $\mathbf{P}$ also has a
monad structure $(\mathbf{P},\eta_{\mathbf{P}},\mu_{\mathbf{P}})$. For any set
$X$, the unit $\eta_{\mathbf{P},X}$ sends $x$ to the singleton set $\\{x\\}$;
the multiplication $\mu_{\mathbf{P},X}$ sends a set of subsets of $X$ to their
union. Just as Lemma 2.3 shows for the syntactic monad $\mathbf{F}$ that
$\mathbf{F}$-algebras are the same as $\Sigma$-algebras, it is well-known that
$\mathbf{P}$-algebras are exactly _suplattices_ , i.e. we have an equivalence
— isomorphism, actually — of categories

$\mathbf{SupL}\cong\mathbf{Set}^{\mathbf{P}}.$

By the general theory of monads, this in particular shows that there is an
induced adjunction

$\mathsf{P}:\mathbf{Set}\rightleftarrows\mathbf{SupL}:U_{\mathbf{P}}.$

For each set $X$, $\mathsf{P}X$ gives the free suplattice on $X$, which is the
usual suplattice structure on the carrier set $\mathbf{P}X$ with inclusion
being the partial order. In other words, the power set $\mathbf{P}X$ as a
suplattice is free on the generating set $X$. This free suplattice functor
$\mathsf{P}$ is then a typical example of a functor from $\mathbf{Set}$ to
$\mathbf{SupL}$, and it is the free one. This makes it very convenient for us
to describe consequence relations on concrete formulas in our functorial
approach — another reason to work with suplattices, rather than complete
lattices.

Given any such functor $\mathcal{A}:\mathbf{Set}\to\mathbf{SupL}$, we also use
$A$ to denote the composition with the forgetful functor from $\mathbf{SupL}$
to $\mathbf{Set}$,

$A=\mathcal{A}\fatsemi U_{\mathbf{P}}:\mathbf{Set}\to\mathbf{Set}$

For any set $X$, $AX$ considered as a set then has a unique
$\mathbf{P}$-algebra structure induced by $\mathcal{A}$; hence we will also
loosely view $AX$ as a suplattice when needed so. For any set map $f:X\to Y$,
the induced map $Af$ is then a $\mathbf{P}$-algebra morphism, which means it
preserves arbitrary joins in $AX$. We use $f^{*}(x)$ to denote $Af(x)$ for any
$x\in AX$ when there is no confusion; of course, in that case $f_{*}$ will
denote its right adjoint.

All such functors form a category $[\mathbf{Set},\mathbf{SupL}]$. A morphism
in $[\mathbf{Set},\mathbf{SupL}]$ between two such functors would then a
natural transformation

$q:\mathcal{A}\to\mathcal{B}.$

This explicitly means that for any set $X$, $q_{X}$ is a morphism between
suplattices; and for any set map $f:X\to Y$ the following naturality diagramme
commutes

${\mathcal{A}X}$${\mathcal{B}X}$${\mathcal{A}Y}$${\mathcal{B}Y}$$\scriptstyle{q_{X}}$$\scriptstyle{\mathcal{A}f}$$\scriptstyle{\mathcal{B}f}$$\scriptstyle{q_{Y}}$

On the level of their underlying sets, we also write

$q_{X}^{*}:AX\rightleftarrows BX:q_{X,*},$

such that $q_{X}^{*}$ basically denotes the underlying function of $q_{X}$,
and $q_{X,*}$ is the right adjoint of $q_{X}^{*}$.

One thing to notice is that for any such functor $\mathcal{A}$, $A$ would be
an _internal poset_ in $[\mathbf{Set},\mathbf{Set}]$. For any category
$\mathcal{C}$, an internal binary relation $R$ on some object $C$ in
$\mathcal{C}$ is simply a subobject $R\hookrightarrow C\times C$. There are
also definitions for an internal binary relation to be reflexive, symmetric,
asymmetric, transitive, etc.. For our purposes though, it is enough to note
that in a functor category like $[\mathbf{Set},\mathbf{Set}]$, an internal
binary relation is reflexive, symmetric, asymmetric, or transitive, if and
only it is so component-wise. In particular, a binary relation
$R\hookrightarrow C\times C$ in $[\mathbf{Set},\mathbf{Set}]$ is a preorder
(resp. partial order) if and only if for any set $X$, $RX$ is a preorder
(resp. partial order) on $CX$.

Now given a functor $\mathcal{A}:\mathbf{Set}\to\mathbf{SupL}$, the induced
functor $A$ is indeed an internal poset in $[\mathbf{Set},\mathbf{Set}]$. We
have a following binary relation

$\operatorname{\preceq}\hookrightarrow A\times A,$

where for each set $X$

$\preceq_{X}=\operatorname{\\{}(x,y)\mid x\leq y\text{ in
}\mathcal{A}X\operatorname{\\}}.$

It is indeed a subfunctor of $A\times A$, because for any set map $f:X\to Y$,
$Af$ is a map between suplattices, hence in particular monotone, which means
that

$x\leq y\Rightarrow f^{*}(x)\leq f^{*}(y).$

Evidently, $\preceq$ is an internal partial order in
$[\mathbf{Set},\mathbf{Set}]$. We also use $\succeq$ to denote its dual order;
explicitly, for any set $X$ we have

$\succeq_{X}=\operatorname{\\{}(x,y)\mid x\geq y\text{ in
}\mathcal{A}X\operatorname{\\}}.$

To further address the point that for a functor
$\mathcal{A}:\mathbf{Set}\to\mathbf{SupL}$ the induced suplattice morphisms
$\mathcal{A}f$ should be understood as abstract point-wise substitution, we
look at the free suplattice functor associated to the power set monad for
example. We show how the functor $\mathsf{P}$ models the more complicated
substitution on the level of power set of the set of formulas.

Consider the following composite functor

$\mathsf{P}\mathbf{F}:\mathbf{Set}\to\mathbf{SupL}.$

It takes a set $X$ to the suplattice $\mathsf{P}\mathbf{F}X$ of the power set
of the set of formulas $\mathbf{F}X$. Given any set map $f:X\to Y$ considered
as specifying the way of substituting variables, there is an induced
adjunction

$f^{*}:\mathbf{P}\mathbf{F}X\rightleftarrows\mathbf{P}\mathbf{F}Y:f_{*}.$

By definition, for any $\Phi\subseteq\mathbf{F}X$ we have

$f^{*}(\Phi)=\mathbf{P}\mathbf{F}f(\Phi)=\operatorname{\\{}\varphi^{f}\mid\varphi\in\Phi\operatorname{\\}}=\Phi^{f}.$

This means that $\mathsf{P}\mathbf{F}$ acting on a set map $f$ models point-
wise substitution, which is exactly what we intend it to be. And simply from
definition, such an operation preserves unions. Also, the left adjoint models
inverse substitution: For any $\Psi\subseteq\mathbf{F}Y$, by the description
of right adjoint we have stated before,

$f_{*}(\Psi)=\operatorname{\\{}\Phi\subseteq\mathbf{F}X\mid\Phi^{f}\subseteq\Psi\operatorname{\\}}.$

Of course, the functor $\mathsf{P}$ itself is also another functor from
$\mathbf{Set}$ to $\mathbf{SupL}$. We can view it as modelling the point-wise
substitution when we have a _trivial_ language, i.e. there are no logic
connectives in the language at all. The syntactic monad in this case is then
simply given by the identity functor on $\mathbf{Set}$. The functor
$\mathsf{P}$ then models point-wise substitution on the power set of formulas
of this trivial language.

Our main goal in this section is to prove a similar result of Lemma 3.2,
showing that in the functorial setting the quotients are again in bijective
correspondence to consequence relations, which lifts our general philosophy of
viewing logics as a general way of constructing quotients to this functorial
setting. To show this we first describes what quotients and structural
consequence relations are in this new context.

A quotient of $\mathcal{A}$ should be understood as a surjection in the
category $[\mathbf{Set},\mathbf{SupL}]$, but again only considered up to
isomorphism. Since limits and colimits are computed component-wise in a
functor category, a surjection is then a natural transformation

$q:\mathcal{A}\twoheadrightarrow\mathcal{B},$

such that for every set $X$ the component
$q_{X}:\mathcal{A}X\twoheadrightarrow\mathcal{B}X$ is a surjection of
suplattices. In other words, $q$ is a quotient in the functor category
$[\mathbf{Set},\mathbf{SupL}]$ if and only if it is so for every component.
Similar results holds for injections as well.

In the same spirit, we would also want to define what consequence relations
are in this functorial setting in a component-wise manner. A structural
consequence relation $\operatorname{\vdash}$ on $\mathcal{A}$ is a subfunctor
on $A\times A$

$\operatorname{\vdash}\hookrightarrow A\times A,$

such that, point-wise, $\operatorname{\vdash}_{X}$ is a consequence relation
on the suplattice $AX$ for any set $X$. In particular, this implies that
$\operatorname{\vdash}$ is an _internal preorder_ on $A$ that contains
$\succeq$,

${\succeq}$${\operatorname{\vdash}}$${A\times A}$

But a structural consequence relation $\operatorname{\vdash}$ in this
functoriality setting contains more information than the mere point-wise
consequence relations $\operatorname{\vdash}_{X}$. Functoriality of
$\operatorname{\vdash}$ further implies _structurality_ , i.e. these point-
wise consequence relations are invariant under substitutions. Previously we
have shown that the functor $\mathcal{A}$, or similarly $A$, acting on
morphisms models point-wise substitution; $\operatorname{\vdash}$ being a
subfunctor of $A\times A$ means precisely that for any $x,y\in AX$, we have

$x\operatorname{\vdash}_{X}y\Rightarrow
f^{*}(x)\operatorname{\vdash}_{X}f^{*}(y).$

In our concrete example for consequence relations on $\mathsf{P}\mathbf{F}$,
this means that for any subsets $\Phi,\Psi\subseteq\mathbf{F}X$ we have

$\Phi\operatorname{\vdash}_{X}\Psi\Rightarrow\Phi^{f}\operatorname{\vdash}_{X}\Psi^{f},$

exactly saying that the consequence relation is structural.

After given the necessary definitions, we first show a lemma stating that
given a structural consequence relation, closed theories in each suplattice
$AX$ are preserved by inverse substitution:

######  Lemma 3.4.

Let $\operatorname{\vdash}$ be a structural consequence relation on
$\mathcal{A}$. Then for any set map $f:X\to Y$, if $y\in AY$ is closed under
$\operatorname{\vdash}_{Y}$, i.e. we have

$y=\bigvee_{y\operatorname{\vdash}_{Y}w}w,$

then so is $f_{*}(y)\in AX$ under $\operatorname{\vdash}_{X}$.

###### Proof.

By definition, to prove $f_{*}(y)$ is closed we only need to show

$f_{*}(y)\operatorname{\vdash}_{X}z\Rightarrow z\leq f_{*}(y).$

Note the following calculation

$\displaystyle f_{*}(y)\operatorname{\vdash}_{X}z$ $\displaystyle\Rightarrow
f^{*}f_{*}(y)\operatorname{\vdash}_{Y}f^{*}(z),$ $\displaystyle\Rightarrow
y\operatorname{\vdash}_{Y}f^{*}(z),$ $\displaystyle\Rightarrow f^{*}(z)\leq
y,$ $\displaystyle\Rightarrow z\leq f_{*}(y).$

The first implication holds by functoriality of $\operatorname{\vdash}$; the
second holds because $f^{*}f_{*}(y)\leq y$ thus
$y\operatorname{\vdash}_{Y}f^{*}f_{*}(y)$, and transitivity of
$\operatorname{\vdash}_{Y}$ implies the remainder; the third holds since $y$
is closed; and the final implication holds because $f_{*}$ is right adjoint to
$f^{*}$. ∎

We can now show in the functorial setting that structural consequence
relations are again the same as quotients.

######  Proposition 3.5.

For any $\mathcal{A}$ in $[\mathbf{Set},\mathbf{SupL}]$, consequence relations
and quotients on $\mathcal{A}$ corresponds bijectively to each other.

###### Proof.

Given a quotient $q:\mathcal{A}\twoheadrightarrow\mathcal{B}$, for any set $X$
we have a quotient map between suplattices

$q_{X}^{*}:AX\twoheadrightarrow BX,$

which by Lemma 3.2 uniquely induces a consequence relation
$\operatorname{\vdash}_{X}$ on $AX$. Hence, we only need to show that the
component-wise data $\operatorname{\vdash}_{X}\hookrightarrow AX\times AX$ we
get for every set $X$ indeed organise themselves into a subfunctor.
Explicitly, we need to show that for any set map $f:X\to Y$ and any $x,y\in
AX$,

$x\operatorname{\vdash}_{X}y\Rightarrow
f^{*}(x)\operatorname{\vdash}_{Y}f^{*}(y).$

Recall from Lemma 3.2, the induced consequence relation is defined as follows

$x\operatorname{\vdash}_{X}y\Leftrightarrow q_{X}^{*}(y)\leq q_{X}^{*}(x).$

We then have

$\displaystyle x\operatorname{\vdash}_{X}y$ $\displaystyle\Rightarrow
q_{X}^{*}(y)\leq q_{X}^{*}(x),$ $\displaystyle\Rightarrow
f^{*}q_{X}^{*}(y)\leq f^{*}q_{X}^{*}(x),$ $\displaystyle\Rightarrow
q_{Y}^{*}f^{*}(y)\leq q_{Y}^{*}f^{*}(x),$ $\displaystyle\Rightarrow
f^{*}(x)\operatorname{\vdash}_{Y}f^{*}(y).$

The first and fourth implication holds by the definition of the induced
consequence relation; the second implication holds by the fact that $f^{*}$ is
monotone; the third holds by naturality of $q$. This then close one direction
of the proof.

On the other hand, suppose we are given a structural consequence relation on
$\mathcal{A}$

$\operatorname{\vdash}\hookrightarrow A\times A.$

For any set $X$, $\operatorname{\vdash}_{X}$ is a consequence relation on
$AX$. By Lemma 3.2 again, it uniquely induces a quotient map

$\gamma_{X}^{*}:AX\twoheadrightarrow A_{\gamma}X,$

where $A_{\gamma}X$ is the following set,

$A_{\gamma}X=\operatorname{\\{}x\in AX\mid
x=\bigvee_{x\operatorname{\vdash}_{X}y}y\operatorname{\\}}.$

$\gamma_{X}$ sends any $x$ in $AX$ to its closure
$\bigvee_{x\operatorname{\vdash}_{X}y}y$. Similarly, we only need to show the
functoriality of this construction. Given any set map $f:X\to Y$, by Lemma 3.4
we know that the right adjoint $f_{*}$ restricts to a map

$f_{\gamma,*}:A_{\gamma}Y\to A_{\gamma}X.$

This restricted map actually preserves arbitrary meets, since, as we’ve
mentioned before, meets in $A_{\gamma}X$ and $A_{\gamma}Y$ are computed the
same as in $AX,AY$, respectively, and $f_{*}$ as a right adjoint preserves
arbitrary meets. This in particular implies that we have a left adjoint

$f_{\gamma}^{*}:A_{\gamma}X\to A_{\gamma}Y.$

Explicitly, the left adjoint $f_{\gamma}^{*}$ is given by

$f_{\gamma}^{*}(x)=\gamma_{Y}f^{*}(x),$

where $\gamma_{Y}$ is the induced closure operator on $AY$. We show this by
observing that for any $x\in AX$ and any $y\in A_{\gamma}Y$, since $y$ is
closed the following holds,

$\gamma_{Y}f^{*}(x)\leq y\Leftrightarrow f^{*}(x)\leq y\Leftrightarrow x\leq
f_{*}(y).$

This implies that we have a well-defined functor $\mathcal{A}_{\gamma}$. To
now prove $\gamma$ is a quotient in $[\mathbf{Set},\mathbf{SupL}]$, we only
need to show the following naturality diagramme commutes,

${AX}$${A_{\gamma}X}$${AY}$${A_{\gamma}Y}$$\scriptstyle{\gamma_{X}^{*}}$$\scriptstyle{f^{*}}$$\scriptstyle{f_{\gamma}^{*}}$$\scriptstyle{\gamma_{Y}^{*}}$

Explicitly, we need to show that for any $x\in AX$, the closure of
$f^{*}\gamma_{X}(x)$ and $f^{*}(x)$ coincide. Since we know that $f^{*}(x)\leq
f^{*}\gamma_{X}(x)$, we only need to show

$f^{*}(x)\operatorname{\vdash}_{Y}f^{*}\gamma_{X}(x).$

However, since every element implies its closure

$x\operatorname{\vdash}_{X}\gamma_{X}(x),$

functoriality of $\operatorname{\vdash}_{X}$ then proves the above fact.
Hence, we have shown that such a consequence relation indeed induces a
quotient

$\gamma:\mathcal{A}\twoheadrightarrow\mathcal{A}_{\gamma}.$

Finally, we need to prove the two constructions are mutually inverse to each
other. One direction is easier. Given a consequence relation
$\operatorname{\vdash}$ on $\mathcal{A}$, since both $A_{\gamma}X$ and
$\operatorname{\vdash}_{\gamma,X}$ are induced component-wise for any set $X$,
it is a direct consequence of Lemma 3.2 that $\operatorname{\vdash}$ and
$\operatorname{\vdash}_{\gamma}$ are the same consequence relation. On the
other hand, given a quotient $q:\mathcal{A}\twoheadrightarrow\mathcal{B}$, we
need to show that the quotient $\gamma:\mathcal{A}\to\mathcal{A}_{\gamma}$
induced by the consequence relation $\operatorname{\vdash}_{q}$ is isomorphic
to $q$. Again by the proof of Lemma 3.2, component-wise we have an isomorphism

$q_{X,*}:BX\cong A_{\gamma}X,$

for any set $X$. It is inherited from the right adjoint $q_{X,*}$ from $BX$ to
$AX$. It remains to show naturality of this isomorphism, viz. to prove the
following diagramme commutes,

${BX}$${A_{\gamma}X}$${BY}$${A_{\gamma}Y}$$\scriptstyle{q_{X,*}}$$\scriptstyle{Bf}$$\scriptstyle{f_{\gamma}^{*}}$$\scriptstyle{q_{Y,*}}$

For any $x\in BX$, by definition we have

$\displaystyle f_{\gamma}^{*}(q_{X,*}(x))$
$\displaystyle=\gamma_{Y}Af\bigvee_{q^{*}_{X}(y)=x}y,$
$\displaystyle=q_{Y,*}\bigvee_{q^{*}_{X}(y)=x}q_{Y}^{*}(Af(y)),$
$\displaystyle=q_{Y,*}\bigvee_{q^{*}_{X}(y)=x}Bf(q_{X}^{*}(y)),$
$\displaystyle=q_{Y,*}(Bf(x)).$

The first equality holds by the definition of the right adjoint $q_{X,*}$ and
$f_{\gamma}^{*}$; the second holds since $\gamma_{Y}=q_{Y}^{*}\fatsemi
q_{Y,*}$ and both $q_{Y}^{*}$ and $Af$ preserves joins; the third holds by
naturality of $q$; and the final equality holds by direction computation. As a
result,

$q_{X,*}\fatsemi f_{\gamma}^{*}=Bf\fatsemi q_{Y,*}.$

Hence, the component-wise isomorphisms between $BX$ and $A_{\gamma}X$ indeed
organize themselves to a natural isomorphism
$\mathcal{B}\cong\mathcal{A}_{\gamma}$, representing the same quotient. ∎

We end this section by providing some abstract examples of how to build
further consequence relations on existing ones. In the next section, we will
initiate a more concrete study of how a general class of consequence relations
can be induced from a class of algebras in our functorial setting, which
closely connects to the usual algebraic semantics of a logic.

######  Example 3.6.

Suppose now we have a consequence relation $\operatorname{\vdash}$ on
$\mathcal{A}$. We show how a generalised element of $A$ would induce a new
structural consequence relation based on $\operatorname{\vdash}$. Let $a$ be a
generalised element of $A$, viz. a natural transformation

$a:p\to A.$

For any set $X$ we define a new consequence relation
$\operatorname{\vdash}_{X}^{a}$ on $AX$ as follows: For any $x,y\in AX$, we
define

$x\operatorname{\vdash}_{X}^{a}y\Leftrightarrow x\vee\bigvee_{i\in
p(X)}a_{X}(i)\operatorname{\vdash}_{X}y.$

The induced family of consequence relations $\operatorname{\vdash}_{X}^{a}$ is
still structural. Given any $f:X\to Y$, we observe

$\displaystyle f^{*}\left(x\vee\bigvee_{i\in p(X)}a_{X}(i)\right)$
$\displaystyle=f^{*}(x)\vee\bigvee_{i\in p(X)}f^{*}(a_{X}(i)),$
$\displaystyle=f^{*}(x)\vee\bigvee_{i\in p(X)}a_{Y}(pf(i)),$
$\displaystyle\leq f^{*}(x)\vee\bigvee_{j\in p(Y)}a_{Y}(j).$

This in particular implies that

$f^{*}(x)\vee\bigvee_{j\in
p(Y)}a_{Y}(j)\operatorname{\vdash}_{Y}f^{*}\left(x\vee\bigvee_{i\in
p(X)}a_{X}(i)\right).$

By structurality of $\operatorname{\vdash}$ and the above fact, we then have

$x\operatorname{\vdash}_{X}^{a}y\Rightarrow
f^{*}(x)\operatorname{\vdash}_{Y}^{a}f^{*}(y).$

Intuitively, the newly constructed structural consequence relation
$\operatorname{\vdash}^{a}$ is one that induced from $\operatorname{\vdash}$
by always considering those elements in $AX$ from $p(X)$ along $a$ as axioms.

The majority of cases that will be interesting in ordinary logical studies is
when $p$ is a representable functor $\mathsf{y}^{X}$. By the Yoneda lemma, a
morphism $a$ from $\mathsf{y}^{X}$ to $A$ is the same as an element in $a\in
A(X)$. Given such an element, by definition we have

$x\operatorname{\vdash}_{y}^{a}y\Leftrightarrow x\vee\bigvee_{\sigma:X\to
Y}a^{\sigma}\operatorname{\vdash}_{X}y.$

This corresponds to adding the axiom scheme represented by $a\in A(X)$, viz. a
collection of axioms closed under substitution, into our logical system. ∎

Proposition 3.5 makes it clear that we can identity a consequence relation on
a functor $\mathcal{A}$ as a quotient of $\mathcal{A}$, providing a purely
categorical description of consequence relations. We will then use this
identification in subsequent texts to study algebraisation of logics and
semantics in general. These will be the topics of further sections.

##  4\. Algebraically Induced Consequence Relations

In this section, we consider abstract consequence relations generated by a
subclass of algebras, which further constitutes the algebraic semantics of our
logic. However, the general account of semantics of logic will be described in
more detail in later sections. Let’s first observe how the usual notion of an
algebraic model of a logic on a fixed set of variables can be presented in our
description of syntax using the syntactic monad $\mathbf{F}$.

Recall that the syntactic monad $\mathbf{F}$ induces an adjunction

$\mathsf{F}:\mathbf{Set}\rightleftarrows\mathbf{Set}^{\mathbf{F}}:U_{\mathbf{F}}.$

The free $\mathbf{F}$-algebra functor $\mathsf{F}$ sends any set $X$ to the
_free_ $\mathbf{F}$-algebra
$\mu_{\mathbf{F},X}:\mathbf{F}\mathbf{F}X\to\mathbf{F}X$ on the generating set
$X$.888Recall that $\mathbf{F}$-algebras and $\Sigma$-algebras are essentially
the same thing. Explicitly, it means that given any $\mathbf{F}$-algebra
$\alpha:\mathbf{F}\mathbb{S}\to\mathbb{S}$ and any set map $e:X\to\mathbb{S}$,
there is a _uniquely_ induced $\mathbf{F}$-algebra morphism

$\widetilde{e}:\mathbf{F}X\to\mathbb{S},$

which means the following diagramme commutes,

${\mathbf{F}\mathbf{F}X}$${\mathbf{F}X}$${\mathbf{F}\mathbb{S}}$${\mathbb{S}}$$\scriptstyle{\mu_{\mathbf{F},X}}$$\scriptstyle{\mathbf{F}\widetilde{e}}$$\scriptstyle{\widetilde{e}}$$\scriptstyle{\alpha}$

Explicitly, the function $\widetilde{e}$ is given by the following composite

$\widetilde{e}=\mathbf{F}e\fatsemi\alpha.$

By naturality of $\mu_{\mathbf{F}}$ and the fact that $\mathbb{S}$ with
$\alpha$ is an $\mathbf{F}$-algebra we can indeed show the above diagramme
commutes. In the usual context, $X$ is understood as the set of variables, and
the function $e$ is simply an evaluation function of atoms. The uniquely
induced $\mathbf{F}$-algebra homomorphism $\widetilde{e}$ is usually
inductively defined manually based on $e$. This constitutes an algebraic model
of $\mathbf{F}X$.

######  Definition 4.1.

An _algebraic model_ of $\mathbf{F}X$ is a pair $\langle\mathbb{S},e\rangle$,
where $\mathbb{S}$ is equipped with an $\mathbf{F}$-algebra structure
$\alpha:\mathbf{F}\mathbb{S}\to\mathbb{S}$ and $e$ is an evaluation function
from $X$ to $\mathbb{S}$. Given an algebraic model
$\langle\mathbb{S},e\rangle$, for any formula $\varphi\in\mathbf{F}X$, we
write

$\llbracket\varphi\rrbracket^{e}=\widetilde{e}(\varphi),$

as denoting the evaluation of $\varphi$ in $\mathbb{S}$ induced by $e$.

In later sections we will study more generally what a genuine functorial
description of semantics could be in our framework. Algebraic models in the
above sense naturally provides the notion of satisfaction on _pairs_ of
formulas. For any $\varphi,\psi\in\mathbf{F}X$, we will write
$\varphi\approx\psi$ to denote the pair $(\varphi,\psi)$. Given an algebraic
model $\langle\mathbb{S},e\rangle$, we say a pair $\varphi\approx\psi$ is
_satisfied_ in $\langle\mathbb{S},e\rangle$, denoted as

$\mathbb{S},e\vDash_{X}\varphi\approx\psi,$

if $\llbracket\varphi\rrbracket^{e}=\llbracket\psi\rrbracket^{e}$. For a set
of pairs $E\subseteq\mathbf{F}X\times\mathbf{F}X$, we also write

$\mathbb{S},e\vDash_{X}E,$

if for all pairs $\varphi\approx\psi\in E$,
$\mathbb{S},e\vDash_{X}\varphi\approx\psi$.

The above description of algebraic models for $\mathbf{F}X$ over a set of
variables $X$ then further leads us to study the consequence relations induced
by a class of algebras. As hinted above, this consequence relation will not be
based on $\mathsf{P}\mathbf{F}$, but should relate to _pairs_ of formulas. We
use $\mathbf{Eq}$ to denote the functor $\mathbf{F}\times\mathbf{F}$. Recall
at the end of Section 2 we have discussed how products of $\mathbf{F}$ behave:
$\mathbf{Eq}$ sends each set $X$ to the product
$\mathbf{F}X\times\mathbf{F}X$, the set of pairs of formulas over $X$. For any
function $f:X\to Y$, the action of $\mathbf{Eq}$ on morphisms simply do
substitution along $f$ for each entry of the pair

$(\varphi\approx\psi)^{f}=\mathbf{Eq}f(\varphi\approx\psi)=\varphi^{f}\approx\psi^{f}.$

Similarly, for a subset $E\subseteq\mathbf{Eq}X$, we also write

$E^{f}=\mathbf{P}\mathbf{Eq}f(E)=\operatorname{\\{}\varphi^{f}\approx\psi^{f}\mid\varphi\approx\psi\in
E\operatorname{\\}}.$

This point-wise definition of satisfaction naturally induce the notion of
validity for a given a subclass $\mathcal{K}$ of $\mathbf{F}$-algebras, or
more precisely a full subcategory of $\mathbf{Set}^{\mathbf{F}}$. We describe
now how it will induce a consequence relation on the functor
$\mathsf{P}\mathbf{Eq}$. For any $E,F\subseteq\mathbf{Eq}X$, we say

$E\vDash_{\mathcal{K},X}F,$

if for any algebraic model $\langle\mathbb{S},e\rangle$ in $\mathcal{K}$,
$\mathbb{S},e\vDash_{X}E$ implies $\mathbb{S},e\vDash_{X}F$. As usually in
logic, we if $E$ is the empty set we simply write

$\vDash_{\mathcal{K},X}F.$

Just like in the usual formulation of algebraic semantics of logic,
$\vDash_{\mathcal{K},X}$ is a component-wise consequence relation on the
suplattice $\mathsf{P}\mathbf{Eq}X$, for any set $X$. To see that such data
assemble themselves to a _structural_ consequence relation for the _functor_
$\mathsf{P}\mathbf{Eq}$, we need to further show the functoriality of
$\vDash_{\mathcal{K},X}$.

To do this, we first give a useful fact.

######  Fact 4.2.

Let $\mathcal{K}$ be a subclass of $\mathbf{F}$-algebras. Given any
$\mathbf{F}$-algebra $\alpha:\mathbf{F}\mathbb{S}\to\mathbb{S}$ and any
evaluation map $e:X\to\mathbb{S}$, for any function $f:Y\to X$ and for any
$\varphi\in\mathbf{F}Y$ the following holds

$\llbracket\varphi^{f}\rrbracket^{e}=\llbracket\varphi\rrbracket^{f\fatsemi
e}.$

###### Proof.

This can be directly calculated from relevant definition on evaluation
function of formulas and the functorial representation of substitution: For
any $\varphi\in\mathbf{F}Y$ we have

$\llbracket\varphi^{f}\rrbracket^{e}=\widetilde{e}(\mathbf{F}f\varphi)=\alpha(\mathbf{F}e(\mathbf{F}f\varphi))=\alpha\mathbf{F}(f\fatsemi
e)(\varphi)=\llbracket\varphi\rrbracket^{f\fatsemi e}.\qed$

We can now show that the class of algebras $\mathcal{K}$ induces a well-
defined structural consequence relation $\vDash_{\mathcal{K}}$ on
$\mathsf{P}\mathbf{Eq}$, such that for any set $X$, its component
$\vDash_{\mathcal{K},X}$ is the previously defined component-wise consequence
relation on $\mathsf{P}\mathbf{F}X$.

######  Proposition 4.3.

The component-wise relations $\vDash_{\mathcal{K},X}$ extends to a subfunctor

$\operatorname{\vDash_{\mathcal{K}}}\hookrightarrow\mathbf{P}\mathbf{Eq}\times\mathbf{P}\mathbf{Eq},$

constituting a structural consequence relation on $\mathsf{P}\mathbf{Eq}$.

###### Proof.

As mentioned before, we only need to show the functoriality of
$\vDash_{\mathcal{K}}$, i.e. given any function $f:Y\to X$ and
$E,F\subseteq\mathbf{Eq}Y$, we need to show that

$E\vDash_{\mathcal{K},Y}F\Rightarrow E^{f}\vDash_{\mathcal{K},X}F^{f}.$

For any $\mathbf{F}$-algebra $\alpha:\mathbf{F}\mathbb{S}\to\mathbb{S}$ in
$\mathcal{K}$, any evaluation function $e:X\to\mathbb{S}$ and any function
$f:Y\to X$, from Fact 4.2 we have the following observation: For any subset
$E\subseteq\mathbf{Eq}Y$, we have

$\displaystyle\mathbb{S},e\vDash_{X}E^{f}$
$\displaystyle\Leftrightarrow\forall\varphi\approx\psi\in E,\
\mathbb{S},e\vDash_{X}\varphi^{f}\approx\psi^{f},$
$\displaystyle\Leftrightarrow\forall\varphi\approx\psi\in E,\
\llbracket\varphi^{f}\rrbracket^{e}=\llbracket\psi^{f}\rrbracket^{e},$
$\displaystyle\Leftrightarrow\forall\varphi\approx\psi\in E,\
\llbracket\varphi\rrbracket^{f\fatsemi e}=\llbracket\psi\rrbracket^{f\fatsemi
e},$ $\displaystyle\Leftrightarrow\forall\varphi\approx\psi\in E,\
\mathbb{S},f\fatsemi e\vDash_{X}\varphi\approx\psi,$
$\displaystyle\Leftrightarrow\mathbb{S},f\fatsemi e\vDash_{Y}E.$

Now suppose we have $E,F\subseteq\mathbf{Eq}Y$ that
$E\vDash_{\mathcal{K},Y}F$. Then by the above computation we have

$\mathbb{S},e\vDash_{X}E^{f}\Rightarrow\mathbb{S},f\fatsemi
e\vDash_{Y}E\Rightarrow\mathbb{S},f\fatsemi
e\vDash_{Y}F\Rightarrow\mathbb{S},e\vDash_{X}F^{f}.$

The first and last implication follows from the above equivalence; the second
implication follows from the fact that $E\vDash_{\mathcal{K},Y}F$. This
completes the proof that $\vDash_{\mathcal{K}}$ is functorial, and thus
constitutes a structural consequence relation on $\mathsf{P}\mathbf{Eq}$. ∎

We end this section by considering the special case where $\mathcal{K}$ is a
variety of algebras. A variety of algebras, by definition, is an equational
class; it is a subclass of the class of all algebraic structures of a given
signature that satisfies a given set of identities. In particular, it is
(strictly) monadic over $\mathbf{Set}$: There exists a monad $\mathbf{K}$,
such that we have an equivalence (isomorphism) of categories

$\mathcal{K}\cong\mathbf{Set}^{\mathbf{K}}.$

Such a setting allows us to generate the Lindenbaum–Tarski algebra
construction from general category theory, by exploring the duality between
monads and monad maps on one hand, and categories of monad algebras (monadic
functors) on the other hand.

The collection of monads over $\mathbf{Set}$ actually forms a category
$\mathbf{Mnd}$. Given two monads $\mathbf{F},\mathbf{K}$, a morphism from
$\mathbf{F}$ to $\mathbf{K}$ in $\mathbf{Mnd}$ is a natural transformation

$\lambda:\mathbf{F}\to\mathbf{K},$

that interacts well with the monad structure of both $\mathbf{F}$ and
$\mathbf{K}$, making the following two diagrammes commute,

${\mathsf{y}}$${\mathbf{F}}$${\mathbf{K}}$$\scriptstyle{\eta_{\mathbf{F}}}$$\scriptstyle{\eta_{\mathbf{K}}}$$\scriptstyle{\lambda}$
${\mathbf{F}\mathbf{F}}$${\mathbf{F}}$${\mathbf{K}\mathbf{K}}$${\mathbf{K}}$$\scriptstyle{\mu_{\mathbf{F}}}$$\scriptstyle{\lambda\circ\lambda}$$\scriptstyle{\lambda}$$\scriptstyle{\mu_{\mathbf{K}}}$

Such a monad map induces a pullback functor between the corresponding
categories of algebras

$\lambda^{*}:\mathbf{Set}^{\mathbf{K}}\to\mathbf{Set}^{\mathbf{F}}.$

For any $\mathbf{K}$-algebra $\alpha:\mathbf{K}S\to S$, $\lambda^{*}\alpha$ is
the following composition

$\lambda^{*}\alpha=\lambda_{S}\fatsemi\alpha:\mathbf{F}S\to\mathbf{K}S\to S.$

One can directly verify that $\lambda^{*}\alpha$ is indeed an
$\mathbf{F}$-algebra, using the fact that $\lambda$ is a monad map and
$\alpha$ is a $\mathbf{K}$-algebra, which we leave for the readers to check.
For a given $\mathbf{K}$-algebra morphism $f:S\to T$ from
$\alpha:\mathbf{K}S\to S$ to $\beta:\mathbf{K}T\to T$, it also lifts to a
morphism $\lambda^{*}f$ from $\lambda^{*}\alpha$ to $\lambda^{*}\beta$ by
simply using $f$ itself,

${\mathbf{F}S}$${\mathbf{K}S}$${S}$${\mathbf{F}T}$${\mathbf{K}T}$${T}$$\scriptstyle{\lambda_{S}}$$\scriptstyle{\mathbf{F}f}$$\scriptstyle{\alpha}$$\scriptstyle{\mathbf{K}f}$$\scriptstyle{f}$$\scriptstyle{\lambda_{T}}$$\scriptstyle{\beta}$

It is easy to see from the above definition that the induced functor
$\lambda^{*}$ between the two category of algebras are compatible with the
forgetful functors $U_{\mathbf{K}},U_{\mathbf{F}}$, i.e. we have

$\lambda^{*}\fatsemi U_{\mathbf{F}}=U_{\mathbf{K}}.$

On the other hand of the duality lies monadic functors on $\mathbf{Set}$ over
$U_{\mathbf{F}}$. A monadic functor is by definition equivalent to a forgetful
functor for some monads, and a morphism between monadic functors
$U_{\mathbf{T}},U_{\mathbf{F}}$ is then a single functor
$G:\mathbf{Set}^{\mathbf{T}}\to\mathbf{Set}^{\mathbf{F}}$ that commutes with
the forgetful functors $U_{\mathbf{T}},U_{\mathbf{F}}$,

${\mathbf{Set}^{\mathbf{T}}}$${\mathbf{Set}^{\mathbf{F}}}$${\mathbf{Set}}$$\scriptstyle{U_{\mathbf{T}}}$$\scriptstyle{G}$$\scriptstyle{U_{\mathbf{F}}}$

We use $\mathbf{MnF}$ to denote the category of monadic functors on
$\mathbf{Set}$.

Recall that for any set $X$, $\mathsf{K}X$, the free $\mathbf{K}$-algebra on
$X$, is given by the multiplication
$\mu_{\mathbf{T},X}:\mathbf{T}\mathbf{T}X\to\mathbf{T}X$. Since $G$ commutes
with the forgetful functors, it then follows that the functor $G$ then
associate an $\mathbf{F}$-algebra structure on $\mathbf{T}X$

$G\mathsf{K}X:\mathbf{F}\mathbf{T}X\to\mathbf{T}X.$

Again, $\mu_{\mathbf{F},X}$ is the free $\mathbf{F}$-algebra on $X$, and we
have a canonical map $\eta_{\mathbf{T},X}$. This then implies that we have a
canonically induced $\mathbf{F}$-algebra morphism

$\widetilde{\eta_{\mathbf{T},X}}=\mathbf{F}\eta_{\mathbf{T},X}\fatsemi
G\mathsf{K}X:\mathbf{F}X\to\mathbf{F}\mathbf{T}X\to\mathbf{T}X.$

We can then simply define a natural transformation
$\delta:\mathbf{F}\to\mathbf{T}$, making the $X$-component of $\delta$ be
$\widetilde{\eta_{\mathbf{T},X}}$. Naturality of $\delta$, and the fact that
it is furthermore a monad map from $\mathbf{F}$ to $\mathbf{T}$, follows from
the fact that $G$ is a functor that commutes with the two forgetful functors.
It is well-known that the above described two-sided constructions indeed form
a functorial bijective correspondence. We refer the readers to [14, p. 108]
for a proof. Here we in particular notice the following refined
correspondence:

######  Lemma 4.4.

Quotient monad maps $\lambda:\mathbf{F}\twoheadrightarrow\mathbf{K}$ on
syntactic monad $\mathbf{F}$, viz. monad maps that are component-wise
surjective out of $\mathbf{F}$, bijectively corresponds to varieties of
algebras $\mathcal{K}$ that form a full subcategory of
$\mathbf{Set}^{\mathbf{F}}$.

###### Proof Sketch.

We first show monad maps $\lambda:\mathbf{F}\twoheadrightarrow\mathbf{K}$ that
are component-wise surjective induces a full subcategory inclusion
$\mathbf{Set}^{\mathbf{K}}\hookrightarrow\mathbf{Set}^{\mathbf{F}}$, or more
precisely, the inclusion functor is fully faithful and injective on objects.
Given a $\mathbf{K}$-algebra $\alpha:\mathbf{K}X\to X$, according to the
previously mentioned construction, the induced $\mathbf{F}$-algebra is given
by

${\mathbf{F}X}$${\mathbf{K}X}$${X.}$$\scriptstyle{\lambda_{X}}$$\scriptstyle{\alpha}$

Since $\lambda_{X}$ is surjective, it is obvious that there are no
$\mathbf{K}$-algebra structure on $X$ that gives out the same
$\mathbf{F}$-algebra. Thus, the inclusion is injective on objects. It is easy
to see that the inclusion is faithful. We only need to show it is full, i.e.
in the following diagramme, if the outer square commutes then so does the
right square

${\mathbf{F}X}$${\mathbf{K}X}$${X}$${\mathbf{F}Y}$${\mathbf{K}Y}$${Y}$$\scriptstyle{\lambda_{X}}$$\scriptstyle{\mathbf{F}f}$$\scriptstyle{\mathbf{K}f}$$\scriptstyle{\alpha}$$\scriptstyle{f}$$\scriptstyle{\lambda_{Y}}$$\scriptstyle{\beta}$

Notice that the left square commutes by naturality of $\lambda$. We finally
observe that

$\lambda_{X}\fatsemi\alpha\fatsemi
f=\mathbf{F}f\fatsemi\lambda_{Y}\fatsemi\beta=\lambda_{X}\fatsemi\mathbf{K}f\fatsemi\beta.$

This equation, together with the fact that $\lambda_{X}$ is surjective, shows
that

$\alpha\fatsemi f=\mathbf{K}f\fatsemi\beta.$

Hence, the inclusion is also full.

The other direction of the proof is more tricky. It will use the fact that our
syntactic monad preserves surjections, and the fact that a variety of full
subcategory of $\mathbf{Set}^{\mathbf{F}}$ is closed under forming products,
subalgebras, and reflexive coequalisers, which ultimately relies on Birkhoff’s
theorem. Or we can use an adjoint lifting theorem described in [9], showing
that $\mathcal{K}$ would be a reflexive subcategory of
$\mathbf{Set}^{\mathbf{F}}$. We refer the readers to [14, p. 110] for a
complete proof. ∎

We further show that the induced quotient map on monads is essentially
providing us with the Lindenbaum–Tarski algebra construction, by observing the
following fact:

######  Proposition 4.5.

For any set $X$ and any pair of formulas $\varphi\approx\psi\in\mathbf{Eq}X$,

$\vDash_{\mathcal{K},X}\varphi\approx\psi\Leftrightarrow\mathbf{K}X,\eta_{\mathbf{K},X}\vDash_{X}\varphi\approx\psi,$

where $\mathbf{K}X$ is viewed as the free $\mathbf{K}$-algebra on $X$ included
in $\mathbf{Set}^{\mathbf{F}}$.

###### Proof.

The left to right direction is trivial. For the right to left direction, we
show that $\lambda_{X}$ consists of an $\mathbf{F}$-algebra morphism from
$\mathsf{K}X$ included into $\mathbf{Set}^{\mathbf{F}}$, to $\mathsf{F}X$; and
it is the initial one among $\mathcal{K}$, i.e. $\mathbf{F}$-algebras that
lies in the image of $\lambda^{*}$.

We first observe that the following diagramme commutes by the fact that
$\lambda$ commutes with multiplications of $\mathbf{F}$ and $\mathbf{K}$,

${\mathbf{F}\mathbf{K}X}$${\mathbf{K}\mathbf{K}X}$${\mathbf{K}X}$${\mathbf{F}\mathbf{F}X}$${\mathbf{F}X}$$\scriptstyle{\lambda_{\mathbf{K}X}}$$\scriptstyle{\mu_{\mathbf{K},X}}$$\scriptstyle{\mathbf{F}\lambda_{X}}$$\scriptstyle{\mu_{\mathbf{F},X}}$$\scriptstyle{(\lambda\circ\lambda)_{X}}$$\scriptstyle{\lambda_{X}}$

We also know

$\eta_{\mathbf{F},X}\fatsemi\lambda_{X}=\eta_{\mathbf{K},X}.$

Together they show that $\lambda_{X}$ is the uniquely induced
$\mathbf{F}$-algebra morphism from the set map $\eta_{\mathbf{K},X}$, since
$\mathbf{F}X$ is free. We can also see this fact by direct computation,

$\widetilde{\eta_{\mathbf{K},X}}=\mathbf{F}\eta_{\mathbf{K},X}\fatsemi\lambda_{\mathbf{K}X}\fatsemi\mu_{\mathbf{K},X}=\lambda_{X}\fatsemi\eta_{\mathbf{K},\mathbf{K}X}\fatsemi\mu_{\mathbf{K},X}=\lambda_{X}.$

Next we show the initialness of $\lambda_{X}$ of $\mathbf{F}$-algebra
morphisms from $\mathbf{F}X$ to ones in $\mathcal{K}$. Explicitly, we show
that for any $\mathbf{F}$-algebra $\mathbb{S}$ of the form

$\leavevmode\hbox to104.81pt{\vbox
to14.25pt{\pgfpicture\makeatletter\hbox{\hskip 52.40276pt\lower-7.17621pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-52.40276pt}{-7.07637pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
10.34723pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-6.04169pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathbf{F}\mathbb{S}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
10.34723pt\hfil&\hfil\hskip 34.9722pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-6.66669pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathbf{K}\mathbb{S}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
10.97223pt\hfil&\hfil\hskip 31.0833pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.77779pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathbb{S}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
7.08333pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-31.5083pt}{-4.57637pt}\pgfsys@lineto{-8.30829pt}{-4.57637pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.1083pt}{-4.57637pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-22.8611pt}{-0.85693pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\lambda_{\mathbb{S}}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{14.43613pt}{-4.57637pt}\pgfsys@lineto{37.63614pt}{-4.57637pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{37.83612pt}{-4.57637pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{23.99716pt}{-2.2236pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{\alpha}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},$

where $\alpha$ is a $\mathbf{K}$-algebra morphism, any $\mathbf{F}$-algebra
homomorphism from $\mathbf{F}X$ to $\mathbb{S}$ factors through $\lambda_{X}$:

${\mathbf{F}\mathbb{S}}$${\mathbf{K}\mathbb{S}}$${\mathbb{S}}$${\mathbf{F}\mathbf{K}X}$${\mathbf{K}\mathbf{K}X}$${\mathbf{K}X}$${\mathbf{F}\mathbf{F}X}$${\mathbf{F}X}$$\scriptstyle{\lambda_{\mathbb{S}}}$$\scriptstyle{\alpha}$$\scriptstyle{\lambda_{\mathbf{K}X}}$$\scriptstyle{\mathbf{F}\overline{e}}$$\scriptstyle{\mu_{\mathbf{K},X}}$$\scriptstyle{\mathbf{K}\overline{e}}$$\scriptstyle{\overline{e}}$$\scriptstyle{\mathbf{F}\lambda_{X}}$$\scriptstyle{\mu_{\mathbf{F},X}}$$\scriptstyle{\lambda_{X}}$$\scriptstyle{\widetilde{e}}$

For any set map $e:X\to\mathbb{S}$ — as previously mentioned, every
$\mathbf{F}$-algebra homomorphism from $\mathsf{F}X$ to $\alpha$ is of the
form $\widetilde{e}$ for some $e$ since $\mathsf{F}X$ is free — $\overline{e}$
is the uniquely induced $\mathbf{K}$-algebra morphism from $\mathsf{K}X$ to
$\alpha$. The diagramme commutes because $\overline{e}$ is a
$\mathbf{K}$-algebra homomorphism and due to the naturality of $\lambda$. By
uniqueness of the induced map $\widetilde{e}$, it then follows that
$\widetilde{e}$ factors through $\lambda_{X}$. We can also prove it by direct
computation:

$\widetilde{e}=\mathbf{F}e\fatsemi\lambda_{\mathbb{S}}\fatsemi\alpha=\lambda_{X}\fatsemi\mathbf{K}e\fatsemi\alpha=\lambda_{X}\fatsemi\overline{e}.$

Finally, we suppose that

$\mathbf{K}X,\eta_{\mathbf{K},X}\vDash_{X}\varphi\approx\psi,$

or in other words

$\lambda_{X}(\varphi)=\lambda_{X}(\psi).$

Then for any algebraic semantics $\langle\mathbb{S},e\rangle$ with
$\mathbb{S}$ an algebra in $\mathcal{K}$, the initialness of $\lambda_{X}$
implies

$\widetilde{e}(\varphi)=\overline{e}\circ\lambda_{X}(\varphi)=\overline{e}\circ\lambda_{X}(\psi)=\widetilde{e}(\psi)\Rightarrow\mathbb{S},e\vDash_{X}\varphi\approx\psi.$

Thus, we have

$\mathbf{K}X,\eta_{\mathbf{K},X}\vDash_{X}\varphi\approx\psi\Rightarrow\operatorname{\vDash}_{\mathcal{K},X}\varphi\approx\psi.\qed$

Proposition 4.5 then shows that the induced free $\mathbf{K}$-algebra
$\mathsf{K}X$ with the evaluation $\eta_{\mathbf{K},X}$ contains all the
semantic information of the class $\mathcal{K}$ with respect to the set of
formulas $\mathbf{F}X$. The evaluation map from $\mathbf{F}X$ to $\mathbf{K}X$
is precisely given by the $X$-component of the monad quotient map $\lambda$.
Putting all these together then explicitly shows how the usual story of
Lindenbaum-Tarski algebra can be recovered from our categorical setting. And
by the previous Lemma 4.4, given any such class of variety of algebras
$\mathcal{K}$ serving as algebraic models and generating a structural
consequence relation on $\mathsf{P}\mathbf{Eq}$, by general category theory
there is a uniquely induced quotient monad $\lambda:\mathbf{F}\to\mathbf{K}$,
that (1) on the functorial level it provides the construction of Lindenbaum-
Tarski algebra, which is generally a _quotient_ of the syntactic term algebra;
and (2) this quotient $\lambda_{X}$ on each component can then be viewed as
evaluation map of our syntactic objects in $\mathbf{F}X$, which contains the
full semantic information about the class $\mathcal{K}$. Such a setting is
another incarnation of our general philosophy that logic is describing general
ways of constructing quotients.

##  5\. Category of Consequence Relations

In Section 3 we have identified structural consequence relations in its full
generality as quotients of $\mathcal{A}$, with $\mathcal{A}$ being functors in
$[\mathbf{Set},\mathbf{SupL}]$. Section 4 implements a concrete example of a
consequence relation on the functor $\mathsf{P}\mathbf{Eq}$, with a given
subclass of $\mathbf{F}$-algebras as providing semantics on pairs of formulas.
However, when we study usual logics with an algebraic signature, as for
propositional logic or other modal logics, the proof system we give does not
generate consequence relations on $\mathsf{P}\mathbf{Eq}$, or
$\mathbf{P}(\mathrm{Fml}\times\mathrm{Fml})$ where the set of variables is
fixed, but on $\mathsf{P}\mathbf{F}$ or $\mathbf{P}\mathrm{Fml}$. However,
viewing logics from a universal algebra perspective, especially the
construction of Lindenbaum-Tarski algebras discussed in the previous section,
has proven to be a very successful approach to study logical systems in
general. And there is a precise notion of when such an algebraic study of
logics is equivalent to the proof theoretic one. This is the notion of
_algebraisation_ of logics, first systematically studied in [2].

Conceptually, a proof system, or a structural consequence relation on
$\mathsf{P}\mathbf{F}$, is algebraisable if and only if it is equivalent — in
a sense we are going to state more precisely later — to a consequence relation
on $\mathsf{P}\mathbf{Eq}$ generated by a class of algebras as studied in the
previous section. Hence, in the following texts we will first take up a
general study of relations between different consequence relations. More
specifically, we will investigate when a structural consequence relation is
_represented_ or _equivalent_ to another one. In other words, we will be
interested in the _category of structural consequence relation_. Many of the
results presented in this section is a direct generalisation of results
obtained in [5].

Now in Section 3, Proposition 3.5 has provided us with a very nice
identification, establishing that structural consequence relations corresponds
bijectively to quotients in $[\mathbf{Set},\mathbf{SupL}]$. We will heavily
rely on such an identification in this section, since quotients are much more
easy to describe categorically. We let $\mathbf{Quo}$ be the category of
surjections in $[\mathbf{Set},\mathbf{SupL}]$. Explicitly, objects in
$\mathbf{Quo}$ are surjections $q:\mathcal{A}\twoheadrightarrow\mathcal{B}$ in
$[\mathbf{Set},\mathbf{SupL}]$; a morphism from
$q_{1}:\mathcal{A}_{1}\twoheadrightarrow\mathcal{B}_{1}$ to
$q_{2}:\mathcal{A}_{2}\twoheadrightarrow\mathcal{B}_{2}$ is a pair of
morphisms $(\tau,\rho)$ in $[\mathbf{Set},\mathbf{SupL}]$ that makes the
following diagramme commute,

${\mathcal{A}_{1}}$${\mathcal{A}_{2}}$${\mathcal{B}_{1}}$${\mathcal{B}_{2}}$$\scriptstyle{\tau}$$\scriptstyle{q_{1}}$$\scriptstyle{q_{2}}$$\scriptstyle{\rho}$

A morphism in $\mathbf{Quo}$, in a sense, gives a way of translating the
information of consequence relation $\operatorname{\vdash}$ induced by $q_{1}$
on $\mathcal{A}_{1}$ to the one $\operatorname{\Vdash}$ induced by $q_{2}$ on
$\mathcal{A}_{2}$. Suppose we are given such a morphism $(\tau,\rho)$, then
for any set $X$ and any $x,y\in A_{1}X$, by definition we have

$\displaystyle x\operatorname{\vdash}_{X}y$ $\displaystyle\Leftrightarrow
q_{1,X}^{*}(y)\leq q_{1,X}^{*}(y),$
$\displaystyle\Rightarrow\rho_{X}^{*}(q_{1,X}^{*}(y))\leq\rho_{X}^{*}(q_{1,X}^{*}(x)),$
$\displaystyle\Rightarrow q_{2,X}^{*}(\tau_{X}^{*}(y))\leq
q_{2,X}^{*}(\tau_{X}^{*}(x)),$
$\displaystyle\Rightarrow\tau_{X}^{*}(x)\operatorname{\Vdash}_{X}\tau_{X}^{*}(y).$

Among all of such morphisms, we are in particularly interested in the case
where it induces a _faithful_ translation. We say the consequence relation
$\operatorname{\vdash}$ induced by $q_{1}$ is _faithfully represented_ , or
simply _represented_ , by the consequence relation $\operatorname{\Vdash}$
induced by $q_{2}$ along $(\tau,\rho)$, if for any set $X$ and any
$x,y\in\mathcal{A}X$

$x\operatorname{\vdash}_{X}y\Leftrightarrow\tau^{*}_{X}(x)\operatorname{\Vdash}_{X}\tau^{*}_{X}(y).$

Below we give a precise characterisation of when a morphism in $\mathbf{Quo}$
induces a faithful representation.

Recall again that limits and colimits in a functor category like
$[\mathbf{Set},\mathbf{SupL}]$ are computed component-wise. In particular,
what we have described as the image-factorisation of suplattices in Example
3.3 can be almost seamlessly transported to the functorial case in
$[\mathbf{Set},\mathbf{SupL}]$. It turns out that representation of
consequence relations has a close connection with image-factorisations.

######  Lemma 5.1.

Let $(\tau,\rho)$ be a morphism in $\mathbf{Quo}$ from
$q_{1}:\mathcal{A}_{1}\twoheadrightarrow\mathcal{B}_{1}$ to
$q_{2}:\mathcal{A}_{2}\twoheadrightarrow\mathcal{B}_{2}$. Then it consists of
a representation of $\operatorname{\vdash}$ by $\operatorname{\Vdash}$ iff
$q_{1}$ and $\rho$ make up of the image-factorisation of $\tau\fatsemi q_{2}$,
iff $\rho$ is injective.

###### Proof.

From the component-wise description of images in
$[\mathbf{Set},\mathbf{SupL}]$ we know that $\mathcal{B}_{2}$ is the image of
$\tau\fatsemi q_{2}$ iff $\rho$ is injective. Suppose we have such a morphism
with $\rho$ being injective. Let $X$ be any set and $x,y$ any elements in
$\mathcal{A}_{1}X$. From the correspondence between consequence relations and
quotients, we have

$x\operatorname{\vdash}_{X}y\Leftrightarrow q_{1,X}^{*}(y)\leq
q_{1,X}^{*}(x).$

Since $\rho$ is injective, in particular $\rho_{X}^{*}$ is injective for any
set $X$, this means that $\rho_{X}^{*}$ is a poset-embedding of
$\mathcal{B}_{1}X$ into $\mathcal{B}_{2}X$. As a result, for any
$a,b\in\mathcal{B}_{1}X$, $a\leq b$ if and only if
$\rho_{X}^{*}(a)\leq\rho_{X}^{*}(b)$. We can then further compute

$\displaystyle x\operatorname{\vdash}_{X}y$ $\displaystyle\Leftrightarrow
q_{1,X}^{*}(y)\leq q_{1,X}^{*}(x),$
$\displaystyle\Leftrightarrow\rho^{*}_{X}q_{1,X}^{*}(y)\leq\rho^{*}_{X}q_{1,X}^{*}(x),$
$\displaystyle\Leftrightarrow q_{2,X}^{*}\tau_{X}^{*}(y)\leq
q_{2,X}^{*}\tau_{X}^{*}(x),$
$\displaystyle\Leftrightarrow\tau_{X}^{*}(x)\operatorname{\Vdash}_{X}\tau_{X}^{*}(y).$

The first and last equivalence follows from the correspondence between
quotients and consequence relations; the second equivalence follows from the
fact that each $\rho_{X}^{*}$ is a poset-embedding; the third equivalence is a
result of the commuting diagramme in the definition of morphisms in
$\mathbf{Quo}$.

On the other hand, suppose $\operatorname{\vdash}$ is faithfully represented
by $\operatorname{\Vdash}$ in $(\tau,\rho)$. We need to show that $\rho$ is
injective, which is equivalent to show that $\rho_{X}^{*}$ is injective for
any set $X$. First, since $q_{1}$ is a surjection, it follows that every
element in $\mathcal{B}_{1}X$ has the form $q_{1,X}^{*}(x)$ for some
$x\in\mathcal{A}_{1}X$. We know that for any $x,y\in\mathcal{A}_{1}X$

$\tau_{X}^{*}(x)\operatorname{\Vdash}_{X}\tau_{X}^{*}(y)\Rightarrow
x\operatorname{\vdash}_{X}y.$

From previous computations we already know that

$\tau_{X}^{*}(x)\operatorname{\Vdash}_{X}\tau_{X}^{*}(y)\Leftrightarrow\rho_{X}^{*}q_{1,X}^{*}(y)\leq\rho_{X}^{*}q_{1,X}^{*}(x);$
$x\operatorname{\vdash}_{X}y\Leftrightarrow q_{1,X}^{*}(y)\leq
q_{1,X}^{*}(x).$

It then follows that

$\rho_{X}^{*}q_{1,X}^{*}(y)\leq\rho_{X}^{*}q_{1,X}^{*}(x)\Rightarrow
q_{1,X}^{*}(y)\leq q_{1,X}^{*}(x),$

which, together with the fact that $q_{1,X}^{*}$ is surjective, implies that
$\rho_{X}^{*}$ is a poset-embedding, thus injective. ∎

Now intuitively, two consequence relations
$\operatorname{\vdash},\operatorname{\Vdash}$ are equivalent if, and only if
each one of them can be faithfully represented by the other. According to the
above result, this in particular means that we must have a morphism
$(\tau,\rho)$ in $\mathbf{Quo}$ from $q_{1}$ to $q_{2}$ where $\rho$ is
injective, and another morphism $(\delta,\gamma)$ from $q_{2}$ to $q_{1}$ with
$\gamma$ being injective. Set-theoretically, we know that if there are two-
sided injections between two sets then they are isomorphic. Lifting this
point-wise result to our category $[\mathbf{Set},\mathbf{SupL}]$ shows that
$\mathcal{B}_{1}$ and $\mathcal{B}_{2}$ must be isomorphic either. Hence, we
define an _equivalence_ between two consequence relations as a tuple
$(\tau,\delta,\rho)$ with $\rho$ being an isomorphism, such that in the below
diagramme

${\mathcal{A}_{1}}$${\mathcal{A}_{2}}$${\mathcal{B}_{1}}$${\mathcal{B}_{2}}$$\scriptstyle{\tau}$$\scriptstyle{q_{1}}$$\scriptstyle{q_{2}}$$\scriptstyle{\delta}$$\scriptstyle{\rho}$$\scriptstyle{\rho^{-1}}$

$(\tau,\rho)$ exhibits a representation of $\operatorname{\vdash}$ by
$\operatorname{\Vdash}$, and $(\delta,\rho^{-1})$ exhibits a representation of
$\operatorname{\Vdash}$ by $\operatorname{\vdash}$. We have the following
characterisation of equivalences between consequence relations.

######  Lemma 5.2.

Given two quotients $q_{1}:\mathcal{A}_{1}\twoheadrightarrow\mathcal{B}_{1}$
and $q_{2}:\mathcal{A}_{2}\twoheadrightarrow\mathcal{B}_{2}$, two morphisms
$\tau:\mathcal{A}_{1}\rightleftarrows\mathcal{A}_{2}:\delta$ induce an
equivalence between the two consequence relations iff one of the two
conditions holds:

  1. (1)

$q_{1}$ exhibits $\mathcal{B}_{1}$ as the image of $\tau\fatsemi q_{2}$ and
$\delta\fatsemi\tau\fatsemi q_{2}=q_{2}$;

  2. (2)

$q_{2}$ exhibits $\mathcal{B}_{2}$ as the image of $\delta\fatsemi q_{1}$ and
$\tau\fatsemi\delta\fatsemi q_{1}=q_{1}$.

###### Proof.

It is easy to see that an equivalence between the two induced consequence
relations implies both (1) and (2). Suppose (1) holds. If $q_{1}$ exhibits
$\mathcal{B}_{1}$ as the image of $\tau\fatsemi q_{2}$, we would then have an
injective morphism $\rho:\mathcal{B}_{1}\to\mathcal{B}_{2}$ such that

$q_{1}\fatsemi\rho=\tau\fatsemi q_{2}.$

To show $\rho$ is an isomorphism we then only need to show it is also
surjective. For any set $X$, let $y$ be an element in $\mathcal{B}_{2}X$.
Since $q_{2}$ is surjective, we choose $x\in\mathcal{A}_{2}X$ that
$q_{2,X}(x)=y$. We can then compute

$\rho_{X}(q_{1,X}(\delta_{X}(x)))=q_{2,X}(\tau_{X}(\delta_{X}(x)))=q_{2,X}(x)=y.$

The first equality holds by the fact that $q_{1}$ and $\rho$ is the image-
factorisation of $\tau\fatsemi q_{2}$; the second holds because by assumption
$\delta\fatsemi\tau\fatsemi q_{2}=q_{2}$. It then follows that $\rho$ is
indeed surjective, hence isomorphic. Finally, we observe

$q_{2}\fatsemi\rho^{-1}=\delta\fatsemi\tau\fatsemi
q_{2}\fatsemi\rho^{-1}=\delta\fatsemi
q_{2}\fatsemi\rho\fatsemi\rho^{-1}=\delta\fatsemi q_{2}.$

This finally shows that $(\delta,\rho^{-1})$ is also a morphism in
$\mathbf{Quo}$, thus $(\tau,\delta,\rho)$ is indeed an equivalence of
consequence relations. The proof of (2) is completely similar. ∎

In terms of consequence relations, we have the following result.

######  Corollary 5.3.

A pair of morphisms
$\tau:\mathcal{A}_{1}\rightleftarrows\mathcal{A}_{2}:\delta$ induces an
equivalence between the two consequence relations
$\operatorname{\vdash},\operatorname{\Vdash}$ iff the following conditions
hold: For any set $X$,

  * •

for any $x,y\in A_{1}X$,
$x\operatorname{\vdash}_{X}y\Leftrightarrow\tau_{X}^{*}(x)\operatorname{\Vdash}_{X}\tau_{X}^{*}(y)$;

  * •

for any $z\in A_{2}X$,
$z\operatorname{\text{\reflectbox{$\Vdash$}}\\!\Vdash}\tau_{X}^{*}(\delta_{X}^{*}(z))$.

Or equivalently, iff for any set $X$ the following conditions hold:

  * •

for any $x,y\in A_{2}X$,
$x\operatorname{\Vdash}_{X}y\Leftrightarrow\delta_{X}^{*}(x)\operatorname{\vdash}_{X}\delta^{*}_{X}(y)$;

  * •

for any $z\in A_{1}X$,
$z\operatorname{\text{\reflectbox{$\vdash$}}\\!\vdash}\delta_{X}^{*}(\tau_{X}^{*}(z))$.

###### Proof.

Similarly we only prove the result for the first set of conditions. From Lemma
5.1 we know that
$x\operatorname{\vdash}_{X}y\Leftrightarrow\tau_{X}^{*}(x)\operatorname{\Vdash}\tau_{X}^{*}(y)$
implies that $\mathcal{B}_{1}$ is the image of $\tau\fatsemi q_{2}$. On the
other hand, for any $z\in A_{2}X$,
$z\operatorname{\text{\reflectbox{$\Vdash$}}\\!\Vdash}\tau_{X}^{*}(\delta_{X}^{*}(z))$
simply means that

$q_{2,X}^{*}(z)=q_{2,X}^{*}(\tau_{X}^{*}(\delta_{X}^{*}(z))),$

which shows $q_{2}=\delta\fatsemi\tau\fatsemi q_{2}$. By Lemma 5.2 we then
know $\tau,\delta$ induce an equivalence of consequence relations. ∎

Corollary 5.3 has shown us that given an equivalence between consequence
relations $\operatorname{\vdash}$ and $\operatorname{\Vdash}$, what we
essentially have is two translations $\tau,\delta$ that induce faithful
representations of one consequence relation by another, and vice versa.
Furthermore, if you translate something back and force along $\tau$ and
$\delta$, the result you get would be the same as the original element you
begin with relative to the consequence relation. This has nicely summarised
what we want for two equivalence relations to be equivalent in a precise
technical sense.

In particular, when the consequence relation $\operatorname{\vdash}$ on
$\mathsf{P}\mathbf{F}$ generated by a proof system is equivalent to the
consequence relation $\vDash_{\mathcal{K}}$ on $\mathsf{P}\mathbf{Eq}$
generated by a subclass of $\mathbf{F}$-algebras $\mathcal{K}$, we say the
logic on $\mathsf{P}\mathbf{F}$ is _algebraisable_ , and it is _algebraised by
$\mathcal{K}$_. There are already many examples of algebraisable systems
presented in the literature, see [2] for instance. Most of these examples,
though not formulated in our categorical framework, can be easily seen to
still be algebraisable in our extended sense. We do not further pursue any
concrete examples here, but end with a discussion of how the fore mentioned
Lindenbaum-Tarski algebra construction understood in our categorical framework
can be seen to induce an algebraisation of certain logics.

##  6\. Projective Objects and Algebraisation

In this section we provide a detailed study of an important theorem proved in
[2] that characterises when algebraisation is available for general concrete
logical systems. The theorem says that a concrete logical system with
consequence relation $\operatorname{\vdash}$ is algebraisable by some class of
algebras, with the induced consequence relation $\vDash$ on pairs of formulas,
if, and only if the induced lattice of theories
$\mathrm{Th}_{\operatorname{\vdash}}$ is isomorphic to the lattice of theories
$\mathrm{Th}_{\vDash}$, such that the isomorphism commutes with inverse
substitutions. Our approach extends [5] as a more general categorical study of
the characterisation of algebraisation, and provides a more general result.

Let’s first recall the definition of a projective objects in a category. In
any category $\mathcal{C}$, $P$ is projective if and only if for any
epimorphism $q:A\twoheadrightarrow B$ and any morphism $s:P\to B$, there
exists a lift of $s$ along $q$,

${A}$${P}$${B}$$\scriptstyle{q}$$\scriptstyle{\exists}$$\scriptstyle{s}$

making the above diagramme commute. In other words, the Hom-functor
$\mathcal{C}(P,-)$ preserves epimorphisms. The fact that $\mathsf{P}$ is the
free suplattice functor plays an essential role in the following result.

######  Lemma 6.1.

The functor $\mathsf{P}\circ(-)$ from $[\mathbf{Set},\mathbf{Set}]$ to
$[\mathbf{Set},\mathbf{SupL}]$ preserves projective elements. In other worlds,
for any endo-functor $T:\mathbf{Set}\to\mathbf{Set}$, if $T$ is projective in
$[\mathbf{Set},\mathbf{Set}]$ then $\mathsf{P}T$ is projective in
$[\mathbf{Set},\mathbf{SupL}]$.

###### Proof.

Suppose $T$ is projective in $[\mathbf{Set},\mathbf{Set}]$, and
$q:\mathcal{A}\twoheadrightarrow\mathcal{B}$ is a surjection in
$[\mathbf{Set},\mathbf{SupL}]$. Let $a$ be any morphism
$a:\mathsf{P}T\to\mathcal{B}$. We know that
$U_{\mathbf{P}}q:A\twoheadrightarrow B$ is a surjection in $\mathbf{Set}$;
since $T$ is projective, it follows that there exists $l$ making the following
diagramme commute,

${T}$${A}$${\mathbf{P}T}$${B}$$\scriptstyle{l}$$\scriptstyle{\eta_{\mathbf{P}}\circ\operatorname{id}_{T}}$$\scriptstyle{U_{\mathbf{P}}q}$$\scriptstyle{U_{\mathbf{P}}a}$

Now we know that $\mathsf{P}$ is the free suplattice functor. Hence, for any
set $X$, the function $l_{X}:TX\to AX$ will induces a unique suplattice
morphism

$\widetilde{l_{X}}=\mathbf{P}l_{X}\fatsemi A_{X}:\mathbf{P}TX\to AX,$

such that $A_{X}:\mathbf{P}AX\to AX$ is the $\mathbf{P}$-algebra structure
corresponding to the suplattice $\mathcal{A}X$. We first show the naturality
of this construction. For any function $f:X\to Y$,

$\widetilde{l_{X}}\fatsemi Af=\mathbf{P}l_{X}\fatsemi A_{X}\fatsemi
Af=\mathbf{P}l_{X}\fatsemi\mathbf{P}Af\fatsemi
A_{Y}=\mathbf{P}Tf\fatsemi\mathbf{P}l_{Y}\fatsemi
A_{Y}=\mathbf{P}Tf\fatsemi\widetilde{l_{Y}}.$

We have the second equality because $Af$ is a $\mathbf{P}$-algebra morphism;
the third equality is due to naturality of $l$. It follows that we then have a
natural transformation $\widetilde{l}:\mathbf{P}T\to A$, such that each
component $\widetilde{l}_{X}$ is given by $\widetilde{l_{X}}$, and
$\widetilde{l}_{X}$ is furthermore a suplattice morphism. It then follows that
we now have a morphism in $[\mathbf{Set},\mathbf{SupL}]$, whose underlying
functor is $\widetilde{l}$. We finally need to verify that $\widetilde{l}$ is
indeed a lift of $a$, and we can verify this at the level of underlying set.
According to our definition, for any set $X$ we have

$\displaystyle\widetilde{l}_{X}\fatsemi(U_{\mathbf{P}}q)_{X}$
$\displaystyle=\mathbf{P}l_{X}\fatsemi A_{X}\fatsemi(U_{\mathbf{P}}q)_{X}$
$\displaystyle=\mathbf{P}l_{X}\fatsemi\mathbf{P}(U_{\mathbf{P}}q)_{X}\fatsemi
B_{X}$
$\displaystyle=\mathbf{P}\eta_{\mathbf{P},TX}\fatsemi\mathbf{P}(U_{\mathbf{P}}a)_{X}\fatsemi
B_{X}$
$\displaystyle=\mathbf{P}\eta_{\mathbf{P},TX}\fatsemi\mu_{\mathbf{P},X}\fatsemi(U_{\mathbf{P}}a)_{X}$
$\displaystyle=(U_{\mathbf{P}}a)_{X}$

The first equality holds by definition of $\widetilde{l}_{X}$; the second
holds due to the fact that $q_{X}$ is a morphism between suplattices; the
third holds because $l$ is a lifting of
$\eta_{\mathbf{P}}\circ\operatorname{id}_{T}\fatsemi U_{\mathbf{P}}a$ along
$U_{\mathbf{P}}q$; the fourth is again because $a_{X}$ is a morphism between
suplattices and the $\mathbf{P}$-algebra structure on the free suplattice
$\mathsf{P}T$ is given by $\mu_{\mathbf{P},X}$; the final equality holds due
to the triangular identity of the power set monad. Such a computation shows
that we indeed have a lift of $a$ along $q$. Thus, $\mathsf{P}T$ is also
projective in $[\mathbf{Set},\mathbf{SupL}]$. ∎

Lemma 6.1 implies that to show a functor $\mathsf{P}T$ is projective in
$[\mathbf{Set},\mathbf{SupL}]$, it is enough to show that $T$ is projective in
$[\mathbf{Set},\mathbf{Set}]$. A very important class of projective objects in
$[\mathbf{Set},\mathbf{Set}]$ are polynomial functors. It is well-known in the
literature that polynomial functors are projective. For sake of completeness
we provide the proof here. We first show that representable functors are
projective.

######  Lemma 6.2.

Any representable functor $\mathsf{y}^{X}$ in $[\mathbf{Set},\mathbf{Set}]$
for any set $X$ is projective.

###### Proof.

By Yoneda lemma, a morphism $a:\mathsf{y}^{X}\to A$ is the same as an element
in $A(X)$. Given any surjection $q:A\twoheadrightarrow B$ and any morphism
$s:\mathsf{y}^{X}\to B$, or equivalently $s\in B(X)$, by surjectivity we can
find an element $t\in A(X)$ such that $q_{X}(t)=s$. By Yoneda again, it
follows that the following diagramme commutes,

${A}$${\mathsf{y}^{X}}$${B}$$\scriptstyle{q}$$\scriptstyle{t}$$\scriptstyle{s}$

Thus, $\mathsf{y}^{X}$ is projective. ∎

It is also well-known that arbitrary coproducts of projective objects is again
projective.

######  Lemma 6.3.

If $P_{i}$ is projective for any $i\in I$, then if the coproducts $\sum_{i\in
I}P_{i}$ exists, $\sum_{i\in I}P_{i}$ is also projective.

###### Proof.

Given an epimorphism $q:A\to B$, a morphism from $\sum_{i\in I}P_{i}\to B$ is
of the form

$[(f_{i})_{i\in I}]:\sum_{i\in I}P_{i}\to B,$

with each $f_{i}:P_{i}\to B$. Now since $P_{i}$ is projective, there exists a
lift $l_{i}:P_{i}\to A$ such that

$l_{i}\fatsemi q=f_{i}.$

Hence, we can construct the lift for $[(f_{i})_{i\in I}]$ as $[(l_{i})_{i\in
I}]$, which implies

$[(l_{i})_{i\in I}]\fatsemi q=[(l_{i}\fatsemi q)_{i\in I}]=[(f_{i})_{i\in
I}].$

Thus $\sum_{i\in I}P_{i}$ is also projective. ∎

######  Corollary 6.4.

All polynomial functors in $[\mathbf{Set},\mathbf{Set}]$ are projective.

###### Proof.

By definition, polynomial functors in $[\mathbf{Set},\mathbf{Set}]$ are
exactly coproducts of representable functors in $[\mathbf{Set},\mathbf{Set}]$.
∎

Recall in Remark 2.4 we’ve mentioned that the syntactic monad $\mathbf{F}$ is
a free monad on a polynomial functor $H$, which makes itself a polynomial
monad. Explicitly, the polynomial functor $H$ is given by

$H=\sum_{\star\in\Sigma}\mathsf{y}^{\mathsf{ar}(\star)}.$

We can also see more directly that $\mathbf{F}$ is a polynomial functor, since
by definition it can be described as the following coproduct

$\mathbf{F}\cong\mathsf{y}+H+H\circ H+\cdots.$

For any set $X$, $HX$ can be identified as the set of all terms of the form
$\star(x_{1},\cdots,x_{n})$, with $\star\in\Sigma$ and $x_{1},\cdots,x_{n}\in
X$. Hence, the set of all formulas, or $\Sigma$-terms, $\mathbf{F}X$ is then
naturally identified as follows

$\mathbf{F}X\cong X+HX+HHX+\cdots.$

Since the full subcategory $\mathbf{Poly}$ of polynomial functors in
$[\mathbf{Set},\mathbf{Set}]$ is closed under products, coproducts and
compositions (see [15]), it follows that $\mathbf{F}$ is indeed a polynomial
functor, and so does $\mathbf{Eq}$, or more generally the functor
$\mathbf{Seq}_{n,m}\cong\mathbf{F}^{n}\times\mathbf{F}^{m}$ that encodes
$(n,m)$-sequents of formulas. Hence, By Corollary 6.4, $\mathbf{F}$, as well
as $\mathbf{Eq}$ and $\mathbf{Seq}_{n,m}$, is projective in
$[\mathbf{Set},\mathbf{Set}]$; and further by Lemma 6.1 it follows that
$\mathsf{P}\mathbf{F}$ is also projective in $[\mathbf{Set},\mathbf{SupL}]$.

If $\mathcal{P}$ is a projective object in $[\mathbf{Set},\mathbf{SupL}]$,
then given any quotients $q_{1}:\mathcal{P}\twoheadrightarrow\mathcal{Q}$ and
$q_{2}:\mathcal{A}\twoheadrightarrow\mathcal{B}$, if we have a morphism
$\rho:\mathcal{Q}\to\mathcal{B}$, then by projectivity of $\mathcal{P}$ it
follows that there must be a lifting of $q_{1}\fatsemi\rho$ along $q_{2}$,
viz. a morphism $\tau$ making the following diagramme commute,

${\mathcal{P}}$${\mathcal{A}}$${\mathcal{Q}}$${\mathcal{B}}$$\scriptstyle{q_{1}}$$\scriptstyle{\tau}$$\scriptstyle{q_{2}}$$\scriptstyle{\rho}$

This implies that once we have a morphism $\rho$ from $\mathcal{Q}$ to
$\mathcal{B}$, we are guaranteed to find a morphism
$\tau:\mathcal{P}\to\mathcal{A}$, making the above diagramme a morphism in
$\mathbf{Quo}$. Furthermore, if both quotients are quotients of projective
objects, then we have the following corollary of equivalence of consequence
relations.

######  Corollary 6.5.

For quotients $q_{1}:\mathcal{P}_{1}\twoheadrightarrow\mathcal{Q}_{1}$,
$q_{2}:\mathcal{P}_{2}\twoheadrightarrow\mathcal{Q}_{2}$ with
$\mathcal{P}_{1},\mathcal{P}_{2}$ being projective in
$[\mathbf{Set},\mathbf{SupL}]$, they are equivalent as consequence relations
if, and only if $\mathcal{Q}_{1}$ and $\mathcal{Q}_{2}$ are isomorphic.

###### Proof.

The only if direction is easy. Suppose $\mathcal{Q}_{1}$ and $\mathcal{Q}_{2}$
are isomorphic with the isomorphism
$\rho:\mathcal{Q}_{1}\cong\mathcal{Q}_{2}$, then by projectivity of
$\mathcal{P}_{1},\mathcal{P}_{2}$, there exists morphisms
$\tau:\mathcal{P}_{1}\rightleftarrows\mathcal{P}_{2}:\delta$, such that

$\tau\fatsemi q_{2}=q_{1}\fatsemi\rho,\quad\delta\fatsemi
q_{1}=q_{2}\fatsemi\rho^{-1}.$

By definition, it follows that the two consequence relations are equivalent. ∎

## References

  * Blok and Jónsson, [2006] Blok, W. J. and Jónsson, B. (2006).  Equivalence of consequence operations.  Studia Logica, 83(1):91–110.
  * Blok and Pigozzi, [1989] Blok, W. J. and Pigozzi, D. (1989).  Algebraizable logics, volume 77.  American Mathematical Soc.
  * Borceux, [1994] Borceux, F. (1994).  Handbook of categorical algebra: volume 1, Basic category theory, volume 1.  Cambridge University Press.
  * Borceux, [2005] Borceux, Francis, J. G. Z. K. G. M. (2005).  Internal object actions.  Commentationes Mathematicae Universitatis Carolinae, 46(2):235–255.
  * Galatos and Tsinakis, [2009] Galatos, N. and Tsinakis, C. (2009).  Equivalence of consequence relations: an order-theoretic and categorical perspective.  The Journal of Symbolic Logic, 74(3):780–810.
  * Gambino and Kock, [2013] Gambino, N. and Kock, J. (2013).  Polynomial functors and polynomial monads.  In Mathematical proceedings of the cambridge philosophical society, volume 154, pages 153–192. Cambridge University Press.
  * Halbach and Leigh, [2021] Halbach, V. and Leigh, G. (2021).  The road to paradox: A guide to syntax, truth, and modality.  To be published.
  * Hyland and Power, [2007] Hyland, M. and Power, J. (2007).  The category theoretic understanding of universal algebra: Lawvere theories and monads.  Electronic Notes in Theoretical Computer Science, 172:437–458.
  * Johnstone, [1975] Johnstone, P. T. (1975).  Adjoint lifting theorems for categories of algebras.  Bulletin of the London Mathematical Society, 7(3):294–297.
  * Johnstone, [1982] Johnstone, P. T. (1982).  Stone spaces, volume 3.  Cambridge university press.
  * Joyal and Tierney, [1984] Joyal, A. and Tierney, M. (1984).  An extension of the Galois theory of Grothendieck, volume 309.  American Mathematical Soc.
  * Kelly, [1980] Kelly, G. M. (1980).  A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on.  Bulletin of the Australian Mathematical Society, 22(1):1–83.
  * Mac Lane, [2013] Mac Lane, S. (2013).  Categories for the working mathematician, volume 5.  Springer Science & Business Media.
  * Manes, [2003] Manes, E. (2003).  Monads of sets.  In Handbook of algebra, volume 3, pages 67–153. Elsevier.
  * Spivak and Nelson, [2021] Spivak, D. and Nelson, N. (2021).  Polynomial Functors: A General Theory of Interaction.  Topos Institute.  Sept. 8th version.
  * Tarski, [1928] Tarski, A. (1928).  Remarques sur les notions fondamentales de la méthodologie des mathématiques.  In Annales de la Société Polonaise de Mathématique, volume 7, pages 270–272.