Cintula, Petr Metcalfe, George Metcalfe, George ††thanks: The first author was
supported by RVO 67985807 and Czech Science Foundation grant GA22-01137S, and
the second two authors by Swiss National Science Foundation grant
200021_215157. This project has also received funding from the European
Union’s Horizon 2020 research and innovation programme under the Marie
Skłodowska-Curie grant agreement No 101007627.

# One-variable fragments of first-order logics

Petr Cintula  Institute of Computer Science
Czech Academy of Sciences
Prague, Czech Republic<EMAIL_ADDRESS>George Metcalfe  Mathematical
Institute
University of Bern
Bern, Switzerland<EMAIL_ADDRESS>Naomi Tokuda  Mathematical
Institute
University of Bern
Bern, Switzerland<EMAIL_ADDRESS>
###### Abstract

The one-variable fragment of a first-order logic may be viewed as an “S5-like”
modal logic, where the universal and existential quantifiers are replaced by
box and diamond modalities, respectively. Axiomatizations of these modal
logics have been obtained for special cases — notably, the modal counterparts
$\mathrm{S5}$ and $\mathrm{MIPC}$ of the one-variable fragments of first-order
classical logic and intuitionistic logic — but a general approach, extending
beyond first-order intermediate logics, has been lacking. To this end, a
sufficient criterion is given in this paper for the one-variable fragment of a
semantically-defined first-order logic — spanning families of intermediate,
substructural, many-valued, and modal logics — to admit a natural
axiomatization. More precisely, such an axiomatization is obtained for the
one-variable fragment of any first-order logic based on a variety of algebraic
structures with a lattice reduct that has the superamalgamation property,
building on a generalized version of a functional representation theorem for
monadic Heyting algebras due to Bezhanishvili and Harding. An alternative
proof-theoretic strategy for obtaining such axiomatization results is also
developed for first-order substructural logics that have a cut-free sequent
calculus and admit a certain interpolation property.

###### keywords:

First-Order Logic, One-Variable Fragment, Modal Logic, Substructural Logic,
Superamalgamation, Sequent Calculus.

##  1 Introduction

The one-variable fragment of any standard first-order logic — intermediate,
substructural, many-valued, modal, or otherwise — consists of consequences in
the logic constructed using one distinguished variable $x$, unary relation
symbols, propositional connectives, and the quantifiers $(\forall{x})$ and
$(\exists{x})$. Such a fragment may be conveniently reformulated as a
propositional modal logic by replacing occurrences of an atom $P(x)$ with a
propositional variable $p$, and occurrences of $(\forall{x})$ and
$(\exists{x})$ with $\Box$ and $\Diamond$, respectively. Typically, this modal
logic is algebraizable — that is, it enjoys soundness and completeness with
respect to some suitable class of algebraic structures – and hence, unlike the
full first-order logic, can be studied using the tools of universal algebra.

Any standard semantics for a first-order logic, where quantifiers range over
domains of models, yields a relational semantics for the one-variable
fragment. On the other hand, a Hilbert-style axiomatization does not (at least
directly) yield an axiomatization for the fragment, since a derivation of a
one-variable formula may involve additional variables. Axiomatizations are
well known for the modal counterparts $\mathrm{S5}$ [Hal55] and
$\mathrm{MIPC}$ [MV57, Bul66] of the one-variable fragments of first-order
classical logic and intuitionistic logic, respectively, and similar results
have been obtained for modal counterparts of one-variable fragments of other
first-order intermediate logics [OS88, Suz89, Suz90, Bez98, BH02, CR15,
CMRR17, CMRT22] and many-valued logics [Rut59, dNG04, CCVR20, MT20]. However,
a general approach to axiomatizing one-variable fragments of first-order
logics has, until now, been lacking.111A precursor to this paper, reporting
preliminary results restricted to a smaller class of logics, was published in
the proceedings of AiML 2022 [CMT22].

In this paper, we address the aforementioned axiomatization problem for a
broad family of semantically-defined first-order logics. First, in Section 2,
we introduce (one-variable) first-order logics based on models defined over
classes of $\mathcal{L}$-lattices: structures for an algebraic signature
$\mathcal{L}$ that have a lattice reduct. In particular, first-order
intermediate and substructural logics can be defined over classes of Heyting
algebras and $\mathsf{FL_{e}}$-algebras, respectively. For the sake of
generality (e.g., when $\mathcal{L}$-lattices are just lattices), consequence
is defined over equations between first-order formulas; however, this often —
in particular, for intermediate and substructural logics — corresponds to the
usual notion of consequence between formulas.

In Section 3, we introduce potential axiomatizations for consequence in the
modal counterparts of the one-variable fragments of these semantically-defined
first-order logics. We define an m-$\mathcal{L}$-lattice to be an
$\mathcal{L}$-lattice expanded with modalities $\Box$ and $\Diamond$
satisfying certain equations familiar from modal logic, and given any class
$\mathsf{K}$ of $\mathcal{L}$-lattices, let $\mathsf{mK}$ denote the class of
m-$\mathcal{L}$-lattices with an $\mathcal{L}$-lattice reduct in $\mathsf{K}$.
For example, if $\mathsf{K}$ is a variety of Heyting algebras, then
$\mathsf{mK}$ is a variety of monadic Heyting algebras in the sense of [MV57].
We then show that m-$\mathcal{L}$-lattices are in one-to-one correspondence
with $\mathcal{L}$-lattices equipped with a subalgebra satisfying a relative
completeness condition, generalizing previous results in the literature (see,
e.g., [Bez98, Tuy21]). We also show that if $\mathsf{K}$ is any class of
$\mathcal{L}$-lattices closed under taking subalgebras and direct powers (in
particular, any variety), then consequence in the one-variable fragment of the
first-order logic defined over $\mathsf{K}$ corresponds to consequence in the
functional members of $\mathsf{mK}$: m-$\mathcal{L}$-lattices consisting of
functions from a set $W$ to an $\mathcal{L}$-lattice
$\mathbf{A}\in\mathsf{K}$.

In Section 4, we close the circle, obtaining an axiomatization of consequence
in the one-variable fragment of any first-order logic defined over a variety
of $\mathcal{L}$-lattices that has the superamalgamation property: a well-
studied algebraic property equivalent in some cases to Craig interpolation for
the associated logic. That is, we show that for such a variety $\mathsf{V}$,
every member of $\mathsf{mV}$ is functional — generalizing Bezhanishvili and
Harding’s representation theorem for monadic Heyting algebras [BH02] — and
hence that the defining equations for $\mathsf{mV}$ provide the desired
axiomatization. As a consequence, we obtain axiomatizations of the one-
variable fragments of a broad range of first-order logics, including the seven
consistent first-order intermediate logics admitting Craig interpolation,
first-order extensions of substructural logics such as $\mathsf{FL_{e}}$,
$\mathsf{FL_{ew}}$, and $\mathsf{FL_{ec}}$, a first-order lattice logic, and a
first-order version of the modal logic $\mathrm{K}$.

In Section 5, we present an alternative proof-theoretic strategy for
establishing completeness of an axiomatization for the one-variable fragment
of a first-order logic, the key idea being to show that additional variables
can be eliminated from derivations of one-variable formulas in a suitable
sequent calculus. As a concrete example, we obtain a new completeness proof
for the one-variable fragment of the first-order version of the substructural
logic $\mathrm{FL_{e}}$ by establishing an interpolation property for
derivations in a cut-free sequent calculus. We then explain how the proof
generalizes to a family of first-order substructural logics, including
$\mathrm{FL_{ew}}$, $\mathrm{FL_{ec}}$, and $\mathrm{FL_{ewc}}$
(intuitionistic logic). Finally, in Section 6, we discuss the limitations of
the methods described in the paper and potential extensions to broader
families of first-order logics.

##  2 A family of first-order logics

Let $\mathcal{L}$ be any algebraic signature, and let $\mathcal{L}_{n}$ denote
the set of operation symbols of $\mathcal{L}$ of arity $n\in\mathbb{N}$. We
will assume throughout this paper that $\mathcal{L}_{2}$ contains distinct
symbols $\land$ and $\lor$, referring to such a signature as lattice-oriented.

We call an algebraic structure
$\mathbf{A}=\langle{A,\\{\mathop{\star}^{\mathbf{A}}\mid
n\in\mathbb{N},\,\mathop{\star}\in\mathcal{L}_{n}\\}}\rangle$ an
$\mathcal{L}$-lattice if $\mathop{\star}^{\mathbf{A}}$ is an $n$-ary operation
on $A$ for each $\mathop{\star}\in\mathcal{L}_{n}$ ($n\in\mathbb{N}$), and
$\langle{A,\land^{\mathbf{A}},\lor^{\mathbf{A}}}\rangle$ is a lattice with
respect to the induced order $x\leq^{\mathbf{A}}y:\Longleftrightarrow
x\land^{\mathbf{A}}y=x$. As usual, superscripts will be omitted when these are
clear from the context.

######  Example 2.1.

Let $\mathcal{L}_{s}$ be the lattice-oriented signature with binary operation
symbols $\land$, $\lor$, $\cdot$, and $\to$, and constant symbols ${\rm f}$
and ${\rm e}$. An $\mathsf{FL_{e}}$-algebra — also referred to as a
commutative pointed residuated lattice — is an $\mathcal{L}_{s}$-lattice
$\mathbf{A}=\langle{A,\land,\lor,\cdot,\to,{\rm f},{\rm e}}\rangle$ such that
$\langle{A,\cdot,{\rm e}}\rangle$ is a commutative monoid and $\to$ is the
residuum of $\cdot$, that is, $a\cdot b\leq c\iff a\leq b\to c$, for all
$a,b,c\in~{}A$. The class of $\mathsf{FL_{e}}$-algebras forms a variety
$\mathsf{FL_{e}}$ that provides algebraic semantics for the full Lambek
calculus with exchange $\mathrm{FL_{e}}$ — also known as multiplicative
additive intuitionistic linear logic without additive constants (see, e.g.,
[GJKO07, MPT23]). Algebraic semantics for other well-known substructural
logics are provided by various subvarieties of $\mathsf{FL_{e}}$; in
particular,

  1. $\bullet$

the full Lambek calculus with exchange and weakening $\mathrm{FL_{ew}}$, and
full Lambek calculus with exchange and contraction $\mathrm{FL_{ec}}$,
correspond to the varieties $\mathsf{FL_{ew}}$ and $\mathsf{FL_{ec}}$ of
$\mathsf{FL_{e}}$-algebras satisfying the equations ${\rm f}\leq x\leq{\rm
e}$, and $x\leq x\cdot x$, respectively;

  2. $\bullet$

intuitionistic logic $\mathrm{IL}$ corresponds to the variety $\mathsf{HA}$ of
Heyting algebras, term-equivalent to
$\mathsf{FL_{ewc}}=\mathsf{FL_{ew}}\cap\mathsf{FL_{ec}}$ (just identify
$\cdot$ and $\land$);

  3. $\bullet$

classical logic $\mathrm{CL}$ and Gödel logic $\mathrm{G}$ correspond to the
varieties $\mathsf{BA}$ of Boolean algebras, and $\mathsf{GA}$ of Gödel
algebras, axiomatized relative to $\mathsf{HA}$ by the equations $(x\to{\rm
f})\to{\rm f}\approx x$ and $(x\to y)\lor(y\to x)\approx{\rm e}$,
respectively;

  4. $\bullet$

Łukasiewicz logic Ł corresponds to the variety $\mathsf{MV}$ of MV-algebras,
term-equivalent to the variety of $\mathsf{FL_{ew}}$-algebras satisfying
$(x\to y)\to y\approx x\lor y$.

Full first-order logics can be defined over an arbitrary predicate language
with formulas built using propositional connectives in the algebraic signature
$\mathcal{L}$ (see, e.g., [CN21, Section 7.1]). However, for the purposes of
this paper it suffices to restrict our attention to the one-variable setting
with a fixed (generic) predicate language. Let ${\rm
Fm}_{\forall}^{1}(\mathcal{L})$ denote the set of one-variable
$\mathcal{L}$-formulas $\varphi,\psi,\dots$, built inductively as usual from a
countably infinite set of unary predicates $\\{P_{i}\\}_{i\in\mathbb{N}}$, a
distinguished variable $x$, connectives in $\mathcal{L}$, and quantifiers
$\forall,\exists$. We also call an ordered pair of one-variable
$\mathcal{L}$-formulas $\varphi,\psi\in{\rm Fm}_{\forall}^{1}(\mathcal{L})$,
written $\varphi\approx\psi$, an ${\rm
Fm}_{\forall}^{1}(\mathcal{L})$-equation, and let $\varphi\leq\psi$ denote
$\varphi\land\psi\approx\varphi$.222Let us emphasize that an ${\rm
Fm}_{\forall}^{1}(\mathcal{L})$-equation $\varphi\approx\psi$ is a primitive
syntactic object that relates two formulas and not terms. In some settings
(e.g., first-order substructural logics), $\varphi\approx\psi$ can be replaced
by a formula such as $\varphi\leftrightarrow\psi$ and semantical consequence
can be defined between formulas, but this is not always the case.

Now let $\mathbf{A}$ be any $\mathcal{L}$-lattice, let $S$ be a non-empty set,
and let $\mathcal{I}(P_{i})$ be a map from $S$ to $A$ for each
$i\in\mathbb{N}$, writing $u\mapsto f(u)$ to denote a map assigning to each
$u\in S$ some $f(u)\in A$. We call the ordered pair
${\mathfrak{{S}}}=\langle{S,\mathcal{I}}\rangle$ an $\mathbf{A}$-structure if
the following inductively defined partial map
$\left\|{\cdot}\right\|^{\mathfrak{{S}}}\colon{\rm
Fm}_{\forall}^{1}(\mathcal{L})\to A^{S}$ is total:

$\displaystyle\left\|{P_{i}(x)}\right\|^{\mathfrak{{S}}}$
$\displaystyle=\mathcal{I}(P_{i})\quad$ $\displaystyle i\in\mathbb{N}$
$\displaystyle\left\|{\mathop{\star}(\varphi_{1},\dots,\varphi_{n})}\right\|^{\mathfrak{{S}}}$
$\displaystyle=u\mapsto{\mathop{\star}}^{\mathbf{A}}\big{(}\left\|{\varphi_{1}}\right\|^{\mathfrak{{S}}}(u)\,\dots,\,\left\|{\varphi_{n}}\right\|^{\mathfrak{{S}}}(u)\big{)}\quad$
$\displaystyle n\in\mathbb{N},\mathop{\star}\in\mathcal{L}_{n}$
$\displaystyle\left\|{(\forall{x})\varphi}\right\|^{\mathfrak{{S}}}$
$\displaystyle=u\mapsto\bigwedge\big{\\{}\left\|{\varphi}\right\|^{{\mathfrak{{S}}}}(v)\mid
v\in S\big{\\}}$
$\displaystyle\left\|{(\exists{x})\varphi}\right\|^{\mathfrak{{S}}}$
$\displaystyle=u\mapsto\bigvee\big{\\{}\left\|{\varphi}\right\|^{{\mathfrak{{S}}}}(v)\mid
v\in S\big{\\}}.$

