###### Abstract

Following a characterization [10] of locally tabular logics with finitary (or
unitary) unification by their Kripke models we determine the unification types
of some intermediate logics (extensions of INT). There are exactly four
maximal logics with nullary unification ${\mathsf{L}}(\mathfrak{R}_{2}+)$,
${\mathsf{L}}(\mathfrak{R}_{2})\cap{\mathsf{L}}(\mathfrak{F}_{2})$,
${\mathsf{L}}(\mathfrak{G}_{3})$ and ${\mathsf{L}}(\mathfrak{G}_{3}+)$ and
they are tabular. There are only two minimal logics with hereditary finitary
unification: L($\mathbf{F}_{un}$), the least logic with hereditary unitary
unification, and L( $\mathbf{F}_{pr}$) the least logic with hereditary
projective approximation; they are locally tabular. Unitary and non-projective
logics need additional variables for mgu’s of some unifiable formulas, and
unitary logics with projective approximation are exactly projective. None of
locally tabular intermediate logics has infinitary unification. Logics with
finitary, but not hereditary finitary, unification are rare and scattered
among the majority of those with nullary unification, see the example of
$\mathsf{H}_{3}\mathsf{B}_{2}$ and its extensions.

Unification types and union splittings in intermediate logics

####

Institute of Mathematics, Silesian University, Bankowa 14, Katowice 40-007,
Poland<EMAIL_ADDRESS>
Institute of Computer Science, University of Opole, Oleska 48, Opole 45-052,
Poland<EMAIL_ADDRESS>
Institute of Computer Science, University of Opole, Oleska 48, Opole 45-052,
Poland<EMAIL_ADDRESS>

####

Keywords: unification types, intermediate logics, locally tabular logics,
Kripke models.

##  1 Introduction.

Unification, in general, is concerned with finding a substitution that makes
two terms equal. Unification in logic is the study of substitutions under
which a formula becomes provable in a a given logic L. In this case the
substitutions are called the unifiers of the formula in L (L-unifiers). If an
L-unifier for a formula $A$ exists, $A$ is called unifiable in L. An L-unifier
$\sigma$ for $A$ can be more general than the other L-unifier $\tau$, in
symbols $\sigma\preccurlyeq\tau$; the pre-order $\preccurlyeq$ of
substitutions gives rise to four unification types: $1$, $\omega$, $\infty$,
and $0$, from the ”best” to the ”worst”, see [2, 1]. Unification is unitary,
or it has the type $1$, if there is a most general unifier (mgu) for every
unifiable formula. Unification is finitary or infinitary if, for every
unifiable formula, there is a (finite or infinite) basis of unifiers. Nullary
unification means that no such basis of unifiers exists at all.

Silvio Ghilardi introduced unification in propositional (intuitionistic [14]
and modal [15]) logic. In [14] he showed that unification in INT is finitary,
but in KC it is unitary and any intermediate logic with unitary unification
contains KC. Dzik [5] uses the particular splitting of the lattice of
intermediate logics by the pair (L($\mathfrak{F}_{2}$),KC), where
L($\mathfrak{F}_{2}$) is the logic determined by the ‘2-fork frame’
$\mathfrak{F}_{2}$ depicted in Figure 3, to give location of logics with
finitary but not unitary unification: they all are included in
L($\mathfrak{F}_{2})$. In Wro$\acute{\rm n}$ski [29, 30], see also [7], it is
shown that unification in any intermediate logic L is projective iff L is an
extension of LC (that is it is one of Gödel-Dummett logics); projective
implies unitary unification. In Ghilardi [17] first examples of intermediate
logics with nullary unification are given. Iemhoff [19] contains a proof-
theoretic account of unification in fragments of intuitionistic logics. Many
papers concern unification in modal logics, see e.g. [15, 21, 3, 8, 22], and
also in intuitionistic predicate logic, see [9]. No (modal or intermediate)
logic with infinitary unification has been found so far and it is expected
that no such logic exists.

Generally, similar results on unification types in transitive modal logics and
corresponding intermediate logics are given in [10].

In [17] Ghilardi studied unification in intermediate logics of finite slices
(or finite depths). He applied his method, based on Category Theory, of
finitely presented projective objects (see [13]) and duality, and
characterized injective objects in finite posets. He gave some positive and
negative criteria for unification to be finitary. From these criteria it
follows, for instance, that bounded depth axioms $\mathsf{H_{n}}$ plus bounded
width axioms $\mathsf{B_{k}}$ keep unification finitary. It also follows that
there are logics without finitary unification.111Ghilardi’s original notation
of frames, as well as our notation of frames in [10], was quite different. All
frames depicted in this paper represent finite po-sets. He considered, among
others, the following frames:

$\mathfrak{G}_{1}:$$\mathfrak{G}_{2}:$$\mathfrak{G}_{3}:$${\mathfrak{G}_{3}}+:$
Fig. 1: Ghilardi’s Frames

Since $\mathsf{L}(\mathfrak{G}_{1})$, the logic of $\mathfrak{G}_{1}$,
coincides with $\mathsf{H}_{3}\mathsf{B}_{2}$, it has finitary unification by
[17]. Theorem 9, p.112 of [17]) says that, if $\mathfrak{G}_{3}$ is a frame of
any intermediate logic with finitary unification, then $\mathfrak{G}_{2}$ is a
frame of this logic, as well. It means, in particular, that
$\mathsf{L}(\mathfrak{G}_{3})$ has not finitary unification. (the unification
type of $\mathsf{L}(\mathfrak{G}_{2})$ and $\mathsf{L}(\mathfrak{G}_{3})$ was
not determined). Ghilardi announced that ‘attaching a final point everywhere’
provide examples in which unification is nullary. Thus,
$\mathsf{L}({\mathfrak{G}_{3}}+)$ has nullary unification.222The frame
received from $\mathfrak{F}$, by adding a top (=final) element is denoted by
${\mathfrak{F}}+$. He also showed that replacing one of maximal elements in
$\mathfrak{G}_{3}$ with any finite (rooted) po-set $\mathfrak{P}$, gives a
frame of logic without finitary unification, see Figure 2.

$\mathfrak{G}_{3\mathfrak{P}}:$$\mathfrak{P}$
Fig. 2: Frames of Logics with Nullary Unification

Hence, there are infinitely many intermediate logics without finitary (by
[10]: with nullary) unification. In [10] we gave necessary and sufficient
conditions for finitary (or unitary) unification in locally tabular logics
solely in terms of mappings between (bounded) Kripke models. Our approach was
entirely different from that in [17]. A simpler variant of the conditions
characterizes logics with projective approximation. Then we applied the
conditions to determine the unification types of logics (intermediate or
modal) given by relatively simple frames. In particular, we studied tabular
modal and intermediate logics determined by the frames in Figure 3.

$\mathfrak{L}_{1}:$$\mathfrak{L}_{2}:$$\mathfrak{L}_{3}:$$\mathfrak{F}_{2}:$${\mathfrak{R}_{2}}:$

$\mathfrak{G}_{3}:$${\mathfrak{G}_{3}}+:$$\mathfrak{F}_{3}:$${\mathfrak{R}_{3}}:$

Fig. 3: Frames of [10]

We proved that unification in the modal (as well as intermediate) logics of
the frames
$\mathfrak{L}_{1},\mathfrak{L}_{2},\mathfrak{L}_{3},{\mathfrak{R}_{2}}$ and
${\mathfrak{R}_{3}}$ is unitary, in (the logic of) $\mathfrak{F}_{2}$ and
$\mathfrak{F}_{3}$ it is finitary and in $\mathfrak{G}_{3}$ and
$\mathfrak{G}_{3}+$ it is nullary. We have also considered $n$-forks
${\mathfrak{F}_{n}}$ and $n$-rhombuses ${\mathfrak{R}_{n}}$, for any $n\geq
2$, see Figure 4. We showed that the logic of any fork (including the infinite
‘fork frame’ ${\mathfrak{F}_{\infty}}$) has projective approximation, and
hance it has finitary unification. The logic of any rhombus (including
${\mathfrak{R}_{\infty}}$) has unitary unification.

${\mathfrak{F}_{n}}:$$\mathfrak{R}_{n}={\mathfrak{F}_{n}}+:$ Fig. 4: $n$-Fork
and $n$-Rhombus Frames, for $n\geq 1$.

Still many questions about unification of intermediate logics and location of
particular types remained open. Here is a summary of the results in the
present paper.
1) We give another proof that our conditions (see Theorem 22) are necessary
and sufficient for finitary/unitary unification, as well as for projective
approximation (Theorem 27) in locally tabular intermediate logics. Variants of
the frames in Figure 3 are considered and we determine the unification types
of their logics. In particular, we prove that unification in
$\mathsf{L}(\mathfrak{G}_{2})$ is finitary and though (we know that) it is
also finitary in $\mathsf{L}(\mathfrak{F}_{3})$, it is nullary in their
intersection $\mathsf{L}(\mathfrak{G}_{2})\cap\mathsf{L}(\mathfrak{F}_{3})$ .
2) It turns out that intermediate logics with unitary unification are either
projective (hence they are extensions of LC) or they need new variables for
mgu’s of some unifiable formulas. It means that any (non-projective) logic
with unitary unification has a unifiable formula $A(x_{1},\dots,x_{n})$ which
do not have any mgu in $n$-variables (but its mgu’s must introduce additional
variables – like in filtering unification). The same result for transitive
modal logics is proved in [10].
3) We prove that a locally tabular intermediate logic with infinitary
unification does not exist and we think that no intermediate logic has
infinitary unification.
4) We claim (and give some evidences) that ’most of’ intermediate logics have
nullary unification. For instance, logics of the following frames are nullary:

$\mathfrak{Y}_{1}:$$\mathfrak{Y}_{2}$:$\mathfrak{Y}_{2}+$:$\mathfrak{Y}_{3}$:${\mathfrak{Y}_{3}}+$:
Fig. 5: Frames of Logics with Nullary Unification

Intermediate logics with nullary unification can be found ’almost everywhere’.
Extensions of finitary/unitary logics may have nullary unification,
intersections of finitary logics may be nullary. We cannot put apart logics
with finitary/unitary unification from those with the nullary one.

5) In structurally complete logics 333We consider rules
$r\\!\\!:\\!\\!{A}/{B}$, where $A,B$ play the role of formula schemata, i.e.
$r$ enables us to derive $\varepsilon(B)$ from $\varepsilon(A)$, for any
substitution $\varepsilon$. The rule is said to be admissible in an
intermediate logic L (or L-admissible), if $\vdash_{\sf L}\varepsilon(A)$
implies $\vdash_{\sf L}\varepsilon(B)$, for any substitution $\varepsilon$,
that is any L-unifier for $A$ must be an L-unifier for $B$. The rule is
L-derivable if $A\vdash_{\sf L}B$. A logic L is structurally complete if every
its admissible rule is derivable (the reverse inclusion always holds).
Hereditary structural completeness of L means that any extension of L is
structurally complete. the situation is somehow similar. A.Citkin (see Tzitkin
[27]) characterized hereditary structurally complete logics (instead of
structurally complete) and showed that a logic L is hereditary structurally
complete iff L omits (i.e. L is falsified in) the following frames:

$\mathfrak{C}_{1}:$$\mathfrak{C}_{2}:$$\mathfrak{C}_{3}:$$\mathfrak{C}_{4}:$$\mathfrak{C}_{5}:$
Fig. 6: Citkin’s Frames

We consider logics with hereditary finitary unification that is logics all
their extensions have either finitary or unitary unification. We prove that
there are exactly four maximal logics with nullary unification:
$\mathsf{L}(\mathfrak{Y}_{1})$,
$\mathsf{L}(\mathfrak{R}_{2})\cap\mathsf{L}(\mathfrak{F}_{2})$,
$\mathsf{L}(\mathfrak{G}_{3})$ and $\mathsf{L}(\mathfrak{G}_{3}+)$. Thus, an
intermediate logic has hereditary finitary unification if it omits
$\mathfrak{Y}_{1}$, $\mathfrak{G}_{3}$, $\mathfrak{G}_{3}+$ and one of the
frames $\\{\mathfrak{R}_{2},\mathfrak{F}_{2}\\}$. This characterization is not
optimal as, for instance, omitting $\mathfrak{F}_{2}$ the logic omits
$\mathfrak{G}_{3}$; omitting $\mathfrak{R}_{2}$ it omits $\mathfrak{G}_{3}+$
and $\mathfrak{Y}_{1}$.

There is no correlation between structural completeness and finitary
unification. In particular, since $\mathfrak{C}_{1}=\mathfrak{F}_{3}$ the
logic of $\mathfrak{C}_{1}$ has projective approximation (and therefore it is
finitary), since $\mathfrak{C}_{2}=\mathfrak{R}_{3}$, $\mathfrak{C}_{2}$ is
unitary and we will show that the fifth $\mathsf{L}(\mathfrak{C}_{5})$ is
finitary but not hereditary finitary. The remaining frames $\mathfrak{C}_{3}$
and $\mathfrak{C}_{4}$ coincide with ${\mathfrak{G}_{\sf 3}}$ and
${\mathfrak{G}_{\sf 3}}+$ and their logics have nullary unification.
6) Two additional classes of logics emerge here: logics with hereditary
unitary unification and logics with hereditary projective approximation. We
show that an intermediate logic L has hereditary unitary unification iff L
omits the frames $\mathfrak{Y}_{1}$, $\mathfrak{F}_{2}$ and
$\mathfrak{G}_{3}+$. A logic L has hereditary projective approximation iff L
omits the frames $\mathfrak{R}_{2}$ and $\mathfrak{G}_{3}$. Thus, L has
hereditary finitary unification iff either L has hereditary unitary
unification or L has hereditary projective characterization. Logics with
hereditary projective approximation can be characterized by frames
$\mathfrak{L}_{d}+\mathfrak{F}_{n}$, for any $d,n\geq 0$ (that is forks on
chains), whereas logics with hereditary unitary unification by
$\mathfrak{L}_{d}+\mathfrak{R}_{n}$, for any $d,n\geq 0$ (that is rhombuses on
chains); see Figure 7.

$\mathbf{H}_{pa}$:$\mathbf{H}_{un}$: Fig. 7: Frames of Logics with Hereditary
Finitary Unification.

$\mathsf{L}(\mathbf{H}_{pa})$ is the least intermediate logic with hereditary
projective approximation and $\mathsf{L}(\mathbf{H}_{un})$ is the least logic
with hereditary unitary unification. The logics $\mathsf{L}(\mathbf{H}_{pa})$
and $\mathsf{L}(\mathbf{H}_{un})$ are locally tabular and they are (the only)
minimal logics with hereditary finitary unification. We have
$\mathsf{L}(\mathsf{L}(\mathbf{H}_{pa})\cup\mathsf{L}(\mathbf{H}_{un}))=\mathsf{LC}$
as, it is proved that, any unitary intermediate logic with projective
approximation is projective.

##  2 Basic Concepts.

###  2.1 Intermediate Logics.

We consider the standard language of intuitionistic propositional logic
$\\{\rightarrow,\lor,\land,\bot\\}$ where $\leftrightarrow,\neg,\top$ are
defined in the usual way. Let $\mathsf{Var}=\\{x_{1},x_{2},\dots\\}$ be the
set of propositional variables and $\mathsf{Fm}$ be the set of
(intuitionistic) formulas, denoted by $A,B,C,\dots$ For any $n\geq 0$, let
$\mathsf{Fm^{n}}$, be the set of formulas in the variables
$\\{x_{1},\dots,x_{n}\\}$, that is
$A\in\mathsf{Fm^{n}}\Leftrightarrow\mathsf{Var}(A)\subseteq\\{x_{1},\dots,x_{n}\\}\Leftrightarrow
A=A(x_{1},\dots,x_{n}).$

Substitutions $\alpha,\beta,\dots$ are finite mappings; for each $\alpha$
there are $k,n\geq 0$ such that
$\alpha\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$. The extension of
$\alpha$ to an endomorphism of $\mathsf{Fm}$ is also denoted by $\alpha$.
Thus, $\alpha(A)$ means the substitution of a formula $A$. Let
$\alpha\circ\tau$ be the composition of the substitutions, that is a
substitution such that $\alpha\circ\tau(A)=\alpha(\tau(A))$, for any $A$.

An intermediate logic L is any set of formulas containing the intuitionistic
logic INT, closed under the modus ponens rule MP and closed under
substitutions.444Intermediate logics may be regarded as fragments of
transitive modal logics (or extensions of S4, or Grz); the intuitionistic
variable $x_{i}$ is meant as $\Box^{+}x_{i}$ and $A\rightarrow B=\Box^{+}(\neg
A\lor B)$. All intermediate logics form, under inclusion, a (complete
distributive) lattice where inf$\\{\mathsf{L}_{i}\\}_{i\in I}=\bigcap_{i\in
I}\mathsf{L}_{i}$. Let $\mathsf{L}(X)$, for any set $X$ of formulas, mean the
least intermediate logic containing $X$. Given two intermediate logics L and
L’, we say L’ is an extension of L if
$\mathsf{L}\subseteq\mathsf{L}^{\prime}$. The least intermediate logic is INT.
Consistent logics are proper subsets of $\mathsf{Fm}$. We will refer to the
following list of formulas/logics:

$\begin{array}[]{ll}\mathsf{LC}:(x_{1}\rightarrow x_{2})\lor(x_{2}\rightarrow
x_{1});\qquad\qquad\mathsf{KC}:\neg x\lor\neg\neg x;&\\\
\mathsf{SL}:((\neg\neg x\rightarrow x)\rightarrow(\neg x\lor\neg\neg
x))\rightarrow(\neg x\lor\neg\neg x):&\mathsf{}\\\ \mathsf{PWL}:(x_{2}\to
x_{1})\lor\bigl{(}((x_{1}\to x_{2})\to x_{1})\to x_{1}\bigr{)};&{}\\\
\mathsf{H_{n}}:\ \mathsf{H}_{1}=x_{1}\lor\neg
x_{1},\qquad\mathsf{H}_{n+1}=x_{n+1}\lor(x_{n+1}\rightarrow\mathsf{H}_{n});&\mathsf{}\\\
\mathsf{B_{n}}:\bigwedge_{i=1}^{n+1}\Bigl{(}\bigl{(}x_{i}\rightarrow\bigvee_{j\not=i}x_{j}\bigr{)}\rightarrow\bigvee_{j\not=i}x_{j}\Bigr{)}\rightarrow\bigvee_{i=1}^{n+1}x_{i}.&\mathsf{}\end{array}$
Fig. 8: Intermediate Logics.

KC is called the logic of weak excluded middle or Jankov logic or de Morgan
logic (see [14]). SL is Scott logic and PWL is the logic of weak law of
Peirce, see [11].

We define the consequence relation $\vdash_{\mathsf{L}}$, for any given
intermediate logic $\mathsf{L}$, admitting only the rule $\mathsf{MP}$ in
derivations. Then we prove the deduction theorem

$X,A\vdash_{\mathsf{L}}B\quad\Leftrightarrow\quad
X\vdash_{\mathsf{L}}A\rightarrow B.$ $None$

The relation of $\mathsf{L}-equivalent$ formulas,

$A=_{\mathsf{L}}B\qquad\Leftrightarrow\qquad\vdash_{\mathsf{L}}A\leftrightarrow
B,$

leads to the standard Lindenbaum-Tarski algebra. The relation $=_{\mathsf{L}}$
extends to substitutions, $\varepsilon=_{\mathsf{L}}\mu$ means that
$\varepsilon(A)=_{\mathsf{L}}\mu(A)$, for each formula $A$. We define a pre-
order (that is a reflexive and transitive relation) on the set of
substitutions:

$\varepsilon\preccurlyeq_{\mathsf{L}}\mu\qquad\Leftrightarrow\qquad\bigl{(}\alpha\circ\varepsilon=_{\mathsf{L}}\mu,\mbox{
for some $\alpha$}\bigr{)}.$

Note that
$\varepsilon\preccurlyeq_{\mathsf{L}}\mu\land\mu\preccurlyeq_{\mathsf{L}}\varepsilon$
does not yield $\varepsilon=_{\mathsf{L}}\mu$. If
$\varepsilon\preccurlyeq_{\mathsf{L}}\mu$, we say that $\varepsilon$ is more
general than $\mu$. If it is not misleading, we omit the subscript L and write
$=$ and $\preccurlyeq$, instead of $=_{\mathsf{L}}$ and
$\preccurlyeq_{\mathsf{L}}$, correspondingly.

A frame $\mathfrak{F}=(W,R,w_{0})$ consists of a non-empty set $W$, a pre-
order $R$ on $W$ and a root $w_{0}\in W$ such that $w_{0}Rw$, for any $w\in
W.$ For any set $U$, let $P(U)=\\{V:V\subseteq U\\}$. Let $n$ be a natural
number. Any $n$-model $\mathfrak{M}^{n}=(W,R,w_{0},V^{n})$, over the frame
$(W,R,w_{0})$, contains a valuation $V^{n}:W\to P(\\{x_{1},\dots,x_{n}\\})$
which is monotone:

$uRw\quad\Rightarrow\quad V^{n}(u)\subseteq V^{n}(w),\quad\mbox{for each
}u,w\in W.$

Thus, $n$-models, are (bounded) variants of usual Kripke models
$\mathfrak{M}=(W,R,w_{0},V)$ where all variables are valuated; $V:W\to
P(\mathsf{Var})$. Given $\mathfrak{M}^{n}$ and $\mathfrak{M}^{k}$ (for
$n\not=k$), we do not assume that $\mathfrak{M}^{n}$ and $\mathfrak{M}^{k}$
have anything in common. In particular, we do not assume that there is any
model $\mathfrak{M}$ such that $\mathfrak{M}^{n}$ and $\mathfrak{M}^{k}$ are
its fragments. If $\mathfrak{M}^{k}=(W,R,w_{0},V^{k})$ and $n\leq k$, then
$\mathfrak{M}^{k}\\!\\!\upharpoonright_{n}$ is the restriction of
$\mathfrak{M}^{k}$ to the $n$-model. Thus,
$\mathfrak{M}^{k}\\!\\!\upharpoonright_{n}=(W,R,w_{0},V^{n})$ is the $n$-model
over the same frame as $\mathfrak{M}^{k}$ in which
$V^{n}(w)=V^{k}(w)\cap\\{x_{1},\dots,x_{n}\\}$, for each $w\in W$. We say
$(W,R,w_{0})$ is a po-frame, and $(W,R,w_{0},V^{n})$ is a po-model, if the
relation $R$ is a partial order.

