Introduction
An
-ary partial function on a set
is a function
for some
. In this case, the set
will be called the domain of
and will be denoted by
. This notion can be extended to classes of algebras as follows. An
-ary partial function on a class of algebras
is a sequence
, where
is an
-ary partial function on
for each
. By a partial function on
we mean an
-ary partial function on
for some
. When
is a partial function on
and
, we denote the
-component of
by
. Lastly, throughout this note by a formula we mean a first order formula.
DefinitionΒ 1
A formula
with
in the language of a class of algebras
is said to be functional in
when for all
and
there exists at most one
such that
.
In other words,
is functional in
when
In this case,
induces an
-ary partial function
on each
with domain
defined for every
as
, where
is the unique element of
such that
. Consequently,
is an
-ary partial function on
.
DefinitionΒ 2
An
-ary partial function
on a class of algebras
is said to be
We denote the class of implicit operations of
by
.
In elementary classes, implicit operations admit the following description (see Thm.~3.9 CKMIMP).
TheoremΒ 1
Let
be a partial function on an elementary class
. Then
is an implicit operation of
if and only if it is defined by an existential positive formula.
exaΒ 1
[Monoids] A typical example of an implicit operation of the variety
of monoids arises from the idea of ``taking inverses''. More precisely, for every
let
be the unary partial function on
with
defined for every
as
Then
is an implicit operation of
. \qed
Although concrete examples of implicit operations have long been known, the theory of implicit operations received its first systematic treatment in CKMIMP. In this note, we exhibit two counterexamples relevant to the general theory of implicit operations. For this, we assume familiarity with the concepts and notation of CKMIMP, as well as with the basics of the theory of Heyting algebras (see, e.g., Ch.~IX BD74).
A variety with a pp expansion that is a proper quasivariety
Consider the linearly ordered Heyting algebra
with universe
We consider the algebra
obtained by endowing
with a constant for the element
as well as with a pair of binary operations
and
and a pair of unary operations
and
defined for every
as follows:
Our aim is to prove the following.
TheoremΒ 2
The variety
has a pp expansion that is a proper quasivariety and is not congruence preserving.
Proof.
By Thm.~12.9 CKMIMP every congruence preserving pp expansion of a variety is a variety. So, it is sufficient to show that
has a pp expansion that is a proper quasivariety. The proof proceeds through a series of claims. First, observe that
is the universe of a subalgebra
of
.
proof}[Proof of the Claim] As
is a subalgebra of
, it suffices to prove the inclusion
, which amounts to
. First, observe that
contains the interpretations
, and
of the constants. As
we conclude that
contains
, and
as well. Hence,
.
ClaimΒ 2
Let
be a finite nontrivial chain with second largest element
. Then
is subdirectly irreducible with monolith
.
Proof.
[Proof of the Claim] It suffices to show that
is the monolith of
. First, observe that
because
, where
is the maximum of
. Then consider
. As
, there exist distinct
such that
. Since
, we have
and
, where
is a shorthand for
. As
is the second largest element of
, this implies
and
. Together with
, this yields
, whence
.
Observe that
is a congruence of
. Then let
Proof.
[Proof of the Claim] Observe that all
, and
are finite nontrivial chains. Therefore, the inclusion from right to left follows from Claim \ref{Claim : new claim on B chain SI}.
To prove the inclusion from left to right, observe that the variety
is congruence distributive because it has a lattice reduct (see, e.g., Thm.~7.2 CKMIMP). By J\'onsson's Theorem (see, e.g., Thm.~6.8 BuSa00) and Thm. 5.6(2) Ber11 we have
. Together with Claim \ref{Claim : subalgebras of A}, this yields
Therefore, to conclude the proof, it will be enough to show that
is simple and that, up to isomorphism, the only nontrivial homomorphic images of
are
and
.
We begin by proving that
is simple, which means that
has exactly two elements. In view of Claim \ref{Claim : new claim on B chain SI}, it suffices to show that
. Observe that
. As the lattice reduct of
is a chain with extrema
and
, this guarantees that
.
Lastly, we prove that, up to isomorphism, the only nontrivial homomorphic images of
are
and
. By the definition of
it will be enough to show that for every
,
Consider
. Observe that the definition of
and Claim \ref{Claim : new claim on B chain SI} guarantee that
. Therefore, there exist
such that
. From the definition of
it follows that
As
and the lattice reduct of
is a chain, we can assume that
. From
, the right hand side of the above display, and the fact that
is the second largest element of
it follows that
, whence
. Consequently,
and, therefore,
. As before, this yields
.
Consider the pp formula
ClaimΒ 4
The formula
defines an extendable implicit operation
of
such that
is a total function defined for every
as
Proof.
[Proof of the Claim] We will show that
defines an extendable implicit operation
of
. The description of
in the statement will be an immediate consequence of our proof.
In view of Cor.~8.14 CKMIMP, it suffices to show that every member of
can be extended to one of
in which
defines a total unary function. Recall from \cref{Claim : the SI members of V(A) in pp counterexample} that
. As
, we have
. Consequently, it will be enough to show that
defines a total unary function both on
and
.
We begin with the case of
.\ We need to prove that for every
there exists a unique
such that
. To this end, consider
. We have two cases: either
or
. First, suppose that
. Since
the definition of
guarantees that
. Therefore, it only remains to show that
for every
such that
. Consider
such that
. Then
for some
. As
, we have
. Together with
and
, this implies
From the definition of
it thus follows that
, as desired.
Then we consider the case where
. Since
, the definition of
guarantees that
. Therefore, it only remains to show that
for every
such that
. Consider
such that
. Then
for some
. As
, we have
. Together with
and
, this implies
From the definition of
it thus follows that
.
Next we consider the case of
. Since
the definition of
guarantees that for every
,
Then let
. As before, we have two cases: either
or
. First, suppose that
. Since
from
it follows that
By the definition of
this guarantees that
. Therefore, it only remains to show that
for every
such that
. Consider
such that
. Let
be the element given by the right hand side of (\ref{Eq : Miriam new equation}). As
, we have
. Together with
, the right hand side of (\ref{Eq : Miriam new equation}) ensures that
. By the definition of
we obtain
. As
, we conclude that
, as desired. Then we consider the case where
. In this case,
. Therefore,
by the definition of
. It only remains to show that
for every
such that
. Consider
such that
. As before, let
be the element given by right hand side of (\ref{Eq : Miriam new equation}). Since
, we have
. Together with
and the right hand side of (\ref{Eq : Miriam new equation}), it follows that
. By the definition of
we obtain
, whence
.
By \cref{Claim : varphi in ext} the formula
defines some
. Consider the
-expansion
of
obtained by adding a new unary function symbol
to
. Moreover, let
be the pp expansion
of
induced by
and
. To conclude the proof, it only remains to show that
is a proper quasivariety.
First,
is a quasivariety by Thm.~10.3(ii) CKMIMP. We will prove that
is not a variety, i.e., it is not closed under
. Recall from \cref{Claim : varphi in ext} that
is a total function. Therefore, the algebra
is well defined. Moreover, the definition of
and the description of
in Claim \ref{Claim : varphi in ext} guarantee that
is the universe of a subalgebra
of
. Then from the definition of
it follows that
Now recall that
As
is a congruence of
which, moreover, is compatible with the new operation
by \cref{Claim : varphi in ext}, we obtain that
is also a congruence of
. We will prove that
. As
, this will imply that
is not closed under
, as desired.
Suppose, with a view to contradiction, that
. By the definition of
there exists
such that
is total and
. Observe that
Since
and
, this yields
Together with the definition of
, this guarantees
. Since
is a pp formula and
, from Prop.~8.1 CKMIMP it follows that
. As
is a formula in
and
, we obtain
. Since
is the formula defining
and
, this yields
Therefore,
because
. On the other hand, we will prove that
thus obtaining the desired contradiction. The first equality above holds by the definition of a quotient algebra, the second because
, the third by the definition of
, and the fourth by \cref{Claim : varphi in ext}. Finally, the inequality at the end of the above display follows from the definition of
. \end{proof}
A nonequational congruence preserving Beth companion
All the examples of Beth companions considered in CKMIMP are induced by implicit operations defined by conjunctions of equations, as opposed to arbitrary pp formulas. Such Beth companions have particularly nice properties. For example, they have an equational axiomatization relative to the original class of algebras (see Thm.~10.4 CKMIMP) and are congruence preserving (see Thm.~12.4 CKMIMP). One might therefore wonder whether every quasivariety
with a Beth companion also has a Beth companion induced by implicit operations defined by conjunctions of equations. This is the case, for instance, when
has the amalgamation property (see Thm.~12.7 CKMIMP and Rem.~11.12(vi) CKMIMP). Our aim is to show that the previous conjecture fails, even when
is a variety with a congruence preserving Beth companion. Actually, a counterexample can be found among some of the simplest varieties of Heyting algebras, as we proceed to illustrate.
For every cardinal
let
be the unique Heyting algebra whose lattice reduct is obtained by adding a new maximum
to the powerset lattice
. The implication of
is defined by the rule
As expected,
and the powerset Boolean algebra
are closely related, in the sense that
is isomorphic to the algebra obtained by quotienting
under the congruence that glues
with
and leaves any other element untouched.
The varieties generated by Heyting algebras of the form
form the chain
where
for every infinite cardinal
(see HO70).\footnote{Although we shall not rely on this fact, we remark that these are precisely the nontrivial varieties of Heyting algebras of depth
(see also Exa.~10.18 CKMIMP).}
The remainder of this section is devoted to showing that for
the variety
provides a counterexample to the conjecture that every congruence preserving Beth companion of a variety is equational. More precisely, we will establish the next result.
It is known that
, and
have the strong epimorphism surjectivity property (see Thm.~8.1 Mak00). Consequently, they are their own Beth companions by Thm.~11.6 CKMIMP. When viewed as Beth companions of themselves, they are obviously equational Beth companions. Moreover, recall that all Beth companions of a quasivariety
are faithfully term equivalent relative to
(see Thm.~11.7 CKMIMP). Consequently, if
has an equational Beth companion, then all Beth companions of
are equational. Hence, in order to prove \cref{Thm : proper Beth companion}, it will be enough to establish the following.
The proof of \cref{Thm : proper Beth companion : main} proceeds through a series of observations. First, if an algebra
has a lattice reduct, then
is congruence distributive (see, e.g., Thm.~7.2 CKMIMP). Therefore, the following is an immediate consequence of a version of J\'onssonβs Theorem for finitely subdirectly irreducible algebras (see, e.g., Thm.~2.12 CKMIMP) and Thm. 5.6(2) Ber11.
As an application of Proposition \ref{Prop : Jonsson lattice : easy}, we obtain a transparent description of
.
Proof.
By Proposition \ref{Prop : Jonsson lattice : easy} we have
. Moreover, by inspection it is possible to check that (up to isomorphism) the finitely subdirectly irreducible members of
are
. Together with
, this yields
. Lastly, the equality
is an immediate consequence of the definition of
.
Proof.
From the Subdirect Decomposition Theorem (see, e.g., Thm.~8.6 BuSa00) and \cref{Prop : proper Beth completion : FSI members of V(An)} it follows that
Since the inclusion
always holds, we conclude that
.
We will make use of the following properties typical of the Heyting algebras of the form
for a cardinal
. As all of them are immediate consequences of the definition of
, their proof is omitted. First, observe that
has a second largest element (namely,
) that we denote by
. For every
we have
We recall that an element
of an algebra
with a bounded lattice reduct is an atom when
and there exists no
such that
. To simplify notation, we will make use of the following shorthands for every algebra
with a bounded lattice reduct and
:
Moreover, for every
and
the following holds:
We also rely on the following properties that hold in every Heyting algebra. First, for every
,
Second, for every
,
Now, fix
. For each positive
let
and
denote the terms
where
are variables. Then let
be the conjunction of the following formulas:
For each positive
let
be the formula
and define
Observe that
is a pp formula for every
and positive
. We will prove the following.
Proof.
We begin by proving the implication from left to right. Suppose that
. Then there exist
such that
and for every positive
both
and
Together with (\ref{Eq : tricks for An : Beth completion : 1}), (\ref{Eq : tricks for An : Beth completion : 6}), and (\ref{Eq : tricks for An : Beth completion : 7}), the above display yields that for every
,
By the definition of
we have two cases: either
or
. First, suppose that
. We need to prove that
. To this end, observe that for every
,
where the first inequality holds by (\ref{Eq : tricks for An : Beth completion : 8}), the second is straightforward, and the last equality by (\ref{Eq : proper Beth completion : total 3}). Since
, we have
by (\ref{Eq : tricks for An : Beth completion : 3}). Together with the above display, we obtain
for every
. By (\ref{Eq : proper Beth completion : total 1}) we conclude that
, as desired.
Next, we consider the case where
. In this case,
by (\ref{Eq : tricks for An : Beth completion : 2}). Therefore, from (\ref{Eq : proper Beth completion : total 2}) it follows that
for all positive
and
. By (\ref{Eq : tricks for An : Beth completion : 2}) this yields
We have two subcases: either the number of atoms below
is
or
. First, suppose that it is
. We need to prove that
. As
has
atoms by definition, the number of atoms below
is
by (\ref{Eq : tricks for An : Beth completion : 5}). From (\ref{Eq : proper Beth completion : total 4}) in the case where
it follows that
The right hand side of the first line of the above display implies that the sets of atoms below each of the
for
must be pairwise disjoint. Moreover, observe that
is finite and, therefore, each nonzero element is above an atom. Together with \eqref{Eq : proper Beth completion : total 5}, this implies that there is at least one atom below each
. Consequently, there must be at least
distinct atoms below the join of
. Together with the left hand side of the first line of the above display, this implies that the number of atoms below
is
, which is false by assumption. Therefore,
As before, the right hand side of the above display and (\ref{Eq : proper Beth completion : total 5}) imply that the number of distinct atoms below the join of
must be at least
. Observe that by the left hand side of the above display and \eqref{Eq : tricks for An : Beth completion : 4} it follows that every atom below the join of
must be also below
. As by assumption the number of atoms below
is precisely
, the set of atoms below
must coincide with the set of atoms below
. Therefore, using \eqref{Eq : tricks for An : Beth completion : 4} we obtain
Together with (\ref{Eq : proper Beth completion : total 3}), this yields
As
by assumption, from (\ref{Eq : tricks for An : Beth completion : 2}) and (\ref{Eq : tricks for An : Beth completion : 3}) it follows that
. Therefore, the above display yields
By (\ref{Eq : proper Beth completion : total 1}) we conclude that
, as desired. It only remains to consider the case where the number of atoms below
is
. We need to prove that
. As
has
atoms by definition, the number of atoms below
is
by (\ref{Eq : tricks for An : Beth completion : 5}). Then consider a positive
. Since
, the number of atoms below
is
. Since (\ref{Eq : proper Beth completion : total 5}) and the second line of (\ref{Eq : proper Beth completion : total 4}) would imply that the number of atoms below
is
, we conclude that the first line of (\ref{Eq : proper Beth completion : total 4}) holds. Consequently,
We will prove that the following holds:
The first and the last steps above hold by
and (\ref{Eq : tricks for An : Beth completion : 2}), the second is straightforward, the third by (\ref{Eq : proper Beth completion : definition of phi : qwert}) and (\ref{Eq : tricks for An : Beth completion : 8}), and the fourth by
, which follows from
and (\ref{Eq : tricks for An : Beth completion : 3b}). Together with (\ref{Eq : proper Beth completion : total 3}), the above display yields
. As this holds for every
, from (\ref{Eq : proper Beth completion : total 1}) it follows that
, as desired.
Next we prove the implication from right to left in the statement. Recall from the definition of
that it suffices to find
for
and
such that
First, suppose that
. In this case,
by assumption. Choose
and
for all
and
. Clearly, we have
From \eqref{Eq : tricks for An : Beth completion : 1} it follows that for each
we have
and, therefore,
which proves the validity of the first two conjuncts of
. Moreover, it holds that
This establishes \eqref{Eq : to show psi} for the case where
.
It only remains to consider the case where
. Observe that choosing
for all
and
guarantees that
by \eqref{Eq : tricks for An : Beth completion : 2}. Moreover, \eqref{Eq : tricks for An : Beth completion : 4} implies that, in order to guarantee that
it suffices to choose
so that one of the following holds:
We distinguish three cases. First, let
. Then
by assumption. Choose
for all
and
such that
are precisely the
distinct atoms of
and let
for each
. Then condition \eqref{Eq : long equation conditions 1} is satisfied, since
, and thus
. Therefore, to verify \eqref{Eq : to show psi}, it only remains to observe that for each
we have
which is true by \eqref{Eq : tricks for An : Beth completion : 3} and
.
Next we consider the case where
and
. Then
by assumption. For all
and
consider
such that
and
. Moreover, for all
and
consider
such that
and
. Then for
condition \eqref{Eq : long equation conditions 1} is satisfied and by \eqref{Eq : tricks for An : Beth completion : 2}, (\ref{Eq : tricks for An : Beth completion : 3}), \eqref{Eq : tricks for An : Beth completion : 3b}, and
we have
On the other hand, for every
such that
condition \eqref{Eq : long equation conditions 2} is satisfied. Moreover, using \eqref{Eq : tricks for An : Beth completion : 2}, \eqref{Eq : tricks for An : Beth completion : 3}, and
, we obtain
Since
(because
), this verifies that \eqref{Eq : to show psi} holds.
It only remains to consider the case where
and
. In this case, we have
by assumption. Then for all
and
consider
such that
. Also choose
for each
. Then \eqref{Eq : long equation conditions 1} it satisfied because
. Therefore, to conclude the proof of \eqref{Eq : to show psi}, it only remains to observe that for each
we have
which holds by \eqref{Eq : tricks for An : Beth completion : 2}, \eqref{Eq : tricks for An : Beth completion : 3b}, and
. This completes the proof.
As a consequence of Proposition \ref{Prop : proper Beth completion : varphi is functional}, we get the following.
CorollaryΒ 2
For every
and positive
the formula
defines an implicit operation
such that
is total and for every
,
Proof.
In view of Proposition \ref{Prop : proper Beth completion : varphi is functional}, the pp formula
is functional in
. By Cor.~3.11 CKMIMP it is also functional in
. In view of \cref{Cor : proper Beth completion : V(An) = Q(An)}, this means that
is functional in
and, therefore, defines an implicit operation
. From \cref{Prop : proper Beth completion : varphi is functional} it follows that
is total and defined as in the statement. As
is total, we can apply Prop.~8.11(ii) CKMIMP to the case where
and
, obtaining that
is extendable. Thus, we conclude that
.
Now, for every
let
Observe that
by Corollary \ref{Cor : proper Beth completion : fnk is extendable}. Then consider an
-expansion
of the language
of Heyting algebras and let
be the corresponding pp expansion of
. Our aim is to prove the following.
To this end, recall from Corollary \ref{Cor : proper Beth completion : fnk is extendable} that
is total for every
, whence the algebra
is defined. We begin with the following observation.
Proof.
We begin with the following observation.
proof}[Proof of the Claim] First, we show that
Clearly, it will be enough to prove the above display for an arbitrary
. The inclusion
is straightforward. To prove the reverse one, consider
. From
it follows that
. As
and
are Heyting algebras and the variety of Heyting algebras has the congruence extension property, there exists
such that
. From Prop.~12.13 CKMIMP and the definition of
it follows that
. Therefore,
. Together with
, this yields
, as desired.
Next, we prove
. By \cref{Prop : Jonsson lattice : easy} we have
. Therefore, it suffices to show that the finitely subdirectly irreducible members of
are precisely the members of
. To this end, consider a finitely subdirectly irreducible
. Then there exist
and
such that
. By Prop.~2.10 CKMIMP the congruence
is meet irreducible in
. By (\ref{Eq : addendum : answering Luca's question}) it is also a meet irreducible member of
. Since
, one can check by inspection that the only meet irreducible congruences of
are
and the congruences
of
with exactly two equivalences, namely,
and
. If
, then
and, therefore,
because
. On the other hand, if
has exactly two equivalence classes
and
, then
is isomorphic to the subalgebra of
with universe
, whence
. Finally, we show that every member of
is finitely subdirectly irreducible. Let
. Then
by (\ref{Eq : addendum : answering Luca's question}). Since
, the definition of
guarantees that
. By inspection one can check that every member of
is finitely subdirectly irreducible. Consequently, so is
. By Prop.~2.10 CKMIMP the congruence
is meet irreducible in
. As
, it is also meet irreducible in
. Hence, we conclude that
is finitely subdirectly irreducible by Prop.~2.10 CKMIMP.
By \cref{Claim : new claim to answer Luca's question} and the Subdirect Decomposition Theorem (see, e.g., Thm.\ 3.1.1 Go98a) we obtain
.\ Consequently,
. As the reverse inclusion always holds, we conclude that
.
Now, recall from \cref{Cor : proper Beth completion : V(An) = Q(An)} that
. As
, this allows us to apply Thm.~10.5 CKMIMP to the case where
,
, and
, obtaining
. Since
, we obtain
. Therefore,
. Lastly, since
has a Heyting algebra reduct, the variety
is arithmetical (see, e.g., p.~80 BuSa00). \end{proof}
An endomorphism of an algebra
is a homomorphism
. When
is an isomorphism, we say that it is an automorphism of
. The sets of endomorphisms and of automorphisms of
will be denoted, respectively, by
and
.
Similarly to the case of complete atomic Boolean algebras (cf.\ Cor.~14.2 BAGiHa), one can easily verify that every permutation of the atoms of
for some
induces an automorphism of
in the following way.
PropositionΒ 5
Let
and let
be a permutation. Then the map
defined for every
as
is an automorphism of
.
We will also make use of the next observation on the automorphisms of
.
Proof.
(\ref{item : proper Beth completion : automorphisms : 1}): Consider
and
. For every
let
We will prove that
forms a partition of
. As
, for every distinct
we have
. Therefore, it only remains to show that for every
there exists
such that
, i.e.,
. Consider
. We begin by showing that
. If
, we have
and, therefore,
. Then we consider the case where
. In this case, there exists
such that
. Observe that
and
. Consequently, using \eqref{Eq : tricks for An : Beth completion : 2} and \eqref{Eq : tricks for An : Beth completion : 4}, we obtain
Hence, we conclude that
, as desired. Therefore,
because
and every atom of
is below
. Since
, from
it follows that
for some
. Hence,
forms a partition of
, as desired.
Now, observe that
because
. Together with the assumption that
, this yields
. We will show that there exist
and
such that
and
. We have two cases: either
or
. First, suppose that
. Then
and
. Since
, there exist
such that
and
, as desired.\ Next we consider the case where
. Recall from the first part of the proof that
is a partition of
. Therefore,
. Suppose, with a view to contradiction, that for every
we have
or
. Then
It follows that
where the first equality holds by \eqref{Eq : tricks for An : Beth completion : 4} and
(the latter follows from
), the second by \eqref{Eq : at(b) in terms of X_a}, the third by the definition of
, and the fourth follows from \eqref{Eq : tricks for An : Beth completion : 4} because
(the latter holds because
and
). But this is a contradiction to the assumption that
. Therefore, there exists
such that
. Consequently, we can choose
to obtain
such that
and
such that
. Thus, in both cases, there exist
and
with
Then let
be a permutation such that
Notice that
exists because
by the first item of (\ref{Eq : proper Beth completion : sigma fixes the partition : new}). Recall that
. Thus, we can consider the automorphism
defined in \cref{Prop : proper Beth completion : the auto sigma}, which by Prop.~9.5 CKMIMP is also an automorphism of
. Therefore, in order to complete the proof, it only remains to show that
and
for every
.
We begin by proving that
The first step in the above display holds by the definition of
and
, the second by the second item of (\ref{Eq : proper Beth completion : sigma fixes the partition : new}), and the third by the right hand side of (\ref{Eq : proper Beth completion : sigma fixes the partition}). Together with the third item of (\ref{Eq : proper Beth completion : sigma fixes the partition : new}), the above display yields
.
Lastly, we will prove that
for every
. Consider
. If
, then
by the definition of
. Then we consider the case where
. We will prove that
The above equalities are justified as follows: the first and the last hold by \eqref{Eq : tricks for An : Beth completion : 4} and
, the second and the second to last because
, the third because
is a homomorphism of bounded lattices and, therefore, it preserves finite (possibly empty) joins, the fourth by the definition of
and the fact that
implies
, the fifth by the left hand side of (\ref{Eq : proper Beth completion : sigma fixes the partition}), and the sixth because
implies
, whence (\ref{Eq : tricks for An : Beth completion : 4}) guarantees that
. Thus, we conclude that
for every
.
(\ref{item : proper Beth completion : automorphisms : 2}): Consider a pair of embeddings
. As
and
are homomorphisms of bounded lattices, we have
and
. Therefore, if
, we have
and we are done letting
be the identity map on
.
Then we may assume that
, that is,
. Since
are embeddings, both
and
are subalgebras of
containing at least an element
other than
and
. Then they must also contain
and, therefore,
by \eqref{Eq : tricks for An : Beth completion : 2}. As
is the second largest element of
and
and
are embeddings of lattices, we obtain that
possesses a second largest element
such that
. Moreover,
because
is the second largest element to
and
. If
, we have
and we are done letting
be the identity map on
.
Then we may assume that
, that is,
. We rely on the following series of observations.
proof}[Proof of the Claim]
By symmetry it suffices to show that
. To this end, consider
. Then
. Moreover, since
is the second largest element of
and
contains an element other than
, and
, from
it follows that
. Therefore,
. Since
is a embedding of bounded lattices, we obtain
. As we already established
, we conclude that
.
Proof.
[Proof of the Claim] Recall that
has
atoms by definition. As
is an expansion of
, we obtain that
has
atoms as well. Then consider
and observe that
because
by \eqref{Eq : tricks for An : Beth completion : 4} would imply
. Recall that
. Therefore, from \cref{Cor : proper Beth completion : fnk is extendable} and
it follows that for every
,
To prove the statement of the claim, consider
. By Claim \ref{Claim : proper Beth completion : automorphism : 1} we have
. Then
is a positive integer
. In view of (\ref{Eq : proper Beth completion : automorphisms : 2}), for every positive
,
Since
is an embedding such that
and
, this yields that for every positive
,
As
is also an embedding such that
and
, we obtain that for every positive
,
Together with (\ref{Eq : proper Beth completion : automorphisms : 2}), this yields
.
Proof.
[Proof of the Claim] Suppose that
. By symmetry it suffices to show that
. From
and
it follows that
. Consequently,
because
is an embedding. Therefore, we conclude that
.
In view of Claims \ref{Claim : proper Beth completion : automorphism : 2} and \ref{Claim : proper Beth completion : automorphism : 3} there exists a permutation
such that
As
, the map
can also be viewed as a permutation of
. Consequently, \cref{Prop : proper Beth completion : the auto sigma} yields an automorphism
, which by Prop.~9.5 CKMIMP is also an automorphism of
. To conclude the proof, it only remains to show that
, for in this case we can take
.
From the assumption that
, and
are homomorphisms of bounded lattices it follows that
, whence
. Therefore, it suffices to show that
for every
. We will prove that for every
,
The above equalities are justified as follows. The first and the last hold by \eqref{Eq : tricks for An : Beth completion : 4} and the assumption that
, the second and the second to last because
, and
preserve finite (possibly empty) joins because they are homomorphisms of bounded lattices, the third by Claim \ref{Claim : proper Beth completion : automorphism : 1} and (\ref{Eq : tricks for An : Beth completion : 4}), the fourth by (\ref{Eq : proper Beth completion : automorphisms : 3}), and the fifth follows from \cref{Claim : proper Beth completion : automorphism : 1} and the definition of
. Hence, we conclude that
. \end{proof}
Finalizing the proof of the fact that
is a congruence preserving Beth companion of
(\cref{Thm : proper Beth completion : B(n) is the companion}) requires some further investigation of the variety
and its properties. While
lacks the amalgamation property for every
(see Thm.~2 Mak77), this property holds in the pp expansion
of
, as we proceed to illustrate. To this end, we will employ the following result Thm.\ 3.4 FMfsi\footnote{Our formulation of Theorem \ref{Thm : AP : George Wesley} is slightly different from the one of Thm.\ 3.4 FMfsi. However, the difference is insubstantial and amounts to the fact that in FMfsi the class
is defined as
.} (see also Thm.\ 3 GLAP), together with the observation that
has the congruence extension property for each
.
Given a quasivariety
, let
TheoremΒ 6
Let
be a quasivariety with the relative congruence extension property such that
is closed under nontrivial subalgebras. Then
has the amalgamation property if and only if
has the amalgamation property.
To show that
has the congruence extension property for each
, we rely on the following preservation result.
PropositionΒ 7
Let
be a pp expansion of a quasivariety
. If
has the relative congruence extension property, then so does
.
Proof.
Suppose that
has the relative congruence extension property. Then consider
and
. We need to find some
such that
. Since
, from Rem.~12.2 CKMIMP it follows that
, whence
. Since
is a pp expansion of
, it is of the form
. Together with
, this implies
for some
. Consequently,
. As
and
has the relative congruence extension property by assumption, there exists
such that
. Recall from Prop.~12.13 CKMIMP that
implies
, whence
. This yields
and
because
and
. Hence, we are done letting
.
Proof.
We recall that every variety of Heyting algebras has the congruence extension property. In particular,
has the congruence extension property for every
. Therefore, \cref{Prop : CEP preserved in pp exp} yields that the pp expansion
of
has the congruence extension property.
Proof.
Recall from \cref{Prop : proper Beth completion : B(n) has only the CEP} that the variety
has the congruence extension property. Moreover,
is closed under subalgebras by \cref{Prop : B(n) : proper Beth completion : arithmetical}.\ Therefore, in view of \cref{Thm : AP : George Wesley}, in order to prove that
has the amalgamation property, it suffices to show that
has the amalgamation property. To this end, consider a pair of embeddings
and
with
. We need to find a pair of embeddings
and
with
such that
.
We have two cases depending on whether
is trivial or nontrivial. First, suppose that
is trivial. As
is closed under subalgebras by Proposition \ref{Prop : B(n) : proper Beth completion : arithmetical} and finitely subdirectly irreducible algebras are nontrivial, we obtain that no member of
has a trivial subalgebra. Since
embeds into
and
, this yields
. Therefore,
and
are trivial because
. Consequently,
, and
are all trivial and the embeddings
and
are isomorphisms. Therefore, we may assume that
and that
and
are the identity map
on
. Hence, letting
and
, we are done.
Next we consider the case where
is nontrivial. Since
embeds into
and
, we obtain that
and
are also nontrivial. Together with
, this yields
. Recall from \cref{Prop : B(n) : proper Beth completion : arithmetical} that
, whence
. Therefore, we may assume that
and that
and
are embeddings of
into
. By Proposition \ref{Prop : proper Beth completion : automorphisms}(\ref{item : proper Beth completion : automorphisms : 2}) there exists
such that
. Let
,
, and
the identity map on
. Clearly,
are embeddings such that
.
We are now ready to prove \cref{Thm : proper Beth completion : B(n) is the companion}.
Proof.
Recall that
is a pp expansion of
. Moreover, since
has the congruence extension property, we can apply Thm.~12.4(ii) CKMIMP, obtaining that
is congruence preserving. Hence, by Thm.~11.6 CKMIMP it will be enough to prove that
has the strong epimorphism surjectivity property. Recall from Propositions \ref{Prop : B(n) : proper Beth completion : arithmetical} and \ref{Prop : B(n) : proper Beth completion : AP and CEP : final} that
is an arithmetical variety with the amalgamation property. Therefore, in view of Cor.~7.16 CKMIMP, it will be enough to show that every
lacks proper
-epic subalgebras. To this end, consider
with
proper. Then there exists
. Moreover, we may assume that
by Proposition \ref{Prop : B(n) : proper Beth completion : arithmetical}, whence
.
Let
be the identity map on
. As
and
, to conclude the proof, it will be enough to find some
such that
and
. For, by considering the restrictions of
and
to
, we obtain that
is not
-epic, as desired.
We have two cases: either
or
. First, suppose that
. Since
, we have
. Together with
and \eqref{Eq : tricks for An : Beth completion : 2}, this yields
. Then
because
. Let
and consider the map
defined for every
as
Since
and
, from Prop.~9.5 CKMIMP it follows that
. Moreover,
and the definition of
imply
. Then
because
. Thus,
are homomorphisms such that
and
(the latter because
and both
and
preserve the constants
and
).
Lastly, we consider the case where
. As
is proper and
, there exists
. By Proposition \ref{Prop : proper Beth completion : automorphisms}(\ref{item : proper Beth completion : automorphisms : 1}) there also exists
such that
and
for every
. Thus,
are homomorphisms such that
and
.
Lastly, we prove Theorem \ref{Thm : proper Beth companion : main}. Notice that this concludes the proof of Theorem \ref{Thm : proper Beth companion}.
Proof.
As
is a congruence preserving Beth companion of
by Theorem \ref{Thm : proper Beth completion : B(n) is the companion}, it will be enough to show that
is not equational. Suppose the contrary, with a view to contradiction. Then let
be an atom of
and consider
. The following is an immediate consequence of the definition of
.
ClaimΒ 9
The universe of
is
. Moreover, the Heyting algebra reduct of
is isomorphic to
with minimum
, maximum
, second largest element
, and atoms
and
.
As
is an atom of
and
shares its bounded lattice reduct with
, the number of atoms of
below
is
. Since
has
atoms, from (\ref{Eq : tricks for An : Beth completion : 5}) it follows that the number of atoms of
below
is
. Therefore, from \cref{Cor : proper Beth completion : fnk is extendable} it follows that
and
. As
, we obtain
Recall from the assumptions that
is equational. Therefore, by Rem.~11.12(vi) CKMIMP it is faithfully term equivalent relative to
to a Beth companion
of
induced by implicit operations defined by conjunctions of equations. By Thm.~10.4 CKMIMP the Beth companion
is of the form
with
and
an
-expansion of the language
of Heyting algebras. Furthermore, recall that
is a variety by \cref{Prop : B(n) : proper Beth completion : arithmetical}. Therefore, from Rem.~11.12(v) CKMIMP it follows that the class
is also a variety.
Let
and
be the maps witnessing the fact that
and
are faithfully term equivalent relative to
. We may assume that for every
,
As
and
is a variety by \cref{Prop : B(n) : proper Beth completion : arithmetical}, we have
. Then
by the left hand side of (\ref{Eq : proper Beth completion : f on A is asymmetric : 23}). Consequently, there exists
such that
is defined and
. Together with the right hand side of (\ref{Eq : proper Beth completion : f on A is asymmetric : 23}), this yields
In view of the above display,
is the Heyting algebra reduct of
and, therefore, is isomorphic to
with atoms
and
by \cref{Claim : proper Beth completion : term equivalence : 0 claim}. This allows us to apply \cref{Prop : proper Beth completion : the auto sigma} to the permutation
that switches
and
, thus obtaining an automorphism
with
Moreover, from
it follows that
. Together with (\ref{Eq : proper Beth completion : f on A is asymmetric : 1}), this implies
Recall from Prop.~10.22(ii) CKMIMP that there exists
such that
Together with the left hand side of (\ref{Eq : proper Beth completion : f on A is asymmetric : 3}), this yields
. As the implicit operation
is preserved by homomorphisms, we can apply the automorphism
of
in (\ref{Eq : proper Beth completion : f on A is asymmetric : 2}) to deduce
and, therefore,
by \eqref{Eq : g = rho-ell-f}. Since
, this contradicts the right hand side of (\ref{Eq : proper Beth completion : f on A is asymmetric : 3}). Hence, we conclude that
is a congruence preserving Beth companion of
that is not equational.