If $\mathbf{A}$ is complete — that is, $\bigwedge X$ and $\bigvee X$ exist in
$A$, for all $X\subseteq A$ — then
${\mathfrak{{S}}}=\langle{S,\mathcal{I}}\rangle$ is always an
$\mathbf{A}$-structure; otherwise, whether or not the partial map
$\left\|{\cdot}\right\|^{\mathfrak{{S}}}$ is total depends on $\mathcal{I}$.
E.g., for $\mathbf{A}=\langle{\mathbb{N},\min,\max}\rangle$ and
$S=\mathbb{N}$, if $\mathcal{I}(P_{0})(n)\coloneqq n$, for all
$n\in\mathbb{N}$, then
$\left\|{(\exists{x})P_{0}(x)}\right\|^{\mathfrak{{S}}}$ is undefined, but if
$\mathcal{I}(P_{i})(n)\leq K$ for all $i\in\mathbb{N}$ and $n\in S$, for some
fixed $K\in\mathbb{N}$, then ${\mathfrak{{S}}}$ is an $\mathbf{A}$-structure.

We say that an ${\rm Fm}_{\forall}^{1}(\mathcal{L})$-equation
$\varphi\approx\psi$ is valid in an $\mathbf{A}$-structure ${\mathfrak{{S}}}$,
and write ${\mathfrak{{S}}}\models\varphi\approx\psi$, if
$\left\|{\varphi}\right\|^{\mathfrak{{S}}}=\left\|{\psi}\right\|^{\mathfrak{{S}}}$.
More generally, consider any class of $\mathcal{L}$-lattices $\mathsf{K}$. We
say that an ${\rm Fm}_{\forall}^{1}(\mathcal{L})$-equation
$\varphi\approx\psi$ is a (sentential) semantical consequence of a set of
${\rm Fm}_{\forall}^{1}(\mathcal{L})$-equations $T$ in $\mathsf{K}$, and write
$T\vDash^{\forall}_{\mathsf{K}}\varphi\approx\psi$, if for any
$\mathbf{A}\in\mathsf{K}$ and $\mathbf{A}$-structure ${\mathfrak{{S}}}$,

$\displaystyle{\mathfrak{{S}}}\models\varphi^{\prime}\approx\psi^{\prime}\text{,
for all }\varphi^{\prime}\approx\psi^{\prime}\in
T\enspace\Longrightarrow\enspace{\mathfrak{{S}}}\models\varphi\approx\psi.$

In certain cases, we can restrict attention to the complete members of
$\mathsf{K}$. Let us say that $\mathsf{K}$ admits regular completions if, for
any $\mathbf{A}\in\mathsf{K}$, there exists an $\mathcal{L}$-lattice embedding
$h$ of $\mathbf{A}$ into a complete member $\mathbf{B}$ of $\mathsf{K}$ that
preserves all existing meets and joins, noting that for any
$\mathbf{A}$-structure ${\mathfrak{{S}}}=\langle{S,\mathcal{I}}\rangle$, the
$\mathbf{B}$-structure
${\mathfrak{{S}}}^{h}=\langle{S,\mathcal{I}^{h}}\rangle$, with
$\mathcal{I}^{h}(P_{i})\coloneqq h\circ\mathcal{I}(P_{i})$ for each $i\in I$,
satisfies
$\left\|{\varphi}\right\|^{{\mathfrak{{S}}}^{h}}=h\circ\left\|{\varphi}\right\|^{{\mathfrak{{S}}}}$
for each $\varphi\in{\rm Fm}_{\forall}^{1}(\mathcal{L})$. Clearly, semantical
consequence in such a class $\mathsf{K}$ coincides with semantical consequence
in the class of complete members of $\mathsf{K}$.

######  Example 2.2.

A sufficient, but by no means necessary, condition for a class of
$\mathcal{L}$-lattices to admit regular completions is closure under MacNeille
completions (see, e.g., [Har08]). This is the case in particular for
$\mathsf{BA}$ and $\mathsf{HA}$; indeed, they are the only non-trivial
varieties of Heyting algebras that have this property [BH04]. A broad family
of varieties of $\mathsf{FL_{e}}$-algebras — including $\mathsf{FL_{e}}$,
$\mathsf{FL_{ew}}$, and $\mathsf{FL_{ec}}$ — are also closed under MacNeille
completions (see, e.g., [CGT12]), and for a still broader family — including
$\mathsf{GA}$ — this is true for the class of their subdirectly irreducible
members [CGT11]. Note, however, that in some cases — e.g., $\mathsf{MV}$
[GP02] — neither the variety nor the class of its subdirectly irreducible
members admits regular completions.

Next, let us denote by ${\rm Fm}_{\Box}(\mathcal{L})$ the set of propositional
formulas $\alpha,\beta,\dots$ built inductively as usual from a countably
infinite set of propositional variables $\\{p_{i}\\}_{i\in\mathbb{N}}$,
connectives in $\mathcal{L}$, and unary connectives $\Box$ and $\Diamond$, and
call an ordered pair of formulas $\alpha,\beta\in{\rm
Fm}_{\Box}(\mathcal{L})$, written $\alpha\approx\beta$, an ${\rm
Fm}_{\Box}(\mathcal{L})$-equation. The (standard) translation functions
$({-})^{\ast}$ and $({-})^{\circ}$ between ${\rm
Fm}_{\forall}^{1}(\mathcal{L})$ and ${\rm Fm}_{\Box}(\mathcal{L})$ are defined
inductively by

$\displaystyle(P_{i}(x))^{\ast}$ $\displaystyle=p_{i}$ $\displaystyle
p_{i}^{\circ}$ $\displaystyle=P_{i}(x)$ $\displaystyle i\in\mathbb{N}$
$\displaystyle(\mathop{\star}(\varphi_{1},\dots,\varphi_{n}))^{\ast}$
$\displaystyle=\mathop{\star}(\varphi^{\ast}_{1},\dots,\varphi^{\ast}_{n})\ \
$ $\displaystyle(\mathop{\star}(\alpha_{1},\dots,\alpha_{n}))^{\circ}$
$\displaystyle=\mathop{\star}(\alpha^{\circ}_{1},\dots,\alpha^{\circ}_{n})$
$\displaystyle\mathop{\star}\in\mathcal{L}_{n}$
$\displaystyle((\forall{x})\varphi)^{\ast}$ $\displaystyle=\Box\varphi^{\ast}$
$\displaystyle(\Box\alpha)^{\circ}$ $\displaystyle=(\forall{x})\alpha^{\circ}$
$\displaystyle((\exists{x})\varphi)^{\ast}$
$\displaystyle=\Diamond\varphi^{\ast}$ $\displaystyle(\Diamond\alpha)^{\circ}$
$\displaystyle=(\exists{x})\alpha^{\circ},$

and lift in the obvious way to (sets of) ${\rm
Fm}_{\forall}^{1}(\mathcal{L})$-equations and ${\rm
Fm}_{\Box}(\mathcal{L})$-equations.

Clearly, $(\varphi^{\ast})^{\circ}=\varphi$ for any $\varphi\in{\rm
Fm}_{\forall}^{1}(\mathcal{L})$ and $(\alpha^{\circ})^{\ast}=\alpha$ for any
$\alpha\in{\rm Fm}_{\Box}(\mathcal{L})$, and we may therefore switch between
first-order and modal notations as convenient. Indeed, to achieve our goal of
axiomatizing consequence in the one-variable first-order logic based on a
class of $\mathcal{L}$-lattices $\mathsf{K}$, it suffices to find a (natural)
axiomatization of a variety $\mathsf{V}$ of algebras in the signature of
$\mathcal{L}$ expanded with $\Box,\Diamond$ such that
$\vDash^{\forall}_{\mathsf{K}}$ corresponds to equational consequence in
$\mathsf{V}$. More precisely, let us call a homomorphism from the formula
algebra with universe ${\rm Fm}_{\Box}(\mathcal{L})$ to
$\mathbf{A}\in\mathsf{V}$ an $\mathbf{A}$-evaluation, and define for any set
$\mathrm{\Sigma}\cup\\{\alpha\approx\beta\\}$ of ${\rm
Fm}_{\Box}(\mathcal{L})$-equations,

$\displaystyle\mathrm{\Sigma}\vDash_{\mathsf{V}}\alpha\approx\beta\>:\Longleftrightarrow\enspace$
$f(\alpha)=f(\beta)$, for every $\mathbf{A}\in\mathsf{V}$ and
$\mathbf{A}$-evaluation $f$ satisfying $f(\alpha^{\prime})=f(\beta^{\prime})$
for all $\alpha^{\prime}\approx\beta^{\prime}\in\mathrm{\Sigma}$.

Our goal is to provide a (natural) axiomatization of a variety $\mathsf{V}$
such that for any set of ${\rm Fm}_{\forall}^{1}(\mathcal{L})$-equations
$T\cup\\{\varphi\approx\psi\\}$,

$\displaystyle
T\vDash^{\forall}_{\mathsf{K}}\varphi\approx\psi\>\iff\>T^{\ast}\vDash_{\mathsf{V}}\varphi^{\ast}\approx\psi^{\ast}.$

######  Example 2.3.

If $\mathsf{K}$ is $\mathsf{BA}$, then $\vDash^{\forall}_{\mathsf{K}}$ is
consequence in the one-variable fragment of first-order classical logic,
corresponding to $\mathrm{S5}$, and $\mathsf{V}$ is the variety of monadic
Boolean algebras defined in [Hal55]. If $\mathsf{K}$ is $\mathsf{HA}$, then
$\vDash^{\forall}_{\mathsf{K}}$ is consequence in the one-variable fragment of
first-order intuitionistic logic, corresponding to $\mathrm{MIPC}$, and
$\mathsf{V}$ is the variety of monadic Heyting algebras defined in [MV57].
Analogous results have been obtained for first-order intermediate logics
[OS88, Suz89, Suz90, Bez98, BH02, CR15, CMRR17, CMRT22]. In particular, if
$\mathsf{K}$ is $\mathsf{GA}$, then $\vDash^{\forall}_{\mathsf{K}}$ is
consequence in the one-variable fragment of the first-order logic of linear
frames, and $\mathsf{V}$ is the variety of monadic Heyting algebras satisfying
the prelinearity axiom $(x\to y)\lor(y\to x)\approx{\rm e}$ [CMRT22]. However,
if $\mathsf{K}$ is the class of totally ordered members of $\mathsf{GA}$, then
$\vDash^{\forall}_{\mathsf{K}}$ is consequence in the one-variable fragment of
first-order Gödel logic, the first-order logic of linear frames with a
constant domain, and $\mathsf{V}$ is the variety of monadic Gödel algebras,
i.e., monadic Heyting algebras satisfying the prelinearity axiom and the
constant domain axiom $\Box(\Box x\lor y)\approx\Box x\lor\Box y$ [CR15].
Similarly, if $\mathsf{K}$ is the class of totally ordered MV-algebras, then
$\vDash^{\forall}_{\mathsf{K}}$ is consequence in the one-variable fragment of
first-order Łukasiewicz logic, and $\mathsf{V}$ is the variety of monadic MV-
algebras [Rut59].

##  3 An algebraic approach

As our basic modal structures, let us define an _m-lattice_ to be any
algebraic structure $\langle{L,\land,\lor,\Box,\Diamond}\rangle$ with lattice
reduct $\langle{L,\land,\lor}\rangle$ that satisfies the following equations:

$\begin{array}[]{r@{\quad}l@{\qquad\qquad}r@{\quad}l}{\rm(L1_{\Box})}&\Box
x\land x\approx\Box x&{\rm(L1_{\Diamond})}&\Diamond x\lor x\approx\Diamond
x\\\ {\rm(L2_{\Box})}&\Box(x\land y)\approx\Box x\land\Box
y&{\rm(L2_{\Diamond})}&\Diamond(x\lor y)\approx\Diamond x\lor\Diamond y\\\
{\rm(L3_{\Box})}&\Box\Diamond x\approx\Diamond
x&{\rm(L3_{\Diamond})}&\Diamond\Box x\approx\Box x.\end{array}$

Let $\alpha\leq\beta$ stand for $\alpha\land\beta\approx\alpha$. It is easily
shown that every m-lattice also satisfies the following equations and quasi-
equations:

$\begin{array}[]{r@{\quad}l@{\qquad\qquad}r@{\quad}l}{\rm(L4_{\Box})}&\Box\Box
x\approx\Box x&{\rm(L4_{\Diamond})}&\Diamond\Diamond x\approx\Diamond x\\\
{\rm(L5_{\Box})}&x\leq y\,\Longrightarrow\,\Box x\leq\Box
y&{\rm(L5_{\Diamond})}&x\leq y\,\Longrightarrow\,\Diamond x\leq\Diamond
y.\end{array}$

Now let $\mathcal{L}$ be any fixed lattice-oriented signature. We define an
m-$\mathcal{L}$-lattice to be any algebraic structure
$\langle{\mathbf{A},\Box,\Diamond}\rangle$ such that $\mathbf{A}$ is an
$\mathcal{L}$-lattice, $\langle{A,\land,\lor,\Box,\Diamond}\rangle$ is an
m-lattice, and the following equation is satisfied for each $n\in\mathbb{N}$
and $\mathop{\star}\in\mathcal{L}_{n}$:

$\begin{array}[]{rl}(\mathop{\star}_{\Box})&\Box(\mathop{\star}(\Box
x_{1},\dots,\Box x_{n}))\approx\mathop{\star}(\Box x_{1},\dots,\Box
x_{n}).\end{array}$

Using ($\mathop{\star}$□), (L3□), and (L3◇), it follows that
$\langle{\mathbf{A},\Box,\Diamond}\rangle$ also satisfies for each
$n\in\mathbb{N}$ and $\mathop{\star}\in\mathcal{L}_{n}$, the equation

$\begin{array}[]{rl}(\mathop{\star}_{\Diamond})&\Diamond(\mathop{\star}(\Diamond
x_{1},\dots,\Diamond x_{n}))\approx\mathop{\star}(\Diamond
x_{1},\dots,\Diamond x_{n}).\end{array}$

Finally, given a class $\mathsf{K}$ of $\mathcal{L}$-lattices, let
$\mathsf{mK}$ denote the class of m-$\mathcal{L}$-lattices with an
$\mathcal{L}$-lattice reduct in $\mathsf{K}$. Note that if $\mathsf{K}$ is a
variety, then so is $\mathsf{mK}$.