Let $\mathfrak{F}=(W,\leq,w_{0})$ be a finite po-frame. We define the depth,
$d_{\mathfrak{F}}(w)$, of any element $w\in W$ in $\mathfrak{F}$. We let
$d_{\mathfrak{F}}(w)=1$ if $w$ is a $\leq$-maximal element ($\leq$-maximal
elements are also called end elements) and $d_{\mathfrak{F}}(w)=i+1$ if all
elements in $\\{u\in W\colon w<u\\}$ are of the depth at most $i$ and there is
at least one element $u>w$ of the depth $i$. The depth of the root,
$d_{\mathfrak{F}}(w_{0})$, is the depth of the frame $\mathfrak{F}$ (or any
$n$-model over $\mathfrak{F}$).

Let $\mathfrak{F}=(W,\leq_{W},w_{0})$ and $\mathfrak{G}=(U,\leq_{U},u_{0})$ be
two disjoint (that is $W\cap U=\emptyset$) po-frames. The join
$\mathfrak{F}+\mathfrak{G}$ of the frames is the frame $(W\cup U,\leq,w_{0})$
where

$x\leq y\qquad\Leftrightarrow\qquad x\leq_{W}y\quad\mbox{or}\quad
x\leq_{U}y\quad\mbox{or}\quad(x\in W\land y\in U).$

If $\mathfrak{F}$ and $\mathfrak{G}$ are not disjoint, we take their disjoint
isomorphic copies and the join of the copies is called the join of
$\mathfrak{F}$ and $\mathfrak{G}$ (it is also denoted by
$\mathfrak{F}+\mathfrak{G}$). Thus, the join of frames is defined up to an
isomorphism. The join is associative (up to an isomorphism) and it is not
commutative. Instead of $\mathfrak{F}+\mathfrak{L}_{1}$ and
$\mathfrak{L}_{1}+\mathfrak{G}$, where $\mathfrak{L}_{1}$ is one-element frame
(see Figure 3), we write $\mathfrak{F}+$ and $+\mathfrak{G}$, correspondingly.

Let $(W,R,w_{0},V^{n})$ be any $n$-model. The subsets $\\{V^{n}(w)\\}_{w\in
W}$ of $\\{x_{1},\dots,x_{n}\\}$ are usually given by their characteristic
functions $\mathfrak{f}_{w}^{n}\colon\\{x_{1},\dots,x_{n}\\}\to\\{0,1\\}$ or
binary strings $\mathfrak{f}_{w}^{n}=i_{1}\dots i_{n}$, where
$i_{k}\in\\{0,1\\}$. Thus, $n$-models may also appear in the form
$(W,R,w_{0},\\{V^{n}(w)\\}_{w\in W})$, or
$(W,R,w_{0},\\{\mathfrak{f}_{w}^{n}\\}_{w\in W})$. $n$-Models are usually
depicted as graphs whose nodes are labeled with binary strings.

The forcing relation $\mathfrak{M}^{n}\Vdash_{w}A$, for any $w\in W$ and
$A\in\mathsf{Fm}^{n}$, is defined as usual

$\mathfrak{M}^{n}\Vdash_{w}x_{i}\quad\Leftrightarrow\quad x_{i}\in
V^{n}(w),\qquad\mbox{ for any }i\leq
n;\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$
$\mathfrak{M}^{n}\Vdash_{w}\bot,\quad\mbox{for none }w\in
W;\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$
$\mathfrak{M}^{n}\Vdash_{w}(A\rightarrow
B)\quad\Leftrightarrow\quad\forall_{u}\bigl{(}wRu\quad\mbox{and}\quad\mathfrak{M}^{n}\Vdash_{u}A\quad\Rightarrow\quad\mathfrak{M}^{n}\Vdash_{u}B\bigr{)};\qquad\qquad\qquad\qquad\qquad\qquad$
$\mathfrak{M}^{n}\Vdash_{w}(A\lor
B)\quad\Leftrightarrow\quad\bigl{(}\mathfrak{M}^{n}\Vdash_{w}A\quad\mbox{or}\quad\mathfrak{M}^{n}\Vdash_{w}B\bigr{)};\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$
$\mathfrak{M}^{n}\Vdash_{w}(A\land
B)\quad\Leftrightarrow\quad\bigl{(}\mathfrak{M}^{n}\Vdash_{w}A\quad\mbox{and}\quad\mathfrak{M}^{n}\Vdash_{w}B\bigr{)}.\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$

###### Lemma 1

If $uRw$ and $\mathfrak{M}^{n}\Vdash_{u}A$, then
$\mathfrak{M}^{n}\Vdash_{w}A,\quad\mbox{for any }u,w\in W\mbox{ and
any}A\in\mathsf{Fm}^{n}.$

Let $(W)_{w}=\\{u\in W\colon wRu\\}$, for any $w\in W$. The subframe of
$(W,R,w_{0})$ generated by $w$ is $((W)_{w},R\upharpoonright_{(W)_{w}},w)$;
the submodel of $\mathfrak{M}^{n}$ generated by $w$ is

$(\mathfrak{M}^{n})_{w}=((W)_{w},R\\!\upharpoonright_{(W)_{w}},w,V^{n}\\!\\!\upharpoonright_{(W)_{w}}).$

We write $\mathfrak{M}^{n}\Vdash A$ if $\mathfrak{M}^{n}\Vdash_{w_{0}}A$ and
we obviously have $(\mathfrak{M}^{n})_{w}\Vdash
A\Leftrightarrow\mathfrak{M}^{n}\Vdash_{w}A$. For any $n$-model, we put
$\mathsf{Th}(\mathfrak{M}^{n})=\\{A\in\mathsf{Fm}^{n}\colon\mathfrak{M}^{n}\Vdash
A\\}$. Given two $n$-models $\mathfrak{M}^{n}$ and $\mathfrak{N}^{n}$, we say
they are equivalent, in symbols $\mathfrak{M}^{n}\thicksim\mathfrak{N}^{n}$,
if $\mathsf{Th}(\mathfrak{M}^{n})=\mathsf{Th}(\mathfrak{N}^{n}).$

Let $(W,\leq,w_{0},V^{n})$ and $(W,\leq,w_{0},V^{\prime\ n})$ be $n$-models
over the same po-frame, we say they are (mutual) variants if
$V(w)=V^{\prime}(w)$ for each $w\not=w_{0}$.

Let $\mathbf{F}$ be a class of frames and $\mathbf{M}^{n}(\mathbf{F})$, for
any $n\geq 0$, be the class of $n$-models over the frames $\mathbf{F}$; we
write $\mathbf{M}^{n}$, instead of $\mathbf{M}^{n}(\mathbf{F})$, if there is
no danger of confusion. The intermediate logic determined by $\mathbf{F}$ is
denoted by $\mathsf{L}(\mathbf{F})$. Thus, if $A\in\mathsf{Fm^{n}}$, then

$A\in\mathsf{L}(\mathbf{F})\quad\Leftrightarrow\quad(\mathfrak{M}^{n}\Vdash
A,\mbox{ for every }\mathfrak{M}^{n}\in\mathbf{M}^{n}).$

We say that F are frames of an intermediate logic L if
$\mathsf{L}\subseteq\mathsf{L}(\mathbf{F})$ and L omits a frame $\mathfrak{F}$
if $\mathfrak{F}$ is not a frame of L. A logic L is Kripke complete if
$\mathsf{L}=\mathsf{L}(\mathbf{F})$ for some $\mathbf{F}$. The logic
$\mathsf{L}(\mathbf{F})$ is said to be tabular if $\mathbf{F}$ is a finite
family of finite frames. L is Halldén complete (H-complete) if for any
formulas $A,B$ with $\mathsf{Var}(A)\cap\mathsf{Var}(B)=\emptyset$ we have

$\mathsf{L}\vdash A\lor B\quad\Rightarrow\quad\mathsf{L}\vdash A\quad\mbox{ or
}\quad\mathsf{L}\vdash B.$

###### Theorem 1

Let F be finite. Then $\mathsf{L}(\mathbf{F})$ is H-complete iff
$\mathsf{L}(\mathbf{F})=\mathsf{L}(\mathfrak{F})$ for some
$\mathfrak{F}\in\mathbf{F}$.

A logic L is locally tabular if Fm${}^{n}/\\!\\!=_{\mathsf{L}}$ is finite, for
each $n\geq 0$. Tabular logics are locally tabular but not vice versa. For
each locally tabular logic L there exists a family $\mathbf{F}$ of finite
frames such that $\mathsf{L}=\mathsf{L}(\mathbf{F})$. Thus, locally tabular
logics have the finite model property but, again, the converse is false. A
logic L is said to be in the $n$-slice if $\mathsf{L}=\mathsf{L}(\mathbf{F})$
for a family F of finite po-frames such that $d(\mathfrak{F})\leq n$, for any
$\mathfrak{F}\in\mathbf{F}$.

###### Theorem 2

Suppose that the family F consists of finite frames. Then
$\mathsf{L}(\mathbf{F})$ is locally tabular iff
$\mathbf{M}^{n}/\\!\\!\thicksim$ is finite, for each $n$.

  * Proof.

$(\Rightarrow)$ Using finitely many (up to equivalence) formulas we do not
distinguish infinitely many models. $(\Leftarrow)$ is obvious.

###### Corollary 1

(i) If L and L’ are locally tabular intermediate logics, then their
intersection $\mathsf{L}\cap\mathsf{L}^{\prime}$ is also a locally tabular
intermediate logic;
(ii) any extension of any locally tabular intermediate logic is locally
tabular.

  * Proof.

(i) Let L=$\mathsf{L}({\mathbf{F}})$ and L’=L(G) for some classes F,G of
finite frames. Then
$\mathsf{L}\cap\mathsf{L^{\prime}}=\mathsf{L}(\mathbf{F}\cup\mathbf{G})$ and
$\mathbf{M}^{n}(\mathbf{F}\cup\mathbf{G})=\mathbf{M}^{n}(\mathbf{F})\ \cup\
\mathbf{M}^{n}(\mathbf{G})$ .Thus,
$\mathbf{M}^{n}(\mathbf{F}\cup\mathbf{G})/\\!\\!\thicksim$ is finite if
$\mathbf{M}^{n}(\mathbf{F})/\\!\\!\thicksim$ and
$\mathbf{M}^{n}(\mathbf{G})/\\!\\!\thicksim$ are finite. (ii) is obvious.

Let us characterize po-frames of the logics in Figure 8. Thus, LC-frames are
chains and we let $\mathfrak{L}_{d}$, for any natural number $d\geq 1$, be the
chain on $\\{1,2,\dots,d\\}$ with the reverse (natural) ordering $\geq$, where
$d$ is the root and $1$ is the top (=greatest) element. Finite KC-frames have
top elements. $\mathsf{H}_{n}$-Frames are of the depth $\leq n$ and
$\mathsf{H}_{n}\mathsf{B}_{m}$-frames have (additionally) $m$-bounded
branching, that is each point has at most $m$ immediate successors. To get
PWL-frames we need unrooted frames; PWL-frames are

$\mathfrak{F}_{n}+\mathfrak{I}_{n_{1}}+\cdots+\mathfrak{I}_{n_{k}},\quad\mbox{where
$n\geq 0$ and $n_{1},\dots,n_{k}\geq 1$;}$

where $\mathfrak{I}_{n}$ is the frame with the identity relation on an
$n$-element set (and we agree that $\mathfrak{F}_{0}=\mathfrak{L}_{1}$ and
$\mathfrak{F}_{1}=\mathfrak{L}_{2}$). Note that the frames in Figure 7 are
PWL-frames and hence $\mathsf{L}({\mathbf{H}}_{pa})$ and
$\mathsf{L}({\mathbf{H}}_{un})$ are extensions of PWL.

There are three pretabular intermediate logics, see [23]: LC of Gödel and
Dummett, given by all chains $\mathfrak{L}_{n}$, LJ of Jankov, given by all
$n$-forks $\mathfrak{F}_{n}$, and LH of Hosoi, given by all rhombuses
$\mathfrak{R}_{n}$; see Figure 4.

A pair of logics $(\mathsf{L}_{1},\mathsf{L}_{2})$ is a splitting pair of the
lattice of (intermediate) logics if
$\mathsf{L}_{2}\not\subseteq\mathsf{L}_{1}$ and, for any intermediate logic
$\mathsf{L}$, either $\mathsf{L}\subseteq\mathsf{L}_{1}$, or
$\mathsf{L}_{2}\subseteq\mathsf{L}$.777In the same way, one can define a
splitting pair in any complete lattice. Then we say $\mathsf{L}_{1}$ splits
the lattice and $\mathsf{L}_{2}$ is the splitting (logic) of the lattice, see
[31]. Jankov [20] characteristic formula of a finite rooted frame
$\mathfrak{F}$ is denoted by $\chi(\mathfrak{F})$. 888Jankov originally
defined $\chi(\mathfrak{F})$ for any subdirectly irreducible finite Heyting
algebra. By duality, finite rooted frames are tantamount to finite s.i.
algebras and hence we proceed as if $\chi(\mathfrak{F})$ were defined for
frames.

###### Theorem 3