######  Example 3.1.

It is straightforward to show that the notion of an
m-$\mathcal{L}_{s}$-lattice encompasses other algebraic structures considered
in the literature. In particular, $\mathsf{mBA}$ and $\mathsf{mHA}$ are the
varieties of monadic Heyting algebras [MV57] and monadic Boolean algebras
[Hal55], respectively. Moreover, if $\mathbf{A}$ is an
$\mathsf{FL_{e}}$-algebra, then every m-$\mathcal{L}_{s}$-lattice
$\langle{\mathbf{A},\Box,\Diamond}\rangle$ satisfies the equations

$\begin{array}[]{r@{\quad}l@{\qquad\qquad}r@{\quad}l}{\rm(L6_{\Box})}&\Box(x\to\Box
y)\approx\Diamond x\to\Box y&{\rm(L6_{\Diamond})}&\Box(\Box x\to y)\approx\Box
x\to\Box y,\end{array}$

and $\mathsf{mFL_{e}}$ is therefore the variety of monadic
$\mathsf{FL_{e}}$-algebras introduced in [Tuy21]. Let us just check (L6□), the
proof for (L6◇) being very similar. Consider any $a,b\in A$. Since
$a\leq\Diamond a$, by (L1◇), also $\Diamond a\to\Box b\leq a\to\Box b$. Hence,
using (L3□), ($\to_{\Box}$), and (L5□),

$\displaystyle\Diamond a\to\Box b=\Box\Diamond a\to\Box b=\Box(\Box\Diamond
a\to\Box b)=\Box(\Diamond a\to\Box b)\leq\Box(a\to\Box b).$

Conversely, since $\Box(a\to\Box b)\leq a\to\Box b$, by (L1□), it follows by
residuation that $a\leq\Box(a\to\Box b)\to\Box b$ and hence, using (L5◇),
(L3◇), and ($\to_{\Diamond}$),

$\displaystyle\Diamond a\leq\Diamond(\Box(a\to\Box b)\to\Box b)=\Box(a\to\Box
b)\to\Box b.$

By residuation again, $\Box(a\to\Box b)\leq\Diamond a\to\Box b$.

######  Example 3.2.

The variety $\mathsf{mGA}$ corresponds to the one-variable fragment of Corsi’s
first-order logic of linear frames [CMRT22], whereas the variety of monadic
Gödel algebras — axiomatized relative to $\mathsf{mGA}$ by the constant domain
axiom — corresponds to the one-variable fragment of first-order Gödel logic,
the first-order logic of linear frames with a constant domain [CR15]. Note,
however, that the variety axiomatized relative to $\mathsf{mMV}$ by the
constant domain axiom does not satisfy $\Diamond x\cdot\Diamond
x\approx\Diamond(x\cdot x)$ and therefore properly contains the variety of
monadic MV-algebras studied in [Rut59, dNG04, CCVR20]. Consider, for example,
the MV-algebra
$\textbf{\L}_{3}=\langle{\\{0,\frac{1}{2},1\\},\land,\lor,\cdot,\to,0,1}\rangle$
(in the language of $\mathsf{FL_{e}}$-algebras) with the usual order, where
$a\cdot b:=\max(0,a+b-1)$ and $a\to b:=\min(1,1-a+b)$. Let $\Box
0=\Box\frac{1}{2}=\Diamond 0=0$ and $\Box 1=\Diamond\frac{1}{2}=\Diamond 1=1$.
Then $\langle{\textbf{\L}_{3},\Box,\Diamond}\rangle\in\mathsf{mMV}$ satisfies
the constant domain axiom, but
$\Diamond\frac{1}{2}\cdot\Diamond\frac{1}{2}=1\cdot 1=1\neq 0=\Diamond
0=\Diamond(\frac{1}{2}\cdot\frac{1}{2})$.

We now provide a useful description of m-$\mathcal{L}$-lattices that
generalizes results in the literature for varieties such as monadic Heyting
algebras [Bez98] and monadic $\mathsf{FL_{e}}$-algebras [Tuy21].

######  Lemma 3.3.

Let $\langle{\mathbf{A},\Box,\Diamond}\rangle$ be any m-$\mathcal{L}$-lattice.
Then $\Box A\coloneqq\\{\Box a\mid a\in A\\}$ forms a subalgebra
$\Box\mathbf{A}$ of $\mathbf{A}$, where $\Box A=\Diamond A\coloneqq\\{\Diamond
a\mid a\in A\\}$ and for any $a\in A$,

$\displaystyle\Box a=\max\\{b\in\Box A\mid b\leq
a\\}\quad\text{and}\quad\Diamond a=\min\\{b\in\Box A\mid a\leq b\\}.$

###### Proof.

The fact that $\Box A$ forms a subalgebra of $\mathbf{A}$ follows directly
using ($\mathop{\star}$□) for each operation symbol $\mathop{\star}$ of
$\mathcal{L}$, and $\Box A=\Diamond A$ follows from (L3□) and (L3◇). Now
consider any $a\in A$. If $b\in\Box A$ satisfies $b\leq a$, then $b=\Box
b\leq\Box a$, by (L4□) and (L5□). But $\Box a\leq a$, by (L1□), so $\Box
a=\max\\{b\in\Box A\mid b\leq a\\}$. Analogous reasoning yields $\Diamond
a=\min\\{b\in\Box A\mid a\leq b\\}$. ∎

Let us call a sublattice $\mathbf{L}_{0}$ of a lattice $\mathbf{L}$
_relatively complete_ if for any $a\in L$, the set $\\{b\in L_{0}\mid b\leq
a\\}$ contains a maximum and the set $\\{b\in L_{0}\mid a\leq b\\}$ contains a
minimum. Equivalently, $\mathbf{L}_{0}$ is relatively complete if the
inclusion map $f_{0}$ from $\langle{L_{0},\leq}\rangle$ to
$\langle{L,\leq}\rangle$ has left and right adjoints, that is, if there exist
order-preserving maps $\Box\colon L\to L_{0}$ and $\Diamond\colon L\to L_{0}$
such that for all $a\in L$ and $b\in L_{0}$,

$\displaystyle f_{0}(b)\leq a\iff b\leq\Box a\quad\text{and}\quad a\leq
f_{0}(b)\iff\Diamond a\leq b.$

Let us also say that a subalgebra $\mathbf{A}_{0}$ of an $\mathcal{L}$-lattice
$\mathbf{A}$ is relatively complete if this property holds with respect to
their lattice reducts. In particular, by Lemma 3.3, the subalgebra
$\Box\mathbf{A}$ of $\mathbf{A}$ is relatively complete for any
m-$\mathcal{L}$-lattice $\langle{\mathbf{A},\Box,\Diamond}\rangle$. The
following result establishes a converse.

######  Lemma 3.4.

Let $\mathbf{A}_{0}$ be a relatively complete subalgebra of an
$\mathcal{L}$-lattice $\mathbf{A}$, and define $\Box_{0}a\coloneqq\max\\{b\in
A_{0}\mid b\leq a\\}$ and $\Diamond_{0}a\coloneqq\min\\{b\in A_{0}\mid a\leq
b\\}$ for each $a\in A$. Then
$\langle{\mathbf{A},\Box_{0},\Diamond_{0}}\rangle$ is an
m-$\mathcal{L}$-lattice and $\Box_{0}A=\Diamond_{0}A=A_{0}$.

###### Proof.

It is straightforward to check that
$\langle{A,\land,\lor,\Box_{0},\Diamond_{0}}\rangle$ is an m-lattice; for
example, it satisfies (L2□), since for any $a_{1},a_{2}\in A$,

$\displaystyle\Box_{0}(a_{1}\land a_{2})$ $\displaystyle=\max\\{b\in A_{0}\mid
b\leq a_{1}\land a_{2}\\}$ $\displaystyle=\max\\{b\in A_{0}\mid b\leq
a_{1}\text{ and }b\leq a_{2}\\}$ $\displaystyle=\max\\{b\in A_{0}\mid b\leq
a_{1}\\}\land\max\\{b\in A_{0}\mid b\leq a_{2}\\}$
$\displaystyle=\Box_{0}a_{1}\land\Box_{0}a_{2}.$

Since $\mathbf{A}_{0}$ is a subalgebra of $\mathbf{A}$, clearly
$\langle{\mathbf{A},\Box_{0},\Diamond_{0}}\rangle$ also satisfies
($\mathop{\star}$□). Hence $\langle{\mathbf{A},\Box_{0},\Diamond_{0}}\rangle$
is an m-$\mathcal{L}$-lattice and $\Box_{0}A=\Diamond_{0}A=A_{0}$. ∎

Lemmas 3.3 and 3.4 together yield the following representation theorem for
m-$\mathcal{L}$-lattices.

######  Theorem 3.5.

Let $\mathsf{K}$ be any class of $\mathcal{L}$-lattices. Then there exists a
one-to-one correspondence between the members of $\mathsf{mK}$ and ordered
pairs $\langle{\mathbf{A},\mathbf{A}_{0}}\rangle$ such that
$\mathbf{A}\in\mathsf{K}$ and $\mathbf{A}_{0}$ is a relatively complete
subalgebra of $\mathbf{A}$, implemented by the maps
$\langle{\mathbf{A},\Box,\Diamond}\rangle\mapsto\langle{\mathbf{A},\Box\mathbf{A}}\rangle$
and
$\langle{\mathbf{A},\mathbf{A}_{0}}\rangle\mapsto\langle{\mathbf{A},\Box_{0},\Diamond_{0}}\rangle$.

Next, given any $\mathcal{L}$-lattice $\mathbf{A}$ and set $W$, let
$\mathbf{A}^{W}$ be the $\mathcal{L}$-lattice with universe $A^{W}$, where the
operations are defined pointwise.

######  Proposition 3.6.

Let $\mathbf{A}$ be an $\mathcal{L}$-lattice, $W$ a set, and $\mathbf{B}$ a
subalgebra of $\mathbf{A}^{W}$ such that for each $f\in B$, the elements
$\bigwedge_{v\in W}f(v)$ and $\bigvee_{v\in W}f(v)$ exist in $\mathbf{A}$ and
the following constant functions belong to $B$,

$\displaystyle\Box f\colon W\to A;\>u\mapsto\bigwedge_{v\in
W}f(v)\quad\text{and}\quad\Diamond f\colon W\to A;\>u\mapsto\bigvee_{v\in
W}f(v).$

Then $\langle{\mathbf{B},\Box,\Diamond}\rangle$ is an m-$\mathcal{L}$-lattice.
Moreover, if $\mathbf{A}$ belongs to a class $\mathsf{K}$ of
$\mathcal{L}$-lattices closed under taking subalgebras and direct powers, then
$\langle{\mathbf{B},\Box,\Diamond}\rangle\in\mathsf{mK}$.

###### Proof.

It is straightforward to check that
$\langle{B,\land,\lor,\Box,\Diamond}\rangle$ satisfies the equations
${\rm(L1_{\Box})}$–${\rm(L3_{\Box})}$ and
${\rm(L1_{\Diamond})}$–${\rm(L3_{\Diamond})}$ and is hence an m-lattice. To
show that $\langle{\mathbf{B},\Box,\Diamond}\rangle$ is an
m-$\mathcal{L}$-lattice — and therefore, if $\mathbf{A}$ belongs to a class
$\mathsf{K}$ of $\mathcal{L}$-lattices closed under taking subalgebras and
direct powers, a member of $\mathsf{mK}$ — observe that for any
$n\in\mathbb{N}$, $\mathop{\star}\in\mathcal{L}_{n}$, $f_{1},\dots,f_{n}\in
B$, and $u\in W$,

$\displaystyle\Box(\mathop{\star}(\Box f_{1},\dots,\Box f_{n}))(u)$
$\displaystyle=\bigwedge_{v\in W}\mathop{\star}(\Box f_{1},\dots,\Box
f_{n})(v)$ $\displaystyle=\bigwedge_{v\in W}\mathop{\star}(\Box
f_{1}(v),\dots,\Box f_{n}(v))$ $\displaystyle=\mathop{\star}(\Box
f_{1}(u),\dots,\Box f_{n}(u))$ $\displaystyle=\mathop{\star}(\Box
f_{1},\dots,\Box f_{n})(u),$

noting that in the third equality we have used the fact that $\Box
f_{i}(v)=\Box f_{i}(u)$ for all $v\in W$ and $i\in\\{1,\dots,n\\}$. ∎

Let us call an m-$\mathcal{L}$-lattice
$\langle{\mathbf{B},\Box,\Diamond}\rangle$
$\langle{\mathbf{A},W}\rangle$-functional if it is constructed as described in
Proposition 3.6 for some $\mathcal{L}$-lattice $\mathbf{A}$ and set $W$.
Consider any class of $\mathcal{L}$-lattices $\mathsf{K}$. We call an
m-$\mathcal{L}$-lattice $\mathsf{K}$-functional if it is isomorphic to an
$\langle{\mathbf{A},W}\rangle$-functional m-$\mathcal{L}$-lattice for some
$\mathbf{A}\in\mathsf{K}$ and set $W$, omitting the prefix $\mathsf{K}$\- if
the class is clear from the context.

The following result identifies the semantics of one-variable first-order
logics with evaluations into functional m-$\mathcal{L}$-lattices.

######  Proposition 3.7.

Let $\mathbf{A}$ be any $\mathcal{L}$-lattice.

  1. (a)

Let ${\mathfrak{{S}}}=\langle{S,\mathcal{I}}\rangle$ be any
$\mathbf{A}$-structure. Then
$B\coloneqq\\{\left\|{\varphi}\right\|^{\mathfrak{{S}}}\mid\varphi\in{\rm
Fm}_{\forall}^{1}(\mathcal{L})\\}$ forms an
$\langle{\mathbf{A},S}\rangle$-functional m-$\mathcal{L}$-lattice $\mathbf{B}$
and the $\mathbf{B}$-evaluation $g^{\mathfrak{{S}}}$, defined by
$g^{\mathfrak{{S}}}(p_{i})\coloneqq\mathcal{I}(P_{i})$ for each
$i\in\mathbb{N}$, satisfies for all $\varphi,\psi\in{\rm
Fm}_{\forall}^{1}(\mathcal{L})$,

$\displaystyle
g^{\mathfrak{{S}}}(\varphi^{\ast})=\left\|{\varphi}\right\|^{\mathfrak{{S}}}\quad\text{and}\quad{\mathfrak{{S}}}\models\varphi\approx\psi\iff
g^{\mathfrak{{S}}}(\varphi^{\ast})=g^{\mathfrak{{S}}}(\psi^{\ast}).$

  2. (b)