The pair $(\mathsf{L}(\mathfrak{F}),\mathsf{L}(\chi(\mathfrak{F}))$ is a
splitting pair, for any finite frame $\mathfrak{F}$. Thus, for any
intermediate logic L and any finite frame $\mathfrak{F}$, the logic L omits
$\mathfrak{F}$ iff $\chi(\mathfrak{F})\in\mathsf{L}$.

For instance $\mathsf{KC}=\mathsf{L}(\\{\chi({\mathfrak{F}_{2}})\\}$ is the
splitting logic. If $\\{\mathsf{L}_{i}\\}_{i\in I}$ is a family of splitting
logics, then $\mathsf{L}(\bigcup_{i\in I}\mathsf{L}_{i})$ is called a union
splitting. For instance,
$\mathsf{LC}=\mathsf{L}(\\{\chi({\mathfrak{F}_{2}}),\chi({\mathfrak{R}_{2}})\\})$
is a union splitting but not a splitting.

###### Corollary 2

If $\\{(\mathsf{L}^{\prime}_{i},\mathsf{L}_{i})\\}_{i\in I}$ is a family of
splitting pairs and $\mathsf{L}=\mathsf{L}(\bigcup_{i\in I}\mathsf{L}_{i})$,
then $\mathsf{L}$ is a union splitting and, for any intermediate logic
$\mathsf{L}^{\prime}$, either
$\mathsf{L}^{\prime}\subseteq\mathsf{L}^{\prime}_{i}$ for some $i\in I$, or
$\mathsf{L}\subseteq\mathsf{L}^{\prime}$.

###  2.2 The Problem of Unification.

A substitution $\varepsilon$ is a _unifier_ for a formula $A$ in a logic
$\mathsf{L}$ (an $\mathsf{L}$-_unifier_ for $A$) if
$\varepsilon(A)\in\mathsf{L}$. In any intermediate logic, the set of unifiable
formulas coincides with the set of consistent formulas. A set $\Sigma$ of
L-unifiers for $A$ is said to be complete, if for each L-unifier $\mu$ of $A$,
there is a unifier $\varepsilon\in\Sigma$ such that
$\varepsilon\preccurlyeq_{\sf L}\mu$.

The unification type of L is $1$ (in other words, unification in L is unitary)
if the set of unifiers of any unifiable formula $A$ contains a least, with
respect to $\preccurlyeq_{L}$, element called a most general unifier of $A$,
(an mgu of $A$). In other words, unification in L is unitary if each unifiable
formula has a one-element complete set of unifiers. The unification type of L
is $\omega$ (unification in L is finitary), if it is not $1$ and each
unifiable formula has a finite complete set of unifiers. The unification type
of L is $\infty$ (unification in L is infinitary) if it is not $1$, nor
$\omega$, and each unifiable formula has a minimal (with respect to inclusion)
complete set of unifiers. The unification type of L is $0$ (unification in L
is nullary) if there is a unifiable formula which has no minimal complete set
of unifiers. In a similar way one defines the unification type of any
L-unifiable formula. The unification type of the logic is the worst
unification type of its unifiable formulas.

Ghilardi [14] introduced projective unifiers and formulas; an
$\mathsf{L}$-unifier $\varepsilon$ for $A$ is called _projective_ if
$A\vdash_{\mathsf{L}}\varepsilon(x)\leftrightarrow x$, for each variable $x$
(and consequently $A\vdash_{\mathsf{L}}\varepsilon(B)\leftrightarrow B$, for
each $B$). A formula $A$ is said to be projective in $\mathsf{L}$ (or
$\mathsf{L}$-projective) if it has a projective unifier in $\mathsf{L}$. It is
said that a logic $\mathsf{L}$ enjoys projective unification if each
L-unifiable formula is $\mathsf{L}$-projective. An $\mathsf{L}$-projective
formula may have many non-equivalent in $\mathsf{L}$-projective unifiers and
each L-projective unifier is its mgu:

###### Lemma 2

If $\varepsilon$ is an L-projective unifier for $A$ and $\sigma$ is any
L-unifier for $A$, then $\sigma\circ\varepsilon=_{\mathsf{L}}\sigma$.

Thus, projective unification implies unitary unification. If
$A\in\mathsf{Fm^{n}}$ is L-projective, then $A$ has a projective unifier
$\varepsilon\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{n}$ that is a mgu
preserving the variables of $A$ (which is not always the case with unitary
unification). In contrast to unitary unification, projective unification is
also monotone:

###### Lemma 3

If $A$ is $\mathsf{L}$-projective and
$\mathsf{L}\subseteq\mathsf{L}^{\prime}$, then $A$ is
$\mathsf{L}^{\prime}$-projective.

Ghilardi [14] gives a semantical characterization of projective formulas. The
condition (ii) is called the extension property.999More specifically, the
theorem says that the class of models of a projective formula enjoys extension
property.:

###### Theorem 4

Let $\mathbf{F}$ be a class of finite po-frames and
$\mathsf{L}=\mathsf{L}(\mathbf{F})$. The followings are equivalent:
(i) $A$ is L-projective;
(ii) for every $n$-model $\mathfrak{M}^{n}=(W,\leq,w_{0},V^{n})$ over a po-
frame $(W,\leq,w_{0})$ of the logic L:
if $(\mathfrak{M}^{n})_{w}\Vdash A$ for each $w\not=w_{0}$, then
$\mathfrak{N}^{n}\Vdash A$ for some variant $\mathfrak{N}^{n}$ of
$\mathfrak{M}^{n}$.

Wroński [29, 30] proved that

###### Theorem 5

An intermediate logic L has projective unification iff LC $\subseteq$ L.

There are unitary logics which are not projective. Following Ghilardi and
Sachetti [18], unification in L is said to be _filtering_ if given two
unifiers, for any formula $A$, one can find a unifier that is more general
than both of them. Unitary unification is filtering. If unification is
filtering, then every unifiable formula either has an mgu or no basis of
unifiers exists (unification is nullary). It is known, see e.g. [5], that

###### Theorem 6

Unification in any intermediate logic L is filtering iff KC $\subseteq$ L.

If $\varepsilon,\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$ are
unifiers of a formula $A(x_{1},\dots,x_{n})$ in (any extension of) KC, then,
as a more general unifier for $\varepsilon,\sigma$ the following substitution
$\mu$ can be taken (where $y$ is a fresh variable,
i.e.$y\not\in\mathsf{Fm^{k}}$):

$\mu(x_{i})\qquad=\qquad(\varepsilon(x_{i})\land\neg
y)\quad\lor\quad(\sigma(x_{i})\land\neg\neg y),\qquad\mbox{for
$i=1,\dots,n$.}$

Thus, unifiers in filtering unification introduce new variables. We have, see
[5, 14],

###### Theorem 7

KC is the least intermediate logic with unitary unification. All extensions of
KC have nullary or unitary unification. All intermediate logics with finitary
unification are included in L($\mathfrak{F}_{2}$), the logic determined by the
‘fork frame’ $\mathfrak{F}_{2}$ see Figure 3. (L($\mathfrak{F}_{2}$),KC) is a
splitting pair of the lattice of intermediate logics.

Logics with finitary and unitary unification are separated by the splitting
(L($\mathfrak{F}_{2}$),KC). Let us agree that having good unification means
either unitary, or finitary one. Given a logic L with good unification, it has
unitary or finitary unification depending only on that if L contains KC or
not. Our aim would be to distinguish logics with good unification from those
with nullary one. We show in later that locally tabular intermediate logics
with infinitary unification do not exist at all. Let us notice that the
splitting generated by (L($\mathfrak{F}_{2}$),KC) is irrelevant for logics
with nullary unification; there are extensions of KC, as well as sublogics of
L($\mathfrak{F}_{2}$), that have nullary unification.

A logic L is said to have projective approximation if, for each formula $A$
one can find a finite set $\Pi(A)$ of L-projective formulas such that:
(i) $\mathsf{Var}(B)\subseteq\mathsf{Var}(A)$ and $B\vdash_{\mathsf{L}}A$, for
each $B\in\Pi(A)$;
(ii) each L-unifier of $A$ is an L-unifier of some $B\in\Pi(A)$.101010Ghilardi
[13, 14], instead of assuming $\Pi(A)$ is finite, postulates $deg(B)\leq
deg(A)$, for each $B\in\Pi(A)$, from which it follows that $\Pi(A)$ is finite.
The condition $deg(B)\leq deg(A)$ is relevant for logics with disjunction
property, like INT, but is irrelevant for locally tabular logics where
$\mathsf{Var}(B)\subseteq\mathsf{Var}(A)$ is sufficient. We decided,
therefore, to modify slightly Ghilardi’s formulations preserving, we hope, his
ideas.

If a finite $\Pi(A)$ exists we can assume that all $B\in\Pi(A)$ are maximal
(with respect to $\vdash_{\sf L}$) L-projective formulas fulfilling (i). But,
even if there is finitely many maximal L-projective formulas fulfilling (i),
we cannot be sure (ii) is fulfilled.

###### Theorem 8

Each logic with projective approximation has finitary (or unitary)
unification.

Logics with projective approximation play a similar role for finitary
unification as projective logics do for unitary unification, even though
projective approximation is not monotone. Ghilardi [14] proved that

###### Theorem 9

Intuitionistic propositional logic INT enjoys projective approximation and
hence unification in INT is finitary.

##  3 Intuitionistic Kripke $n$-Models.

###  3.1 p-Morphisms.

Let $(W,R,w_{0},V^{n})$ and $(U,S,u_{0},V^{\prime n})$ be $n$-models. A
mapping $p\colon W{\to}U$, from $W$ onto $U$, is said to be a p-morphisms of
their frames, $p\colon(W,R,w_{0})\to(U,S,u_{0}),\mbox{if}$
(i) $wRv\Rightarrow p(w)Sp(v),\quad\mbox{for any }w,v\in W$;
(ii) $p(w)Sa\Rightarrow\exists_{v\in W}\bigl{(}wRv\land
p(v)=a\bigr{)},\quad\mbox{for any }w\in W\ \mbox{and }\ a\in U$;
(iii) $p(w_{0})=u_{0}$.
A p-morphism of $n$-models, $p\colon(W,R,w_{0},V^{n})\to(U,S,u_{0},V^{\prime
n})$ fulfills (additionally)
(iv) $V^{n}(w)=V^{\prime n}(p(w))$, for any $w\in W$.

If $p\colon\mathfrak{M}^{n}\to\mathfrak{N}^{n}$ is a p-morphism, then
$\mathfrak{N}^{n}$ is called a p-morphic image (or reduct, see [31]) of
$\mathfrak{M}^{n}$ and we write $p(\mathfrak{M}^{n})=\mathfrak{N}^{n}$.
Reducing $\mathfrak{M}^{n}$ (by a p-morphism), we preserve its logical
properties. In particular, $p(\mathfrak{M}^{n})\thicksim\mathfrak{M}^{n}$ as

###### Lemma 4

If $p\colon\mathfrak{M}^{n}\to\mathfrak{N}^{n}$ is a p-morphism of $n$-models,
$w\in W$ and $A\in\mathsf{Fm}^{n}$, then

$\mathfrak{M}^{n}\Vdash_{w}A\quad\Leftrightarrow\quad
p(\mathfrak{M}^{n})\Vdash_{p(w)}A.$

p-Morphisms are also used in modal logic. The above property is generally
valid which means it also holds for modal models and modal formulas and it can
be shown without assuming that $R$ is a pre-order and $V^{n}$ is monotone.

###### Example 1

Let $\mathfrak{M}^{n}=(W,R,w_{0},V^{n})$ be an $n$-model in which the pre-
order $R$ is not a partial order. Let $w\thickapprox v\Leftrightarrow wRv\land
vRw$, for any $w,v\in W$. Then $\thickapprox$ is an equivalence relation on
$W$ and one can easily show that the canonical mapping
$p(w)=[w]_{\thickapprox}$, for any $w\in W$, is a p-morphism from
$\mathfrak{M}^{n}$ onto the quotient model

$\mathfrak{M}^{n}/\\!\\!\thickapprox\quad=\quad\bigl{(}W/\\!\\!\thickapprox,R/\\!\\!\thickapprox,[w_{0}]_{\thickapprox},V^{n}\\!\\!/\\!\thickapprox\bigr{)}.$

Reducing all $R$-clusters to single points, we receive an equivalent $n$-model
over a po-set; and hence po-sets (not pre-orders) are often taken as
intuitionistic frames.

If a p-morphism $p\colon\mathfrak{M}^{n}\to\mathfrak{N}^{n}$ is one-to-one,
then $wRv\Leftrightarrow p(w)Sp(v),$ for any $w,v\in W$ which means $p$ is an
isomorphism and, if there is an isomorphism between the $n$-models, we write
$\mathfrak{M}^{n}\equiv\mathfrak{N}^{n}$. It is usual to identify isomorphic
objects.

###  3.2 Bisimulations.

Bisimulations (between Kripke frames) were introduced by K.Fine [12], by
imitating Ehrenfeucht games. They found many applications. In particular,
S.Ghilardi [14] used bounded bisimulation to characterize projective formulas.
We show that bisimulations are closely related to p-morphisms. In our approach
we follow A.Patterson [24].

A binary relation $B$ on $W$ is a bisimulation of the frame $(W,R,w_{0})$ if

$wBv\Rightarrow\forall_{w^{\prime}}\exists_{v^{\prime}}(wRw^{\prime}\Rightarrow
vRv^{\prime}\land
w^{\prime}Bv^{\prime})\land\forall_{v^{\prime}}\exists_{w^{\prime}}(vRv^{\prime}\Rightarrow
wRw^{\prime}\land w^{\prime}Bv^{\prime}).$

$w$$v$$w^{\prime}$$v^{\prime}$$B$$B$$R$$R$ Fig. 9: Bisimulation

Note that
$wBv\Rightarrow\forall_{w^{\prime}}\exists_{v^{\prime}}(wRw^{\prime}\Rightarrow
vRv^{\prime}\land w^{\prime}Bv^{\prime})$ suffices if $B$ is symmetric. A
bisimulation of the $n$-model $(W,R,w_{0},V^{n})$ additionally fulfils
$V^{n}(w)=V^{n}(v)$ if $wBv$.

###### Lemma 5

(i) If $B$ is a bisimulation of $\mathfrak{M}^{n}$, then
$B\\!\\!\upharpoonright_{(W)_{w}}$ is a bisimulation of
$(\mathfrak{M}^{n})_{w}$;
(ii) if $B$ is a bisimulation of $(\mathfrak{M}^{n})_{w}$, then $B$ is a
bisimulation of $\mathfrak{M}^{n}$; for any $w\in W$.

###### Lemma 6

If $B$ is a bisimulation (of a frame or an $n$-model), then the least
equivalence relation $B^{\star}$ containing $B$ is also a bisimulation.

  * Proof.

A proof of this lemma can be found in [24]. Let us only specify properties of
bisimulations which are useful here.

(i) $\\{(w,w)\colon w\in W\\}$ is a bisimulation.

(ii) $B$ is a bisimulation $\Rightarrow$ $B^{-1}$ is a bisimulation.

(iii) $\forall_{i}(B_{i}$ is a bisimulation)
$\Rightarrow\quad\bigcup_{i}B_{i}$ is a bisimulation.

(iv) $B$ is a bisimulation $\Rightarrow$ the transitive closure of $B$ is a
bisimulation.

Suppose that $B$ is an equivalence bisimulation of an $n$-model
$\mathfrak{M}^{n}=(W,R,w_{0},V^{n})$. Let us define
$\mathfrak{M}^{n}/B=(W/B,R/B,[w_{0}]_{B},[V]^{n})$ where $W/B=\\{[w]_{B}\colon
w\in W\\}$, and $[V]^{n}([w]_{B})=V^{n}(w)$ for any $w\in W$, and

$[w]_{B}\ R/B\
[v]_{B}\quad\Leftrightarrow\quad\exists_{w^{\prime}v^{\prime}}\bigl{(}wBw^{\prime}\land
vBv^{\prime}\land w^{\prime}Rv^{\prime}\bigr{)}.$

###### Theorem 10

If $B$ is an equivalence bisimulation of an $n$-model $\mathfrak{M}^{n}$, then
$\mathfrak{M}^{n}/B$ is an $n$-model and the canonical mapping $[\ ]_{B}\colon
W\to W/B$ is a p-morphism of the $n$-models.

  * Proof.

We should show that $R/B$ is a pre-order. If $w=v$, one can take
$w^{\prime}=v^{\prime}=w$ (in the definition of $R/B$) to show $[w]_{B}\ R/B\
[w]_{B}$. Thus, $R/B$ is reflexive.

Suppose that $[w]_{B}\ R/B\ [v]_{B}\ R/B\ [u]_{B}$, for some $w,v,u\in W$.
Then $wBw^{\prime}\land vBv^{\prime}\land w^{\prime}Rv^{\prime}$ and
$vBv^{\prime\prime}\land uBu^{\prime\prime}\land
v^{\prime\prime}Ru^{\prime\prime}$, for some
$w^{\prime},v^{\prime},v^{\prime\prime},u^{\prime\prime}\in W$. But $B$ is an
equivalence, hence $v^{\prime\prime}Bv^{\prime}$ and, by
$v^{\prime\prime}Ru^{\prime\prime}$, we get $v^{\prime}Ru^{\prime}\land
u^{\prime\prime}Bu^{\prime}$, for some $u^{\prime}\in W$, as $B$ is a
bisimulation. By transitivity of $R$, we have $w^{\prime}Ru^{\prime}$ and
$uBu^{\prime}$ as $B$ is an equivalence relation. Thus, $[w]_{B}\ R/B\
[u]_{B}$; the relation $R/B$ is transitive.

There remains to show that the canonical mapping is a p-morphism.
(i) If $wRv$, then $[w]_{B}\ R/B\ [v]_{B}$, by the definition of $R/B$.

(ii) Suppose that $[w]_{B}\ R/B\ [v]_{B}$, for some $w,v\in W$. Then
$wBw^{\prime}$, and $vBv^{\prime}$, and $w^{\prime}Rv^{\prime}$, for some
$w^{\prime},v^{\prime}\in W$. As $B$ is a bisimulation,
$wRv^{\prime\prime}\land v^{\prime\prime}Bv^{\prime}$, for some
$v^{\prime\prime}\in B$. Thus, $wRv^{\prime\prime}$ and
$[v^{\prime\prime}]_{B}=[v]_{B}$, as required.

The conditions (iii) and (iv) are obviously fulfilled.

###### Theorem 11

If $B$ and $B^{\prime}$ are equivalence bisimulations of an $n$-model
$\mathfrak{M}^{n}=(W,R,w_{0},V^{n})$ and $B^{\prime}\subseteq B$, then there
is a p-morphism $q\colon\mathfrak{M}^{n}/B^{\prime}\to\mathfrak{M}^{n}/B$ such
that the diagram in Figure 10 commutes.

$\mathfrak{M}^{n}/B^{\prime}$$\mathfrak{M}^{n}$$\mathfrak{M}^{n}/B$$q$$[\
]_{B^{\prime}}$$[\ ]_{B}$ Fig. 10: Comparison of Bisimulations.

  * Proof.

Let us define $q([w]_{B^{\prime}})=[w]_{B}$ and notice that the mapping is
well-defined and maps $W/B^{\prime}$ onto $W/B$. We should only cheque that
$q$ is a p-morphism. Note that the conditions (i),(iii) and (iv) are quite
obvious.

(ii) Suppose that $q([w]_{B^{\prime}})R/B\ [u]_{B}$. By the definition of
$R/B$, there are $w^{\prime},u^{\prime}$ such that
$wBw^{\prime}Ru^{\prime}Bu$. Since $B$ is a bisimulation and
$wBw^{\prime}Ru^{\prime}$ there is an $u^{\prime\prime}$ such that
$wRu^{\prime\prime}Bu^{\prime}$. Thus, $[w]_{B^{\prime}}R/B^{\prime}\
[u^{\prime\prime}]_{B^{\prime}}$ and
$q([u^{\prime\prime}]_{B^{\prime}})=[u^{\prime\prime}]_{B}=[u]_{B}$ as
required.

###### Theorem 12

If $p:\mathfrak{M}^{n}\to\mathfrak{N}^{n}$ is a p-morphism of $n$-models, then

$wBv\quad\Leftrightarrow\quad p(w)=p(v)$

is an equivalence bisimulation of the $n$-model $\mathfrak{M}^{n}$, and
$\mathfrak{M}^{n}/B\equiv\mathfrak{N}^{n}$.

  * Proof.

Let $wBv$ and $wRw^{\prime}$ for some $w,w^{\prime},v\in W$ (see Figure 9).
Then $p(w)=p(v)$ and $p(w)Sp(w^{\prime})$, where $S$ is the accessibility
relation in $\mathfrak{N}^{n}$. Thus, $p(v)Sp(w^{\prime})$. Since $p$ is a
p-morphism, $vRv^{\prime}$ and $p(v^{\prime})=p(w^{\prime})$, for some
$v^{\prime}\in W$. Thus, $vRv^{\prime}$ and $w^{\prime}Bv^{\prime}$.

In the same way one shows $wBv$ and $vRv^{\prime}$ give us $wRw^{\prime}$ and
$w^{\prime}Bv^{\prime}$, for some $w^{\prime}$, and we obviously have
$V^{n}(w)=V^{n}(v)$ if $wBv$.

The $n$-models $\mathfrak{M}^{n}/B$ and $\mathfrak{N}^{n}$ are isomorphic as
the mapping $i([w]_{B})=p(w)$ is well defined, one-to-one and p-morphic.

Bisimulations preserve such properties of frames as reflexivity, symmetry,
transitivity; consequently, p-morphic images preserve these properties, as
well. There are, however, some properties which are not preserved by
p-morphisms.

###### Example 2

Let $W=\\{u_{i}\colon i\geq 0\\}\cup\\{v_{i}\colon i\geq 0\\}\cup\\{w_{0}\\}$
and a partial order $R$ on $W$, and a bisimulation $B$ on $W$, are defined as
in the following picture (see Figure 11)

$w_{0}$$u_{0}$$v_{0}$$u_{1}$$v_{1}$$u_{2}$$v_{2}$$u_{3}$$v_{3}$$[u_{i}]_{B}=\\{u_{0},u_{1},u_{2},\dots\\}$$[v_{i}]_{B}=\\{v_{0},v_{1},v_{2},\dots\\}$$[w_{0}]_{B}=\\{w_{0}\\}$$[w_{0}]_{B}$$[u_{0}]_{B}$$[v_{0}]_{B}$
Fig. 11: Weak Asymmetry is not Preserved.

Thus, a p-morphic image of a partial order is not a partial order (only pre-
order).

Note that the set $W$ in the above Example is infinite which is essential as

###### Corollary 3

Any p-morhic image of any finite po-frame is a po-frame.

###  3.3 p-Irreducible $n$-Models.

An $n$-model $\mathfrak{M}^{n}$ is said to be p-irreducible if each p-morphism
$p\colon\mathfrak{M}^{n}\to\mathfrak{N}^{n}$, for any $n$-model
$\mathfrak{N}^{n}$, is an isomorphism. Thus, any p-morphic image of any
irreducible $n$-model is its isomorphic copy.111111 The concept of
p-irreducibility, in contrast to other concepts in this Section, would make no
sense for frames. Irreducible $n$-models are po-sets, see Example 1, and we
show any $n$-model can be reduced to a p-irreducible one.

###### Theorem 13

For each $n$-model $\mathfrak{M}^{n}$ there exists a p-irreducible $n$-model
$\mathfrak{N}^{n}$ which is a p-morphic image of $\mathfrak{M}^{n}$ (and
$\mathfrak{N}^{n}$ is unique up to $\equiv$).

  * Proof.

Let $\mathfrak{M}^{n}=(W,R,w_{0},\\{\mathfrak{f}^{n}_{w}\\}_{w\in W})$ and $B$
be the least equivalence on $W$ containing $\bigcup\\{B_{i}\colon B_{i}\
\mbox{is a bisimulation on }\mathfrak{M}^{n}\\}.$ By Lemma 6, $B$ is the
greatest bisimulation on $\mathfrak{M}^{n}$. Take
$\mathfrak{N}^{n}=\mathfrak{M}^{n}\\!\\!/B$, see Theorem 10. Since the
composition of any two p-morphisms is a p-morphism, any p-morphic image
$\mathfrak{N^{\prime}}^{n}$ of $\mathfrak{N}^{n}$ would be a p-morphic image
of $\mathfrak{M}^{n}$. Thus, by maximality of $B$, we would get, by Theorem
11, an isomorphism
$p^{\prime}\colon\mathfrak{N^{\prime}}^{n}\equiv\mathfrak{N}^{n}$ which means
$\mathfrak{N}^{n}$ is p-irreducible.

The uniqueness of $\mathfrak{N}^{n}$ also follows; if
$\mathfrak{N^{\prime}}^{n}$ were another p-irreducible p-morphic image of
$\mathfrak{M}^{n}$, we would get by Theorems 11 and 12, a p-morphism
$p^{\prime}\colon\mathfrak{N^{\prime}}^{n}\to\mathfrak{N}^{n}$ which would
mean that $\mathfrak{N^{\prime}}^{n}$ and $\mathfrak{N}^{n}$ are isomorphic.

The following theorem could give another characterization of p-irreducible
$n$-models.

###### Theorem 14

If an $n$-model $\mathfrak{M}^{n}$ is p-irreducible, then for any $n$-model
$\mathfrak{N}^{n}$ there is at most one p-morphism
$p\colon\mathfrak{N}^{n}\to\mathfrak{M}^{n}$.

  * Proof.

Let $\mathfrak{M}^{n}=(W,R,w_{0},V^{n})$ be p-irreducible and
$p,q\colon\mathfrak{N}^{n}\to\mathfrak{M}^{n}$ be two (different) p-morphisms
for some $\mathfrak{N}^{n}=(U,S,u_{0},V^{\prime n})$. Take
$B=\\{(p(v),q(v))\colon v\in V\\}$ and let us show $B$ is a bisimulation on
$\mathfrak{M}^{n}$. This would be a contradiction as, if $B^{\star}$ were the
least equivalence relation containing $B$ (see Lemma 6), $[\
]_{B^{\star}}\colon\mathfrak{M}^{n}\to\mathfrak{M}^{n}/B^{\star}$ would be a
non-isomorphic p-morphism, see Theorem 10, and it would mean that
$\mathfrak{M}^{n}$ were not p-irreducible.

Let $p(v)Rw$, for some $v\in V$ and $w\in W$. As $p$ is a p-morphism,
$p(v^{\prime})=w$ and $vSv^{\prime}$ for some $v^{\prime}\in V$. Then
$q(v)Rq(v^{\prime})$, as $q$ is a p-morphism, and $wBq(v^{\prime})$ as
$w=p(v^{\prime})$.

Similarly, if $q(v)Rw$, for some $v\in V$ and $w\in W$, then $q(v^{\prime})=w$
and $vSv^{\prime}$, for some $v^{\prime}\in V$, and hence $p(v)Rp(v^{\prime})$
and $p(v^{\prime})Bw$ (as $w=q(v^{\prime}))$.

###### Theorem 15

If $\mathfrak{M}^{n}$ is p-irreducible, then $(\mathfrak{M}^{n})_{w}$ is
p-irreducible for each $w\in W$.

  * Proof.

Let $\mathfrak{M}^{n}=(W,R,w_{0},V^{n})$ and suppose $(\mathfrak{M}^{n})_{w}$
is not p-irreducible for some $w\in W$. By Theorem 12, there is a (non-
trivial) bisimulation $B$ on $(\mathfrak{M}^{n})_{w}$. Since (by Lemma 5) $B$
is a bisimulation of $\mathfrak{M}^{n}$, if we extend $B$ (see Lemma 6) to an
equivalence bisimulation $B^{\star}$ of $\mathfrak{M}^{n}$, we get a (non-
isomorphic) p-morphism of $\mathfrak{M}^{n}$, see Theorem 10. Thus,
$\mathfrak{M}^{n}$ is not p-irreducible.

###  3.4 Finite $n$-Models.

It follows from Example 1 that, without loosing any generality, we can confine
ourselves to frames/$n$-models defined over partial orders (not pre-orders).
So, in what follows, we assume that all frames/$n$-model are (defined over)
po-sets even though we (sometimes) keep the notation
$\mathfrak{M}^{n}=(W,R,w_{0},V^{n})$. We examine here specific properties of
finite $n$-models such as Corollary 3.

###### Theorem 16

If $\mathfrak{M}^{n}$ is a finite $n$-model, then one can define
$\Delta(\mathfrak{M}^{n})\in\mathsf{Fm}^{n}$ (called the character of
$\mathfrak{M}^{n}$)121212The explicit definition of the character can be found
in many papers; for instance, see Ghilardi [14], p.869. The idea of
characterizing finite structures by formulas is due to Jankov [20] but the
character should not be missed with the characteristic formula of a frame. If
we consider $n$-models of a given locally tabular logic L, where there is only
finitely many (up to $=_{\sf L}$) formulas in $n$-variables, one could define
the character of any finite $n$-model as the conjunction of the formulas (out
of the finitely many) which are true in the model. such that
$\mathfrak{N}^{n}\Vdash\Delta(\mathfrak{M}^{n})\quad\Leftrightarrow\quad\mathsf{Th}(\mathfrak{M}^{n})\subseteq\mathsf{Th}(\mathfrak{N}^{n})$,
for any $n$-model $\mathfrak{N}^{n}$.

The next theorem is due to Patterson [24]:

###### Theorem 17

If $\\{\mathsf{Th}((\mathfrak{M}^{n})_{w})\\}_{w\in W}$ is finite (which is
the case when $\mathfrak{M}^{n}$ is finite), then

$\mathsf{Th}(\mathfrak{M}^{n})\subseteq\mathsf{Th}(\mathfrak{N}^{n})\quad\Leftrightarrow\quad\mathfrak{N}^{n}\thicksim(\mathfrak{M}^{n})_{w},\
\mbox{for some}\ w\in W,\quad\mbox{for any $n$-model $\mathfrak{N}^{n}$}.$

  * Proof.

The implication $(\Leftarrow)$ is obvious by Lemma 1. Let us prove
$(\Rightarrow)$. If not all of $\mathsf{Th}(\mathfrak{N}^{n})$ is true at
$(\mathfrak{M}^{n})_{w}$, we pick $A_{w}\in\mathsf{Th}(\mathfrak{N}^{n})$ such
that $A_{w}\not\in\mathsf{Th}((\mathfrak{M}^{n})_{w})$ or $A_{w}=\top$
otherwise. As $\\{\mathsf{Th}((\mathfrak{M}^{n})_{w})\colon w\in W\\}$ is
finite, we take $A=\bigwedge A_{w}$ and notice $\mathfrak{M}^{n}\Vdash_{w}A$
means that
$\mathsf{Th}(\mathfrak{N}^{n})\subseteq\mathsf{Th}((\mathfrak{M}^{n})_{w})$.

If a formula not in $\mathsf{Th}(\mathfrak{N}^{n})$ is true at
$(\mathfrak{M}^{n})_{w}$, we pick $B_{w}\not\in\mathsf{Th}(\mathfrak{N}^{n})$
such that $B_{w}\in\mathsf{Th}((\mathfrak{M}^{n})_{w})$ (or $B_{w}=\bot$ if
$\mathsf{Th}(\mathfrak{N}^{n})\supseteq\mathsf{Th}((\mathfrak{M}^{n})_{w}$)),
for each $w\in W$. Take $B=\bigvee B_{w}$ and notice
$\mathfrak{M}^{n}\not\Vdash_{w}B$ yields
$\mathsf{Th}(\mathfrak{N}^{n})\supseteq\mathsf{Th}((\mathfrak{M}^{n})_{w})$.

Clearly, $(A\Rightarrow B)\not\in\mathsf{Th}(\mathfrak{N}^{n})$. Thus,
$(A\Rightarrow B)\not\in\mathsf{Th}(\mathfrak{M}^{n})$ and hence
$\mathfrak{M}^{n}\Vdash_{w}A$ and $\mathfrak{M}^{n}\not\Vdash_{w}B$, for some
$w\in W$, and this means that
$\mathsf{Th}(\mathfrak{N}^{n})=\mathsf{Th}((\mathfrak{M}^{n})_{w})$.

###### Theorem 18

If $\\{\mathsf{Th}((\mathfrak{M}^{n})_{w})\\}_{w\in W}$ is finite, then the
greatest bisimulation $B$ of $\mathfrak{M}^{n}$ is:

$wBv\quad\Leftrightarrow\quad(\mathfrak{M}^{n})_{w}\thicksim(\mathfrak{M}^{n})_{v}.$

  * Proof.

Let $wBv\land wRw^{\prime}$. Then
$\mathsf{Th}((\mathfrak{M}^{n})_{v})=\mathsf{Th}((\mathfrak{M}^{n})_{w})\subseteq\mathsf{Th}((\mathfrak{M}^{n})_{w^{\prime}})$
and, by Theorem 17, $w^{\prime}Bv^{\prime}\land vRv^{\prime}$ for some
$v^{\prime}$. Thus, $B$ is a bisimulation as $B$ is symmetric.

Let $wB^{\prime}v$ and $B^{\prime}$ be a bisimulation of $\mathfrak{M}^{n}$.
By Theorem 10, there is a p-morphism
$p\colon\mathfrak{M}^{n}\to\mathfrak{M}^{n}/B^{\prime}$ such that $p(w)=p(v)$.
Hence, by Lemma 4, $(\mathfrak{M}^{n})_{w}\thicksim(\mathfrak{M}^{n})_{v}$
which means $wBv$. Thus, we have showed $B^{\prime}\subseteq B$.

###### Corollary 4

If $\\{\mathsf{Th}((\mathfrak{M}^{n})_{w})\\}_{w\in W}$ is finite, then there
is a p-morphism from $\mathfrak{M}^{n}$ onto the $n$-model:

$\Bigl{(}\\{\mathsf{Th}((\mathfrak{M}^{n})_{w})\\}_{w\in W},\ \subseteq,\
\mathsf{Th}(\mathfrak{M}^{n}),\
\\{\\{x_{1},\dots,x_{n}\\}\cap\mathsf{Th}((\mathfrak{M}^{n})_{w})\\}_{w\in
W}\Bigr{)}.$

  * Proof.

By the above Theorem and by Theorem 10.

###### Corollary 5

$\mathfrak{M}^{n}$ is finitely reducible (which means there is a p-morphism
$p\colon\mathfrak{M}^{n}\to\mathfrak{N}^{n}$ for some finite $n$-model
$\mathfrak{N}^{n}$) if and only if
$\\{\mathsf{Th}((\mathfrak{M}^{n})_{w})\\}_{w\in W}$ is finite.

###### Corollary 6

Let $\mathfrak{M}^{n}$ and $\mathfrak{N}^{n}$ be finite (or finitely
reducible) $n$-models. Then $\mathfrak{M}^{n}\thicksim\mathfrak{N}^{n}$ if and
only if $\mathfrak{M}^{n}$ and $\mathfrak{N}^{n}$ have a common p-morphic
image.

  * Proof.

Let $\mathfrak{M}^{n}=(W,R,w_{0},V^{n})$ and
$\mathfrak{N}^{n}=(U,S,u_{0},V^{\prime n})$. It suffices to notice that
$\mathfrak{M}^{n}\thicksim\mathfrak{N}^{n}$ yields, by Theorem 17,
$\\{\mathsf{Th}((\mathfrak{M}^{n})_{w})\\}_{w\in
W}=\\{\mathsf{Th}((\mathfrak{N}^{n})_{u})\\}_{u\in U}$.

###### Corollary 7

If $\mathfrak{M}^{n}=(W,R,w_{0},V^{n})$ and
$\mathfrak{N}^{n}=(U,S,u_{0},V^{\prime n})$ are finite and
$\mathfrak{M}^{n}\thicksim\mathfrak{N}^{n}$, then
(i) for every $w\in W$ there is an element $u\in U$ such that
$(\mathfrak{M}^{n})_{w}\thicksim(\mathfrak{N}^{n})_{u}$;
(ii) for every $u\in U$ there is an element $w\in W$ such that
$(\mathfrak{M}^{n})_{w}\thicksim(\mathfrak{N}^{n})_{u}$.

  * Proof.

Let $p$ and $q$ be p-morphisms from $\mathfrak{M}^{n}$ and $\mathfrak{N}^{n}$,
correspondingly, onto a common p-morphic image. By Lemma 4,
$(\mathfrak{M}^{n})_{w}\thicksim(\mathfrak{N}^{n})_{u}$ if $p(w)=q(u)$.

###  3.5 $\sigma$-Models.

This is the key notion and it was defined by Ghilardi [14]. Let
$\sigma:\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm^{k}}$, for $k,n\geq 0$. For any
$\mathfrak{M}^{k}=(W,R,w_{0},V^{k})$, let
$\sigma(\mathfrak{M}^{k})=(W,R,w_{0},V^{n})$ where

$x_{i}\in
V^{n}(w)\quad\Leftrightarrow\quad\mathfrak{M}^{k}\Vdash_{w}\sigma(x_{i}),\quad\mbox{
for any $w\in W$ \ and \ $i=1,\dots,n$}.$

###### Lemma 7

For every $w\in W$ and every $A\in\mathsf{Fm^{n}}$, we have

$\sigma(\mathfrak{M}^{k})\Vdash_{w}A\quad\Leftrightarrow\quad\mathfrak{M}^{k}\Vdash_{w}\sigma(A).$

###### Lemma 8

(i) $\mathfrak{M}^{k}$ and $\sigma(\mathfrak{M}^{k})$ are models over the same
frame;
(ii) $\sigma((\mathfrak{M}^{k})_{w})=(\sigma(\mathfrak{M}^{k}))_{w}$, for
every $w\in W$;
(iii) if
$\mathsf{Th}(\mathfrak{M}^{k})\subseteq\mathsf{Th}(\mathfrak{N}^{k})$, then
$\mathsf{Th}(\sigma(\mathfrak{M}^{k}))\subseteq\mathsf{Th}(\sigma(\mathfrak{N}^{k}))$.

  * Proof.

We get (i) and (ii) by the definition of $\sigma(\mathfrak{M}^{k})$. As
concerns (iii):
$\sigma(\mathfrak{M}^{k})\Vdash A\ \Leftrightarrow\
\mathfrak{M}^{k}\Vdash\sigma(A)\ \Rightarrow\ \mathfrak{N}^{k}\Vdash\sigma(A)\
\Leftrightarrow\ \sigma(\mathfrak{N}^{k})\Vdash A$.

###### Lemma 9

If $p\colon\mathfrak{M}^{k}\to\mathfrak{N}^{k}$ is a p-morphism of $k$-models,
then $p\colon\sigma(\mathfrak{M}^{k})\to\sigma(\mathfrak{N}^{k})$ is also a
p-morphism of $n$-models and hence
$p(\sigma(\mathfrak{M}^{k}))=\sigma(p(\mathfrak{M}^{k}))$ (see Figure. 12).

$\sigma(\mathfrak{M}^{n})$$\mathfrak{M}^{k}$$\sigma$$\sigma(\mathfrak{N}^{k})$$\mathfrak{N}^{k}$$\sigma$$p$$p$
Fig. 12: p-Morphic images of $\sigma$-models.

The above does not mean that $\sigma$-models are closed under p-morphic
images. Two (counter)examples below show that they may be not.

###### Example 3

Let $\sigma(x_{1})=x_{2}\lor(x_{2}\to(x_{1}\lor\neg x_{1})).$ The $1$-model
over the two-element chain (in Figure 13) cannot be any $\sigma$-model as to
falsify $\sigma(x_{1})$ at the root one needs at least three elements in the
chain.

$00$$11$$01$$\sigma$$0$$1$$1$$p$$0$$1$ Fig. 13: The First Counterexample.

Let $\sigma(x)=\neg\neg x\lor\neg x$ (we write $x$ instead of $x_{1}$). Models
and the p-morphism are defined in Figure 14. The $1$-model over a two-element
chain cannot be any $\sigma$-model as to falsify $\sigma(x)$ at the root one
needs at least two end elements above the root.

$0$$1$$0$$\sigma$$0$$1$$1$$p$$0$$1$ Fig. 14: The Second Counterexample.

Nowhere (but Theorem 16) we have used the fact that valuations of any
$n$-model are restricted to the $n$-initial variables. It would make no change
in our argument if we replaced (everywhere) valuations $V^{n}$ with $V$,
valuations of all variables. Thus, all results (but Theorem 16) of this
section remain valid for usual Kripke models.

##  4 Locally Tabular Logics.

For any class F of frames, let sm(F) be the least class (of frames) containing
F and closed under generated subframes and p-morphic images.

###### Lemma 10

$\mathsf{L}(sm(\mathbf{F}))=\mathsf{L}(\mathbf{F}).$

  * Proof.

By Lemma 4 and Lemma 1

Extending any class of frames with generated subframes and p-morphic images
does not change the logic but it enables us to characterize extensions of
$\mathsf{L}(\mathbf{F})$:131313The following theorem resembles (not without
reasons) characterizations, see [28, 25], of extensions of logics given by
logical matrices.

###### Theorem 19

Let $\mathbf{F}$ be a class of finite frames and
$\mathsf{L}=\mathsf{L}(\mathbf{F})$ be locally tabular. If L’ is an
intermediate logic such that $\mathsf{L}\subseteq\mathsf{L}^{\prime}$, then
$\mathsf{L^{\prime}}=\mathsf{L}(\mathbf{G})$, for some $\mathbf{G}\subseteq
sm(\mathbf{F})$.

  * Proof.

Let $\mathbf{G}=\\{\mathfrak{F}\in
sm(\mathbf{F})\colon\mathsf{L^{\prime}}\subseteq\mathsf{L}(\mathfrak{F})\\}$.
Clearly, $\mathsf{L^{\prime}}\subseteq\mathsf{L}(\mathbf{G})$. We need to show
the reverse inclusion. So, assume $A\not\in\mathsf{L^{\prime}}$ and show
$A\not\in\mathsf{L}(\mathfrak{F})$ for some $\mathfrak{F}\in\mathbf{G}$.

Suppose that $A=A(x_{1},\dots,x_{k})$, for some $k\geq 0$, and let
$A_{0},\dots,A_{j}$ be all (non-equivalent in L) formulas in
$\mathsf{Fm^{k}}\cap\mathsf{L^{\prime}}$. Let

$B=\bigwedge_{i=0}^{j}A_{i}\ \rightarrow\ A.$

If $B\in\mathsf{L}(\mathbf{F})$, then $B\in\mathsf{L^{\prime}}$ and it would
give $A\in\mathsf{L^{\prime}}$, a contradiction. Thus, we have
$B\not\in\mathsf{L}(\mathbf{F})$. There is a $k$-model
$\mathfrak{M}^{k}=(W,R,w_{0},V^{k})$ over a frame from F such that
$\mathfrak{M}^{k}\Vdash_{w}A_{i}$, for all $i\leq j$, and
$\mathfrak{M}^{k}\not\Vdash_{w}A$, for some $w\in W$. Let
$p\colon\mathfrak{M}^{k}\to\mathfrak{N}^{k}$ be a p-morphism from
$\mathfrak{M}^{k}$ onto a $p$-irreducible $k$-model $\mathfrak{N}^{k}$, see
Theorem 13. We take the frame of $(\mathfrak{N}^{k})_{p(w)}$ as our
$\mathfrak{F}$. Let $\mathfrak{F}=(U,\leq,p(w))$. Since
$(\mathfrak{N}^{k})_{p(w)}$ is a $k$-model over $\mathfrak{F}$, we have
$A\not\in\mathsf{L}(\mathfrak{F})$. There remains to show that
$\mathsf{L^{\prime}}\subseteq\mathsf{L}(\mathfrak{F})$.

Suppose that $C\not\in\mathsf{L}(\mathfrak{F})$ for some
$C\in\mathsf{L^{\prime}}$. Let $C=C(x_{1},\dots,x_{n})$ and let
$\mathfrak{N}^{n}$ be an $n$-model over $\mathfrak{F}$ such that
$\mathfrak{N}^{n}\not\Vdash C$. We define a substitution
$\varepsilon\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm^{k}}$ taking
$\varepsilon(x_{i})=\bigvee\\{\Delta((\mathfrak{N}^{k})_{u})\colon\mathfrak{N}^{n}\Vdash_{u}x_{i}\\}$,
for any $i\leq n$. Then we have
$\mathfrak{N}^{k}\Vdash_{v}\varepsilon(x_{i})\Leftrightarrow$
$\exists_{u\in
U}\bigl{(}\mathfrak{N}^{k}\Vdash_{v}\Delta((\mathfrak{N}^{k})_{u})\land\mathfrak{N}^{n}\Vdash_{u}x_{i}\bigr{)}\Leftrightarrow\exists_{u\in
U}\bigl{(}\mathsf{Th}((\mathfrak{N}^{k})_{u})\subseteq\mathsf{Th}((\mathfrak{N}^{k})_{v})\land\mathfrak{N}^{n}\Vdash_{u}x_{i}\bigr{)}\Leftrightarrow\exists_{u\in
U}(u\leq
v\land\mathfrak{N}^{n}\Vdash_{u}x_{i})\Leftrightarrow\mathfrak{N}^{n}\Vdash_{v}x_{i}$,
for any $i\leq n$ and $v\in U$. Note that the last but one equivalence needs
Corollary 4. This shows
$\mathfrak{N}^{k}\Vdash_{v}\varepsilon(C)\Leftrightarrow\mathfrak{N}^{n}\Vdash_{v}C$,
for any $v\in U$ and hence we get
$\mathfrak{N}^{k}\not\Vdash_{p(w)}\varepsilon(C)$, that is
$\mathfrak{M}^{k}\not\Vdash_{w}\varepsilon(C)$, which cannot happen as
$\varepsilon(C)$ is one of the $A_{i}$’s and must be true at
$(\mathfrak{M}^{k})_{w}$.

###  4.1 Substitutions in Locally Tabular Logics.

Let $\mathbf{F}$ be a class of finite frames,
$\mathsf{L}=\mathsf{L}(\mathbf{F})$ be locally tabular and
$\mathbf{M}^{n}=\mathbf{M}^{n}(\mathbf{F})$, for any $n\geq 0$. Assume,
additionally, that F is closed under generated subframes and p-morphic images,
that is sm(F)=F, see Lemma 10. For any
$\sigma:\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm^{k}}$, define
$H_{\sigma}\colon\mathbf{M}^{k}\to\mathbf{M}^{n}$ putting
$H_{\sigma}(\mathfrak{M}^{k})=\sigma(\mathfrak{M}^{k})$, for each
$\mathfrak{M}^{k}$.141414Ghilardi wrote $\sigma(u)$ for any Kripke model $u$
and hence we have $\sigma(\mathfrak{M}^{k})$. We should, perhaps, wrote
$\sigma\colon\mathbf{M}^{k}\to\mathbf{M}^{n}$ but we think it could be
misleading as we already have
$\sigma:\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm^{k}}$ and
$\sigma:\mathsf{Fm}\to\mathsf{Fm}$. Talking about the mapping $\sigma$, it
would be unclear if we had in mind a mapping between formulas or models. For
this reason we decided to introduce $H_{\sigma}$, to replace $\sigma$, though
it could be seen as an excessive reaction.

###### Lemma 11

Suppose that $\varepsilon,\sigma:\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm^{k}}$.
Then $\varepsilon=_{\sf L}\sigma$ iff $H_{\sigma}\thicksim
H_{\varepsilon}$.151515where $H_{\sigma}\thicksim H_{\varepsilon}$ obviously
means $H_{\sigma}(\mathfrak{M}^{k})\thicksim
H_{\varepsilon}(\mathfrak{M}^{k})$ for each $\mathfrak{M}^{k}$.

  * Proof.

$(\Rightarrow)$ is obvious. $(\Leftarrow)$. Let
$H_{\sigma}(\mathfrak{M}^{k})\thicksim H_{\varepsilon}(\mathfrak{M}^{k})$, for
any $\mathfrak{M}^{k}\in\mathbf{M}^{k}$. Then
$\mathfrak{M}^{k}\vdash\sigma(A)\Leftrightarrow\sigma(\mathfrak{M}^{k})\vdash
A\Leftrightarrow\varepsilon(\mathfrak{M}^{k})\vdash
A\Leftrightarrow\mathfrak{M}^{k}\vdash\varepsilon(A).$ Thus, $\vdash_{\sf
L}\sigma(A)\leftrightarrow\varepsilon(A)$, for any $A\in\mathsf{Fm^{n}}$,
which shows $\varepsilon=_{\sf L}\sigma$.

The assumptions that the frames F are finite and L(F) is locally tabular do
not play any role in the above Lemma but they are essential in the subsequent
theorem, to prove that the conditions (i)-(iii) of Lemma 8 characterize
substitutions:

###### Theorem 20

Let $H\colon\mathbf{M}^{k}\to\mathbf{M}^{n}$. Then $H\thicksim H_{\sigma}$,
for some $\sigma:\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm^{k}}$ if and only if $H$
fulfills the following conditions:
(i) the $n$-model $H(\mathfrak{M}^{k})$ has the same frame as the $k$-model
$\mathfrak{M}^{k}$, for any $\mathfrak{M}^{k}\in\mathbf{M}^{k}$;
(ii) $H((\mathfrak{M}^{k})_{w})\thicksim(H(\mathfrak{M}^{k}))_{w}$, for any
$\mathfrak{M}^{k}=(W,R,w_{0},V^{k})\in\mathbf{M}^{k}$ and $w\in W$;
(iii) if $\mathfrak{N}^{k}\thicksim\mathfrak{M}^{k}$, then
$H(\mathfrak{N}^{k})\thicksim H(\mathfrak{M}^{k})$, for any
$\mathfrak{M}^{k},\mathfrak{N}^{k}\in\mathbf{M}^{k}.$

  * Proof.

$(\Leftarrow)$ follows from Lemma 8. The conditions (i)-(iii) of Lemma 8 seem
to be stronger than the above ones, but they are not (see Theorem 17).

To prove $(\Rightarrow)$ we assume $H\colon\mathbf{M}^{k}\to\mathbf{M}^{n}$
fulfills the above (i)–(iii). Let

$\sigma(x_{i})=\bigvee\\{\Delta(\mathfrak{N}^{k})\colon\
\mathfrak{N}^{k}\in\mathbf{M}^{k}\ \land\ H(\mathfrak{N}^{k})\Vdash
x_{i}\\},\qquad\mbox{ for $i=1,\dots,n$}.$

By Theorem 2, we can claim that we have defined
$\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$. For any $k$-model
$\mathfrak{M}^{k}=(W,R,w_{0},V^{k})\in\mathbf{M}^{k}$, we have

$\sigma(\mathfrak{M}^{k})\Vdash_{w}x_{i}\quad\Leftrightarrow\quad\sigma((\mathfrak{M}^{k})_{w})\Vdash
x_{i}\quad\Leftrightarrow\quad(\mathfrak{M}^{k})_{w}\Vdash\sigma(x_{i})\quad\Leftrightarrow$
$\exists_{\mathfrak{N}^{k}}\bigl{(}(\mathfrak{M}^{k})_{w}\Vdash\Delta(\mathfrak{N}^{k})\land
H(\mathfrak{N}^{k})\Vdash x_{i}\bigr{)}\ \Leftrightarrow\
H((\mathfrak{M}^{k})_{w})\Vdash x_{i}\ \Leftrightarrow\
H(\mathfrak{M}^{k})\Vdash_{w}x_{i},$

for any $i=1,\dots,n$ and any $w\in W$. Hence
$\sigma(\mathfrak{M}^{k})\thicksim H(\mathfrak{M}^{k})$.

The above theorem is useful to define substitutions. However, the condition
(iii) is hard to check if there is too many p-morphisms between models. So, we
would prefer a variant of 20, given below, concerning p-irreducible models.
The closure of F under p-morphic images is not necessary for the above theorem
(it suffices the closure under generated subframes) but it is necessary for
the subsequent theorem.