Let $\mathbf{B}$ be any $\langle{\mathbf{A},W}\rangle$-functional
m-$\mathcal{L}$-lattice for some set $W$, and let $e$ be any
$\mathbf{B}$-evaluation. Then
${\mathfrak{{W}}}=\langle{W,\mathcal{J}}\rangle$, where
$\mathcal{J}(P_{i})\coloneqq e(p_{i})$ for each $i\in\mathbb{N}$, is an
$\mathbf{A}$-structure satisfying for all $\varphi,\psi\in{\rm
Fm}_{\forall}^{1}(\mathcal{L})$,

$\displaystyle
e(\varphi^{\ast})=\left\|{\varphi}\right\|^{\mathfrak{{W}}}\quad\text{and}\quad{\mathfrak{{W}}}\models\varphi\approx\psi\iff
e(\varphi^{\ast})=e(\psi^{\ast}).$

###### Proof.

(a) To show that $\mathbf{B}$ is $\langle{\mathbf{A},S}\rangle$-functional, it
suffices to observe that for any $\left\|{\varphi}\right\|^{\mathfrak{{S}}}\in
B$, since ${\mathfrak{{S}}}$ is an $\mathbf{A}$-structure, the elements
$\bigwedge\\{\left\|{\varphi}\right\|^{\mathfrak{{S}}}(v)\mid v\in S\\}$ and
$\bigvee\\{\left\|{\varphi}\right\|^{\mathfrak{{S}}}(v)\mid v\in S\\}$ exist
in $\mathbf{A}$ and correspond to the constant functions
$\left\|{(\forall{x})\varphi}\right\|^{\mathfrak{{S}}}\in B$ and
$\left\|{(\exists{x})\varphi}\right\|^{\mathfrak{{S}}}\in B$, respectively.
The fact that
$g^{\mathfrak{{S}}}(\varphi^{\ast})=\left\|{\varphi}\right\|^{\mathfrak{{S}}}$
for all $\varphi\in{\rm Fm}_{\forall}^{1}(\mathcal{L})$, follows by a
straightforward induction on the definition of $\varphi$, from which it
follows directly also that ${\mathfrak{{S}}}\models\varphi\approx\psi\iff
g^{\mathfrak{{S}}}(\varphi^{\ast})=g^{\mathfrak{{S}}}(\psi^{\ast})$, for all
$\varphi,\psi\in{\rm Fm}_{\forall}^{1}(\mathcal{L})$.

(b) Since $\mathbf{B}$ is $\langle{\mathbf{A},W}\rangle$-functional, the
elements $\bigwedge_{v\in W}f(v)$ and $\bigvee_{v\in W}f(v)$ exist in
$\mathbf{A}$ for every $f\in B$. We prove that
$e(\varphi^{\ast})=\left\|{\varphi}\right\|^{\mathfrak{{W}}}$, by induction on
the definition of $\varphi$, from which it follows immediately that
${\mathfrak{{W}}}=\langle{W,\mathcal{J}}\rangle$ is an $\mathbf{A}$-structure
and ${\mathfrak{{W}}}\models\varphi\approx\psi\iff
e(\varphi^{\ast})=e(\psi^{\ast})$, for all $\varphi,\psi\in{\rm
Fm}_{\forall}^{1}(\mathcal{L})$. In particular, for the case where
$\varphi=(\forall{x})\psi$, using the induction hypothesis for the second
line,

$\displaystyle\left\|{(\forall{x})\psi}\right\|^{\mathfrak{{W}}}(u)$
$\displaystyle=\bigwedge\\{\left\|{\psi}\right\|^{\mathfrak{{W}}}(v)\mid v\in
W\\}$ $\displaystyle=\bigwedge\\{e(\psi^{\ast})(v)\mid v\in W\\}$
$\displaystyle=\Box e(\psi^{\ast})(u)$
$\displaystyle=e(((\forall{x})\psi)^{\ast})(u).$

The case where $\varphi=(\exists{x})\psi$ is very similar. ∎

As a direct consequence of this theorem, we obtain the following relationship
between consequence in the first-order logic defined over a (suitable) class
$\mathsf{K}$ of $\mathcal{L}$-lattices and consequence in the variety
$\mathsf{mK}$.

######  Corollary 3.8.

For any class $\mathsf{K}$ of $\mathcal{L}$-lattices closed under taking
subalgebras and direct powers, and set of ${\rm
Fm}_{\forall}^{1}(\mathcal{L})$-equations $T\cup\\{\varphi\approx\psi\\}$,

$\displaystyle
T^{\ast}\vDash_{\mathsf{mK}}\varphi^{\ast}\approx\psi^{\ast}\quad\Longrightarrow\quad
T\vDash^{\forall}_{\mathsf{K}}\varphi\approx\psi.$

Moreover, if every member of $\mathsf{mK}$ is $\mathsf{K}$-functional

$\displaystyle
T^{\ast}\vDash_{\mathsf{mK}}\varphi^{\ast}\approx\psi^{\ast}\quad\Longleftrightarrow\quad
T\vDash^{\forall}_{\mathsf{K}}\varphi\approx\psi.$

Let us remark that a stricter notion of a functional algebra for a class
$\mathsf{K}$ of $\mathcal{L}$-lattices is considered in [BH02, CMT22] that
coincides in our setting with the notion of being $\mathsf{K}^{c}$-functional,
where $\mathsf{K}^{c}$ is the class of complete members of $\mathsf{K}$. That
is, an m-$\mathcal{L}$-lattice $\langle{\mathbf{B},\Box,\Diamond}\rangle$ is
$\mathsf{K}^{c}$-functional if it is isomorphic to a subalgebra of
$\langle{\mathbf{A}^{W},\Box,\Diamond}\rangle$ for some complete
$\mathcal{L}$-lattice $\mathbf{A}\in\mathsf{K}$ and set $W$, where $\Box$ and
$\Diamond$ are defined as described in Proposition 3.6.

##  4 A functional representation theorem

Adapting the proof of a similar result for Heyting Algebras [BH02, Theorem
3.6], we prove in this section that if a variety $\mathsf{V}$ of
$\mathcal{L}$-lattices has the superamalgamation property, then every member
of $\mathsf{mV}$ is $\mathsf{V}$-functional, and hence, by Corollary 3.8,
consequence in the one-variable first-order logic defined over $\mathsf{V}$
corresponds to consequence in $\mathsf{mV}$.

We first recall the necessary algebraic notions. Let $\mathsf{K}$ be a class
of $\mathcal{L}$-lattices. A V-formation in $\mathsf{K}$ is a $5$-tuple
$\langle{\mathbf{A},\mathbf{B}_{1},\mathbf{B}_{2},f_{1},f_{2}}\rangle$
consisting of $\mathbf{A},\mathbf{B}_{1},\mathbf{B}_{2}\in\mathsf{K}$ and
embeddings $f_{1}\colon\mathbf{A}\to\mathbf{B}_{1}$,
$f_{2}\colon\mathbf{A}\to\mathbf{B}_{2}$. An amalgam in $\mathsf{K}$ of a
V-formation
$\langle{\mathbf{A},\mathbf{B}_{1},\mathbf{B}_{2},f_{1},f_{2}}\rangle$ in
$\mathsf{K}$ is a triple $\langle{\mathbf{C},g_{1},g_{2}}\rangle$ consisting
of $\mathbf{C}\in\mathsf{K}$ and embeddings
$g_{1}\colon\mathbf{B}_{1}\to\mathbf{C}$,
$g_{2}\colon\mathbf{B}_{2}\to\mathbf{C}$ such that $g_{1}\circ
f_{1}=g_{2}\circ f_{2}$; it is called a superamalgam if also for any $b_{1}\in
B_{1}$, $b_{2}\in B_{2}$ and distinct $i,j\in\\{1,2\\}$,

$\displaystyle g_{i}(b_{i})\leq g_{j}(b_{j})\enspace\Longrightarrow\enspace
g_{i}(b_{i})\leq g_{i}\circ f_{i}(a)=g_{j}\circ f_{j}(a)\leq
g_{j}(b_{j})\,\text{ for some }a\in A.$

The class $\mathsf{K}$ is said to have the superamalgamation property if every
V-formation in $\mathsf{K}$ has a superamalgam in $\mathsf{K}$.

######  Theorem 4.1.

Let $\mathsf{K}$ be a class of $\mathcal{L}$-lattices that is closed under
taking direct limits and subalgebras, and has the superamalgamation property.
Then every member of $\mathsf{K}$ is functional.

###### Proof.

Consider any $\langle{\mathbf{A},\Box,\Diamond}\rangle\in\mathsf{mK}$. Then
$\mathbf{A}\in\mathsf{K}$ and, since $\mathsf{K}$ is closed under taking
subalgebras, also $\Box\mathbf{A}\in\mathsf{K}$. We let $W:=\mathbb{N}^{>0}$
and define inductively a sequence of $\mathcal{L}$-lattices
$\langle{\mathbf{A}_{i}}\rangle_{i\in W}$ in $\mathsf{K}$ and sequences of
$\mathcal{L}$-lattice embeddings
$\langle{f_{i}\colon\Box\mathbf{A}\to\mathbf{A}_{i}}\rangle_{i\in W}$,
$\langle{g_{i}\colon\mathbf{A}\to\mathbf{A}_{i}}\rangle_{i\in W}$,
$\langle{s_{i}\colon\mathbf{A}_{i-1}\to\mathbf{A}_{i}}\rangle_{i\in W}$.

Let $\mathbf{A}_{0}\coloneqq\mathbf{A}$ and let
$f_{0}\colon\Box\mathbf{A}\to\mathbf{A}$ be the inclusion map. For each $i\in
W$, there exists inductively, by assumption, a superamalgam
$\langle{\mathbf{A}_{i},s_{i},g_{i}}\rangle$ of the V-formation
$\langle{\Box\mathbf{A},\mathbf{A}_{i-1},\mathbf{A},f_{i-1},f_{0}}\rangle$,
and we define also $f_{i}\coloneqq s_{i}\circ f_{i-1}=g_{i}\circ
f_{0}=g_{i}|_{\Box A}$.

Now let $\mathbf{L}$ be the direct limit of the system
$\langle{\langle{\mathbf{A}_{i},s_{i}}\rangle}\rangle_{i\in W}$ with an
associated sequence of $\mathcal{L}$-lattice embeddings
$\langle{l_{i}\colon\mathbf{A}_{i}\to\mathbf{L}}\rangle_{i\in W}$. Since
$\mathsf{K}$ is closed under taking direct limits, $\mathbf{L}$ belongs to
$\mathsf{K}$. The first two superamalgamation steps of this construction are
depicted in the following diagram:

$\Box\mathbf{A}$$\mathbf{A}$$\mathbf{A}$$\mathbf{A}_{1}$$\mathbf{A}_{2}$$\mathbf{A}_{3}$$\mathbf{L}$$\cdots$$f_{0}$$f_{0}$$f_{1}$$g_{3}$$g_{2}$$g_{1}$$s_{1}$$s_{2}$$s_{3}$$l_{1}$$l_{2}$$l_{3}$

Since the operations of $\mathbf{L}^{W}$ are defined pointwise,
$B\coloneqq\\{\langle{l_{i}\circ g_{i}(a)}\rangle_{i\in W}\mid a\in A\\}$ is
the universe of a subalgebra $\mathbf{B}$ of $\mathbf{L}^{W}$. We can also
show that for each $a\in A$, the elements

$\displaystyle\bigwedge_{j\in W}l_{j}\circ
g_{j}(a)\qquad\text{and}\qquad\bigvee_{j\in W}l_{j}\circ g_{j}(a)$

exist in $L$ and hence that $\langle{\mathbf{B},\Box,\Diamond}\rangle$, with
$\Box$ and $\Diamond$ defined in Proposition 3.6, is an
$\langle{\mathbf{L},W}\rangle$-functional m-$\mathcal{L}$-lattice. Let $a\in
A$ and fix some $i\in W$. It suffices to show that $l_{i}\circ g_{i}(\Box a)$
and $l_{i}\circ g_{i}(\Diamond a)$ are the greatest lower bound and least
upper bound, respectively, of $S\coloneqq\\{l_{j}\circ g_{j}(a)\mid j\in
W\\}$. Observe first that for any $k\in W$,

$\displaystyle l_{k}\circ g_{k}(\Box a)=l_{k}\circ f_{k}(\Box a)=l_{k+1}\circ
s_{k+1}\circ f_{k}(\Box a)=l_{k+1}\circ g_{k+1}(\Box a),$

where the first and last equations follow from the definition of $f_{k}$ and
the second follows from the fact that $\mathbf{L}$ is a direct limit. Hence
for each $j\in W$,

$\displaystyle l_{i}\circ g_{i}(\Box a)=l_{j}\circ g_{j}(\Box a)\leq
l_{j}\circ g_{j}(a).$

So $l_{i}\circ g_{i}(\Box a)$ is a lower bound of $S$. Now suppose that $c\in
L$ is another lower bound of $S$. Since $\mathbf{L}$ is a direct limit, there
exist $k\in W$ and $d\in A_{k}$ such that

$\displaystyle l_{k+1}\circ s_{k+1}(d)=l_{k}(d)=c\leq l_{k+1}\circ
g_{k+1}(a).$

Since $l_{k+1}$ is an embedding, $s_{k+1}(d)\leq g_{k+1}(a)$. Hence, since
$\langle{\mathbf{A}_{k+1},s_{k+1},g_{k+1}}\rangle$ is a superamalgam of
$\langle{\Box\mathbf{A},\mathbf{A}_{k},\mathbf{A},f_{k},f_{0}}\rangle$, there
exists $b\in\Box A$ such that

$\displaystyle s_{k+1}(d)\leq s_{k+1}\circ f_{k}(b)=g_{k+1}\circ f_{0}(b)\leq
g_{k+1}(a).$

But $s_{k+1}$ and $g_{k+1}$ are embeddings and $f_{0}$ is the inclusion map,
so $d\leq f_{k}(b)$ and $b\leq a$. The latter inequality together with
$b\in\Box A$, yields $b=\Box b\leq\Box a$. Hence also $f_{k}(b)\leq f_{k}(\Box
a)=g_{k}(\Box a)$, and, using the first inequality,

$\displaystyle c=l_{k}(d)\leq l_{k}\circ f_{k}(b)\leq l_{k}\circ g_{k}(\Box
a)=l_{i}\circ g_{i}(\Box a).$

So $\bigwedge_{j\in W}l_{j}\circ g_{j}(a)=l_{i}\circ g_{i}(\Box a)$ exists in
$L$ and the constant function $\langle{l_{i}\circ g_{i}(\Box a)}\rangle_{i\in
W}$ belongs to $B$. Also, symmetrically, $\bigvee_{j\in W}l_{j}\circ
g_{j}(a)=l_{i}\circ g_{i}(\Diamond a)$ exists in $L$ and the constant function
$\langle{l_{i}\circ g_{i}(\Diamond a)}\rangle_{i\in W}$ belongs to $B$.