Let $\mathbf{M}^{n}_{ir}$, for any $n\geq 0$, be the class of p-irreducible
$n$-models over the frames $\mathbf{F}$. According to Theorem 13, for any
$A\in\mathsf{Fm}^{n}$

$A\in\mathsf{L}\quad\Leftrightarrow\quad(\mathfrak{M}^{n}\Vdash A,\mbox{ for
every }\mathfrak{M}^{n}\in\mathbf{M}^{n}_{ir}).$

###### Theorem 21

If $H\colon\mathbf{M}^{k}_{ir}\to\mathbf{M}^{n}$ fulfills
(i) the $n$-model $H(\mathfrak{M}^{k})$ has the same frame as the $k$-model
$\mathfrak{M}^{k}$, for any $\mathfrak{M}^{k}\in\mathbf{M}^{k}_{ir}$;
(ii) $H((\mathfrak{M}^{k})_{w})\thicksim(H(\mathfrak{M}^{k}))_{w}$, for any
$\mathfrak{M}^{k}=(W,R,w_{0},V^{k})\in\mathbf{M}^{k}_{ir}$ and any $w\in W$;
(iii) if $\mathfrak{N}^{k}\equiv\mathfrak{M}^{k}$, then
$H(\mathfrak{N}^{k})\thicksim H(\mathfrak{M}^{k})$, for any
$\mathfrak{M}^{k},\mathfrak{N}^{k}\in\mathbf{M}^{k}_{ir};$
then there is exactly one (up to $=_{\sf L}$) substitution
$\sigma:\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm^{k}}$ such that
$H(\mathfrak{M}^{k})\thicksim H_{\sigma}(\mathfrak{M}^{k})$, for each
$\mathfrak{M}^{k}\in\mathbf{M}^{k}_{ir}.$

  * Proof.

We proceed in the same way as above. In particular, we define

$\sigma(x_{i})=\bigvee\\{\Delta(\mathfrak{N}^{k})\colon\
\mathfrak{N}^{k}\in\mathbf{M}^{k}_{ir}\ \land\ H(\mathfrak{N}^{k})\Vdash
x_{i}\\},\qquad\mbox{ for $i=1,\dots,n$}$

and prove $H(\mathfrak{M}^{k})\thicksim H_{\sigma}(\mathfrak{M}^{k})$, for any
$\mathfrak{M}^{k}\in\mathbf{M}^{k}_{ir}$. The crucial step in our argument

$\exists_{\mathfrak{N}^{k}}\bigl{(}(\mathfrak{M}^{k})_{w}\Vdash\Delta(\mathfrak{N}^{k})\land
H(\mathfrak{N}^{k})\Vdash x_{i}\bigr{)}\ \Rightarrow\
H((\mathfrak{M}^{k})_{w})\Vdash x_{i}$

follows from the fact that, if
$(\mathfrak{M}^{k})_{w}\thicksim(\mathfrak{N}^{k})_{u}$, for some $u$, then
$(\mathfrak{M}^{k})_{w}$ and $(\mathfrak{N}^{k})_{u}$ are p-irreducible by
Theorem 15 and hence $(\mathfrak{M}^{k})_{w}\equiv(\mathfrak{N}^{k})_{u}$ by
Corollary 6. Thus, by (iii), we have $H((\mathfrak{M}^{k})_{w})\Vdash x_{i}$
if $H(\mathfrak{N}^{k})\Vdash x_{i}$.

The uniqueness of $\sigma$ follows from Lemma 11 (and Theorem 13).

Suppose we need $H\colon\mathbf{M}^{k}_{ir}\to\mathbf{M}^{n}$ fulfilling the
above (i)–(iii). Let $\mathfrak{M}^{k}=(W,\leq,w_{0},V^{k})$ be a
p-irreducible $k$-model. We should have
$H(\mathfrak{M}^{k})=(W,\leq,w_{0},V^{n})$, for some $V^{n}$, which means only
the valuations $V^{n}$ are to be defined. By Theorem 15,
$(\mathfrak{M}^{k})_{w}$ is p-irreducible, for any $w\in W$, and hence we
could define $H((\mathfrak{M}^{k})_{w})$ inductively with respect to
$d_{\mathfrak{F}}(w)$, where $\mathfrak{F}=(W,\leq,w_{0})$. First, we define
$H((\mathfrak{M}^{k})_{w})$ for $n$-models over 1-element reflexive frames,
that is we define $V^{n}(w)$ for end elements $w\in W$; any subset of
$\\{x_{1},\dots,x_{k}\\}$ can be taken as $V^{n}(w)$. Then, assuming
$H((\mathfrak{M}^{k})_{u})$ has been defined for any $u>w$, and hence we have
$V^{n}(u)$ for any $u>w$, we define $V^{n}(w)$. The only restriction is
monotonicity, that is we should have $V^{n}(w)\subseteq V^{k}(u)$ for any
$u>w$. The condition (ii) would be satisfied as we would even have
$H((\mathfrak{M}^{k})_{w})=(H(\mathfrak{M}^{k}))_{w}$. The condition (iii)
should not produce any harm if we define $H$ on the equivalence classes
$[\mathfrak{M}^{k}]_{\equiv}$. We should get
$H\colon\mathbf{M}^{k}_{ir}/\\!\\!\equiv\ \to\
\mathbf{M}^{n}/\\!\\!\thicksim$. Note that it would be much easier to satisfy
this condition than to satisfy the corresponding (iii) of Theorem 20 where we
should get $H\colon\mathbf{M}^{k}/\\!\\!\thicksim\ \to\
\mathbf{M}^{n}/\\!\\!\thicksim$.

Since L is locally tabular, any formula $A\in\mathsf{Fm}^{n}$ is a disjunction
of the characters of all $A$-models (that is $n$-models
$\mathfrak{M}^{n}\in\mathbf{M}^{n}$ such that $A$ is true at
$\mathfrak{M}^{n}$):

$A=_{\sf L}\bigvee\\{\Delta(\mathfrak{M}^{n})\colon\Delta(\mathfrak{M}^{n})\to
A\in\mathsf{L}\\}=_{\sf
L}\bigvee\\{\Delta(\mathfrak{M}^{n})\colon\mathfrak{M}^{n}\Vdash A\\}.$ $None$

It also shows that each L-consistent (that is $\not=_{\sf L}\bot$) formula is
L-unifiable.

###### Lemma 12

A substitution $\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$ is an
L-unifier for $A\in\mathsf{Fm}^{n}$ iff $\sigma(\mathfrak{M}^{k})\Vdash A$ for
each $k$-model $\mathfrak{M}^{k}$. In other words, $\sigma$ is a unifier for
$A$ iff all $\sigma$-models are $A$-models.

  * Proof.

$\sigma(\mathfrak{M}^{k})\Vdash A$ iff $\mathfrak{M}^{k}\Vdash\sigma(A)$, for
each $\mathfrak{M}^{k}$. Thus, $\sigma(\mathfrak{M}^{k})\Vdash A$ for each
$\mathfrak{M}^{k}$ iff $\mathfrak{M}^{k}\Vdash\sigma(A)$ for each
$\mathfrak{M}^{k}$. But $\sigma$ is an L-unifier for $A$ iff
$\mathfrak{M}^{k}\Vdash\sigma(A)$ for each $\mathfrak{M}^{k}$.

Accordingly, $\sigma$ is a unifier for $A$ iff the disjunction
$\bigvee\\{\Delta(\mathfrak{M}^{n})\colon\mathfrak{M}^{n}\Vdash A\\}$ in
$(\star)$ contains the characters of all $\sigma$-models. To put it in other
words:

###### Corollary 8

A substitution $\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$ is an
L-unifier for a formula $A\in\mathsf{Fm}^{n}$ iff $A_{\sigma}\to
A\in\mathsf{L}$, where
$A_{\sigma}=\bigvee\\{\Delta(\sigma(\mathfrak{M}^{k}))\colon\mathfrak{M}^{k}\in\mathbf{M}^{k}\\}.$

Thus, each substitution $\sigma$ is an L-unifier of some formulas
$A\in\mathsf{Fm}^{n}$ and among these formulas we can find the strongest (or
the smallest in the Lindenbum algebra) formula $A_{\sigma}$. Using Lemma 12
and Lemma 17 we can now characterize all unifiers of $A_{\sigma}$.

###### Corollary 9

Let $\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$. A substitution
$\tau\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{m}$ is an L-unifier for
$A_{\sigma}$ iff all $\tau$-models are (equivalent to) $\sigma$-models, that
is iff
(iv) for every $\mathfrak{M}^{m}\in\mathbf{M}^{m}$ there is an
$\mathfrak{M}^{k}\in\mathbf{M}^{k}$ such that
$\tau(\mathfrak{M}^{m})\thicksim\sigma(\mathfrak{M}^{k})$.

The above condition (iv) can be also written down as the inclusion

$\tau(\mathbf{M}^{m})/\\!\\!\thicksim\quad\subseteq\quad\sigma(\mathbf{M}^{k})/\\!\\!\thicksim.$

There remains to characterize the relation $\preccurlyeq$ (of being a more
general substitution) in terms of $\sigma$-models.

###### Lemma 13

A substitution $\tau\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{m}$ is more
general than $\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$ (that is
$\tau\preccurlyeq\sigma$) iff there is
$F\colon\mathbf{M}^{k}\to\mathbf{M}^{m}$, fulfilling (i)–(iii) of Theorem 20,
such that
(v) $\tau(F(\mathfrak{M}^{k}))\thicksim\sigma(\mathfrak{M}^{k})$, for every
$\mathfrak{M}^{k}\in\mathbf{M}^{k}$.
Consequently, if $\tau\preccurlyeq\sigma$, then all $\sigma$-models are
(equivalent to) $\tau$-models and hence

$\tau(\mathbf{M}^{m})/\\!\\!\thicksim\quad\supseteq\quad\sigma(\mathbf{M}^{k})/\\!\\!\thicksim.$

  * Proof.

Suppose that $\nu\circ\tau=_{\sf L}\sigma$ for some
$\nu\colon\\{x_{1},\dots,x_{m}\\}\to\mathsf{Fm}^{k}$ and $F=H_{\nu}$. Then,
$\tau(F(\mathfrak{M}^{k}))=\tau(\nu(\mathfrak{M}^{k}))$ and, for each
$B\in\mathsf{Fm}^{n}$, $\tau(\nu(\mathfrak{M}^{k}))\Vdash B\ \Leftrightarrow\
\nu(\mathfrak{M}^{k})\Vdash\tau(B)\ \Leftrightarrow\
\mathfrak{M}^{k}\Vdash\nu(\tau(B))\ \Leftrightarrow\
\mathfrak{M}^{k}\Vdash\sigma(B)\ \Leftrightarrow\
\sigma(\mathfrak{M}^{k})\Vdash B.$ Hence we get (v).

The reverse implication is shown in the same way. We get
$\nu\colon\\{x_{1},\dots,x_{m}\\}\to\mathsf{Fm}^{k}$ such that
$F(\mathfrak{M}^{k})=\nu(\mathfrak{M}^{k})$, for each $\mathfrak{M}^{k}$, by
Lemma 12. Then, using (v), we show $\mathfrak{M}^{k}\Vdash\nu(\tau(B))\
\Leftrightarrow\ \mathfrak{M}^{k}\Vdash\sigma(B)$ for each
$B\in\mathsf{Fm}^{n}$ and this yields $\nu\circ\tau=_{\sf L}\sigma$.

###  4.2 Locally Tabular Logics with Finitary Unification.

Now, we give a short proof of the main result of [10] characterizing locally
tabular intermediate logics with finitary (or unitary) unification.

###### Theorem 22

A locally tabular intermediate logic L has finitary (or unitary) unification
if and only if for every $n\geq 0$ there exists a number $m\geq 0$ such that
for every $k\geq 0$ and every
$\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$ there are
$G:\mathbf{M}^{m}\to\mathbf{M}^{n}$ and $F:\mathbf{M}^{k}\to\mathbf{M}^{m}$
such that
(i) $G$ preserves the frame of any $m$-model
$\mathfrak{M}^{m}=(W,R,w_{0},V^{m})\in\mathbf{M}^{m}$;
$F$ preserves the frame of any $k$-model
$\mathfrak{M}^{k}=(W^{\prime},R^{\prime},w^{\prime}_{0},V^{k})\in\mathbf{M}^{k}$;
(ii) $G((\mathfrak{M}^{m})_{w})\thicksim(G(\mathfrak{M}^{m}))_{w}$, for any
$\mathfrak{M}^{m}=(W,R,w_{0},V^{m})\in\mathbf{M}^{m}$ and $w\in W$;
$F((\mathfrak{M}^{k})_{w^{\prime}})\thicksim(F(\mathfrak{M}^{k}))_{w^{\prime}}$,
for any
$\mathfrak{M}^{k}=(W^{\prime},R^{\prime},w_{0}^{\prime},V^{k})\in\mathbf{M}^{k}$
and $w^{\prime}\in W^{\prime}$;
(iii) $\mathfrak{N}^{m}\thicksim\mathfrak{M}^{m}\ \Rightarrow\
G(\mathfrak{N}^{m})\thicksim G(\mathfrak{M}^{m}),\ \mbox{ for any }\
\mathfrak{M}^{m},\mathfrak{N}^{m}\in\mathbf{M}^{m}$;
$\mathfrak{N}^{k}\thicksim\mathfrak{M}^{k}\ \Rightarrow\
F(\mathfrak{N}^{k})\thicksim F(\mathfrak{M}^{k}),\ \mbox{ for any }\
\mathfrak{M}^{k},\mathfrak{N}^{k}\in\mathbf{M}^{k}$;
(iv) for every $\mathfrak{M}^{m}\in\mathbf{M}^{m}$ there is
$\mathfrak{M}^{k}\in\mathbf{M}^{k}$ such that
$G(\mathfrak{M}^{m})\thicksim\sigma(\mathfrak{M}^{k})$;
(v) $G(F(\mathfrak{M}^{k}))\thicksim\sigma(\mathfrak{M}^{k})$, for every
$\mathfrak{M}^{k}\in\mathbf{M}^{k}$; see Figure 15 below.

$\mathbf{M}^{k}\\!/\\!\\!\thicksim$$\mathbf{M}^{n}\\!/\\!\\!\thicksim$$\mathbf{M}^{m}\\!/\\!\\!\thicksim$$F$$G$$H_{\sigma}$
Fig. 15: Condition (v)

  * Proof.

Since L is locally tabular, $\mathsf{Fm}^{n}$ is finite (up to $=_{\sf L}$),
for each $n$, and each $\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$
is a unifier of $A_{\sigma}\in\mathsf{Fm}^{n}$, see Corollary 8. Thus, if L
has finitary (or unitary) unification, one can find, for every $n\geq 0$, a
number $m$ such that each L-unifiable formula $A\in\mathsf{Fm}^{n}$ (and
$A_{\sigma}$ in particular) has a complete set of unifiers among
$\tau\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{m}$. Suppose
$\tau\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{m}$ is a unifier for
$A_{\sigma}$ and $\tau\preccurlyeq\sigma$. Take $G=H_{\tau}$ and let $F$ be
the mapping determined by Lemma 13. Then the conditions (i)–(v) are obviously
fulfilled.

On the other hand, using the conditions (i)–(v) one shows that the set of
L-unifiers $\tau\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{m}$, for any
unifiable $A\in\mathsf{Fm}^{n}$, is complete. Since $\mathsf{L}$ is locally
tabular, there is only finitely many (up to $=_{\sf L}$) such unifiers $\tau$
and hence unification is finitary (unless unitary).

The above theorem do not need the assumption that F is closed under p-morphic
images; it suffices only the closure under generated subframes. But F=sm(F) is
needed for the following version of 22 where we refer to Theorem 21 (instead
of 20). For this version of 22 we must, however, modify, the condition (v) as
we cannot assume that $F(\mathfrak{M}^{k})$ is p-irreducible even if
$\mathfrak{M}^{k}$ is p-irreducible.

###### Theorem 23

A locally tabular intermediate logic L has finitary (or unitary) unification
if and only if for every $n\geq 0$ there exists a number $m\geq 0$ such that
for every $k\geq 0$ and every
$\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$ there are
$G:\mathbf{M}^{m}_{ir}\to\mathbf{M}^{n}$ and
$F:\mathbf{M}^{k}_{ir}\to\mathbf{M}^{m}$ such that
(i) $G$ preserves the frame of any $m$-model
$\mathfrak{M}^{m}=(W,R,w_{0},V^{m})\in\mathbf{M}^{m}_{ir}$;
$F$ preserves the frame of any $k$-model
$\mathfrak{M}^{k}=(W^{\prime},R^{\prime},w^{\prime}_{0},V^{k})\in\mathbf{M}^{k}_{ir}$;
(ii) $G((\mathfrak{M}^{m})_{w})\thicksim(G(\mathfrak{M}^{m}))_{w}$, for any
$\mathfrak{M}^{m}=(W,R,w_{0},V^{m})\in\mathbf{M}^{m}_{ir}$ and $w\in W$;
$F((\mathfrak{M}^{k})_{w^{\prime}})\thicksim(F(\mathfrak{M}^{k}))_{w^{\prime}}$,
for any
$\mathfrak{M}^{k}=(W^{\prime},R^{\prime},w_{0}^{\prime},V^{k})\in\mathbf{M}^{k}_{ir}$
and $w^{\prime}\in W^{\prime}$;
(iii) $\mathfrak{N}^{m}\equiv\mathfrak{M}^{m}\ \Rightarrow\
G(\mathfrak{N}^{m})\thicksim G(\mathfrak{M}^{m}),\ \mbox{ for any }\
\mathfrak{M}^{m},\mathfrak{N}^{m}\in\mathbf{M}^{m}_{ir}$;
$\mathfrak{N}^{k}\equiv\mathfrak{M}^{k}\ \Rightarrow\
F(\mathfrak{N}^{k})\thicksim F(\mathfrak{M}^{k}),\ \mbox{ for any }\
\mathfrak{M}^{k},\mathfrak{N}^{k}\in\mathbf{M}^{k}_{ir}$;
(iv) for every $\mathfrak{M}^{m}\in\mathbf{M}^{m}_{ir}$ there is
$\mathfrak{M}^{k}\in\mathbf{M}^{k}_{ir}$ such that
$G(\mathfrak{M}^{m})\thicksim\sigma(\mathfrak{M}^{k})$;
(v) if $\mathfrak{N}^{m}\thicksim F(\mathfrak{M}^{k})$, then
$G(\mathfrak{N}^{m})\thicksim\sigma(\mathfrak{M}^{k})$, for every
$\mathfrak{M}^{k}\in\mathbf{M}^{k}_{ir}$ and
$\mathfrak{N}^{m}\in\mathbf{M}^{m}_{ir}$.

In [10] the above theorems is applied to determine the unification types of
locally tabular logics. We use them, as well, in the present paper.

Let us recall that $\mathbf{H}_{un}$ (see Figure 7) consists of all frames
$\mathfrak{L}_{d}+\mathfrak{R}_{s}$ , where $s,d\geq 0$.161616There is no
$\mathfrak{L}_{0}$ (or it would be the empty frame), so we should have here:
all logics determined by $\mathfrak{R}_{s}$ and
$\mathfrak{L}_{d}+\mathfrak{R}_{s}$, where $s\geq 0$ and $d\geq 1$, if we
agree that $\mathfrak{R}_{0}=\mathfrak{F}_{0}=\mathfrak{L}_{1}$. The logic
L($\mathbf{H}_{un}$) is locally tabular as it extends PWL, see [11].

###### Theorem 24

For any $\mathbf{F}\subseteq\mathbf{H}_{un}$, the logic L($\mathbf{F}$) has
unitary unification.

  * Proof.

Let $n\geq 1$, and $m=n\cdot 2^{n}+1$ and
$\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$, for some $k$. We need
$G:\mathbf{M}^{m}_{ir}\to\mathbf{M}^{n}$ and
$F:\mathbf{M}^{k}_{ir}\to\mathbf{M}^{m}$ fulfilling (i)-(v) of Theorem 23. Let
$code(\mathfrak{f}^{k}_{0})=\mathfrak{f}^{n}_{0}\mathfrak{g}^{n}_{2}\mathfrak{g}^{n}_{3}\dots,\mathfrak{g}^{n}_{2^{n}}1\quad\mbox{(the
concatenation of $\mathfrak{f}^{k}_{0},\mathfrak{g}^{n}_{i}$'s and the suffix
$1$)}$ includes all $\mathfrak{g}^{n}_{i}$’s (in any order where repetitions
are allowed) such that

$\mathfrak{g}^{n}_{i}$$\mathfrak{f}^{n}_{0}$

$\quad=\quad\sigma\Bigl{(}$ $\mathfrak{g}^{k}_{i}$$\mathfrak{f}^{k}_{0}$
$\Bigr{)},\quad\mbox{ for some }\mathfrak{g}_{i}^{k}.$ Then we define
$F(\mathfrak{M}^{k})$:

$\mathfrak{M}^{k}$:$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{s}$$\mathfrak{f}^{k}_{s+1}$$\mathfrak{f}^{k}_{s+d+1}$$\mathfrak{f}^{k}_{1}$$\sigma(\mathfrak{M}^{k})$:$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{s}$$\mathfrak{f}^{n}_{s+1}$$\mathfrak{f}^{n}_{s+d+1}$$\mathfrak{f}^{n}_{1}$$F(\mathfrak{M}^{k})$:$\mathfrak{f}^{n}_{0}\mathfrak{g}^{n}_{2}\dots\mathfrak{g}^{n}_{2^{n}}1=code(\mathfrak{f}^{k}_{0})$$\mathfrak{f}^{n}_{s}\mathfrak{g}^{n}_{2}\dots\mathfrak{g}^{n}_{2^{n}}0$$\mathfrak{f}^{n}_{s+1}0\cdots
0$$\mathfrak{f}^{n}_{s+d+1}0\cdots
0$$\mathfrak{f}^{n}_{1}\mathfrak{g}^{n}_{2}\dots\mathfrak{g}^{n}_{2^{n}}0$
Fig. 16:

One checks the conditions (i)-(iii) for the mapping $F$. Note that
$F(\mathfrak{M}^{k})$ could be not p-irreducible, for some p-irreducible
$\mathfrak{M}^{k}$, but one could only collapse elements of the depth $2$ or
elements below $s+1$ that is elements in the ‘leg’ of the model.
A. We put $G(\mathfrak{M}^{m})=\mathfrak{M}^{m}\\!\\!\upharpoonright n$ if
$\mathfrak{M}^{m}\thicksim F(\mathfrak{M}^{k})$ for some $\mathfrak{M}^{k}$.
Let $\mathfrak{M}^{m}=(W,R,w_{0},V^{m})$ and
$\mathfrak{M}^{k}=(U,S,u_{0},V^{k})$. The conditions (i)-(v) for $G$ seem to
be obvious; as concerns (ii), for every $w\in W$ there is $u\in U$ such that
$(\mathfrak{M}^{m})_{w}\thicksim F((\mathfrak{M}^{k})_{u})$. To show (iv) and
(v), let us note that $F(\mathfrak{M}^{k})\\!\\!\upharpoonright
n=\sigma(\mathfrak{M}^{k})$, see Figure 16. Thus,
$G(F(\mathfrak{M}^{k}))=\sigma(\mathfrak{M}^{k})$ and
$G(\mathfrak{M}^{m})=\mathfrak{M}^{m}\\!\\!\upharpoonright n\thicksim
F(\mathfrak{M}^{k})\\!\\!\upharpoonright n=\sigma(\mathfrak{M}^{k})$ if
$\mathfrak{M}^{m}\thicksim F(\mathfrak{M}^{k})$.
B. There remains to define $G(\mathfrak{M}^{m})$ for
$\mathfrak{M}^{m}\in\mathbf{M}^{m}_{ir}$ non-equivalent to any
$F(\mathfrak{M}^{k})$. Our definition is inductive (to secure (ii)) and we
should take into account that for some $w\in W$ and some $\mathfrak{M}^{k}$ we
may have $(\mathfrak{M}^{m})_{w}\thicksim F(\mathfrak{M}^{k})$ and hence we
have defined
$G((\mathfrak{M}^{m})_{w})=(\mathfrak{M}^{m})_{w}\\!\\!\upharpoonright n$.
Since (iii) is obvious and (v) is irrelevant in this case, we have to bother
only about (i) and (iv). Thus, the frame of the $n$-model
$G(\mathfrak{M}^{m})$ should be the same as the frame of $\mathfrak{M}^{m}$
and $G(\mathfrak{M}^{m})$ should always be equivalent with a $\sigma$-model.
Let $\mathfrak{M}^{m}$ be one of the following $m$-models:

$\mathfrak{f}^{m}_{0}$$\mathfrak{f}^{m}_{0}$$\mathfrak{f}^{m}_{1}$where
$s,d\geq
1$$\mathfrak{f}^{m}_{1}$$\mathfrak{f}^{m}_{0}$$\mathfrak{f}^{m}_{s}$$\mathfrak{f}^{m}_{s+1}$$\mathfrak{f}^{m}_{1}$$\mathfrak{f}^{m}_{0}$$\mathfrak{f}^{m}_{s}$$\mathfrak{f}^{m}_{s+1}$$\mathfrak{f}^{m}_{s+d+1}$
Fig. 17:

B1. If $(\mathfrak{M}^{m})_{0}$171717Let us agree that, in Figure 17, the
vertex $i$ is labeled with $\mathfrak{f}^{m}_{i}$. is not equivalent with any
$F(\mathfrak{M}^{k})$, we take any valuation $\mathfrak{f}^{k}$, let
$\sigma(\mathfrak{L}_{1},\\{\mathfrak{f}^{k}\\})=(\mathfrak{L}_{1},\\{\mathfrak{f}^{n}\\})$,
for some $\mathfrak{f}^{n}$, and put
$G(\mathfrak{M}^{m})\thicksim(\mathfrak{L}_{1},\\{\mathfrak{f}^{n}\\})$ (which
uniquely determines $G(\mathfrak{M}^{m})$). Then (i)–(iv) are clearly
fulfilled and (v) is irrelevant. We do the same if $0$ is the only vertex $i$
for which $(\mathfrak{M}^{m})_{i}\thicksim F(\mathfrak{M}^{k})$, with some
$\mathfrak{M}^{k}$; we only take $\mathfrak{f}^{k}=\mathfrak{f}^{k}_{0}$.
B2. We can defined $G((\mathfrak{M}^{m})_{i})$, if $1\leq i\leq s$, using A.
or B1. Thus, if
$(\mathfrak{M}^{m})_{i}=(\mathfrak{L}_{2},\\{\mathfrak{f}^{m}_{0},\mathfrak{f}^{m}_{1}\\})$
and
$\mathfrak{f}^{m}_{0}=\mathfrak{f}^{n}_{0}\mathfrak{g}^{n}_{2}\dots\mathfrak{g}^{n}_{2^{n}}1=code(\mathfrak{f}^{k}_{0})$
and
$\mathfrak{f}^{m}_{1}=\mathfrak{f}^{n}_{1}\mathfrak{g}^{n}_{2}\dots\mathfrak{g}^{n}_{2^{n}}0$,
for some p-irreducible
$\mathfrak{M}^{k}=(\mathfrak{L}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{1}\\})$
(and we have
$\sigma(\mathfrak{M}^{k})=(\mathfrak{L}_{2},\\{\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{1}\\})$),
we put
$G((\mathfrak{M}^{m})_{i})=\sigma(\mathfrak{M}^{k})=(\mathfrak{L}_{2},\\{\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{1}\\})$.
Note that $\mathfrak{f}^{n}_{1}$ must be one of $\mathfrak{g}^{n}_{i}$’s in
$code(\mathfrak{f}^{k}_{0})$. Otherwise,
$G((\mathfrak{M}^{m})_{i})\thicksim\sigma(\mathfrak{L}_{1},\\{\mathfrak{f}^{k}_{0}\\})$,
where
$G((\mathfrak{M}^{m})_{0})=\sigma((\mathfrak{L}_{1},\\{\mathfrak{f}^{k}_{0}\\})$).
Thus, in each case we have
$G((\mathfrak{M}^{m})_{i})=\sigma(\mathfrak{M}^{k})$, for some $k$-model
$\mathfrak{M}^{k}$ over $\mathfrak{L}_{2}$.181818We have added the suffix $0$
or $1$ at the end of $code(\mathfrak{f}^{k}_{0})$, see Figure 16, to be sure
that $F(\mathfrak{M}^{k})$ is p-irreducible if $\mathfrak{M}^{k}$ is a
p-irreducible model over $\mathfrak{L}_{2}$.

B3. The worst case is $G((\mathfrak{M}^{m})_{s+1})$. By B2. and the definition
of $code(\mathfrak{f}^{k}_{0})$ (included in $\mathfrak{f}^{m}_{0}$), we can
assume that, if $1\leq i\leq s$, then
$G((\mathfrak{M}^{m})_{i})=G(\mathfrak{L}_{2},\\{\mathfrak{f}^{m}_{0},\mathfrak{f}^{m}_{i}\\})=\sigma(\mathfrak{M}^{k}_{i})$
for some $k$-model
$\mathfrak{M}^{k}_{i}=(\mathfrak{L}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{i}\\})$;
note that we have the same $\mathfrak{f}^{k}_{0}$ in each of the models
$\mathfrak{M}^{k}_{i}$. There are different $\mathfrak{f}^{k}_{0}$’s with the
same $code(\mathfrak{f}^{k}_{0})$; but we can always decide which
$\mathfrak{f}^{k}_{0}$ is chosen - for instance, our choose could be given
according to the lexicographical order in which all valuations are gven. Then,
assuming $(\mathfrak{M}^{m})_{{s+1}}$ is not equivalent with any
$F(\mathfrak{M}^{k})$, we take the $k$-valuation $0\cdots 0$ and define
$G((\mathfrak{M}^{m})_{{s+1}})$ as it is shown in Figure 18 below.

$\sigma\Bigl{(}\ \
\mathfrak{f}^{k}_{1}$$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{s}\ \Bigr{)}\
=$$0\cdots
0$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{s}$$\mathfrak{f}^{n}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{m}_{1}$$\mathfrak{f}^{m}_{s+d+1}$$\mathfrak{f}^{m}_{0}$$\mathfrak{f}^{m}_{s}$$\mathfrak{f}^{m}_{s+1}$$G\Bigl{(}$$\Bigr{)}\
=$$\mathfrak{f}^{n}$$\mathfrak{f}^{n}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{s}$$\mathfrak{f}^{n}$
Fig. 18:

B4. There remains to define $G((\mathfrak{M}^{m})_{{s+i+1}})$ assuming that
$i\geq 1$, and $(\mathfrak{M}^{m})_{{s+i+1}}$ is not equivalent with any
$F(\mathfrak{M}^{k})$ and $G((\mathfrak{M}^{m})_{{s+i}})$ has already been
defined. Then we approach as it is shown in Figure 19

$\mathfrak{f}^{m}_{1}$$G\Bigl{(}$$\mathfrak{f}^{m}_{0}$$\mathfrak{f}^{m}_{s}$$\
\ \Bigr{)}\
=$$\mathfrak{f}^{m}_{s+1}$$\mathfrak{f}^{m}_{s+i}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{s}$$\mathfrak{f}^{n}_{s+1}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{s+i}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{m}_{1}$$\mathfrak{f}^{m}_{s+i}$$\mathfrak{f}^{m}_{s+d+1}$$\mathfrak{f}^{m}_{0}$$\mathfrak{f}^{m}_{s}$$\mathfrak{f}^{m}_{s+1}$$G\Bigl{(}$$\Bigr{)}\
=$$\mathfrak{f}^{n}_{s+i}$$\mathfrak{f}^{n}_{s+i}$$\mathfrak{f}^{n}_{s+i}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{s}$$\mathfrak{f}^{n}_{s+1}$
Fig. 19:

Thus, we have $G(\mathfrak{M}^{m})\thicksim G((\mathfrak{M}^{m})_{{s+i}})$.

###### Theorem 25

The logic $\mathsf{L}(\mathfrak{C}_{5})$ (see Figure 6) has finitary
unification.

  * Proof.

Let
$\mathbf{F}=\\{\mathfrak{L}_{1},\mathfrak{L}_{2},\mathfrak{F}_{2},\mathfrak{L}_{3},+\mathfrak{F}_{2},\mathfrak{R}_{2},\mathfrak{Y}_{2},\mathfrak{Y}_{3},\mathfrak{C}_{5}\\}$
(see Figure 1 and 3) and let $\mathsf{L}=\mathsf{L}(\mathbf{F})$. Since
$\mathbf{F}=sm(\mathfrak{C}_{5})$, we conclude L is the logic of
$\mathfrak{C}_{5}$; see Lemma 10. Let $n\geq 1$ and $m=n+n\cdot 4^{n}+2$. Take
any $\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$ and show there are
$F\colon\mathbf{M}^{k}\to\mathbf{M}^{m}$ and
$G\colon\mathbf{M}^{m}\to\mathbf{M}^{n}$ fulfilling the conditions (i)–(v) of
Theorem 23.

Let $\mathfrak{f}^{k}$ be any $k$-valuation and let
$\sigma(\mathfrak{L}_{1},\mathfrak{f}^{k})=(\mathfrak{L}_{1},\mathfrak{f}^{n})$
for some $\mathfrak{f}^{n}$. We define the $m$-valuation
$code(\mathfrak{f}^{k})$ a bit different way than in the proof of Theorem 24.
Let
$code(\mathfrak{f}^{k})=\mathfrak{f}^{n}\mathfrak{g}^{n}_{1}\mathfrak{h}^{n}_{1}\dots\mathfrak{g}^{n}_{2^{n}}\mathfrak{h}^{n}_{2^{n}}11\quad\mbox{(the
concatenation of $\mathfrak{f}^{n}$, all
$\mathfrak{g}^{n}_{i},\mathfrak{h}^{n}_{i}$'s and $11$)}$
where $\mathfrak{g}^{n}_{i},\mathfrak{h}^{n}_{i}$’s are all $n$-valuations
such that

$\mathfrak{f}^{n}$$\mathfrak{g}^{n}_{i}$$\mathfrak{h}^{n}_{i}$$=\quad\sigma\Bigl{(}$$\mathfrak{h}_{i}^{k}$$\mathfrak{f}^{k}$$\mathfrak{g}^{k}_{i}$$\Bigr{)},\quad\mbox{
for some }\mathfrak{g}_{i}^{k},\mathfrak{h}_{i}^{k}$. Fig. 20: The definition
of $code(\mathfrak{f}^{k})$

We could make $code(\mathfrak{f}^{k})$ unique, for any $\mathfrak{f}^{k}$. For
instance, let us begin with the sequence
$\mathfrak{g}_{1}^{n}\mathfrak{h}_{1}^{n}\dots\mathfrak{g}_{2^{n}}^{n}\mathfrak{h}_{2^{n}}^{n}$
containing all possible pairs $\mathfrak{g}_{i}^{n}\mathfrak{h}_{i}^{n}$ of
$n$-valuations (regarded as binary strings) put in a lexicographical order.
The sequence contains $4^{n}$ bites. Then, step by step, we would remain the
pair $\mathfrak{g}_{i}^{n}\mathfrak{h}_{i}^{n}$ or replace it with
$\mathfrak{f}^{n}\mathfrak{f}^{n}$ depending if it fulfills (or not) the
equation in Figure 20, for some $\mathfrak{g}_{i}^{k},\mathfrak{h}_{i}^{k}$.
Eventually, we add $\mathfrak{f}^{n}$ at the beginning and $11$ at the end of
the sequence receiving an $m$-valuation.

Now, we are ready to define $F(\mathfrak{M}^{k})$, for any p-irreducible
$k$-model $\mathfrak{M}^{k}$ over any frame in $\mathbf{F}$. So, let
$\mathfrak{M}^{k}$ be one of the following $k$-models:

$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{1}$$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{1}$$\mathfrak{f}^{k}_{0^{\prime}}$$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{2}$$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{1}$$\mathfrak{f}^{k}_{1}$$\mathfrak{f}^{k}_{2}$$\mathfrak{f}^{k}_{0^{\prime}}$$\mathfrak{f}^{k}_{0}$

$\mathfrak{f}^{k}_{2}$$\mathfrak{f}^{k}_{1^{\prime}}$$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{1}$$\mathfrak{f}^{k}_{2}$$\mathfrak{f}^{k}_{1^{\prime}}$$\mathfrak{f}^{k}_{0^{\prime}}$$\mathfrak{f}^{k}_{1}$$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{2}$$\mathfrak{f}^{k}_{1^{\prime}}$$\mathfrak{f}^{k}_{0^{\prime}}$$\mathfrak{f}^{k}_{1}$$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{2}$$\mathfrak{f}^{k}_{1^{\prime}}$$\mathfrak{f}^{k}_{0^{\prime}}$$\mathfrak{f}^{k}_{1}$$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{0^{\prime\prime}}$

Fig. 21:

and let $\sigma(\mathfrak{M}^{k})$ be, correspondingly;

$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{0^{\prime}}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{2}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{2}$$\mathfrak{f}^{n}_{0^{\prime}}$$\mathfrak{f}^{n}_{0}$

$\mathfrak{f}^{n}_{2}$$\mathfrak{f}^{n}_{1^{\prime}}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{2}$$\mathfrak{f}^{n}_{1^{\prime}}$$\mathfrak{f}^{n}_{0^{\prime}}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{2}$$\mathfrak{f}^{n}_{1^{\prime}}$$\mathfrak{f}^{n}_{0^{\prime}}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{2}$$\mathfrak{f}^{n}_{1^{\prime}}$$\mathfrak{f}^{n}_{0^{\prime}}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{0^{\prime\prime}}$

Fig. 22:

We define $F(\mathfrak{M}^{k})$ as one of the following $m$-models:

$code(\mathfrak{f}^{k}_{0})$$\mathfrak{f}^{n}_{1}0\cdots
01$$code(\mathfrak{f}^{k}_{0})$$\mathfrak{f}^{n}_{1}0\cdots
01$$code(\mathfrak{f}^{k}_{0^{\prime}})$$code(\mathfrak{f}^{k}_{0})$$\mathfrak{f}^{n}_{2}0\cdots
0$$code(\mathfrak{f}^{k}_{0})$$\mathfrak{f}^{n}_{1}0\cdots
01$$\mathfrak{f}^{n}_{1}0\cdots 01$$\mathfrak{f}^{n}_{2}0\cdots
0$$code(\mathfrak{f}^{k}_{0^{\prime}})$$code(\mathfrak{f}^{k}_{0})$

$\mathfrak{f}^{n}_{2}0\cdots 0$$\mathfrak{f}^{n}_{1^{\prime}}0\cdots
01$$code(\mathfrak{f}^{k}_{0})$$\mathfrak{f}^{n}_{1}0\cdots
01$$\mathfrak{f}^{n}_{2}0\cdots 0$$\mathfrak{f}^{n}_{1^{\prime}}0\cdots
01$$code(\mathfrak{f}^{k}_{0^{\prime}})$$\mathfrak{f}^{n}_{1}0\cdots
01$$code(\mathfrak{f}^{k}_{0})$$\mathfrak{f}^{n}_{2}0\cdots
0$$\mathfrak{f}^{n}_{1^{\prime}}0\cdots
01$$code(\mathfrak{f}^{k}_{0^{\prime}})$$\mathfrak{f}^{n}_{1}0\cdots
01$$code(\mathfrak{f}^{k}_{0})$$\mathfrak{f}^{n}_{2}0\cdots
0$$\mathfrak{f}^{n}_{1^{\prime}}0\cdots
01$$code(\mathfrak{f}^{k}_{0^{\prime}})$$\mathfrak{f}^{n}_{1}0\cdots
01$$code(\mathfrak{f}^{k}_{0})$$code(\mathfrak{f}^{k}_{0^{\prime\prime}})$

Fig. 23:

The conditions (i)-(iii) of Theorem 23, as concerns the mapping $F$, are
obviously fulfilled. Note that it is important that all binary strings have
the size $m$ and we get intuitionistic models, but it is of no importance what
is included in $code(\mathfrak{f}^{k})$. There remains to define the mapping
$G$. Let

$G(\mathfrak{M}^{m})=\left\\{\begin{array}[]{ll}\mathfrak{M}^{m}\\!\\!\upharpoonright
n&\hbox{if $\mathfrak{M}^{m}\thicksim F(\mathfrak{M}^{k})$ for some
$\mathfrak{M}^{k}$;}\\\ ?&\hbox{otherwise;}\end{array}\right.$

where the $n$-model $\mathfrak{M}^{m}\\!\\!\upharpoonright n$ results from
$\mathfrak{M}^{m}$ by the restriction of all valuations $\mathfrak{f}^{m}_{i}$
of $\mathfrak{M}^{m}$ to $\\{x_{1},\dots,x_{n}\\}$. Note that
$\mathfrak{M}^{m}\thicksim F(\mathfrak{M}^{k})$ yields
$\mathfrak{M}^{m}\\!\\!\upharpoonright n\thicksim
F(\mathfrak{M}^{k})\\!\\!\upharpoonright n$ and hence
$G(\mathfrak{M}^{m})\thicksim\sigma(\mathfrak{M}^{k})$ by the definition of
$F$ and $G$. Thus, (v) is fulfilled. If an $m$-model $\mathfrak{M}^{m}$ is
equivalent with some $F(\mathfrak{M}^{k})$, then any its generated submodel
$(\mathfrak{M}^{m})_{w}$ is equivalent with $F((\mathfrak{M}^{k})_{u})$, for
some $u$; see Corollary 7. Thus, (i)-(v) are fulfilled if the first line of
the definition $G(\mathfrak{M}^{m})$ applies.

There remains to define $G(\mathfrak{M}^{m})$ assuming $\mathfrak{M}^{m}$ is
not equivalent with any $F(\mathfrak{M}^{k})$. Our definition is inductive
with respect to the depth of $\mathfrak{M}^{m}$ to secure (ii). Since (v) is
irrelevant here and (iii) is quite obvious, we should require
$G(\mathfrak{M}^{m})$ and $\mathfrak{M}^{m}$ were defined over the same frame,
and $G(\mathfrak{M}^{m})$ should be equivalent with a $\sigma$-model.

$\mathfrak{L}_{1}$-Models. If
$\mathfrak{M}^{m}=(\mathfrak{L}_{1},\mathfrak{f}^{m})$ is equivalent with some
$F(\mathfrak{M}^{k})$, then we easily get
$\mathfrak{M}^{m}=F(\mathfrak{L}_{1},\mathfrak{f}^{k})$, for some
$\mathfrak{f}^{k}$, and hence $\mathfrak{f}^{m}=code(\mathfrak{f}^{k})$. Thus,
we have

$G(\mathfrak{M}^{m})=(\mathfrak{L}_{1},code(\mathfrak{f}^{k})\\!\\!\upharpoonright
n)=\sigma(\mathfrak{L}_{1},\mathfrak{f}^{k}).$

If $\mathfrak{f}^{m}\not=code(\mathfrak{f}^{k})$, for any $\mathfrak{f}^{k}$,
we could take $G(\mathfrak{M}^{m})=\sigma(\mathfrak{M}^{k})$, for any
$k$-model $\mathfrak{M}^{k}$ over $\mathfrak{L}_{1}$. We can even take the
same $\mathfrak{M}^{k}$, for each $\mathfrak{M}^{m}$. So, we choose some
$\mathfrak{s}^{k}$ and agree that, if $(\mathfrak{L}_{1},\mathfrak{f}^{m})$ is
not equivalent with any $F(\mathfrak{M}^{k})$, we have

$G(\mathfrak{M}^{m})=\sigma(\mathfrak{L}_{1},\mathfrak{s}^{k})=(\mathfrak{L}_{1},code(\mathfrak{s}^{k})\\!\\!\upharpoonright
n).$

$\mathfrak{F}_{2}$\- and $\mathfrak{L}_{2}$-Models. Let
$\mathfrak{M}^{m}=(\mathfrak{F}_{2},\\{\mathfrak{f}^{m}_{0},\mathfrak{f}^{m}_{0^{\prime}},\mathfrak{f}^{m}_{1}\\})$
be a p-irreducible $m$-model over $\mathfrak{F}_{2}$. Assume that
$\mathfrak{M}^{m}\thicksim F(\mathfrak{M}^{k})$, for some $\mathfrak{M}^{k}$.
Then $\mathfrak{M}^{m}\equiv F(\mathfrak{M}^{k})$ as the suffices $11$,$01$
and $00$ prevent any reduction of $F(\mathfrak{M}^{k})$, for any p-irreducible
$\mathfrak{M}^{k}$ of the depth $3$, to a model over $\mathfrak{F}_{2}$. Thus
$\mathfrak{M}^{k}=(\mathfrak{F}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{0^{\prime}},\mathfrak{f}^{k}_{1}\\})$,
and
$\mathfrak{f}^{m}_{0}=code(\mathfrak{f}^{k}_{0})=\mathfrak{f}^{n}_{0}\mathfrak{g}^{n}_{1}\mathfrak{h}^{n}_{1}\dots\mathfrak{g}^{n}_{2^{n}}\mathfrak{h}^{n}_{2^{n}}11$,
and
$\mathfrak{f}^{m}_{0^{\prime}}=code(\mathfrak{f}^{k}_{0^{\prime}})=\mathfrak{f}^{n}_{0^{\prime}}\mathfrak{g^{\prime}}^{n}_{1}\mathfrak{h^{\prime}}^{n}_{1}\dots\mathfrak{g^{\prime}}^{n}_{2^{n}}\mathfrak{h^{\prime}}^{n}_{2^{n}}11$,
and $\mathfrak{f}^{m}_{1}=\mathfrak{f}_{1}^{n}0\cdots 01$ where
$\sigma(\mathfrak{M}^{k})=(\mathfrak{F}_{2},\\{\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{0^{\prime}},\mathfrak{f}^{n}_{1}\\})=G(\mathfrak{M}^{m})$.
By the definition of $code()$, see the Figure 20, the pair
$\mathfrak{f}^{n}_{0}\mathfrak{f}^{n}_{1}$ must occur in
$code(\mathfrak{f}^{k}_{0^{\prime}})$ and
$\mathfrak{f}^{n}_{0^{\prime}}\mathfrak{f}^{n}_{1}$ in
$code(\mathfrak{f}^{k}_{0})$. We would like to preserve this condition even if
$\mathfrak{M}^{m}$ is not equivalent with any $F(\mathfrak{M}^{k})$.

Let $\mathfrak{M}^{m}$ be not equivalent with any $F(\mathfrak{M}^{k})$. We
have
$G(\mathfrak{L}_{1},\mathfrak{f}^{m}_{0})=\sigma(\mathfrak{L}_{1},\mathfrak{f}^{k}_{0})=(\mathfrak{L}_{1},\mathfrak{f}^{n}_{0})$
and
$G(\mathfrak{L}_{1},\mathfrak{f}^{m}_{0^{\prime}})=\sigma(\mathfrak{L}_{1},\\{\mathfrak{f}^{k}_{0^{\prime}}\\})=(\mathfrak{L}_{1},\mathfrak{f}^{n}_{0^{\prime}})$,
for some $\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{0^{\prime}}$ and some
$\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{0^{\prime}}$. Take any
$\mathfrak{f}^{k}_{1}$ such that
$(\mathfrak{F}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{0^{\prime}},\mathfrak{f}^{k}_{1}\\})$
is an intuitionistic model and define

$G(\mathfrak{M}^{m})=\sigma((\mathfrak{F}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{0^{\prime}},\mathfrak{f}^{k}_{1}\\})=(\mathfrak{F}_{2},\\{\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{0^{\prime}},\mathfrak{f}^{n}_{1}\\}),\quad\mbox{for
some }\mathfrak{f}^{n}_{1}.$

We obviously have $\mathfrak{f}^{n}_{0}\mathfrak{f}^{n}_{1}$ in
$code(\mathfrak{f}^{k}_{0^{\prime}})$ and
$\mathfrak{f}^{n}_{0^{\prime}}\mathfrak{f}^{n}_{1}$ in
$code(\mathfrak{f}^{k}_{0})$. For the choice of $\mathfrak{f}^{k}_{1}$, use
the lexicographical order which would also be sufficient to satisfy the
condition (iii) of Theorem 23 saying that isomorphic models have isomorphic
images.

Let
$\mathfrak{M}^{m}=(\mathfrak{L}_{2},\\{\mathfrak{f}^{m}_{0},\mathfrak{f}^{m}_{1}\\})$
be a p-irreducible $m$-model over $\mathfrak{L}_{2}$ and
$\mathfrak{M}^{m}\thicksim F(\mathfrak{M}^{k})$, for some $\mathfrak{M}^{k}$.
We have two possibilities: either $\mathfrak{M}^{k}$ is a model over
$\mathfrak{L}_{2}$ or it is a model over $\mathfrak{F}_{2}$. In the first
case,
$G(\mathfrak{M}^{m})=\sigma(\mathfrak{M}^{k})=\sigma(\mathfrak{L}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{1}\\})=(\mathfrak{L}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{1}\\})$,
for some
$\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{1},\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{1}$,
and $\mathfrak{f}^{m}_{0}=code(\mathfrak{f}^{k}_{0})$. It is clear that
$\mathfrak{f}^{n}_{0}\mathfrak{f}^{n}_{1}$ occurs in
$code(\mathfrak{f}^{k}_{0})$. The second possibilities is worse. We have
$\mathfrak{M}^{k}=(\mathfrak{F}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{0^{\prime}},\mathfrak{f}^{k}_{1}\\})$
and
$\mathfrak{f}^{m}_{0}=code(\mathfrak{f}^{k}_{0})=code(\mathfrak{f}^{k}_{0^{\prime}})$
(which does not yield $\mathfrak{f}^{k}_{0}=\mathfrak{f}^{k}_{0^{\prime}}$).
Since
$\sigma(\mathfrak{M}^{k})=(\mathfrak{F}_{2},\\{\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{0^{\prime}},\mathfrak{f}^{n}_{1}\\})$
and $\mathfrak{f}^{n}_{0}=\mathfrak{f}^{n}_{0^{\prime}}$, we take
$G(\mathfrak{M}^{m})=(\mathfrak{L}_{2},\\{\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{1}\\})=\mathfrak{M}^{m}\\!\\!\upharpoonright
n\thicksim\sigma(\mathfrak{M}^{k})$ and have
$\mathfrak{f}^{n}_{0}\mathfrak{f}^{n}_{1}$ in $code(\mathfrak{f}^{k}_{0})$.