To show that $\langle{\mathbf{A},\Box,\Diamond}\rangle$ is functional, it
remains to prove that the following map is an isomorphism:

$\displaystyle
f\colon\langle{\mathbf{A},\Box,\Diamond}\rangle\to\langle{\mathbf{B},\Box,\Diamond}\rangle;\quad
a\mapsto\langle{l_{i}\circ g_{i}(a)}\rangle_{i\in W}.$

Since the operations of $\mathbf{L}^{W}$ are defined pointwise, it is easily
checked that $f$ is an $\mathcal{L}$-lattice isomorphism. Moreover, recalling
that $l_{i}\circ g_{i}(\Box a)=\bigwedge_{j\in W}l_{i}\circ g_{i}(a)$ for each
$a\in A$, it follows that

$\displaystyle f(\Box a)=\langle{l_{i}\circ g_{i}(\Box a)}\rangle_{i\in
W}=\langle{\bigwedge_{j\in W}l_{j}\circ g_{j}(a)}\rangle_{i\in
W}=\Box\langle{l_{i}\circ g_{i}(a)}\rangle_{i\in W}=\Box f(a),$

and, similarly, $f(\Diamond a)=\Diamond f(a)$ for all $a\in A$. ∎

Combining Theorem 4.1 with Corollary 3.8 yields the following result.

######  Corollary 4.2.

If $\mathsf{V}$ is a variety of $\mathcal{L}$-lattices that has the
superamalgamation property, then for any set $T\cup\\{\varphi\approx\psi\\}$
of ${\rm Fm}_{\forall}^{1}(\mathcal{L})$-equations,

$\displaystyle
T\vDash^{\forall}_{\mathsf{V}}\varphi\approx\psi\quad\Longleftrightarrow\quad
T^{\ast}\vDash_{\mathsf{mV}}\varphi^{\ast}\approx\psi^{\ast}.$

######  Example 4.3.

The variety of lattices has the superamalgamation property [Gra98]. Hence, by
Theorem 4.1, every m-lattice is functional, and consequence in the one-
variable first-order lattice logic corresponds to consequence in m-lattices.

######  Example 4.4.

$\mathsf{FL_{e}}$, $\mathsf{FL_{ew}}$, and $\mathsf{FL_{ec}}$, and many other
varieties of $\mathsf{FL_{e}}$-algebras have the superamalgamation property,
which is equivalent in this setting to the Craig interpolation property for
the associated substructural logic (see, e.g., [GJKO07]). Hence, for any such
variety $\mathsf{V}$ — notably, for
$\mathsf{V}\in\\{\mathsf{FL_{e}},\mathsf{FL_{ew}},\mathsf{FL_{ec}}\\}$ — every
member of $\mathsf{mV}$ is functional, and consequence in the one-variable
first-order substructural logic defined over $\mathsf{V}$ corresponds to
consequence in $\mathsf{mV}$.

######  Example 4.5.

A normal modal logic has the Craig interpolation property if and only if the
associated variety of modal algebras — Boolean algebras with an operator — has
the superamalgamation property [Mak92]. Moreover, there exist infinitely many
such logics [Rau82], including well-known cases such as $\mathrm{K}$,
$\mathrm{KT}$, $\mathrm{K4}$, and $\mathrm{S4}$. Hence our results yield
axiomatizations for the one-variable fragments of infinitely many first-order
logics defined over varieties of modal algebras.

Suppose finally that $\mathsf{K}$ is a class of $\mathcal{L}$-lattices that is
not only closed under taking direct limits and subalgebras and has the
superamalgamation property, but also admits regular completions. In this case,
we can adapt the proof of Theorem 4.1 to show that every member of
$\mathsf{K}$ is $\mathsf{K}^{c}$-functional, which — as noted at the end of
Section 3 — corresponds to the stricter notion of a functional algebra
considered in [BH02, CMT22]. Just observe that, given some
$\langle{\mathbf{A},\Box,\Diamond}\rangle\in\mathsf{mK}$, the direct limit
$\mathbf{L}\in\mathsf{K}$ constructed in the proof embeds into some
$\mathbf{\bar{L}}\in\mathsf{K}^{c}$ and hence, reasoning as before,
$\langle{\mathbf{A},\Box,\Diamond}\rangle$ is isomorphic to a subalgebra of
$\langle{\mathbf{\bar{L}}^{W},\Box,\Diamond}\rangle$.

##  5 A proof-theoretic strategy

In this section, we describe an alternative proof-theoretic strategy for
establishing completeness of axiomatizations for one-variable fragments of
first-order logics. The key step is to prove that a derivation of a one-
variable formula in a sequent calculus for the first-order logic can be
transformed into a derivation that uses just one variable. To illustrate, we
consider the first-order version of the full Lambek calculus with exchange
$\mathrm{FL_{e}}$, then extend the method to a broader family of first-order
substructural logics.

The one-variable fragment of the first-order version of $\mathrm{FL_{e}}$ can
be presented as a cut-free sequent calculus. This presentation has the
advantage that although a derivation of a one-variable formula in the calculus
may use more than one variable, it will not introduce any new occurrences of
quantifiers. We therefore consider the set ${\rm
Fm}_{\forall}^{1+}(\mathcal{L}_{s})$ of first-order formulas built inductively
from unary predicates $\\{P_{i}\\}_{i\in\mathbb{N}}$, variables
$\\{x\\}\cup\\{x_{i}\\}_{i\in\mathbb{N}}$, connectives in $\mathcal{L}_{s}$,
and quantifiers $(\forall{x})$ and $(\exists{x})$, such that no occurrence of
a variable $x_{i}$ lies in the scope of a quantifier. Clearly, ${\rm
Fm}_{\forall}^{1}(\mathcal{L}_{s})\subseteq{\rm
Fm}_{\forall}^{1+}(\mathcal{L}_{s})$. We write $\varphi(\bar{w})$ to denote
that the free variables of $\varphi\in{\rm
Fm}_{\forall}^{1+}(\mathcal{L}_{s})$ belong to the set $\bar{w}$, and indicate
by writing $\varphi(\bar{w},y)$ that $y\not\in\bar{w}$.

For the purposes of this paper, we define a sequent to be an ordered pair of
finite multisets of formulas in ${\rm Fm}_{\forall}^{1+}(\mathcal{L}_{s})$,
denoted by
$\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}$, such
that $\mathrm{\Delta}$ contains at most one $\mathcal{L}_{s}$-formula.333The
full Lambek calculus with exchange is typically presented using sequents
consisting of finite sequences of formulas and an “exchange rule” for
permuting formulas (see, e.g., [GJKO07, MPT23]). As usual, we denote the
multiset sum of two finite multisets of formulas $\mathrm{\Gamma}_{1}$ and
$\mathrm{\Gamma}_{2}$ by $\mathrm{\Gamma}_{1},\mathrm{\Gamma}_{2}$, and the
empty multiset by an empty space. We also define, for $n\in\mathbb{N}^{>0}$
and $\varphi_{1},\dots,\varphi_{n},\psi\in{\rm
Fm}_{\forall}^{1+}(\mathcal{L}_{s})$,

$\displaystyle\textstyle\prod(\varphi_{1},\dots,\varphi_{n})\coloneqq\varphi_{1}\cdots\varphi_{n},\quad\prod()\coloneqq{\rm
e},\quad\sum(\psi)\coloneqq\psi,\quad\sum()\coloneqq{\rm f}.$

The sequent calculus $\mathrm{\forall 1FL_{e}}$ is displayed in Figure 1,
where the quantifier rules are subject to the following side-conditions:

  1. (i)

if the conclusion of an application of $({\forall\\!\Rightarrow})$ or
$(\Rightarrow\\!\exists)$ contains at least one free occurrence of a variable,
then the variable $u$ occurring in the premise also occurs freely in the
conclusion;

  2. (ii)

the variable $y$ occurring in the premise of $(\Rightarrow\\!\forall)$ and
$(\exists\\!\Rightarrow)$ does not occur freely in the conclusion of the rule.

If there exists a derivation $d$ of a sequent
$\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}$ in a
sequent calculus $\mathrm{C}$, we write
$d\vdash_{{}_{\mathrm{\mathrm{C}}}}\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}$
or simply
$\vdash_{{}_{\mathrm{\mathrm{C}}}}\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}$.