Suppose that
$\mathfrak{M}^{m}=(\mathfrak{L}_{2},\\{\mathfrak{f}^{m}_{0},\mathfrak{f}^{m}_{1}\\})$
is not equivalent with any $F(\mathfrak{M}^{k})$. Then
$G(\mathfrak{L}_{1},\mathfrak{f}^{m}_{0})=\sigma(\mathfrak{L}_{1},\mathfrak{f}^{k}_{0})=(\mathfrak{L}_{1},\mathfrak{f}^{n}_{0}),$
for some $\mathfrak{f}^{k}_{0},\mathfrak{f}^{n}_{0}$. Let us take any
$k$-valuation $\mathfrak{f}^{k}_{1}$ such that
$(\mathfrak{L}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{1}\\})$ is an
intuitionistic model and define
$G(\mathfrak{M}^{m})=\sigma((\mathfrak{L}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{1}\\})=(\mathfrak{L}_{2},\\{\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{1}\\}),\quad\mbox{for
some }\mathfrak{f}^{n}_{1}.$ We obviously have
$\mathfrak{f}^{n}_{0}\mathfrak{f}^{n}_{1}$ in $code(\mathfrak{f}^{k}_{0})$.

$\mathfrak{C}_{5}$\- and $\mathfrak{Y}_{3}$-Models. Let $\mathfrak{M}^{m}$ be
a p-irreducible model over $\mathfrak{C}_{5}$ (or over $\mathfrak{Y}_{3}$) and
assume it is not equivalent with any $F(\mathfrak{M}^{k})$. We have (see
Figure 21-23)
$G((\mathfrak{M}^{m})_{1})\thicksim\sigma(\mathfrak{M}^{k})=(\mathfrak{F}_{2},\\{\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{0^{\prime}},\mathfrak{f}^{n}_{1}\\})$,
and
$G((\mathfrak{M}^{m})_{1^{\prime}})\thicksim\sigma(\mathfrak{M^{\prime}}^{k})=(\mathfrak{F}_{2},\\{\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{0^{\prime\prime}},\mathfrak{f}^{n}_{1^{\prime}}\\})$
(or
$\sigma(\mathfrak{M^{\prime}}^{k})=(\mathfrak{F}_{2},\\{\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{0^{\prime}},\mathfrak{f}^{n}_{1^{\prime}}\\})$)
for some
$\mathfrak{M}^{k}=(\mathfrak{F}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{0^{\prime\prime}},\mathfrak{f}^{k}_{1^{\prime}}\\})$
and
$\mathfrak{M^{\prime}}^{k}=(\mathfrak{F}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{0^{\prime\prime}},\mathfrak{f}^{k}_{1^{\prime}}\\})$
(or
$(\mathfrak{F}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{0^{\prime}},\mathfrak{f}^{k}_{1^{\prime}}\\})$),
which are $k$-model over $\mathfrak{F}_{2}$. We have
$\mathfrak{f}^{n}_{0^{\prime}}\mathfrak{f}^{n}_{1^{\prime}}$ and
$\mathfrak{f}^{n}_{0^{\prime\prime}}\mathfrak{f}^{n}_{1}$ (or
$\mathfrak{f}^{n}_{0^{\prime}}\mathfrak{f}^{n}_{1}$) in
$code(\mathfrak{f}^{k}_{0})$ (see Figure 20). Then, for some
$\mathfrak{g}^{k}_{1},\mathfrak{h}^{k}_{1},\mathfrak{g}^{k}_{2},\mathfrak{h}^{k}_{2}$,
we can define $\mathfrak{C}_{5}$-models such that

$\sigma\Bigl{(}$$0\cdots
0$$\mathfrak{h}^{k}_{1}$$\mathfrak{g}^{k}_{1}$$\mathfrak{h}^{k}_{2}$$\mathfrak{f}^{k}_{0}$$\mathfrak{g}^{k}_{2}$$\Bigr{)}\quad=$$\mathfrak{f}^{n}_{2}$$\mathfrak{f}^{n}_{1}$
, for some
$\mathfrak{f}_{2}^{n}$.$\mathfrak{f}^{n}_{0^{\prime}}$$\mathfrak{f}^{n}_{1^{\prime}}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{0^{\prime\prime}}\
(\mbox{or}\ \mathfrak{f}^{n}_{0^{\prime}})$
Fig. 24:

The last $n$-model over $\mathfrak{C}_{5}$ can be taken as
$G(\mathfrak{M}^{m})$. In the case of $\mathfrak{Y}_{3}$ we have
$\mathfrak{f}^{n}_{0^{\prime}}=\mathfrak{f}^{n}_{0^{\prime\prime}}$ and we can
reduce the $\mathfrak{C}_{5}$-model to a $\mathfrak{Y}_{3}$-model taking
$0^{\prime}=0^{\prime\prime}$.

$\mathfrak{R}_{2}$\- and $\mathfrak{Y}_{2}$-Models. Let $\mathfrak{M}^{m}$ be
a p-irreducible model over $\mathfrak{R}_{2}$ and assume it is not equivalent
with any $F(\mathfrak{M}^{k})$. By our inductive hypothesis, we have (see
Figure 21-23)
$G((\mathfrak{M}^{m})_{1})\thicksim\sigma(\mathfrak{M}^{k})=(\mathfrak{F}_{2},\\{\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{0^{\prime}},\mathfrak{f}^{n}_{1^{\prime}}\\})$,
$G((\mathfrak{M}^{m})_{1^{\prime}})\thicksim\sigma(\mathfrak{M^{\prime}}^{k})=(\mathfrak{F}_{2},\\{\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{0^{\prime\prime}},\mathfrak{f}^{n}_{1}\\})$;
for some
$\mathfrak{M}^{k}=(\mathfrak{F}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{0^{\prime}},\mathfrak{f}^{k}_{1^{\prime}}\\})$
and
$\mathfrak{M^{\prime}}^{k}=(\mathfrak{F}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{0^{\prime\prime}},\mathfrak{f}^{k}_{1}\\})$.
We have
$\mathfrak{f}^{n}_{0^{\prime}}=\mathfrak{f}^{n}_{0}=\mathfrak{f}^{n}_{0^{\prime\prime}}$
and $\mathfrak{f}^{n}_{0}\mathfrak{f}^{n}_{1^{\prime}}$,
$\mathfrak{f}^{n}_{0}\mathfrak{f}^{n}_{1}$ occur in
$code(\mathfrak{f}^{k}_{0})$ (see Figure 20). Then for some
$\mathfrak{g}^{k}_{1},\mathfrak{h}^{k}_{1},\mathfrak{g}^{k}_{2},\mathfrak{h}^{k}_{2},\mathfrak{f}_{2}^{n}$

$\sigma\Bigl{(}$$0\cdots
0$$\mathfrak{h}^{k}_{1}$$\mathfrak{g}^{k}_{1}$$\mathfrak{h}^{k}_{2}$$\mathfrak{f}^{k}_{0}$$\mathfrak{g}^{k}_{2}$$\Bigr{)}\quad=$$\mathfrak{f}^{n}_{2}$$\thicksim$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{0^{\prime}}$$\mathfrak{f}^{n}_{1^{\prime}}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{0^{\prime\prime}}$$\mathfrak{f}^{n}_{2}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{1^{\prime}}$$\mathfrak{f}^{n}_{0}$
Fig. 25:

The received $n$-model over $\mathfrak{R}_{2}$ can be taken as
$G(\mathfrak{M}^{m})$. A similar argument (as we used above for
$\mathfrak{R}_{2}$-models) applies for models over $\mathfrak{Y}_{2}$.

$+\mathfrak{F}_{2}$\- and $\mathfrak{L}_{3}$-Models. Let $\mathfrak{M}^{m}$ be
a p-irreducible model over $\mathfrak{L}_{3}$, or over $+\mathfrak{F}_{2}$,
and assume that it is not equivalent with any $F(\mathfrak{M}^{k})$. We can
also assume $G((\mathfrak{M}^{m})_{1})$ has been defined (see Figure 21-23).
If $G((\mathfrak{M}^{m})_{1})=\sigma(\mathfrak{M}^{k})$, for some
$\mathfrak{M}^{k}$, then $\mathfrak{M}^{k}$ is a model over
$\mathfrak{L}_{2}$, or over $\mathfrak{F}_{2}$, and we can take
$G(\mathfrak{M}^{m})=\sigma(\mathfrak{N}^{k})$ where $\mathfrak{N}^{k}$ is an
extension of $\mathfrak{M}^{k}$ with any $k$-valuation $\mathfrak{f}^{k}_{2}$
(the extended model must be an intuitionistic model). Then $\mathfrak{N}^{k}$
is a model over $\mathfrak{L}_{3}$, or over $+\mathfrak{F}_{2}$, as required.
The only problem rises if $G((\mathfrak{M}^{m})_{1})$ is equivalent with some
$\sigma(\mathfrak{M}^{k})$ but it is not any $\sigma$-model. This can happen
if $(\mathfrak{M}^{m})_{1}$ is a model over $\mathfrak{L}_{2}$ and
$\mathfrak{M}^{k}$ over $\mathfrak{F}_{2}$. Then extending $\mathfrak{M}^{k}$
with $\mathfrak{f}^{k}_{2}$ we get a model $\mathfrak{N}^{k}$ over
$+\mathfrak{F}_{2}$ such that $\sigma(\mathfrak{N}^{k})$ is equivalent with an
extension of $G((\mathfrak{M}^{m})_{1})$ to a model over $\mathfrak{L}_{3}$;
and the model over $\mathfrak{L}_{3}$ is $G(\mathfrak{M}^{m})$.

###  4.3 Projective Formulas in Locally Tabular Logics.

Projective formulas are useful in the area of unification. By Ghilardi [14],
any consistent Rasiowa-Harrop formula (e.g. $\neg B$) is projective in INT
and, consequently, in any intermediate logic, see Lemma 3. One can easily
produce other examples of projective formulas. Although conjunctions of
projective formulas may be not projective, for instance $(x_{1}\rightarrow
x_{2}\lor x_{3})\land x_{1}$ is not, we have

###### Lemma 14

If $A=\bigwedge_{i=1}^{s}(B_{i}\leftrightarrow z_{i})$ for some distinct
variables $z_{1},\dots,z_{s}$ which do not occur in the formulas
$B_{1},\dots,B_{s}$, where $s\geq 1$, then $A$ is projective in INT.

  * Proof.

Note that $\varepsilon\colon z_{1}/B_{1}\cdots z_{s}/B_{s}$ is a projective
unifier for $A$.

For locally tabular logics, we can show

###### Theorem 26

Let $\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$ and
$\varepsilon\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{n}$, for some
$k,n\geq 0$. Then $\varepsilon$ is a projective unifier for $A_{\sigma}$ in
the logic L if and only if
(iv) for every $\mathfrak{M}^{n}\in\mathbf{M}^{n}$ there is a
$\mathfrak{M}^{k}\in\mathbf{M}^{k}$ such that
$\varepsilon(\mathfrak{M}^{n})\thicksim\sigma(\mathfrak{M}^{k})$;
(v) $\varepsilon(\sigma(\mathfrak{M}^{k}))\thicksim\sigma(\mathfrak{M}^{k})$,
for every $\mathfrak{M}^{k}\in\mathbf{M}^{k}$, see Figure 26.

$\mathbf{M}^{k}\\!/\\!\\!\thicksim$$\mathbf{M}^{n}\\!/\\!\\!\thicksim$$\mathbf{M}^{n}\\!/\\!\\!\thicksim$$\sigma$$\varepsilon$$\sigma$
Fig. 26: Projective Unifiers

  * Proof.

Assume (iv) and (v). Then $\varepsilon$ is a unifier for $A_{\sigma}$, by
Corollary 9. We need to show
$A_{\sigma}\vdash\varepsilon(x_{i})\leftrightarrow x_{i}$, for each $i$. Let
$\mathfrak{M}^{k}$ be any $k$-model. Then
$\varepsilon(\sigma(\mathfrak{M}^{k}))\thicksim\sigma(\mathfrak{M}^{k})$ by
(v). Hence, see Lemma 7, we get

$\sigma(\mathfrak{M}^{k})\Vdash\varepsilon(x_{i})\ \Leftrightarrow\
\varepsilon(\sigma(\mathfrak{M}^{k}))\Vdash x_{i}\ \Leftrightarrow\
\sigma(\mathfrak{M}^{k})\Vdash x_{i}.$

By Lemma 7, $\sigma$ is a unifier for $\varepsilon(x_{i})\leftrightarrow
x_{i}$ and , by Corollary 8,
$A_{\sigma}\vdash\varepsilon(x_{i})\leftrightarrow x_{i}$.

If $\varepsilon$ is a projective unifier for $A_{\sigma}$, we get (iv) and (v)
using Lemma 12 and 2.

###### Corollary 10

A substitution $\varepsilon\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{n}$ is
a projective unifier for $A_{\varepsilon}$ in L iff
$\varepsilon\circ\varepsilon=_{\mathsf{L}}\varepsilon$.

###### Corollary 11

If $\varepsilon\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{n}$ is an
L-projective unifier for a formula $A\in\mathsf{Fm^{n}}$, then $A=_{\sf
L}\bigwedge_{i=1}^{n}\bigl{(}x_{i}\leftrightarrow\varepsilon(x_{i})\bigr{)}.$

Suppose that $m=n$ and $F=H_{\sigma}$ in Theorem 22. Then, by (iv) and (v),
$G$ would generate a retraction from $\mathbf{M}^{n}\\!/\\!\\!\thicksim$ onto
$\sigma(\mathbf{M}^{k})/\\!\\!\thicksim$. This simplified version of Theorem
22 characterizes logics with projective approximation (see Theorem 8).

###### Theorem 27

The logic L has projective approximation iff for every
$\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$, where $n,k\geq 0$,
there is a mapping $G:\mathbf{M}^{n}\to\mathbf{M}^{n}$ such that:
(i) $G$ preserves the frame of any $n$-model
$\mathfrak{M}^{n}=(W,R,w_{0},V^{n})$;
(ii) $G((\mathfrak{M}^{n})_{w})\thicksim(G(\mathfrak{M}^{n}))_{w},\mbox{ for
every }\quad w\in W;$
(iii) $\mathfrak{N}^{n}\thicksim\mathfrak{M}^{n}\quad\Rightarrow\quad
G(\mathfrak{N}^{n})\thicksim G(\mathfrak{M}^{n}),\quad\mbox{ for every
}\quad\mathfrak{M}^{n},\mathfrak{N}^{n}\in\mathbf{M}^{n}$;
(iv) for every $n$-model $\mathfrak{M}^{n}$, there is a $k$-model
$\mathfrak{M}^{k}$ such that
$G(\mathfrak{M}^{n})\thicksim\sigma(\mathfrak{M}^{k})$;
(v) for every $k$-model $\mathfrak{M}^{k}$, we have
$G(\sigma(\mathfrak{M}^{k}))\thicksim\sigma(\mathfrak{M}^{k})$.

  * Proof.

Suppose that L has projective approximation and let
$\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$, for $k,n\geq 0$. By
Corollary 8, $\sigma$ is a unifier for $A_{\sigma}\in\mathsf{Fm}^{n}$. Let
$B\in\Pi(A_{\sigma})$ be a projective formula in $\mathsf{Fm}^{n}$ such that
$B\vdash_{\mathsf{L}}A_{\sigma}$ and $\vdash_{\mathsf{L}}\sigma(B)$. If
$\varepsilon\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{n}$ is a projective
unifier for $B$, then $\sigma\circ\varepsilon=_{\mathsf{L}}\sigma$ and
$\vdash_{\mathsf{L}}\varepsilon(A_{\sigma})$, by Lemma 2. Thus, if one takes
$G=H_{\varepsilon}$, one easily shows (i)-(v) using Lemma 12 and Corollary 13.

Assume (i)-(v) and let $\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$
be a unifier for a formula $A\in\mathsf{Fm}^{n}$. By Lemma 20, we have
$G\thicksim H_{\varepsilon}$ for some
$\varepsilon\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{n}$. Then, by Lemma
26, $\varepsilon$ is a projective unifier for $A_{\sigma}$. Thus, we have
$A_{\sigma}$ projective, and $A_{\sigma}\vdash A$, and
$A_{\sigma}\in\mathsf{Fm}^{n}$, and $\sigma$ is a unifier for $A_{\sigma}$.
For each $A$ one can define $\Pi(A)$ so that to show projective approximation
in L.

In [10], using the above Theorem, we have shown that any logic determined by
frames of the depth $\leq 2$ has projective approximation. Thus,
L($\mathfrak{F}_{m}$) for any $m$-fork $\mathfrak{F}_{m}$ (see Figure 4) has
finitary unification. Now we extend this result to the logic determined by all
frames from $\mathbf{H}_{pr}$ (that is frames
$\mathfrak{L}_{d}+\mathfrak{F}_{m}$ , where $m,d\geq 0$, see Figure 7). The
logic L($\mathbf{H}_{pa}$) extends PWL, see [11], hence it is locally tabular.

###### Theorem 28

For any $\mathbf{F}\subseteq\mathbf{H}_{pr}$, the logic L($\mathbf{F}$) has
projective approximation.

  * Proof.

Let $\mathbf{F}\subseteq\mathbf{H}_{pr}$. Since $\mathbf{H}_{pr}$ is closed on
p-morphic images and generated subframes, we can assume sm(F)=F; see Lemma 10.
For any $\sigma\colon\\{x_{1},\dots,x_{n}\\}\to\mathsf{Fm}^{k}$, where $k\geq
0$, we need $G\colon\mathbf{M}^{n}\to\mathbf{M}^{n}$ fulfilling (i)-(v).

A. If $\mathfrak{M}^{n}=(W,R,w_{0},V^{n})\in\mathbf{M}^{n}$ is equivalent with
a $\sigma$-model (i.e. $\mathfrak{M}^{n}\thicksim\sigma(\mathfrak{M}^{k})$,
for some $\mathfrak{M}^{k}$), we take $G(\mathfrak{M}^{n})=\mathfrak{M}^{n}$.
Then (i),(iv) and (v) are obvious.

(ii) If $\mathfrak{M}^{n}$ is equivalent with a $\sigma$-model, then so is
$(\mathfrak{M}^{n})_{w}$, for any $w\in W$ (see Corollary 7 and Lemma 8(iii),
and hence
$G((\mathfrak{M}^{n})_{w})=(\mathfrak{M}^{n})_{w}=(G(\mathfrak{M}^{n}))_{w}$.

(iii) If $\mathfrak{M}^{n}$ is equivalent with a $\sigma$-model and
$\mathfrak{M}^{n}\thicksim\mathfrak{N}^{n}$, then $\mathfrak{N}^{n}$ is
equivalent with the same $\sigma$-model and hence
$G(\mathfrak{M}^{n})=\mathfrak{M}^{n}\thicksim\mathfrak{N}^{n}=G(\mathfrak{N}^{n})$.

B. Suppose that $\mathfrak{M}^{n}$ is not equivalent with any $\sigma$-model.
Assume $\mathfrak{M}^{n}$ is p-irreducible and define $G(\mathfrak{M}^{n})$
inductively with respect to the depth of $\mathfrak{M}^{n}$. We could not
bother about (v) as it is irrelevant, our inductive approach secure (ii) and
(iii), see Theorem 21. Our task is to preserve (i) and (iv), that is
$G(\mathfrak{M}^{n})$ should be defined over the frame of $\mathfrak{M}^{n}$
and $G(\mathfrak{M}^{n})$ should be equivalent with some $\sigma$-model.

B1. Let $\mathfrak{M}^{n}$ be an $n$-model over 1-element chain
$\mathfrak{L}_{1}$, that is
$\mathfrak{M}^{n}=(\mathfrak{L}_{1},\mathfrak{f}^{n})$ where
$\mathfrak{f}^{n}=i_{1}\dots i_{n}$ with $i_{j}\in\\{0,1\\}$. All $n$-models
over $\mathfrak{L}_{1}$ are p-irreducible and we have (see [10]): any
$n$-model over $\mathfrak{L}_{1}$ equivalent with some $\sigma$-model is a
$\sigma$-model. We can take any $k$-model
$\mathfrak{M}^{k}=(\mathfrak{L}_{1},\mathfrak{f}^{k})$ over $\mathfrak{L}_{1}$
and define $G(\mathfrak{M}^{n})=\sigma(\mathfrak{M}^{k}).$

B2. Let $\mathfrak{M}^{n}$ be an $n$-model over $m$-fork $\mathfrak{F}_{m}$,
see Figure 27, for $m\geq 1$;

$\cdots$$m$$0$$1$$2$$(m-1)$$3$ Fig. 27: $m$-Fork

By our inductive approach,
$G((\mathfrak{M}^{n})_{i})=(\mathfrak{L}_{1},\mathfrak{g}^{n}_{i})=\sigma(\mathfrak{L}_{1},\mathfrak{f}^{k}_{i})$,
for some $\mathfrak{g}^{n}_{i}$ and $\mathfrak{f}^{k}_{i}$, if $i<m$. We
define $\mathfrak{M}^{k}$, see Figure 28, and put
$G(\mathfrak{M}^{n})=\sigma(\mathfrak{M}^{k}).$

$\cdots$$\mathfrak{f}^{n}_{m}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{m-1}$$\mathfrak{f}^{n}_{2}$$G$$\mathfrak{M}^{n}=$$\cdots$$?$$\mathfrak{g}^{n}_{0}$$\mathfrak{g}^{n}_{1}$$\mathfrak{g}^{n}_{m-1}$$\mathfrak{g}^{n}_{2}$$\sigma$$\cdots$$0\cdots
0$$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{1}$$\mathfrak{f}^{k}_{m-1}$$\mathfrak{f}^{k}_{2}$$=\mathfrak{M}^{k}$
Fig. 28:

We should be more careful about defining the mapping $G$ on isomorphic
$n$-models. Our mapping should be factorized by $\equiv$ and hence we should
get the factorized mapping
$G\colon\mathbf{M}^{n}_{ir}/\\!\\!\equiv\to\mathbf{M}^{n}/\\!\\!\equiv$. Thus,
from any $\equiv$-class, we take only one $\mathfrak{M}^{n}$, define as above
$G(\mathfrak{M}^{n})$ and then extend $G$, on other members of the equivalence
class, taking as the values for $G$ the appropriate isomorphic copy of
$G(\mathfrak{M}^{n})$.

B3. Eventually, suppose that the frame of $\mathfrak{M}^{n}$ is an $m$-fork
extended with an $d$-element chain ’leg‘, where $m,d\geq 0$. Our subsequent
definition of $G$ is inductive with respect to $d$. So, we assume that $d\geq
1$ and $G((\mathfrak{M}^{n})_{m+d-1})$ has already been defined, see Figure
29. We define $G(\mathfrak{M}^{n})$ extending $G((\mathfrak{M}^{n})_{m+d-1})$
with $\mathfrak{g}^{n}_{m+d}=\mathfrak{g}^{n}_{m+d-1}$. So, we get
$G(\mathfrak{M}^{n})\thicksim G((\mathfrak{M}^{n})_{m+d-1})$ which guarantees
the condition (iv).

$\cdots$$\mathfrak{f}^{n}_{m}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{m-1}$$\mathfrak{f}^{n}_{2}$$\mathfrak{M}^{n}=$$\mathfrak{f}^{n}_{m+1}$$\mathfrak{f}^{n}_{m+d-1}$$\mathfrak{f}^{n}_{m+d}$$G((\mathfrak{M}^{n})_{m+d-1})=$$\cdots$$\mathfrak{g}^{n}_{m}$$\mathfrak{g}^{n}_{0}$$\mathfrak{g}^{n}_{1}$$\mathfrak{g}^{n}_{m-1}$$\mathfrak{g}^{n}_{2}$$\mathfrak{g}^{n}_{m+1}$$\mathfrak{g}^{n}_{m+d-1}$$\cdots$$\mathfrak{g}^{n}_{m}$$\mathfrak{g}^{n}_{0}$$\mathfrak{g}^{n}_{1}$$\mathfrak{g}^{n}_{m-1}$$\mathfrak{g}^{n}_{2}$$G(\mathfrak{M}^{n})=$$\mathfrak{g}^{n}_{m+1}$$\mathfrak{g}^{n}_{m+d-1}$$\mathfrak{g}^{n}_{m+d}=\mathfrak{g}^{n}_{m+d-1}$
Fig. 29:

So, we have $G\colon\mathbf{M}^{n}_{ir}\to\mathbf{M}^{n}$. Using Theorem 21,
we extend the mapping to $G\colon\mathbf{M}^{n}\to\mathbf{M}^{n}$ preserving
the conditions (i)-(iii), see Lemma 8. It is an easy task to check that the
conditions (iv) and (v) are also preserved by the extension.

Theorems 22 and 27 can also be used to show that certain locally tabular
logics neither have finitary/unitary unification, nor projective
approximation. Many examples follow in the next section. Here we only give

###### Theorem 29

The logics ${\mathsf{L}}(\mathfrak{G}_{2})$ and
${\mathsf{L}}(\mathfrak{G}_{2})\cap{\mathsf{L}}(\mathfrak{C}_{5})$ (see Figure
1 and 6) have finitary unification but they do not have projective
approximation.

  * Proof.

Let us prove
${\mathsf{L}}(\mathfrak{G}_{2})\cap{\mathsf{L}}(\mathfrak{C}_{5})$ has
finitary unification. We extend the family F (in our proof of Theorem 25) with
the frames $\mathfrak{G}_{2}$ and $\mathfrak{G}_{3}$. The definition of $F$,
see Figure 21-23, needs the following two (additional) clauses:

$\mathfrak{f}^{k}_{2}$$\mathfrak{f}^{k}_{0^{\prime}}$$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{1}$$\sigma\Bigl{(}$$\Bigr{)}\
=$$\mathfrak{M}^{k}=$$\mathfrak{f}^{n}_{2}$$\mathfrak{f}^{n}_{0^{\prime}}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{1}$$F(\mathfrak{M}^{k})\
=$$\mathfrak{f}^{n}_{1}0\cdots 01$$\mathfrak{f}^{n}_{2}0\cdots
0$$code(\mathfrak{f}^{k}_{0^{\prime}})$$code(\mathfrak{f}^{k}_{0})$

$\mathfrak{f}^{k}_{2}$$\mathfrak{f}^{k}_{0^{\prime\prime}}$$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{1}$$\sigma\Bigl{(}$$\Bigr{)}\
=$$\mathfrak{f}^{k}_{0^{\prime}}$$\mathfrak{f}^{n}_{2}$$\mathfrak{f}^{n}_{0^{\prime\prime}}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{0^{\prime}}$$F(\mathfrak{M}^{k})\
=$$code(\mathfrak{f}^{k}_{0^{\prime}})$$\mathfrak{f}^{n}_{1}0\cdots
01$$\mathfrak{f}^{n}_{2}0\cdots
0$$code(\mathfrak{f}^{k}_{0^{\prime\prime}})$$code(\mathfrak{f}^{k}_{0})$

Fig. 30:

Then we need to extend the definition of $G(\mathfrak{M}^{m})$ with:

$\mathfrak{G}_{2}$\- and $\mathfrak{G}_{2}$-models. We only deal with the
worst case. Suppose that
$\mathfrak{M}^{m}=(\mathfrak{G}_{3},\\{\mathfrak{f}^{m}_{0},\mathfrak{f}^{m}_{0^{\prime}},\mathfrak{f}^{m}_{1},\mathfrak{f}^{m}_{2}\\})$
is a p-irreducible model over $\mathfrak{G}_{3}$ (see Figure 30) non-
equivalent with any $F(\mathfrak{M}^{k})$, but
$(\mathfrak{M}^{m})_{1}\thicksim F(\mathfrak{M}^{k})$, where
$\mathfrak{M}^{k}$ is a model over $\mathfrak{F}_{2}$. Then
$(\mathfrak{M}^{m})_{1}\\!\\!\upharpoonright
n=(\mathfrak{L}_{2},\\{\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{1}\\})\thicksim\sigma(\mathfrak{M}^{k})$
for some $\mathfrak{f}^{n}_{0},\mathfrak{f}^{n}_{1}$ where $\thicksim$ cannot
be replaced with $=$. Let
$\mathfrak{M}^{k}=(\mathfrak{F}_{2},\\{\mathfrak{f}^{k}_{0},\mathfrak{f}^{k}_{0^{\prime}},\mathfrak{f}^{k}_{1}\\})$
which means
$\sigma(\mathfrak{L}_{1},\mathfrak{f}^{k}_{0})=\sigma(\mathfrak{L}_{1},\mathfrak{f}^{k}_{0^{\prime}})=(\mathfrak{L}_{1},\mathfrak{f}^{n}_{0})$
and let
$G((\mathfrak{M}^{m})_{0^{\prime}})=\sigma(\mathfrak{L}_{1},\mathfrak{g}^{k}_{0})=(\mathfrak{L}_{1},\mathfrak{f}^{n}_{0^{\prime}}),$
for some $\mathfrak{g}^{k}_{0},\mathfrak{f}^{n}_{0^{\prime}}$. Then, for some
$\mathfrak{f}^{n}_{2}$, we have

$\thicksim$$\mathfrak{f}^{n}_{2}$$\mathfrak{f}^{n}_{0^{\prime}}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{2}$$\mathfrak{f}^{n}_{0^{\prime}}$$\mathfrak{f}^{n}_{0}$$\mathfrak{f}^{n}_{1}$$\mathfrak{f}^{n}_{0}$$\sigma\Bigl{(}$$\mathfrak{f}^{k}_{2}$$\mathfrak{g}^{k}_{0}$$\mathfrak{f}^{k}_{0}$$\mathfrak{f}^{k}_{1}$$\mathfrak{f}^{k}_{0^{\prime}}$$\Bigr{)}\quad=$
Fig. 31:

and the $n$-model over $\mathfrak{G}_{3}$ may be $G(\mathfrak{M}^{m})$; it is
equivalent with a $\sigma$-model over $\mathfrak{G}_{2}$.191919The problem
would rise if we tried in the same way show ${\mathsf{L}}(\mathfrak{G}_{3})$
is finitary, we have no $\sigma$-model over $\mathfrak{G}_{3}$ equivalent with
$G(\mathfrak{M}^{m})$. So, ${\mathsf{L}}(\mathfrak{G}_{3})$ is nullary and the
above may be seen as Ghilardi’s Theorem 9, p.112, [17]. The rest of the proof
remains the same.

In the same way one shows ${\mathsf{L}}(\mathfrak{G}_{2})$ has finitary
unification; from the proof that
${\mathsf{L}}(\mathfrak{G}_{2})\cap{\mathsf{L}}(\mathfrak{C}_{5})$ has
finitary unification, it suffices to remove
$\mathfrak{C}_{5},\mathfrak{R}_{2},\mathfrak{Y}_{2}$ and $\mathfrak{Y}_{3}$.
Then we can even simplify our reasoning and delate
$\mathfrak{g}^{n}_{1}\mathfrak{h}^{n}_{1}\dots\mathfrak{g}^{n}_{2^{n}}\mathfrak{h}^{n}_{2^{n}}$
from $code(\mathfrak{f}^{k})$. Thus, we can take $m=n+2$ and define
$F(\mathfrak{M}^{k})$ using $m$-valuations $\mathfrak{f}^{n}11$,
$\mathfrak{f}^{n}01$, or $\mathfrak{f}^{n}00$. The suffices $11$, $01$ and
$00$ are necessary.202020Using them we avoid problems that could rise
p-morphisms mentioned in Example 3, the first counterexample. For the second
type of p-morphisms, mentioned in the Example, we have no such remedia. The
whole proof is to be shown that for these particular frames we can deal
somehow with p-morphims which collapse $\mathfrak{F}_{2}$ onto
$\mathfrak{L}_{2}$.

We need to show that ${\mathsf{L}}(\mathfrak{G}_{2})$ does not have projective
approximation. Consider the substitution
$\sigma\colon\\{x_{1}\\}\to\mathsf{Fm}^{2}$ such that $\sigma(x_{1})=\neg\neg
x_{1}\land\bigl{(}x_{2}\lor(x_{2}\to x_{1}\lor\neg x_{1})\bigr{)}.$ Any
$\sigma$-model is equivalent with one of the 1-models:

$1$$0$$0$$1$$0$$0$$1$$0$$1$$1$$1$$1$$\thicksim$ Fig. 32:

The above model over $\mathfrak{L}_{2}$ is not a $\sigma$-model but is
equivalent with some $\sigma$-model over $\mathfrak{G}_{2}$. Suppose
${\mathsf{L}}(\mathfrak{G}_{2})$ has projective approximation and let
$G\colon\mathbf{M}^{1}\to\mathbf{M}^{1}$ be the retraction given by Theorem
27. We have $G(\circ\ 0)=\circ\ 0$ and $G(\circ\ 1)=\circ\ 1$. But if

$G\bigl{(}$$0$$1$$\bigr{)}=$

$0$$1$, then

$G\Bigl{(}$

$0$$0$$1$$0$$1$$\Bigr{)}\ =$

$0$$0$$1$$0$$1$

which cannot happen as the last model is not equivalent to any model in Figure
32. Thus, we get a contradiction.

In the same way one shows
${\mathsf{L}}(\mathfrak{G}_{2})\cap{\mathsf{L}}(\mathfrak{C}_{5})$ does not
have projective approximation.

We can also show that ${\mathsf{L}}(\mathfrak{G}_{1})$ (see Figure 1) has
finitary unification; it suffices only to extend the above reasoning admitting
the frames $\mathfrak{G}_{1},\mathfrak{G}_{3\mathfrak{L}_{2}}$ and
$\mathfrak{G}_{3\mathfrak{F}_{2}}$ (see Figure 5). But a detailed proof would
take much time and place (and, above all, would be boring). We think that
original Ghilardi’s reasoning, see [17], is conscious and elegant and,
therefore, we resign from any alternative proof.

##  5 Unification Types.

###  5.1 Unitary Unification.

By Theorem 24, the logic $\mathsf{L}(\mathfrak{R}_{2})$ of rhombus (see figure
4) has unitary unification. We have shown this directly, using Theorem 22, in
[10]. We cannot have $m=n$ in this case. In other words, unification in
$\mathsf{L}(\mathfrak{R}_{2})$ is unitary but it is not true that every
unifiable formula in $n$-variables has a mgu in $n$-variables. A unifiable
$A(x_{1},\dots,x_{n})$ has a mgu in $m$-variables where ($m$ is defined in the
proof and) $n<m$.

Indeed, let $A=x_{1}\lor x_{2}\lor(\neg x_{1}\land\neg x_{2})$ and
$\varepsilon_{1},\varepsilon_{2},\varepsilon_{3}$ be the following unifiers
for $A$:

$\varepsilon_{1}(x_{1})=\top\ ,\
\varepsilon_{1}(x_{2})=x_{2}\quad;\quad\varepsilon_{2}(x_{1})=x_{1}\ ,\
\varepsilon_{2}(x_{2})=\top\quad;\quad\varepsilon_{3}(x_{1})=\varepsilon_{3}(x_{2})=\bot.$

Let $\varepsilon\colon\\{x_{1},x_{2}\\}\to\mathsf{Fm}^{2}$ be a mgu for $A$ in
any intermediate logic ${\mathsf{L}}\subseteq\mathsf{L}(\mathfrak{R}_{2})$.
Then for some $\alpha_{i}\colon\\{x_{1},x_{2}\\}\to\mathsf{Fm}^{2},$ where
$i=1,2,3$, we have $\alpha_{i}\circ\varepsilon=_{\sf L}\varepsilon_{i}$, and
hence the diagram in Figure 33 commutes (up to $\thicksim$) where
$\mathbf{M}^{2}=\mathbf{M}^{2}(sm(\mathfrak{R}_{2}))=\mathbf{M}^{2}(\\{\mathfrak{L}_{1},\mathfrak{L}_{2},\mathfrak{R}_{2}\\})$:

$\mathbf{M}^{2}$$\mathbf{M}^{2}$$\mathbf{M}^{2}$$\alpha_{i}$$\varepsilon$$\varepsilon_{i}$
Fig. 33: Commutative Diagram

Consider all $2$-models over one-element frame $\mathfrak{L}_{1}$. They are
$(\mathfrak{L}_{1},00),(\mathfrak{L}_{1},01)$, $(\mathfrak{L}_{1},10)$ and
$(\mathfrak{L}_{1},11)$. Each of them is a $\varepsilon_{i}$-model for some
$i$ and hence they are $\varepsilon-$models. The mapping
$\varepsilon\colon\mathbf{M}^{2}\to\mathbf{M}^{2}$ must be one-to-one on
$\mathfrak{L}_{1}$-models.

Consider the following $2$-models over $\mathfrak{L}_{2}$ (a two-element
chain):

$11$$10$and$11$ Both are $\varepsilon_{i}$-model for some $i=1,2$ and hence
they are also $\varepsilon-$models. Thus, there are such$01$
$a,b,c,d,e,f\in\\{0,1\\}$ that