$\begin{array}[]{c}\text{Axioms}\\\\[14.45377pt]
\begin{array}[]{ccccc}\varphi{\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi&&{\rm
f}{\vphantom{A}\Rightarrow{\vphantom{A}}}&&{\vphantom{A}\Rightarrow{\vphantom{A}}}{\rm
e}\end{array}\\\\[18.06749pt] \text{Operation Rules}\\\\[14.45377pt]
\begin{array}[]{ccc}\mathrm{\Gamma},{\rm
e}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}&&\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}{\rm
f}\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\\\\[10.84006pt]
\mathrm{\Gamma}_{1},\mathrm{\Gamma}_{2},\varphi\to\psi{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\lx@proof@logical@and\mathrm{\Gamma}_{1}{\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi\mathrm{\Gamma}_{2},\psi{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}&&\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi\to\psi\mathrm{\Gamma},\varphi{\vphantom{A}\Rightarrow{\vphantom{A}}}\psi\\\\[10.84006pt]
\mathrm{\Gamma},\varphi\cdot\psi{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\mathrm{\Gamma},\varphi,\psi{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}&&\mathrm{\Gamma}_{1},\mathrm{\Gamma}_{2}{\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi\cdot\psi\lx@proof<EMAIL_ADDRESS>\mathrm{\Gamma},\varphi\land\psi{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\mathrm{\Gamma},\varphi{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}&&\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi\lor\psi\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi\\\\[10.84006pt]
\mathrm{\Gamma},\varphi\land\psi{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\mathrm{\Gamma},\psi{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}&&\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi\lor\psi\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\psi\\\\[10.84006pt]
\mathrm{\Gamma},\varphi\lor\psi{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\lx@proof@logical@and\mathrm{\Gamma},\varphi{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\mathrm{\Gamma},\psi{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}&&\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi\land\psi\lx@proof<EMAIL_ADDRESS>\mathrm{\Gamma},(\forall{x})\varphi(x){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\mathrm{\Gamma},\varphi(u){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}&&\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}(\forall{x})\psi(x)\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\psi(y)\\\\[10.84006pt]
\mathrm{\Gamma},(\exists{x})\varphi(x){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\mathrm{\Gamma},\varphi(y){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}&&\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}(\exists{x})\psi(x)\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\psi(u)\end{array}\end{array}$

Figure 1: The Sequent Calculus $\mathrm{\forall 1FL_{e}}$

The following relationship between derivability of sequents in
$\mathrm{\forall 1FL_{e}}$ and (first-order) validity of equations in the
variety $\mathsf{FL_{e}}$ is a direct consequence of the completeness of a
cut-free sequent calculus for the first-order version of $\mathrm{FL_{e}}$.

######  Proposition 5.1 (cf. [OK85, Kom86]).

For any sequent
$\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}$
containing formulas from ${\rm Fm}_{\forall}^{1}$,

$\displaystyle\textstyle\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\quad\Longleftrightarrow\quad\>\vDash^{\forall}_{\mathsf{FL_{e}}}\prod\mathrm{\Gamma}\leq\sum\mathrm{\Delta}.$

We now establish an interpolation property for the calculus $\mathrm{\forall
1FL_{e}}$. For any derivation $d$ of a sequent in $\mathrm{\forall 1FL_{e}}$,
let ${\rm md}(d)$ denote the maximum number of applications of the rules
$(\Rightarrow\\!\forall)$ and $(\exists\\!\Rightarrow)$ that occur on a branch
of $d$.

######  Lemma 5.2.

If $d\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y),\Pi(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z)$,
with $y\neq z$ and $x\not\in\bar{w}\cup\\{y,z\\}$, then there exist
$\chi(\bar{w})\in{\rm Fm}_{\forall}^{1+}(\mathcal{L}_{s})$ and derivations
$d_{1},d_{2}$ in $\mathrm{\forall 1FL_{e}}$ such that ${\rm md}(d_{1}),{\rm
md}(d_{2})\leq{\rm md}(d)$ and

$\displaystyle d_{1}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi(\bar{w}),\quad
d_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(\bar{w},z),\chi(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

###### Proof.

We prove the claim by induction on the height of the derivation $d$ in
$\mathrm{\forall 1FL_{e}}$ of
$\mathrm{\Gamma}(\bar{w},y),\Pi(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z)$,
considering in turn the last rule applied in the derivation. Note first that
if $y$ does not occur in $\mathrm{\Gamma}$, we can define
$\chi(\bar{w}):=\prod\mathrm{\Gamma}$, and obtain a derivation $d_{1}$ of
$\mathrm{\Gamma}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi(\bar{w})$,
ending with repeated applications of $(\Rightarrow\\!\cdot)$ and
$(\Rightarrow\\!{\rm e})$, and a derivation $d_{2}$ of
$\Pi(\bar{w},z),\chi(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z)$
extending $d$ with repeated applications of $(\cdot\\!\Rightarrow)$ and $({\rm
e}\\!\Rightarrow)$, such that ${\rm md}(d_{1})=0$ and ${\rm md}(d_{2})\leq{\rm
md}(d)$. Similarly, if $z$ does not occur in $\Pi,\mathrm{\Delta}$, we can
define $\chi(\bar{w}):=\prod\Pi\to\sum\mathrm{\Delta}$, and obtain a
derivation $d_{1}$ of
$\mathrm{\Gamma}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi(\bar{w})$
that extends $d$ with repeated applications of $(\cdot\\!\Rightarrow)$, $({\rm
e}\\!\Rightarrow)$, and $(\Rightarrow\\!{\rm f})$, followed by an application
of $(\Rightarrow\to)$, and a derivation $d_{2}$ of
$\Pi(\bar{w},z),\chi(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z)$
ending with repeated applications of $(\Rightarrow\\!\cdot)$,
$(\Rightarrow\\!{\rm e})$, and $({\rm f}\\!\Rightarrow)$, followed by an
application of $(\to\Rightarrow)$, such that ${\rm md}(d_{1})={\rm md}(d)$ and
${\rm md}(d_{2})=0$.

For the base cases where $d$ ends with $(\textsc{id})$, $(\Rightarrow\\!{\rm
e})$, or $({\rm f}\\!\Rightarrow)$, either $y$ does not occur in
$\mathrm{\Gamma}$ or $z$ does not occur in $\Pi,\mathrm{\Delta}$. For the
remainder of the proof, let us assume without further comment that $y$ occurs
in $\mathrm{\Gamma}$ and $z$ occurs in $\Pi,\mathrm{\Delta}$. The cases where
$d$ ends with an operational rule for one of the propositional connectives are
all straightforward, so let us just consider $(\to\Rightarrow)$ as an example.

Suppose first that $\mathrm{\Gamma}(\bar{w},y)$ is
$\mathrm{\Gamma}_{1}(\bar{w},y),\mathrm{\Gamma}_{2}(\bar{w},y),\varphi(\bar{w},y)\to\psi(\bar{w},y)$
and $\Pi(\bar{w},z)$ is $\Pi_{1}(\bar{w},z),\Pi_{2}(\bar{w},z)$, and

$\displaystyle d^{\prime}_{1}$
$\displaystyle\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}_{1}(\bar{w},y),\Pi_{1}(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi(\bar{w},y),$
$\displaystyle d^{\prime}_{2}$
$\displaystyle\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}_{2}(\bar{w},y),\psi(\bar{w},y),\Pi_{2}(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

Two applications of the induction hypothesis yield formulas
$\chi_{1}(\bar{w}),\chi_{2}(\bar{w})$ and derivations
$d^{\prime}_{11},d^{\prime}_{12},d^{\prime}_{21},d^{\prime}_{22}$ such that

$\displaystyle d^{\prime}_{11}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}_{1}(\bar{w},y),\chi_{1}(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi(\bar{w},y),$
$\displaystyle\quad d^{\prime}_{12}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi_{1}(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi_{1}(\bar{w}),$
$\displaystyle d^{\prime}_{21}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}_{2}(\bar{w},y),\psi(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi_{2}(\bar{w}),$
$\displaystyle\quad d^{\prime}_{22}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi_{2}(\bar{w},z),\chi_{2}(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

Let $\chi(\bar{w}):=\chi_{1}(\bar{w})\to\chi_{2}(\bar{w})$. Then
$d^{\prime}_{11},d^{\prime}_{21}$, together with applications of
$(\to\Rightarrow)$ and $(\Rightarrow\to)$, and
$d^{\prime}_{12},d^{\prime}_{22}$, together with an application of
$(\to\Rightarrow)$, yield derivations $d_{1}$ and $d_{2}$, respectively, such
that

$\displaystyle d_{1}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}_{1}(\bar{w},y),\mathrm{\Gamma}_{2}(\bar{w},y),\varphi(\bar{w},y)\to\psi(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi_{1}(\bar{w})\to\chi_{2}(\bar{w}),$
$\displaystyle d_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi_{1}(\bar{w},z),\Pi_{2}(\bar{w},z),\chi_{1}(\bar{w})\to\chi_{2}(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

Clearly, the constraints on ${\rm md}(d_{1})$ and ${\rm md}(d_{2})$ are
satisfied.

Now suppose that $\mathrm{\Gamma}(\bar{w},y)$ and $\Pi(\bar{w},z)$ are of the
form $\mathrm{\Gamma}_{1}(\bar{w},y),\mathrm{\Gamma}_{2}(\bar{w},y)$ and
$\Pi_{1}(\bar{w},z),\Pi_{2}(\bar{w},z),\varphi(\bar{w},z)\to\psi(\bar{w},z)$,
respectively, and

$\displaystyle d^{\prime}_{1}$
$\displaystyle\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}_{1}(\bar{w},y),\Pi_{1}(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi(\bar{w},z),$
$\displaystyle d^{\prime}_{2}$
$\displaystyle\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}_{2}(\bar{w},y),\Pi_{2}(\bar{w},z),\psi(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

Two applications of the induction hypothesis yield formulas
$\chi_{1}(\bar{w}),\chi_{2}(\bar{w})$ and derivations
$d^{\prime}_{11},d^{\prime}_{12},d^{\prime}_{21},d^{\prime}_{22}$ such that

$\displaystyle d^{\prime}_{11}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}_{1}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi_{1}(\bar{w}),$
$\displaystyle\quad d^{\prime}_{12}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi_{1}(\bar{w},z),\chi_{1}(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi(\bar{w},z),$
$\displaystyle d^{\prime}_{21}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}_{2}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi_{2}(\bar{w}),$
$\displaystyle\quad d^{\prime}_{22}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi_{2}(\bar{w},z),\psi(\bar{w},z),\chi_{2}(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

Let $\chi(\bar{w}):=\chi_{1}(\bar{w})\cdot\chi_{2}(\bar{w})$. Then
$d^{\prime}_{11},d^{\prime}_{21}$, together with an application of
$(\Rightarrow\\!\cdot)$, and $d^{\prime}_{12},d^{\prime}_{22}$, together with
applications of $(\to\Rightarrow)$ and $(\cdot\\!\Rightarrow)$, yield
derivations $d_{1}$ and $d_{2}$, respectively, such that

$\displaystyle d_{1}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}_{1}(\bar{w},y),\mathrm{\Gamma}_{2}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi_{1}(\bar{w})\cdot\chi_{2}(\bar{w}),$
$\displaystyle d_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi_{1}(\bar{w},z),\Pi_{2}(\bar{w},z),\varphi(\bar{w},z)\to\psi(\bar{w},z),\chi_{1}(\bar{w})\cdot\chi_{2}(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

Again, the constraints on ${\rm md}(d_{1})$ and ${\rm md}(d_{2})$ are clearly
satisfied.

Next, we consider all cases where $d$ ends with an application of one of the
quantifier rules.

  1. $\bullet$

$({\forall\\!\Rightarrow})$: Suppose first that $\mathrm{\Gamma}(\bar{w},y)$
is $\mathrm{\Gamma}^{\prime}(\bar{w},y),(\forall{x})\varphi(x)$ and

$\displaystyle d^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}^{\prime}(\bar{w},y),\varphi(u),\Pi(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z),$

where ${\rm md}(d^{\prime})={\rm md}(d)$. For subcase (i), suppose that
$u\in\bar{w}\cup\\{y\\}$. By the induction hypothesis, there exist a formula
$\chi(\bar{w})$ and derivations $d_{1}^{\prime},d_{2}$ such that ${\rm
md}(d_{1}^{\prime}),{\rm md}(d_{2})\leq{\rm md}(d^{\prime})$ and

$\displaystyle d_{1}^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}^{\prime}(\bar{w},y),\varphi(u){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi(\bar{w}),\quad
d_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(\bar{w},z),\chi(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

Extending $d_{1}^{\prime}$ with an application of $({\forall\\!\Rightarrow})$
yields a derivation $d_{1}$ such that ${\rm md}(d_{1})={\rm
md}(d_{1}^{\prime})\leq{\rm md}(d^{\prime})={\rm md}(d)$ and

$\displaystyle d_{1}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}^{\prime}(\bar{w},y),(\forall{x})\varphi(x){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi(\bar{w}).$

For subcase (ii), suppose that $u=z$. By the induction hypothesis, there
exists a formula $\chi^{\prime}(\bar{w})$ and derivations
$d_{1}^{\prime},d_{2}^{\prime}$ such that ${\rm md}(d_{1}^{\prime}),{\rm
md}(d_{2}^{\prime})\leq{\rm md}(d^{\prime})$ and

$\displaystyle d_{1}^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}^{\prime}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi^{\prime}(\bar{w}),\quad
d_{2}^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\varphi(z),\Pi(\bar{w},z),\chi^{\prime}(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

Let $\chi(\bar{w})\coloneqq\chi^{\prime}(\bar{w})\cdot(\forall{x})\varphi(x)$.
Combining an instance
$(\forall{x})\varphi(x){\vphantom{A}\Rightarrow{\vphantom{A}}}(\forall{x})\varphi(x)$
of $(\textsc{id})$ with $d_{1}^{\prime}$ and an application of
$(\Rightarrow\\!\cdot)$ to $d_{1}^{\prime}$ yields a derivation $d_{1}$ such
that ${\rm md}(d_{1})={\rm md}(d_{1}^{\prime})\leq{\rm md}(d^{\prime})={\rm
md}(d)$ and

$\displaystyle d_{1}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}^{\prime}(\bar{w},y),(\forall{x})\varphi(x){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi^{\prime}(\bar{w})\cdot(\forall{x})\varphi(x).$

Also, $d_{2}^{\prime}$ extended with applications of
$({\forall\\!\Rightarrow})$ and $(\cdot\\!\Rightarrow)$ yields a derivation
$d_{2}$ such that ${\rm md}(d_{2})={\rm md}(d_{2}^{\prime})\leq{\rm
md}(d^{\prime})={\rm md}(d)$ and

$\displaystyle d_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(\bar{w},z),\chi^{\prime}(\bar{w})\cdot(\forall{x})\varphi(x){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

Now suppose that $\Pi(\bar{w},z)$ is
$\Pi^{\prime}(\bar{w},z),(\forall{x})\varphi(x)$ and

$\displaystyle d^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y),\Pi^{\prime}(\bar{w},z),\varphi(u){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z),$

where ${\rm md}(d^{\prime})={\rm md}(d)$. The case of $u\in\bar{w}\cup\\{z\\}$
is similar to subcase (i) above, so suppose $u=y$. By the induction
hypothesis, there exist a formula $\chi^{\prime}(\bar{w})$ and derivations
$d_{1}^{\prime},d_{2}^{\prime}$ such that ${\rm md}(d_{1}^{\prime}),{\rm
md}(d_{2}^{\prime})\leq{\rm md}(d^{\prime})$ and

$\displaystyle d_{1}^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y),\varphi(y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi^{\prime}(\bar{w}),\quad
d_{2}^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi^{\prime}(\bar{w},z),\chi^{\prime}(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

Let $\chi(\bar{w})\coloneqq(\forall{x})\varphi(x)\to\chi^{\prime}(\bar{w})$.
Extending $d_{1}^{\prime}$ with applications of $({\forall\\!\Rightarrow})$
and $(\Rightarrow\to)$ yields a derivation $d_{1}$ such that ${\rm
md}(d_{1})={\rm md}(d_{1}^{\prime})\leq{\rm md}(d^{\prime})={\rm md}(d)$ and

$\displaystyle d_{1}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}(\forall{x})\varphi(x)\to\chi^{\prime}(\bar{w}).$

Also, $d_{2}^{\prime}$ and
$(\forall{x})\varphi(x){\vphantom{A}\Rightarrow{\vphantom{A}}}(\forall{x})\varphi(x)$
combined with an application of $(\to\Rightarrow)$ yields a derivation $d_{2}$
such that ${\rm md}(d_{2})={\rm md}(d_{2}^{\prime})\leq{\rm
md}(d^{\prime})={\rm md}(d)$ and

$\displaystyle d_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi^{\prime}(\bar{w},z),(\forall{x})\varphi(x),(\forall{x})\varphi(x)\to\chi^{\prime}(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

  2. $\bullet$

$(\Rightarrow\\!\forall)$: Suppose that $\mathrm{\Delta}(\bar{w},z)$ is
$(\forall{x})\varphi(x)$ and for some variable $u$ that does not occur freely
in
$\mathrm{\Gamma}(\bar{w},y),\Pi(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}(\forall{x})\varphi(x)$,

$\displaystyle d^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y),\Pi(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi(u),$

where ${\rm md}(d^{\prime})={\rm md}(d)-1$. By the induction hypothesis, there
exist a formula $\chi^{\prime}(\bar{w},u)$ and derivations
$d^{\prime}_{1},d^{\prime}_{2}$ such that ${\rm md}(d^{\prime}_{1}),{\rm
md}(d^{\prime}_{2})\leq{\rm md}(d^{\prime})$ and

$\displaystyle d_{1}^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi^{\prime}(\bar{w},u),\quad
d^{\prime}_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(\bar{w},z),\chi^{\prime}(\bar{w},u){\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi(u).$

Let $\chi(\bar{w})\coloneqq(\forall{x})\chi^{\prime}(\bar{w},x)$. Extending
$d_{1}^{\prime}$ with an application of $(\Rightarrow\\!\forall)$ yields a
derivation $d_{1}$ such that ${\rm md}(d_{1})={\rm
md}(d_{1}^{\prime})+1\leq{\rm md}(d^{\prime})+1={\rm md}(d)$ and

$\displaystyle d_{1}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi(\bar{w}).$

Also, extending $d_{2}^{\prime}$ with applications of
$({\forall\\!\Rightarrow})$ and $(\Rightarrow\\!\forall)$ yield a derivation
$d_{2}$ such that ${\rm md}(d_{2})={\rm md}(d^{\prime}_{2})+1\leq{\rm
md}(d^{\prime})+1={\rm md}(d)$ and

$\displaystyle d_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(\bar{w},z),\chi(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}(\forall{x})\varphi(x).$

  3. $\bullet$

$(\Rightarrow\\!\exists)$: Suppose that $\mathrm{\Delta}(\bar{w},z)$ is
$(\exists{x})\varphi(x)$ and

$\displaystyle d^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y),\Pi(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi(u),$

where ${\rm md}(d^{\prime})={\rm md}(d)$. For subcase (i), suppose that
$u\in\bar{w}\cup\\{z\\}$. By the induction hypothesis, there exist a formula
$\chi(\bar{w})$ and derivations $d_{1},d_{2}^{\prime}$ such that ${\rm
md}(d_{1}),{\rm md}(d_{2}^{\prime})\leq{\rm md}(d^{\prime})$ and

$\displaystyle\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi(\bar{w}),\quad
d_{2}^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(\bar{w},z),\chi(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi(u).$

Extending $d_{2}^{\prime}$ with an application of $(\Rightarrow\\!\exists)$
yields a derivation $d_{2}$ such that ${\rm md}(d_{2})={\rm
md}(d_{2}^{\prime})\leq{\rm md}(d^{\prime})$ and

$\displaystyle d_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(\bar{w},z),\chi(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}(\exists{x})\varphi(x).$

For subcase (ii), suppose that $u=y$. By the induction hypothesis, there
exists a formula $\chi^{\prime}(\bar{w})$ and derivations
$d_{1}^{\prime},d_{2}^{\prime}$ such that ${\rm md}(d_{1}^{\prime}),{\rm
md}(d_{2}^{\prime})\leq{\rm md}(d^{\prime})$ and

$\displaystyle d_{1}^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi^{\prime}(\bar{w}),\quad
d_{2}^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y),\chi^{\prime}(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\varphi(y).$

Let $\chi(\bar{w})\coloneqq\chi^{\prime}(\bar{w})\to(\exists{x})\varphi(x)$.
Combining $d_{2}^{\prime}$ with applications of $(\Rightarrow\\!\exists)$ and
$(\Rightarrow\to)$ yields a derivation $d_{1}$ such that ${\rm md}(d_{1})={\rm
md}(d_{2}^{\prime})\leq{\rm md}(d^{\prime})={\rm md}(d)$ and

$\displaystyle d_{1}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi^{\prime}(\bar{w})\to(\exists{x})\varphi(x).$

Also, combining the instance
$(\exists{x})\varphi(x){\vphantom{A}\Rightarrow{\vphantom{A}}}(\exists{x})\varphi(x)$
of $(\textsc{id})$ and $d_{1}^{\prime}$ with $(\to\Rightarrow)$ yields a
derivation $d_{2}$ such that ${\rm md}(d_{2})={\rm md}(d_{1}^{\prime})\leq{\rm
md}(d^{\prime})={\rm md}(d)$ and

$\displaystyle d_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(\bar{w},z),\chi^{\prime}(\bar{w})\to(\exists{x})\varphi(x){\vphantom{A}\Rightarrow{\vphantom{A}}}(\exists{x})\varphi(x).$

  4. $\bullet$

$(\exists\\!\Rightarrow)$: Suppose first that $\mathrm{\Gamma}(\bar{w},y)$ is
$\mathrm{\Gamma}^{\prime}(\bar{w},y),(\exists{x})\varphi(x)$ and for some
variable $u$ that does not occur freely in
$\mathrm{\Gamma}(\bar{w},y),\Pi(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z)$,

$\displaystyle d^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}^{\prime}(\bar{w},y),\varphi(u),\Pi(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z),$

where ${\rm md}(d^{\prime})={\rm md}(d)-1$. By the induction hypothesis, there
exist a formula $\chi^{\prime}(\bar{w},u)$ and derivations
$d_{1}^{\prime},d_{2}^{\prime}$ such that ${\rm md}(d_{1}^{\prime}),{\rm
md}(d_{2}^{\prime})\leq{\rm md}(d^{\prime})$ and

$\displaystyle\qquad d_{1}^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}^{\prime}(\bar{w},y),\varphi(u){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi^{\prime}(\bar{w},u),\quad
d_{2}^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(\bar{w},z),\chi^{\prime}(\bar{w},u){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

We define $\chi(\bar{w})$ to be $(\exists{u})\chi^{\prime}(\bar{w},u)$. Then
applications of $(\Rightarrow\\!\exists)$ and $(\exists\\!\Rightarrow)$ to
$d_{1}$ yield a derivation $d_{1}$ such that ${\rm md}(d_{1})={\rm
md}(d_{1}^{\prime})+1\leq{\rm md}(d^{\prime})+1={\rm md}(d)$ and

$\displaystyle d_{1}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}^{\prime}(\bar{w},y),(\exists{x})\varphi(x){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi(\bar{w}).$

An application of $(\exists\\!\Rightarrow)$ yields a derivation $d_{2}$
satisfying ${\rm md}(d_{2})={\rm md}(d_{2}^{\prime})+1\leq{\rm
md}(d^{\prime})+1={\rm md}(d)$ and

$\displaystyle d_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(\bar{w},z),\chi(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

Now suppose $\Pi(\bar{w},z)$ is
$\Pi^{\prime}(\bar{w},z),(\exists{x})\varphi(x)$ and for some variable $u$
that does not occur freely in
$\mathrm{\Gamma}(\bar{w},y),\Pi(\bar{w},z){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z)$,

$\displaystyle d^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y),\Pi^{\prime}(\bar{w},z),\varphi(u){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z),$

where ${\rm md}(d^{\prime})={\rm md}(d)-1$. By the induction hypothesis, there
exist a formula $\chi^{\prime}(\bar{w},u)$ and derivations
$d_{1}^{\prime},d_{2}^{\prime}$ such that ${\rm md}(d_{1}^{\prime}),{\rm
md}(d_{2}^{\prime})\leq{\rm md}(d^{\prime})$ and

$\displaystyle\quad d_{1}^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi^{\prime}(\bar{w},u),\quad
d_{2}^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi^{\prime}(\bar{w},z),\varphi(u),\chi(\bar{w},u){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$

Let $\chi(\bar{w})\coloneqq(\forall{x})\chi^{\prime}(\bar{w},x)$. The
derivation $d_{1}^{\prime}$ together with an application of
$(\Rightarrow\\!\forall)$ yields a derivation $d_{1}$ satisfying ${\rm
md}(d_{1})={\rm md}(d_{1}^{\prime})+1\leq{\rm md}(d^{\prime})+1={\rm md}(d)$
and

$\displaystyle d_{1}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(\bar{w},y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi(\bar{w}).$

Then $d_{2}^{\prime}$ together with applications of
$({\forall\\!\Rightarrow})$ and $(\exists\\!\Rightarrow)$ yields a derivation
$d_{2}$ satisfying ${\rm md}(d_{2})={\rm md}(d_{2}^{\prime})+1\leq{\rm
md}(d^{\prime})+1={\rm md}(d)$ and

$d_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(\bar{w},y),(\exists{x})\varphi(x),\chi(\bar{w}){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(\bar{w},z).$
∎

∎

Using this lemma we can now reprove using proof-theoretic means the special
case of Corollary 4.2 for the variety $\mathsf{FL_{e}}$.

######  Theorem 5.3.

For any set $T\cup\\{\varphi\approx\psi\\}$ of ${\rm
Fm}_{\forall}^{1}(\mathcal{L}_{s})$-equations,

$\displaystyle
T\vDash^{\forall}_{\mathsf{FL_{e}}}\varphi\approx\psi\quad\Longleftrightarrow\quad
T^{\ast}\vDash_{\mathsf{mFL_{e}}}\varphi^{\ast}\approx\psi^{\ast}.$

###### Proof.

The right-to-left direction follows directly from Corollary 3.8. For the
converse, note first that due to compactness and the local deduction theorem
for $\vDash^{\forall}_{\mathsf{V}}$ (see [CN21, Sections 4.6, 4.8]), we can
restrict to the case where $T=\emptyset$. Hence, by Proposition 5.1, it
suffices to prove that for any sequent
$\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}$
consisting only of formulas from ${\rm Fm}_{\forall}^{1}(\mathcal{L}_{s})$,

$\displaystyle\textstyle d\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\quad\Longrightarrow\quad\vDash_{\mathsf{mFL_{e}}}(\prod\mathrm{\Gamma})^{\ast}\leq(\sum\mathrm{\Delta})^{\ast}.$

We proceed by induction on the lexicographically ordered pair $\langle{{\rm
md}(d),0pt(d)}\rangle$, where $0pt(d)$ is the height of the derivation $d$.
The base cases are clear and the cases for the last application of a rule in
$d$ except $(\Rightarrow\\!\forall)$ and $(\exists\\!\Rightarrow)$ all follow
by applying the induction hypothesis and the equations defining
$\mathsf{mFL_{e}}$. Just note that for each such application, the premises
contain only formulas from ${\rm Fm}_{\forall}^{1}(\mathcal{L}_{s})$ with at
least one fewer symbol. In particular, for $({\forall\\!\Rightarrow})$ and
$(\Rightarrow\\!\exists)$, it can be assumed that the variable $u$ occurring
in the premise is $x$ and the result follows using (L1□) or (L1◇).

Suppose now that the last rule applied in $d$ is $(\Rightarrow\\!\forall)$,
where $\mathrm{\Delta}$ is $(\forall{x})\psi(x)$ and $x$ may occur freely in
$\mathrm{\Gamma}$. Then $d^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\psi(z)$ with
${\rm md}(d^{\prime})={\rm md}(d)-1$, where $z$ is a variable distinct from
$x$. We write $\mathrm{\Gamma}(y)$ and $d^{\prime}(y)$ to denote
$\mathrm{\Gamma}$ and $d^{\prime}$ with all free occurrences of $x$ replaced
by $y$. Clearly, $d^{\prime}(y)\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(y){\vphantom{A}\Rightarrow{\vphantom{A}}}\psi(z)$
with ${\rm md}(d^{\prime}(y))={\rm md}(d^{\prime})$. Hence, by Lemma 5.2,
there exist a sentence $\chi$ and derivations $d_{1},d_{2}$ such that ${\rm
md}(d_{1}),{\rm md}(d_{2})\leq{\rm md}(d^{\prime})$ and

$\displaystyle d_{1}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\mathrm{\Gamma}(y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi,\quad
d_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\chi{\vphantom{A}\Rightarrow{\vphantom{A}}}\psi(z).$

Since $\chi$ is a sentence and $x$ does not occur freely in
$\mathrm{\Gamma}(y)$ or $\psi(z)$, we can assume that $d_{1}$ and $d_{2}$ do
not contain any free occurrences of $x$, and, substituting all occurrences of
$y$ in $d_{1}$, and $z$ in $d_{2}$, by $x$, obtain derivations
$d^{\prime}_{1}$ of
$\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\chi$ and
$d^{\prime}_{2}$ of $\chi{\vphantom{A}\Rightarrow{\vphantom{A}}}\psi(x)$ with
${\rm md}(d^{\prime}_{1})={\rm md}(d_{1})$ and ${\rm md}(d^{\prime}_{2})={\rm
md}(d_{2})$. Hence, by the induction hypothesis twice,
$\vDash_{\mathsf{mFL_{e}}}(\prod\mathrm{\Gamma})^{\ast}\leq\chi^{\ast}$ and
$\vDash_{\mathsf{mFL_{e}}}\chi^{\ast}\leq\psi(x)^{\ast}$. Since $\chi$ is a
sentence, the equations defining $\mathsf{mFL_{e}}$ yield also
$\vDash_{\mathsf{mFL_{e}}}\chi^{\ast}\leq((\forall{x})\psi(x))^{\ast}$. So
$\vDash_{\mathsf{mFL_{e}}}(\prod\mathrm{\Gamma})^{\ast}\leq((\forall{x})\psi(x))^{\ast}$.

Suppose finally that the last rule applied in $d$ is
$(\exists\\!\Rightarrow)$, where $\mathrm{\Gamma}$ is
$\Pi,(\exists{x})\psi(x)$ and $x$ may occur freely in $\Pi$ and
$\mathrm{\Delta}$. Then $d^{\prime}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi,\psi(y){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}$
with ${\rm md}(d^{\prime})={\rm md}(d)-1$, where $y$ is a variable distinct
from $x$. We write $\Pi(z)$, $\mathrm{\Delta}(z)$, and $d^{\prime}(z)$ to
denote $\Pi$, $\mathrm{\Delta}$, and $d^{\prime}$ with all free occurrences of
$x$ replaced by $z$. Clearly,
$d^{\prime}(z)\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(z),\psi(y){\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(z)$
with ${\rm md}(d^{\prime}(z))={\rm md}(d^{\prime})$. By Lemma 5.2, there exist
a sentence $\chi$ and derivations $d_{1},d_{2}$ such that ${\rm
md}(d_{1}),{\rm md}(d_{2})\leq{\rm md}(d^{\prime})$ and

$\displaystyle d_{1}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\psi(y){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi,\quad
d_{2}\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}}}}\Pi(z),\chi{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}(z).$

Since $\chi$ is a sentence and $x$ does not occur freely in $\psi(y)$,
$\Pi(z)$, or $\mathrm{\Delta}(z)$, we can assume that $d_{1}$ and $d_{2}$ do
not contain any free occurrences of $x$, and, substituting all occurrences of
$y$ in $d_{1}$, and $z$ in $d_{2}$, by $x$, obtain derivations
$d^{\prime}_{1}$ of $\psi(x){\vphantom{A}\Rightarrow{\vphantom{A}}}\chi$ and
$d^{\prime}_{2}$ of
$\Pi,\chi{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}$ with ${\rm
md}(d^{\prime}_{1})={\rm md}(d_{1})$ and ${\rm md}(d^{\prime}_{2})={\rm
md}(d_{2})$. Hence, by the induction hypothesis,
$\vDash_{\mathsf{mFL_{e}}}\psi(x)^{\ast}\leq\chi^{\ast}$ and
$\vDash_{\mathsf{mFL_{e}}}(\prod(\mathrm{\Gamma}^{\prime},\chi))^{\ast}\leq(\sum\mathrm{\Delta})^{\ast}$.
Since $\chi$ is a sentence, the equations defining $\mathsf{mFL_{e}}$ yield
also $\vDash_{\mathsf{mFL_{e}}}((\exists{x})\psi(x))^{\ast}\leq\chi^{\ast}$.
So
$\vDash_{\mathsf{mFL_{e}}}(\prod(\Pi,(\exists{x})\psi(x)))^{\ast}\leq(\sum\mathrm{\Delta})^{\ast}$.
∎

The proof-theoretic strategy described above extends easily to varieties of
$\mathsf{FL_{e}}$-algebras axiomatized relative to $\mathsf{FL_{e}}$ by
equations of a certain simple form. Given a variable $x$, let $x^{0}:={\rm e}$
and $x^{k+1}:=x\cdot x^{k}$, for each $k\in\mathbb{N}$, and given a multiset
$\Pi$ and $k\in\mathbb{N}$, let $\Pi^{k}$ denote the multiset union of $k$
copies of $\Pi$. Now let $S$ be the set of equations $\\{x\leq x^{k}\mid
k\in\mathbb{N}\\}\cup\\{{\rm f}\leq x\\}$, and define sequent rules

$\displaystyle r(x\leq
x^{k})=\vbox{$\mathrm{\Gamma}_{1},\Pi,\mathrm{\Gamma}_{2}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\mathrm{\Gamma}_{1},\Pi^{k},\mathrm{\Gamma}_{2}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}$}\quad\text{and}\quad
r({\rm f}\leq
x)=\vbox{$\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}$}.$

Given any $S^{\prime}\subseteq S$, denote by $\mathsf{FL_{e}}+S^{\prime}$ the
variety of $\mathsf{FL_{e}}$-algebras axiomatized relative to
$\mathsf{FL_{e}}$ by the equations in $S^{\prime}$, and by $\mathrm{\forall
1FL_{e}}+r(S^{\prime})$ the sequent calculus $\mathrm{\forall 1FL_{e}}$
extended with the rules $r(\varepsilon)$ for each equation $\varepsilon$ in
$S^{\prime}$. Then for any sequent
$\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}$
containing formulas from ${\rm Fm}_{\forall}^{1}$ (see, e.g., [OK85, Kom86]),

$\displaystyle\textstyle\vdash_{{}_{\mathrm{\mathrm{\forall
1FL_{e}}+r(S^{\prime})}}}\mathrm{\Gamma}{\vphantom{A}\Rightarrow{\vphantom{A}}}\mathrm{\Delta}\quad\Longleftrightarrow\quad\>\vDash^{\forall}_{\mathsf{FL_{e}}+S^{\prime}}\prod\mathrm{\Gamma}\leq\sum\mathrm{\Delta}.$

Moreover, the additional cases required to adapt the proof of Lemma 5.2 to
$\mathrm{\forall 1FL_{e}}+r(S^{\prime})$ are straightforward, since each
application of a rule $r(\varepsilon)$ for $\varepsilon\in S^{\prime}$ has
just one premise. Hence, following the proof of Theorem 5.3 yields the
following more general result.

######  Theorem 5.4.

For any $S^{\prime}\subseteq S$ and set $T\cup\\{\varphi\approx\psi\\}$ of
${\rm Fm}_{\forall}^{1}(\mathcal{L})$-equations,

$\displaystyle
T\vDash^{\forall}_{\mathsf{FL_{e}}+S^{\prime}}\varphi\approx\psi\quad\Longleftrightarrow\quad
T^{\ast}\vDash_{\mathsf{mFL_{e}}+S^{\prime}}\varphi^{\ast}\approx\psi^{\ast}.$

In particular, we obtain new completeness proofs for the axiomatizations of
the one-variable fragments of the first-order extensions of
$\mathrm{FL_{ew}}$, $\mathrm{FL_{ec}}$, and $\mathrm{FL_{ewc}}$
(intuitionistic logic).

##  6 Concluding remarks

Let us conclude this paper by mentioning some interesting directions for
further research. The most general challenge for a class $\mathsf{K}$ of
$\mathcal{L}$-lattices may be stated as follows: provide a (natural)
axiomatization of the equational consequence relation
$\vDash^{\forall}_{\mathsf{K}}$, or, equivalently, in algebraic terms, provide
a (natural) axiomatization of the generalized quasivariety generated by the
class of all $\langle{\mathbf{A},W}\rangle$-functional
m-$\mathcal{L}$-lattices where $\mathbf{A}\in\mathsf{K}$ and $W$ is any set.
In this paper, we have shown that when $\mathsf{K}$ is a variety of
$\mathcal{L}$-lattices that has the superamalgamation property, the required
generalized quasivariety is the variety $\mathsf{mK}$ of
m-$\mathcal{L}$-lattices (Corollary 4.2), axiomatized relative to $\mathsf{K}$
by a set of axioms familiar from modal logic. However, if $\mathsf{K}$ lacks
the superamalgamation property or is not a variety, further axioms may be
required.

One potential generalization is to consider varieties of
$\mathcal{L}$-lattices that have the weaker “super generalized amalgamation
property”, which corresponds for substructural logics (even those without
exchange) to the Craig interpolation property [GJKO07]. In particular, such a
result would yield an axiomatization for the one-variable fragment of the
first-order version of the full Lambek Calculus $\mathrm{FL}$, although we
conjecture that completeness would hold only for valid equations and not
consequences. Alternatively, such a generalization might be established proof-
theoretically for first-order versions of substructural logics like
$\mathrm{FL}$ that have a cut-free sequent calculus, by lifting the proof-
theoretic strategy presented in Section 5 to sequents based on sequences of
formulas.

A further interesting line of inquiry concerns the case where $\mathsf{K}$
consists of the totally ordered members of a variety of
$\mathcal{L}$-lattices, and hence forms a positive universal class. First, let
$\mathsf{V}$ be any variety of semilinear $\mathrm{FL_{e}}$-algebras: algebras
that are isomorphic to a subdirect product of totally ordered
$\mathrm{FL_{e}}$-algebras. It is not hard to show that in this case,
$\vDash^{\forall}_{\mathsf{V}}(\exists{x})\varphi\cdot(\exists{x})\varphi\approx(\exists{x})(\varphi\cdot\varphi)$.
However, if $\textbf{\L}_{3}\in\mathsf{V}$ (e.g., if $\mathsf{V}$ is
$\mathsf{MV}$ or the variety of all semilinear $\mathrm{FL_{e}}$-algebras),
then (as proved in Example 3.2), $\not\vDash_{\mathsf{mV}}\Diamond
x\cdot\Diamond x\approx\Diamond(x\cdot x)$, so $\mathsf{mV}$ does not
correspond to the one-variable fragment of the first-order logic based on
$\mathsf{V}$.

Now let $\mathsf{V_{to}}$ be the class of totally ordered members of
$\mathsf{V}$. Then not only
$\vDash^{\forall}_{\mathsf{V_{to}}}(\exists{x})\varphi\cdot(\exists{x})\varphi\approx(\exists{x})(\varphi\cdot\varphi)$,
but also
$\vDash^{\forall}_{\mathsf{V_{to}}}(\forall{x})(\varphi\lor\psi)\approx(\forall{x})\varphi\lor\psi$,
where $x$ does not occur in $\psi$. Although a general approach to obtaining
axiomatizations of the one-variable fragments of the first-order logics based
on $\mathsf{V}$ and $\mathsf{V_{to}}$ is lacking, success for specific cases
indicate a possible way forward. Most notably, the one-variable fragment of
first-order Łukasiewicz logic can be defined over the class $\mathsf{MV_{to}}$
of totally ordered MV-algebras and corresponds to the variety of monadic MV-
algebras, defined relative to $\mathsf{mMV}$ by $\Diamond x\cdot\Diamond
x\approx\Diamond(x\cdot x)$ and $\Box(\Box x\lor y)\approx\Box x\lor\Box y$
[Rut59]. Interestingly, a proof of this latter result is given in [CCVR20]
using the fact that $\mathsf{MV_{to}}$ has the amalgamation property (see also
[MT20, Tuy21] for related results), suggesting that the approach developed in
this paper might be adapted to one-variable fragments of first-order logics
based on classes of totally ordered algebras that have the amalgamation
property.

## References

  * [1] Bez98 G.G.Bezhanishvili 19980 G. Bezhanishvili Varieties of monadic Heyting algebras - part I, Studia Logica, vol.61(1998), no.3, pp.367–402. bezhanishvili g 1998 varieties of monadic heyting algebras part i
  * [2] BH02 G.G.Bezhanishvili and J.J.Harding 20020 G. Bezhanishvili J. Harding Functional monadic Heyting algebras, Algebra Universalis, vol.48(2002), pp.1–10. bezhanishvili g harding j 2002 functional monadic heyting algebras
  * [3] BH04 G.G.Bezhanishvili and J.J.Harding 20040 MacNeille completions of Heyting algebras, Houston J. Math., vol.30(2004), pp.937–952. bezhanishvili g harding j 2004 macneille completions of heyting algebras
  * [4] Bul66 R.R.A.Bull 19660 R.A. Bull MIPC as formalisation of an intuitionist concept of modality, J. Symb. Log., vol.31(1966), pp.609–616. bull ra 1966 mipc as formalisation of an intuitionist concept of modality
  * [5] CMRR17 X.X.Caicedo, G.G.Metcalfe, R.R.Rodríguez, and J.J.Rogger 20170 X. Caicedo, G. Metcalfe, R. Rodríguez, J. Rogger Decidability in order-based modal logics, J. Comput. System Sci., vol.88(2017), pp.53–74. caicedo x metcalfe g rodriguez r rogger j 2017 decidability in order based modal logics
  * [6] CMRT22 X.X.Caicedo, G.G.Metcalfe, R.R.Rodríguez, and O.O.Tuyt 20220 X. Caicedo, G. Metcalfe, R. Rodríguez, O. Tuyt One-variable fragments of intermediate logics over linear frames., Inform. and Comput., vol.287(2022). caicedo x metcalfe g rodriguez r tuyt o 2022 one variable fragments of intermediate logics over linear frames
  * [7] CR15 X.X.Caicedo and R.R.Rodríguez 20150 X. Caicedo R. Rodríguez Bi-modal Gödel logic over $[0,1]$-valued Kripke frames, J. Logic Comput., vol.25(2015), no.1, pp.37–55. caicedo x rodriguez r 2015 bi modal godel logic over 01 valued kripke frames
  * [8] CCVR20 D.D.Castaño, C.C.Cimadamore, J.J.P.D.Varela, and L.L.Rueda 20210 D. Castaño, C. Cimadamore, J.P.D. Varela, L. Rueda Completeness for monadic fuzzy logics via functional algebras, Fuzzy Sets and Systems, vol.407(2021), pp.161–174. castano d cimadamore c varela jpd rueda l 2021 completeness for monadic fuzzy logics via functional algebras
  * [9] CGT11 A.A.Ciabattoni, N.N.Galatos, and K.K.Terui 20110 A. Ciabattoni, N. Galatos, K. Terui MacNeille completions of FL-algebras, Algebra Universalis, vol.66(2011), no.4, pp.405–420. ciabattoni a galatos n terui k 2011 macneille completions of fl algebras
  * [10] CGT12 A.A.Ciabattoni, N.N.Galatos, and K.K.Terui 20120 Algebraic proof theory for substructural logics: Cut-elimination and completions, Ann. Pure Appl. Logic, vol.163(2012), no.3, pp.266–290. ciabattoni a galatos n terui k 2012 algebraic proof theory for substructural logics cut elimination and completions
  * [11] CMT22 P.P.Cintula, G.G.Metcalfe, and N.N.Tokuda 20220 P. Cintula, G. Metcalfe, N. Tokuda Algebraic semantics for one-variable lattice-valued logics, Procedings of AiML 2022 (D. Fernandéz-Duque, A. Palmigiano, S. Pinchinat, editors), Advances in Modal Logic, vol. 14, College Publications,2022, pp.237–257. cintula p metcalfe g tokuda n 2022 algebraic semantics for one variable lattice valued logics
  * [12] CN21 P.P.Cintula and C.C.Noguera 20210 P. Cintula C. Noguera Logic and implication, Springer,2021. cintula p noguera c 2021 logic and implication
  * [13] dNG04 A.A.diNola and R.R.Grigolia 20040 A. di Nola R. Grigolia On monadic _MV_ -algebras, Ann. Pure Appl. Logic, vol.128(2004), no.1-3, pp.125–139. di nola a grigolia r 2004 on monadic emphmv algebras
  * [14] GJKO07 N.N.Galatos, P.P.Jipsen, T.T.Kowalski, and H.H.Ono 20070 N. Galatos, P. Jipsen, T. Kowalski, H. Ono Residuated lattices: An algebraic glimpse at substructural logics, Elsevier,2007. galatos n jipsen p kowalski t ono h 2007 residuated lattices an algebraic glimpse at substructural logics
  * [15] GP02 M.M.Gehrke and H.H.A.Priestley 20020 M. Gehrke H.A. Priestley Non-canonicity of _MV_ -algebras, Houston J. Math., vol.28(2002), no.3, pp.449–456. gehrke m priestley ha 2002 non canonicity of emphmv algebras
  * [16] Gra98 G.G.Grätzer 19980 G. Grätzer General lattice theory, 2 ed., Birkhäuser,1998. gratzer g 1998 general lattice theory
  * [17] Hal55 P.P.R.Halmos 19550 P.R. Halmos Algebraic logic, I. Monadic Boolean algebras, Compos. Math., vol.12(1955), pp.217–249. halmos pr 1955 algebraic logic i monadic boolean algebras
  * [18] Har08 J.J.Harding 20080 J. Harding A regular completion for the variety generated by the three-element Heyting algebra, Houston J. Math., vol.34(2008), no.3, pp.649–660. harding j 2008 regular completion for the variety generated by the three element heyting algebra
  * [19] Kom86 Y.Y.Komori 19860 Y. Komori Predicate logics without the structural rules, Studia Logica, vol.45(1986), no.4, pp.393–104. komori y 1986 predicate logics without the structural rules
  * [20] Mak92 L.L.L.Maksimova 19920 L.L. Maksimova Modal logics and varieties of modal algebras: The beth properties, interpolation, and amalgamation, Algebra i Logika, vol.31(1992), no.2, pp.145–166. maksimova ll 1992 modal logics and varieties of modal algebras the beth properties interpolation and amalgamation
  * [21] MPT23 G.G.Metcalfe, F.F.Paoli, and C.C.Tsinakis 20230 G. Metcalfe, F. Paoli, C. Tsinakis Residuated structures in algebra and logic, AMS Mathematical Surveys and Monographs, to appear,2023. metcalfe g paoli f tsinakis c 2023 residuated structures in algebra and logic
  * [22] MT20 G.G.Metcalfe and O.O.Tuyt 20200 G. Metcalfe O. Tuyt A monadic logic of ordered abelian groups, Proc. AiML 2020, Advances in Modal Logic, vol. 13, College Publications,2020, pp.441–457. metcalfe g tuyt o 2020 monadic logic of ordered abelian groups
  * [23] MV57 A.A.Monteiro and O.O.Varsavsky 19570 A. Monteiro O. Varsavsky Algebras de Heyting monádicas, Actas de las X Jornadas de la Unión Matemática Argentina, Bahía Blanca,(1957), pp.52–62. monteiro a varsavsky o 1957 algebras de heyting monadicas
  * [24] OK85 H.H.Ono and Y.Y.Komori 19850 H. Ono Y. Komori Logic without the contraction rule, J. Symb. Log., vol.50(1985), pp.169–201. ono h komori y 1985 logic without the contraction rule
  * [25] OS88 H.H.Ono and N.-Y.N.-Y.Suzuki 19880 H. Ono N.-Y. Suzuki Relations between intuitionistic modal logics and intermediate predicate logics, Rep. Math. Logic, vol.22(1988), pp.65–87. ono h suzuki n y 1988 relations between intuitionistic modal logics and intermediate predicate logics
  * [26] Rau82 W.W.Rautenberg 19830 W. Rautenberg Modal tableau calculi and interpolation, J. Philos. Log., vol.12(1983), no.4, pp.403–423. rautenberg w 1983 modal tableau calculi and interpolation
  * [27] Rut59 J.J.D.Rutledge 19590 J.D. Rutledge A preliminary investigation of the infinitely many-valued predicate calculus, Ph.D. thesis, Cornell University, Ithaca,1959. rutledge jd 1959 preliminary investigation of the infinitely many valued predicate calculus
  * [28] Suz89 N.-Y.N.-Y.Suzuki 19890 N.-Y. Suzuki An algebraic approach to intuitionistic modal logics in connection with intermediate predicate logics,, Studia Logica,(1989), pp.141–155. suzuki n y 1989 algebraic approach to intuitionistic modal logics in connection with intermediate predicate logics
  * [29] Suz90 N.-Y.N.-Y.Suzuki 19900 Kripke bundles for intermediate predicate logics and Kripke frames for intuitionistic modal logics, Studia Logica, vol.49(1990), no.3, pp.289–306. suzuki n y 1990 kripke bundles for intermediate predicate logics and kripke frames for intuitionistic modal logics
  * [30] Tuy21 O.O.Tuyt 20210 O. Tuyt One-variable fragments of first-order many-valued logics, Ph.D. thesis, University of Bern,2021. tuyt o 2021 one variable fragments of first order many valued logics
  * [31]