VTeX: Solutions for Science Publishing logo


  • List of journals
  • Browse subjects
  • About Publisher
  • Help
  • Sitemap
Login Register

  1. Home
  2. Journals
  3. VMSTA
  4. To appear
  5. An addendum to ``The theory of implicit ...

An addendum to ``The theory of implicit operations''
Crossmark link logo suggesting to check for updates
Luca Carai   Miriam Kurtzhals   Tommaso Moraschini  

Authors

 
Placeholder
Pub. online: 6 January 2026      Type: Case Report     

Published
6 January 2026

Abstract

In this addendum to CKMIMP, we provide a pair of counterexamples relevant to the theory of implicit operations. More precisely, we exhibit a pp expansion of a variety that fails to be a variety (although it is a quasivariety).\ Furthermore, we construct a sequence of varieties possessing a nonequational congruence preserving Beth companion.

Introduction

An n -ary partial function on a set X is a function f:Yβ†’X for some YβŠ†Xn . In this case, the set Y will be called the domain of f and will be denoted by π–½π—ˆπ—†(f) . This notion can be extended to classes of algebras as follows. An n -ary partial function on a class of algebras π–ͺ is a sequence ⟨f𝐀:π€βˆˆπ–ͺ⟩ , where f𝐀 is an n -ary partial function on A for each π€βˆˆπ–ͺ . By a partial function on π–ͺ we mean an n -ary partial function on π–ͺ for some nβˆˆβ„• . When f is a partial function on π–ͺ and π€βˆˆπ–ͺ , we denote the 𝐀 -component of f by f𝐀 . Lastly, throughout this note by a formula we mean a first order formula.
DefinitionΒ 1
A formula Ο†(x1,…,xn,y) with nβ‰₯1 in the language of a class of algebras π–ͺ is said to be functional in π–ͺ when for all π€βˆˆπ–ͺ and a1,…,an∈A there exists at most one b∈A such that π€βŠ¨Ο†(a1,…,an,b) .
In other words, Ο† is functional in π–ͺ when
π–ͺ⊨(Ο†(x1,…,xn,y)βŠ“Ο†(x1,…,xn,z))β†’yβ‰ˆz.
In this case, Ο† induces an n -ary partial function φ𝐀 on each π€βˆˆπ–ͺ with domain
π–½π—ˆπ—†(φ𝐀)={⟨a1,…,an⟩∈An:there exists b∈A such that π€βŠ¨Ο†(a1,…,an,b)},
defined for every ⟨a1,…,anβŸ©βˆˆπ–½π—ˆπ—†(φ𝐀) as φ𝐀(a1,…,an)=b , where b is the unique element of A such that π€βŠ¨Ο†(a1,…,an,b) . Consequently,
Ο†π–ͺ=βŸ¨Ο†π€:π€βˆˆπ–ͺ⟩
is an n -ary partial function on π–ͺ .
DefinitionΒ 2
An n -ary partial function f on a class of algebras π–ͺ is said to be
  1. defined by a formula Ο† Ο† is functional in π–ͺ and f=Ο†π–ͺ ;
  2. implicit when it is defined by some formula;
  3. an operation of π–ͺ when for each homomorphism h:𝐀→𝐁 with 𝐀,𝐁∈π–ͺ and ⟨a1,…,anβŸ©βˆˆπ–½π—ˆπ—†(f𝐀) we have ⟨h(a1),…,h(an)βŸ©βˆˆπ–½π—ˆπ—†(f𝐁) and
    h(f𝐀(a1,…,an))=f𝐁(h(a1),…,h(an));
  4. an implicit operation of π–ͺ when it is both implicit and an operation of π–ͺ .
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 f be a partial function on an elementary class π–ͺ . Then f 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 f𝐀 be the unary partial function on A with
π–½π—ˆπ—†(f𝐀)={a∈A:a is invertible}
defined for every aβˆˆπ–½π—ˆπ—†(f𝐀) as
f𝐀(a)=the inverse of a.
Then ⟨f𝐀:π€βˆˆπ–ͺ⟩ 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 𝐂8 with universe
0<a1<a2<β‹―<a6<1.
We consider the algebra 𝐀 obtained by endowing 𝐂8 with a constant for the element a5 as well as with a pair of binary operations x+y and x*y and a pair of unary operations β–‘x and β—‡x defined for every a,b∈A as follows:
a+b={a6if a=0 and b∈{a6,1};a5if a=0 and b=a3;a2if (a=0 and bβˆ‰{a3,a6,1}) or (aβ‰ 0 and bβ‰ a1);a1if aβ‰ 0 and b=a1;a*b={1if a=a4 and b=a6;0otherwise;β–‘a={1if a=a5;0otherwise;β—‡a={1if a∈{0,a6,1};a1if a∈{a1,a2};a3if a∈{a3,a5};a5if a=a4.
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 Aβˆ’{a4} is the universe of a subalgebra π€βˆ’{a4} of 𝐀 .
ClaimΒ 1
We have π•Š(𝐀)={𝐀,π€βˆ’{a4}} .
proof}[Proof of the Claim] As π€βˆ’{a4} is a subalgebra of 𝐀 , it suffices to prove the inclusion π•Š(𝐀)βŠ†{𝐀,π€βˆ’{a4}} , which amounts to 𝖲𝗀𝐀(βˆ…)=Aβˆ–{a4} . First, observe that 𝖲𝗀𝐀(βˆ…) contains the interpretations 0,a5 , and 1 of the constants. As
0+1=a6,1+0=a2,β—‡a2=a1, and β—‡a5=a3,
we conclude that 𝖲𝗀𝐀(βˆ…) contains a1,a2,a3 , and a6 as well. Hence, 𝖲𝗀𝐀(βˆ…)=Aβˆ–{a4} .
ClaimΒ 2
Let π‚βˆˆπ•(𝐀) be a finite nontrivial chain with second largest element a . Then 𝐂 is subdirectly irreducible with monolith 𝖒𝗀𝐂(a,1) .
Proof.
[Proof of the Claim] It suffices to show that 𝖒𝗀𝐂(1,a) is the monolith of 𝐂 . First, observe that 𝖒𝗀𝐂(1,a)βˆˆπ–’π—ˆπ—‡(𝐂)βˆ’{idC} because a<1 , where 1 is the maximum of 𝐂 . Then consider ΞΈβˆˆπ–’π—ˆπ—‡(𝐂)βˆ’{idC} . As ΞΈβ‰ idC , there exist distinct b,c∈C such that ⟨b,c⟩∈θ . Since bβ‰ c , we have b↔b=1 and b↔cβ‰ 1 , where x↔y is a shorthand for (xβ†’y)∧(yβ†’x) . As a is the second largest element of 𝐂 , this implies (b↔b)∨a=1 and (b↔c)∨a=a . Together with ⟨b,c⟩∈θ , this yields ⟨1,a⟩∈θ , whence 𝖒𝗀𝐂(1,a)βŠ†ΞΈ .
Observe that
ΞΈ=idAβˆ’{a4}βˆͺ{⟨a6,1⟩,⟨1,a6⟩}
is a congruence of π€βˆ’{a4} . Then let
𝐁=(π€βˆ’{a4})/ΞΈ.
ClaimΒ 3
We have 𝕍(𝐀)si=𝕀({𝐀,π€βˆ’{a4},𝐁}) .
Proof.
[Proof of the Claim] Observe that all 𝐀,π€βˆ’{a4} , 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 𝕍(𝐀)siβŠ†β„π•Š(𝐀) . Together with Claim \ref{Claim : subalgebras of A}, this yields
𝕍(𝐀)siβŠ†β„({𝐀,π€βˆ’{a4}}).
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 π€βˆ’{a4} are π€βˆ’{a4} 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 𝖒𝗀𝐀(a6,1)=AΓ—A . Observe that ⟨1,0⟩=⟨a4*a6,a4*1βŸ©βˆˆπ–’π—€π€(a6,1) . As the lattice reduct of 𝐀 is a chain with extrema 0 and 1 , this guarantees that 𝖒𝗀𝐀(a6,1)=AΓ—A .
Lastly, we prove that, up to isomorphism, the only nontrivial homomorphic images of π€βˆ’{a4} are π€βˆ’{a4} and 𝐁 . By the definition of 𝐁 it will be enough to show that for every Ο•βˆˆπ–’π—ˆπ—‡(π€βˆ’{a4}) ,
Ο•βˆ‰{idAβˆ’{a4},ΞΈ} implies Ο•=(Aβˆ’{a4})Γ—(Aβˆ’{a4}).
Consider Ο•βˆ‰{idAβˆ’{a4},ΞΈ} . Observe that the definition of ΞΈ and Claim \ref{Claim : new claim on B chain SI} guarantee that ΞΈβŠŠΟ• . Therefore, there exist c,d∈Aβˆ’{a4} such that ⟨c,dβŸ©βˆˆΟ•βˆ’ΞΈ . From the definition of ΞΈ it follows that
c≠d and {c,d}≠{a6,1}.
As cβ‰ d and the lattice reduct of π€βˆ’{a4} is a chain, we can assume that c<d . From c<d , the right hand side of the above display, and the fact that a6 is the second largest element of Aβˆ’{a4} it follows that c<a6 , whence c≀a5 . Consequently,
⟨1,a5⟩=⟨a5∨1,a5∨c⟩=⟨a5∨(cβ†’c),a5∨(dβ†’c)βŸ©βˆˆΟ•
and, therefore, ⟨1,0⟩=βŸ¨β–‘a5,β–‘1βŸ©βˆˆΟ• . As before, this yields Ο•=(Aβˆ’{a4})Γ—(Aβˆ’{a4}) .
Consider the pp formula
Ο†(x,y)=βˆƒz(x+yβ‰ˆβ—‡z).
ClaimΒ 4
The formula Ο†(x,y) defines an extendable implicit operation f of 𝕍(𝐀) such that f𝐀 is a total function defined for every a∈A as
f𝐀(a)={a1if aβ‰ 0;a3if a=0.
Proof.
[Proof of the Claim] We will show that Ο† defines an extendable implicit operation f of 𝕍(𝐀) . The description of f𝐀 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 𝕍(𝐀)si can be extended to one of 𝕍(𝐀) in which Ο†(x,y) defines a total unary function. Recall from \cref{Claim : the SI members of V(A) in pp counterexample} that 𝕍(𝐀)si=𝕀({𝐀,π€βˆ’{a4},𝐁}) . As π€βˆ’{a4}≀𝐀 , we have 𝕍(𝐀)siβŠ†π•€π•Š({𝐀,𝐁}) . Consequently, it will be enough to show that Ο†(x,y) defines a total unary function both on 𝐀 and 𝐁 .
We begin with the case of 𝐀 .\ We need to prove that for every a∈A there exists a unique b∈A such that π€βŠ¨Ο†(a,b) . To this end, consider a∈A . We have two cases: either a=0 or aβ‰ 0 . First, suppose that a=0 . Since
a+a3=0+a3=a5=β—‡a4,
the definition of Ο† guarantees that π€βŠ¨Ο†(a,a3) . Therefore, it only remains to show that b=a3 for every b∈A such that π€βŠ¨Ο†(a,b) . Consider b∈A such that π€βŠ¨Ο†(a,b) . Then a+b=β—‡c for some c∈A . As a=0 , we have a+b∈{a2,a5,a6} . Together with β—‡[A]={a1,a3,a5,1} and a+b=β—‡c , this implies a+b=a5 From the definition of + it thus follows that b=a3 , as desired.
Then we consider the case where aβ‰ 0 . Since a+a1=a1=β—‡a1 , the definition of Ο† guarantees that π€βŠ¨Ο†(a,a1) . Therefore, it only remains to show that b=a1 for every b∈A such that π€βŠ¨Ο†(a,b) . Consider b∈A such that π€βŠ¨Ο†(a,b) . Then a+b=β—‡c for some c∈A . As aβ‰ 0 , we have a+b∈{a1,a2} . Together with β—‡[A]={a1,a3,a5,1} and a+b=β—‡c , this implies a+b=a1 From the definition of + it thus follows that b=a1 .
Next we consider the case of 𝐁=(π€βˆ’{a4})/ΞΈ . Since π€βˆ’{a4}≀𝐀 the definition of ΞΈ guarantees that for every a,b∈Aβˆ’{a4} ,
πβŠ¨Ο†(a/ΞΈ,b/ΞΈ)⇔ there exists c∈Aβˆ’{a4} such that either a+𝐀b=◇𝐀c or {a+𝐀b,◇𝐀c}={a6,1}.
Then let a∈Aβˆ’{a4} . As before, we have two cases: either a=0 or aβ‰ 0 . First, suppose that a=0 . Since
a+𝐀a6=0+𝐀a6=a6 and ◇𝐀a6=1,
from ⟨a6,1⟩∈θ it follows that
a/ΞΈ+𝐁a6/ΞΈ=a6/ΞΈ=1/ΞΈ=◇𝐁a6/ΞΈ.
By the definition of Ο† this guarantees that πβŠ¨Ο†(a/ΞΈ,a6/ΞΈ) . Therefore, it only remains to show that b/ΞΈ=a6/ΞΈ for every b∈Aβˆ’{a4} such that πβŠ¨Ο†(a/ΞΈ,b/ΞΈ) . Consider b∈Aβˆ’{a4} such that πβŠ¨Ο†(a/ΞΈ,b/ΞΈ) . Let c∈Aβˆ’{a4} be the element given by the right hand side of (\ref{Eq : Miriam new equation}). As a=0 , we have a+𝐀b∈{a2,a5,a6} . Together with β—‡cβˆˆβ—‡[Aβˆ’{a4}]={a1,a3,1} , the right hand side of (\ref{Eq : Miriam new equation}) ensures that a+𝐀b=a6 . By the definition of + we obtain b∈{a6,1} . As ⟨a6,1⟩∈θ , we conclude that b/ΞΈ=a6/ΞΈ , as desired. Then we consider the case where aβ‰ 0 . In this case, a+𝐀a1=a1=◇𝐀a1 . Therefore, πβŠ¨Ο†(a/ΞΈ,a1/ΞΈ) by the definition of Ο† . It only remains to show that b/ΞΈ=a1/ΞΈ for every b∈Aβˆ’{a4} such that πβŠ¨Ο†(a/ΞΈ,b/ΞΈ) . Consider b∈Aβˆ’{a4} such that πβŠ¨Ο†(a/ΞΈ,b/ΞΈ) . As before, let c∈Aβˆ’{a4} be the element given by right hand side of (\ref{Eq : Miriam new equation}). Since aβ‰ 0 , we have a+𝐀b∈{a1,a2} . Together with β—‡cβˆˆβ—‡[Aβˆ’{a4}]={a1,a3,1} and the right hand side of (\ref{Eq : Miriam new equation}), it follows that a+𝐀b=a1 . By the definition of + we obtain b=a1 , whence b/ΞΈ=a1/ΞΈ .
By \cref{Claim : varphi in ext} the formula Ο† defines some fβˆˆπ–Ύπ—‘π—pp(𝕍(𝐀)) . Consider the f -expansion β„’f of ℒ𝕍(𝐀) obtained by adding a new unary function symbol gf to ℒ𝕍(𝐀) . Moreover, let 𝖬 be the pp expansion π•Š(𝕍(𝐀)[β„’β„±]) of 𝕍(𝐀) induced by
f and β„’f . 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 f𝐀 is a total function. Therefore, the algebra 𝐀[β„’β„±] is well defined. Moreover, the definition of 𝐀 and the description of f𝐀 in Claim \ref{Claim : varphi in ext} guarantee that Aβˆ’{a4} is the universe of a subalgebra 𝐂 of 𝐀[β„’β„±] . Then from the definition of 𝖬 it follows that
π‚βˆˆπ•Š(𝐀[β„’β„±])βŠ†π•Š(𝕍(𝐀)[β„’β„±])=𝖬.
Now recall that
ΞΈ=idAβˆ’{a4}βˆͺ{⟨a6,1⟩,⟨1,a6⟩}.
As ΞΈ is a congruence of π€βˆ’{a4}=𝐂↾ℒ𝕍(𝐀) which, moreover, is compatible with the new operation gf𝐂=f𝐀↾C 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 f𝐃 is total and 𝐂/θ≀𝐃[β„’β„±] . Observe that
0+𝐀1=a6 and ◇𝐀1=1.
Since ⟨a6,1⟩∈θ and 𝐂↾ℒ𝕍(𝐀)=π€βˆ’{a4}≀𝐀 , this yields
0+𝐂/ΞΈ1/ΞΈ=a6/ΞΈ=1/ΞΈ=(◇𝐀1)/ΞΈ=◇𝐂/ΞΈ1/ΞΈ.
Together with the definition of Ο† , this guarantees 𝐂/ΞΈβŠ¨Ο†(0/ΞΈ,1/ΞΈ) . Since Ο† is a pp formula and 𝐂/θ≀𝐃[β„’β„±] , from Prop.~8.1 CKMIMP it follows that 𝐃[β„’β„±]βŠ¨Ο†(0/ΞΈ,1/ΞΈ) . As Ο† is a formula in ℒ𝕍(𝐀) and 𝐃=𝐃[β„’β„±]↾ℒ𝕍(𝐀) , we obtain πƒβŠ¨Ο†(0/ΞΈ,1/ΞΈ) . Since Ο† is the formula defining f and gf𝐃[β„’β„±]=f𝐃 , this yields
gf𝐃[β„’β„±](0/ΞΈ)=f𝐃(0/ΞΈ)=1/ΞΈ.
Therefore, gf𝐂/ΞΈ(0/ΞΈ)=1/ΞΈ because 𝐂/θ≀𝐃[β„’β„±] . On the other hand, we will prove that
gf𝐂/ΞΈ(0/ΞΈ)=gf𝐂(0)/ΞΈ=gf𝐀[β„’β„±](0)/ΞΈ=f𝐀(0)/ΞΈ=a3/ΞΈβ‰ 1/ΞΈ,
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}
RemarkΒ 1
The proof of \cref{Thm: pp exp variety not variety} yields that ΞΈβˆˆπ–’π—ˆπ—‡(𝐂↾ℒ𝕍(𝐀))βˆ’π–’π—ˆπ—‡π–¬(𝐂) , witnessing that the pp expansion 𝖬 of 𝕍(𝐀) is not congruence preserving. \qed

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 1 to the powerset lattice βŸ¨π’«(ΞΊ);∩,βˆͺ⟩ . The implication of 𝐀κ is defined by the rule
aβ†’b={1if a≀b;bif a=1;(ΞΊβˆ’a)βˆͺbif a,bβˆˆπ’«(ΞΊ) and aβ‰°b.
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 1 with ΞΊ and leaves any other element untouched.
The varieties generated by Heyting algebras of the form 𝐀κ form the chain
𝕍(𝐀0)βŠŠπ•(𝐀1)βŠŠβ€¦βŠŠπ•(𝐀n)βŠŠβ€¦βŠŠπ•(𝐀ω),
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 ≀2 (see also Exa.~10.18 CKMIMP).}
DefinitionΒ 3
A pp expansion 𝖬 of a class of algebras π–ͺ is said to be
  1. equational when it is faithfully term equivalent relative to π–ͺ to a pp expansion of π–ͺ of the form π•Š(π–ͺ[β„’β„±]) with β„±βŠ†π–Ύπ—‘π—eq(π–ͺ) ;
  2. an equational Beth companion of π–ͺ when it is equational and a Beth companion of π–ͺ .
The remainder of this section is devoted to showing that for nβ‰₯3 the variety 𝕍(𝐀n) 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.
TheoremΒ 3
The following conditions hold for every ΞΊβˆˆβ„•βˆͺ{Ο‰} :
  1. 𝕍(𝐀κ) has a congruence preserving Beth companion;
  2. 𝕍(𝐀κ) has an equational Beth companion if and only if κ∈{0,1,2,Ο‰} .
It is known that 𝕍(𝐀0),𝕍(𝐀1),𝕍(𝐀2) , 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.
TheoremΒ 4
For every nβ‰₯3 the variety 𝕍(𝐀n) has a congruence preserving Beth companion that is not equational.
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.
PropositionΒ 1
Let 𝐀 be a finite algebra with a lattice reduct. Then 𝕍(𝐀)fsiβŠ†β„π•Š(𝐀) .
As an application of Proposition \ref{Prop : Jonsson lattice : easy}, we obtain a transparent description of 𝕍(𝐀n)fsi .
PropositionΒ 2
For every nβˆˆβ„• we have 𝕍(𝐀n)fsi=𝕀(𝐀0,…,𝐀n)=π•€π•Š(𝐀n) .
Proof.
By Proposition \ref{Prop : Jonsson lattice : easy} we have 𝕍(𝐀n)fsiβŠ†β„π•Š(𝐀n) . Moreover, by inspection it is possible to check that (up to isomorphism) the finitely subdirectly irreducible members of β„π•Š(𝐀n) are 𝐀0,…,𝐀n . Together with 𝕍(𝐀n)fsiβŠ†β„π•Š(𝐀n)βŠ†π•(𝐀n) , this yields 𝕍(𝐀n)fsi=𝕀(𝐀0,…,𝐀n) . Lastly, the equality 𝕀(𝐀0,…,𝐀n)=π•€π•Š(𝐀n) is an immediate consequence of the definition of 𝐀0,…,𝐀n .
CorollaryΒ 1
For every nβˆˆβ„• we have 𝕍(𝐀n)=β„š(𝐀n) .
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
𝕍(𝐀n)=π•€π•Šβ„™(𝕍(𝐀n)fsi)=π•€π•Šβ„™π•€π•Š(𝐀n)βŠ†β„š(𝐀n).
Since the inclusion β„š(𝐀n)βŠ†π•(𝐀n) always holds, we conclude that 𝕍(𝐀n)=β„š(𝐀n) .
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 e . For every a,b∈AΞΊ we have
a∨b=1⇔a=1 or b=1;0<a≀e⇔a∨¬a=e;a∈{0,e,1}⇔¬¬a=1;(aβ‰ e or a=0)⇔¬¬a=a.
We recall that an element a of an algebra 𝐁 with a bounded lattice reduct is an atom when aβ‰ 0 and there exists no b∈B such that 0<b<a . To simplify notation, we will make use of the following shorthands for every algebra 𝐁 with a bounded lattice reduct and a∈B :
𝖺𝗍(𝐁)={b∈B:b is an atom of 𝐁};𝖺𝗍𝐁(a)={bβˆˆπ–Ίπ—(𝐁):b≀a}.
Moreover, for every 𝐁≀𝐀n and a∈B the following holds:
if aβ‰ 1 then a=⋁𝖺𝗍𝐁(a);if bβˆˆπ–Ίπ—(𝐁), then either (b≀a and bβ‰°Β¬a) or (bβ‰°a and b≀¬a).
We also rely on the following properties that hold in every Heyting algebra. First, for every a1,…,am∈AΞΊ ,
β‹€i=1mΒ¬ai=1⇔ai=0 for every i≀m.
Second, for every a,b∈Aκ ,
a≀b⇔aβ†’b=1;a≀b⇒¬¬a≀¬¬b.
Now, fix nβ‰₯3 . For each positive m≀nβˆ’1 let sm,n and d denote the terms
sm,n=⋁i=1n+1zim and d=x∨¬x,
where x,z1m,…,zn+1m are variables. Then let ψm,n(x,y,z1m,…,zn+1m) be the conjunction of the following formulas:
β¨…i=1n+1(d(x)β‰ˆd(zim));d(x)∨¬¬(x∨sm,n)β‰ˆy;((sm,nβ†’x)βˆ§β‹€i,j=1iβ‰ jm+1Β¬(zim∧zjm))∨((sm,nβ†’Β¬x)βˆ§β‹€i,j=m+2iβ‰ jn+1Β¬(zim∧zjm))β‰ˆ1.
For each positive k≀nβˆ’1 let Ξ³k,n(x,y,z11,…,zn+11,…,z1k,…,zn+1k,w1,…,wk) be the formula
(yβ‰ˆβ‹m=1kwm)βŠ“β¨…m=1kψm,n(x,wm,z1m,…,zn+1m)
and define
Ο†k,n(x,y)=βˆƒz11,…,zn+11,…,z1k,…,zn+1k,w1,…,wkΞ³k,n.
Observe that Ο†k,n(x,y) is a pp formula for every nβ‰₯3 and positive k≀nβˆ’1 . We will prove the following.
PropositionΒ 3
For every nβ‰₯3 , positive k≀nβˆ’1 , and a,b∈An ,
𝐀nβŠ¨Ο†k,n(a,b)⇔ either (a∈{0,e,1} and b=1) or (0<a<e and b=1 and the number of atoms below a is ≀k) or (0<a<e=b and the number of atoms below a is β‰₯k+1).
Proof.
We begin by proving the implication from left to right. Suppose that 𝐀nβŠ¨Ο†k,n(a,b) . Then there exist c11,…,cn+11,…,c1k,…,cn+1k,d1,…,dk∈An such that
b=⋁m=1kdm
and for every positive m≀k both
a∨¬a=c1m∨¬c1m=…=cn+1m∨¬cn+1m;dm=a∨¬a∨¬¬(aβˆ¨β‹i=1n+1cim)
and
1=((⋁i=1n+1cimβ†’a)βˆ§β‹€i,j=1iβ‰ jm+1Β¬(cim∧cjm))∨((⋁i=1n+1cimβ†’Β¬a)βˆ§β‹€i,j=m+2iβ‰ jn+1Β¬(cim∧cjm)).
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 m≀k ,
either (⋁i=1n+1cim≀a and cim∧cjm=0 for all distinct i,j with 1≀i,j≀m+1) or (⋁i=1n+1cim≀¬a and cim∧cjm=0 for all distinct i,j with m+2≀i,j≀n+1).
By the definition of 𝐀n we have two cases: either a∈{0,e,1} or 0<a<e . First, suppose that a∈{0,e,1} . We need to prove that b=1 . To this end, observe that for every m≀k ,
¬¬a≀¬¬(aβˆ¨β‹i=1n+1cim)≀a∨¬a∨¬¬(aβˆ¨β‹i=1n+1cim)=dm,
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 a∈{0,e,1} , we have ¬¬a=1 by (\ref{Eq : tricks for An : Beth completion : 3}). Together with the above display, we obtain dm=1 for every m≀k . By (\ref{Eq : proper Beth completion : total 1}) we conclude that b=1 , as desired.
Next, we consider the case where 0<a<e . In this case, a∨¬a=e by (\ref{Eq : tricks for An : Beth completion : 2}). Therefore, from (\ref{Eq : proper Beth completion : total 2}) it follows that cim∨¬cim=e for all positive m≀k and i≀n+1 . By (\ref{Eq : tricks for An : Beth completion : 2}) this yields
0<cim for all positive m≀k and i≀n+1.
We have two subcases: either the number of atoms below a is ≀k or β‰₯k+1 . First, suppose that it is p≀k . We need to prove that b=1 . As 𝐀n has n atoms by definition, the number of atoms below Β¬a is nβˆ’p by (\ref{Eq : tricks for An : Beth completion : 5}). From (\ref{Eq : proper Beth completion : total 4}) in the case where m=p it follows that
either (⋁i=1n+1cip≀a and cip∧cjp=0 for all distinct i,j with 1≀i,j≀p+1) or (⋁i=1n+1cip≀¬a and cip∧cjp=0 for all distinct i,j with p+2≀i,j≀n+1).
The right hand side of the first line of the above display implies that the sets of atoms below each of the cip for 1≀i≀p+1 must be pairwise disjoint. Moreover, observe that 𝐀n 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 cip . Consequently, there must be at least p+1 distinct atoms below the join of c1p,…,cp+1p . Together with the left hand side of the first line of the above display, this implies that the number of atoms below a is β‰₯p+1 , which is false by assumption. Therefore,
⋁i=1n+1cip≀¬a and cip∧cjp=0 for all distinct i,j with p+2≀i,j≀n+1.
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 cp+2p,…,cn+1p must be at least nβˆ’p . 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 cp+2p,…,cn+1p must be also below Β¬a . As by assumption the number of atoms below Β¬a is precisely nβˆ’p , the set of atoms below Β¬a must coincide with the set of atoms below cp+2pβˆ¨β€¦βˆ¨cn+1p . Therefore, using \eqref{Eq : tricks for An : Beth completion : 4} we obtain
Β¬a=⋁i=1n+1cip.
Together with (\ref{Eq : proper Beth completion : total 3}), this yields
a∨¬a∨¬¬(a∨¬a)=a∨¬a∨¬¬(aβˆ¨β‹i=1n+1cip)=dp.
As 0<a<e by assumption, from (\ref{Eq : tricks for An : Beth completion : 2}) and (\ref{Eq : tricks for An : Beth completion : 3}) it follows that ¬¬(a∨¬a)=¬¬e=1 . Therefore, the above display yields
1=a∨¬a∨1=a∨¬a∨¬¬(a∨¬a)=dp.
By (\ref{Eq : proper Beth completion : total 1}) we conclude that b=1 , as desired. It only remains to consider the case where the number of atoms below a is β‰₯k+1 . We need to prove that b=e . As 𝐀n has n atoms by definition, the number of atoms below Β¬a is ≀nβˆ’kβˆ’1 by (\ref{Eq : tricks for An : Beth completion : 5}). Then consider a positive m≀k . Since nβˆ’kβˆ’1<nβˆ’m , the number of atoms below Β¬a is <nβˆ’m . 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 Β¬a is β‰₯nβˆ’m , we conclude that the first line of (\ref{Eq : proper Beth completion : total 4}) holds. Consequently,
⋁i=1n+1cim≀a.
We will prove that the following holds:
e=a∨¬a≀a∨¬a∨¬¬(aβˆ¨β‹i=1n+1cim)≀a∨¬a∨¬¬(a∨a)=a∨¬a=e.
The first and the last steps above hold by 0<a≀e 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 a=¬¬a , which follows from aβ‰ e and (\ref{Eq : tricks for An : Beth completion : 3b}). Together with (\ref{Eq : proper Beth completion : total 3}), the above display yields dm=e . As this holds for every m≀k , from (\ref{Eq : proper Beth completion : total 1}) it follows that b=e , as desired.
Next we prove the implication from right to left in the statement. Recall from the definition of Ο†k,n that it suffices to find cim,dm for i≀n+1 and m≀k such that
𝐀n⊨(bβ‰ˆβ‹m=1kdm)βŠ“β¨…m=1kψm,n(a,dm,c1m,…,cn+1m).
First, suppose that a∈{0,1} . In this case, b=1 by assumption. Choose cim=0 and dm=1 for all i≀n+1 and m≀k . Clearly, we have
b=1=⋁m=1kdm.
From \eqref{Eq : tricks for An : Beth completion : 1} it follows that for each m≀k we have d(a)=1 and, therefore,
d(a)=1=d(0)=d(cim) for each i≀n+1 and d(a)∨¬¬(aβˆ¨β‹i=1n+1cim)=1∨¬¬a=1=dm,
which proves the validity of the first two conjuncts of ψm,n . Moreover, it holds that
((⋁i=1n+1cimβ†’a)βˆ§β‹€i,j=1iβ‰ jm+1Β¬(cim∧cjm))∨((⋁i=1n+1cimβ†’Β¬a)βˆ§β‹€i,j=m+2iβ‰ jn+1Β¬(cim∧cjm))=((0β†’a)βˆ§β‹€i,j=1iβ‰ jm+1Β¬0)∨((0β†’Β¬a)βˆ§β‹€i,j=m+2iβ‰ jn+1Β¬0)=1.
This establishes \eqref{Eq : to show psi} for the case where a∈{0,1} .
It only remains to consider the case where 0<a<1 . Observe that choosing cimβˆˆπ–Ίπ—(𝐀n) for all i≀n+1 and m≀k guarantees that
d(a)=e=d(cim) for all i≀n+1 and m≀k
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
((⋁i=1n+1cimβ†’a)βˆ§β‹€i,j=1iβ‰ jm+1Β¬(cim∧cjm))∨((⋁i=1n+1cimβ†’Β¬a)βˆ§β‹€i,j=m+2iβ‰ jn+1Β¬(cim∧cjm))=1,
it suffices to choose cim so that one of the following holds:
{c1m,…,cn+1m}=𝖺𝗍𝐀n(a) and cimβ‰ cjm for all i,j∈{1,…,m+1} with iβ‰ j,{c1m,…,cn+1m}=𝖺𝗍𝐀n(Β¬a) and cimβ‰ cjm for all i,j∈{m+2,…,n+1} with iβ‰ j.
We distinguish three cases. First, let a=e . Then b=1 by assumption. Choose cimβˆˆπ–Ίπ—(𝐀n)=𝖺𝗍𝐀n(e) for all i≀n+1 and m≀k such that {c1m,…,cnm} are precisely the n distinct atoms of 𝐀n and let dm=1 for each m≀k . Then condition \eqref{Eq : long equation conditions 1} is satisfied, since m≀k≀nβˆ’1 , and thus m+1≀n . Therefore, to verify \eqref{Eq : to show psi}, it only remains to observe that for each m≀k we have
d(a)∨¬¬(aβˆ¨β‹i=1n+1cim)=d(e)∨¬¬(a∨e)=d(e)∨¬¬e=1=dm,
which is true by \eqref{Eq : tricks for An : Beth completion : 3} and a=e .
Next we consider the case where 0<a<e and |𝖺𝗍𝐀n(a)|=p≀k . Then b=1 by assumption. For all m<p and i≀n+1 consider cimβˆˆπ–Ίπ—π€n(a) such that {c1m,…,cpm}=𝖺𝗍𝐀n(a) and dm=e . Moreover, for all p≀m≀k and i≀n+1 consider cimβˆˆπ–Ίπ—π€n(Β¬a) such that {cp+2m,…,cn+1m}=𝖺𝗍𝐀n(Β¬a) and dm=1 . Then for m<p 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 0<a<e we have
d(a)∨¬¬(aβˆ¨β‹i=1n+1cim)=d(a)∨¬¬(a∨a)=e=dm.
On the other hand, for every m such that p≀m≀k 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 0<a<e , we obtain
d(a)∨¬¬(aβˆ¨β‹i=1n+1cim)=d(a)∨¬¬(a∨¬a)=e∨¬¬e=1=dm.
Since 1=⋁m≀kdm (because dk=1 ), this verifies that \eqref{Eq : to show psi} holds.
It only remains to consider the case where 0<a<e and |𝖺𝗍𝐀n(a)|=pβ‰₯k+1 . In this case, we have b=e by assumption. Then for all i≀n+1 and m≀k consider cimβˆˆπ–Ίπ—π€n(a) such that {c1m,…,cpm}=𝖺𝗍𝐀n(a) . Also choose dm=e for each m≀k . Then \eqref{Eq : long equation conditions 1} it satisfied because m+1≀k+1≀p . Therefore, to conclude the proof of \eqref{Eq : to show psi}, it only remains to observe that for each m≀k we have
d(a)∨¬¬(aβˆ¨β‹i=1n+1cim)=d(a)∨¬¬(a∨a)=e=dm,
which holds by \eqref{Eq : tricks for An : Beth completion : 2}, \eqref{Eq : tricks for An : Beth completion : 3b}, and 0<a<e . 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 nβ‰₯3 and positive k≀nβˆ’1 the formula Ο†k,n defines an implicit operation fk,nβˆˆπ–Ύπ—‘π—pp(𝕍(𝐀n)) such that fk,n𝐀n is total and for every a∈An ,
fk,n𝐀n(a)={1if a∈{0,e,1};1if 0<a<e and |𝖺𝗍𝐀n(a)|≀k;eif 0<a<e and |𝖺𝗍𝐀n(a)|β‰₯k+1.
Proof.
In view of Proposition \ref{Prop : proper Beth completion : varphi is functional}, the pp formula Ο†k,n is functional in 𝐀n . By Cor.~3.11 CKMIMP it is also functional in β„š(𝐀n) . In view of \cref{Cor : proper Beth completion : V(An) = Q(An)}, this means that Ο†k,n is functional in 𝕍(𝐀n) and, therefore, defines an implicit operation fk,nβˆˆπ—‚π—†π—‰pp(𝕍(𝐀n)) . From \cref{Prop : proper Beth completion : varphi is functional} it follows that fk,n𝐀n is total and defined as in the statement. As fk,n𝐀n is total, we can apply Prop.~8.11(ii) CKMIMP to the case where π–ͺ=𝕍(𝐀n)=β„š(𝐀n) and 𝖬={𝐀n} , obtaining that fk,n is extendable. Thus, we conclude that fk,nβˆˆπ–Ύπ—‘π—pp(𝕍(𝐀n)) .
Now, for every nβ‰₯3 let
β„±n={fk,n:k is positive and ≀nβˆ’1}.
Observe that β„±nβŠ†π–Ύπ—‘π—pp(𝕍(𝐀n)) by Corollary \ref{Cor : proper Beth completion : fnk is extendable}. Then consider an β„±n -expansion
β„’β„±n=β„’βˆͺ{β„“f:fβˆˆβ„±n}
of the language β„’ of Heyting algebras and let
𝖑(n)=π•Š(𝕍(𝐀n)[β„’β„±n])
be the corresponding pp expansion of 𝕍(𝐀n) . Our aim is to prove the following.
TheoremΒ 5
Let nβ‰₯3 . Then 𝖑(n) is a congruence preserving Beth companion of 𝕍(𝐀n) .
To this end, recall from Corollary \ref{Cor : proper Beth completion : fnk is extendable} that f𝐀n is total for every fβˆˆβ„±n , whence the algebra
𝐁n=𝐀n[β„’β„±n]
is defined. We begin with the following observation.
PropositionΒ 4
For every nβ‰₯3 we have
𝖑(n)=𝕍(𝐁n) and 𝖑(n)fsi=π•€π•Š(𝐁n).
Moreover, 𝖑(n) is an arithmetical variety.
Proof.
We begin with the following observation.
ClaimΒ 5
We have 𝕍(𝐁n)fsi=π•€π•Š(𝐁n) .
proof}[Proof of the Claim] First, we show that
π–’π—ˆπ—‡(𝐂)=π–’π—ˆπ—‡(𝐂↾ℒ) for every π‚βˆˆπ•€π•Š(𝐁n).
Clearly, it will be enough to prove the above display for an arbitrary π‚βˆˆπ•Š(𝐁n) . The inclusion π–’π—ˆπ—‡(𝐂)βŠ†π–’π—ˆπ—‡(𝐂↾ℒ) is straightforward. To prove the reverse one, consider ΞΈβˆˆπ–’π—ˆπ—‡(𝐂↾ℒ) . From 𝐂≀𝐁n it follows that 𝐂↾ℒ≀(𝐁n)β†Ύβ„’=𝐀n . As 𝐂↾ℒ and 𝐀n are Heyting algebras and the variety of Heyting algebras has the congruence extension property, there exists Ο•βˆˆπ–’π—ˆπ—‡(𝐀n) such that ΞΈ=Ο•β†ΎC . From Prop.~12.13 CKMIMP and the definition of 𝐁n it follows that π–’π—ˆπ—‡(𝐀n)=π–’π—ˆπ—‡(𝐁n) . Therefore, Ο•βˆˆπ–’π—ˆπ—‡(𝐁n) . Together with 𝐂≀𝐁n , this yields ΞΈ=Ο•β†ΎCβˆˆπ–’π—ˆπ—‡(𝐂) , as desired.
Next, we prove 𝕍(𝐁n)fsi=π•€π•Š(𝐁n) . By \cref{Prop : Jonsson lattice : easy} we have 𝕍(𝐁n)fsiβŠ†β„π•Š(𝐁n) . Therefore, it suffices to show that the finitely subdirectly irreducible members of β„π•Š(𝐁n) are precisely the members of π•€π•Š(𝐁n) . To this end, consider a finitely subdirectly irreducible π‚βˆˆβ„π•Š(𝐁n) . Then there exist 𝐃≀𝐁n 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 𝐃↾ℒ≀𝐀n , one can check by inspection that the only meet irreducible congruences of 𝐃↾ℒ are idD and the congruences Ο• of 𝐃↾ℒ with exactly two equivalences, namely, 0/Ο• and 1/Ο• . If ΞΈ=idD , then 𝐂≅𝐃 and, therefore, π‚βˆˆπ•€π•Š(𝐁n) because 𝐃≀𝐁n . On the other hand, if ΞΈ has exactly two equivalence classes 0/ΞΈ and 1/ΞΈ , then 𝐃/ΞΈ is isomorphic to the subalgebra of 𝐁n with universe {0,1} , whence π‚βˆˆπ•€π•Š(𝐁n) . Finally, we show that every member of π•€π•Š(𝐁n) is finitely subdirectly irreducible. Let π‚βˆˆπ•€π•Š(𝐁n) . Then π–’π—ˆπ—‡(𝐂)=π–’π—ˆπ—‡(𝐂↾ℒ) by (\ref{Eq : addendum : answering Luca's question}). Since π‚βˆˆπ•€π•Š(𝐁n) , the definition of 𝐁n guarantees that π‚β†Ύβ„’βˆˆπ•€π•Š(𝐀n) . By inspection one can check that every member of π•€π•Š(𝐀n) is finitely subdirectly irreducible. Consequently, so is 𝐂↾ℒ . By Prop.~2.10 CKMIMP the congruence idC 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 𝕍(𝐁n)=π•€π•Šβ„™(𝕍(𝐁n)fsi)=π•€π•Šβ„™π•€π•Š(𝐁n) .\ Consequently, 𝕍(𝐁n)βŠ†β„š(𝐁n) . As the reverse inclusion always holds, we conclude that 𝕍(𝐁n)=β„š(𝐁n) .
Now, recall from \cref{Cor : proper Beth completion : V(An) = Q(An)} that 𝕍(𝐀n)=β„š(𝐀n) . As 𝐁n=𝐀n[β„’β„±n] , this allows us to apply Thm.~10.5 CKMIMP to the case where π–ͺ=𝕍(𝐀n) , 𝖭={𝐀n} , and 𝕆=β„š , obtaining 𝖑(n)=π•Š(𝕍(𝐀n)[β„’β„±n])=β„š(𝐀n[β„’β„±n])=β„š(𝐁n) . Since β„š(𝐁n)=𝕍(𝐁n) , we obtain 𝖑(n)=𝕍(𝐁n) . Therefore, 𝖑(n)fsi=𝕍(𝐁n)fsi=π•€π•Š(𝐁n) . Lastly, since 𝐁n has a Heyting algebra reduct, the variety 𝕍(𝐁n) is arithmetical (see, e.g., p.~80 BuSa00). \end{proof}
An endomorphism of an algebra 𝐀 is a homomorphism h:𝐀→𝐀 . When h 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 𝐀n for some nβˆˆβ„• induces an automorphism of 𝐀n in the following way.
PropositionΒ 5
Let nβˆˆβ„• and let Οƒ:𝖺𝗍(𝐀n)→𝖺𝗍(𝐀n) be a permutation. Then the map Οƒ*:𝐀n→𝐀n defined for every aβˆˆπ€n as
Οƒ*(a)={1if a=1;⋁σ[𝖺𝗍𝐀n(a)]if aβ‰ 1
is an automorphism of 𝐀n .
We will also make use of the next observation on the automorphisms of 𝐁n .
PropositionΒ 6
The following conditions hold for every nβ‰₯3 :
  1. for every 𝐀≀𝐁n and b∈Bnβˆ’(Aβˆͺ{e}) there exists hβˆˆπ–Ίπ—Žπ—(𝐁n) such that bβ‰ h(b) and a=h(a) for every a∈A ;
  2. for every pair of embeddings g,h:𝐀→𝐁n there exists iβˆˆπ–Ίπ—Žπ—(𝐁n) such that g=i∘h .
Proof.
(\ref{item : proper Beth completion : automorphisms : 1}): Consider 𝐀≀𝐁n and b∈Bnβˆ’(Aβˆͺ{e}) . For every aβˆˆπ–Ίπ—(𝐀) let
Xa=𝖺𝗍𝐁n(a).
We will prove that {Xa:aβˆˆπ–Ίπ—(𝐀)} forms a partition of 𝖺𝗍(𝐁n) . As 𝐀≀𝐁n , for every distinct a,cβˆˆπ–Ίπ—(𝐀) we have Xa∩Xc=βˆ… . Therefore, it only remains to show that for every aβˆˆπ–Ίπ—(𝐁n) there exists cβˆˆπ–Ίπ—(𝐀) such that a∈Xc , i.e., a≀c . Consider aβˆˆπ–Ίπ—(𝐁n) . We begin by showing that e≀⋁𝖺𝗍(𝐀) . If A={0,1} , we have 1βˆˆπ–Ίπ—(𝐀) and, therefore, e≀⋁𝖺𝗍(𝐀)=1 . Then we consider the case where Aβ‰ {0,1} . In this case, there exists a∈A such that 0<a<1 . Observe that Β¬a∈A and 𝖺𝗍𝐀(a)βˆͺ𝖺𝗍𝐀(Β¬a)βŠ†π–Ίπ—(𝐀) . Consequently, using \eqref{Eq : tricks for An : Beth completion : 2} and \eqref{Eq : tricks for An : Beth completion : 4}, we obtain
e=a∨¬a=⋁𝖺𝗍𝐀(a)βˆ¨β‹π–Ίπ—π€(Β¬a)≀⋁𝖺𝗍(𝐀).
Hence, we conclude that e≀⋁𝖺𝗍(𝐀) , as desired. Therefore, a≀⋁𝖺𝗍(𝐀) because aβˆˆπ–Ίπ—(𝐁n) and every atom of 𝐁n is below e . Since aβˆˆπ–Ίπ—(𝐁n) , from a≀⋁𝖺𝗍(𝐀) it follows that a≀c for some cβˆˆπ–Ίπ—(𝐀) . Hence, {Xa:aβˆˆπ–Ίπ—(𝐀)} forms a partition of 𝖺𝗍(𝐁n) , as desired.
Now, observe that 1∈A because 𝐀≀𝐁n . Together with the assumption that bβˆ‰Aβˆͺ{e} , this yields b<e . We will show that there exist aβˆˆπ–Ίπ—(𝐀) and c,d∈Xa such that c≀b and dβ‰°b . We have two cases: either A={0,1} or Aβ‰ {0,1} . First, suppose that A={0,1} . Then 𝖺𝗍(𝐀)={1} and X1=𝖺𝗍(𝐁n) . Since b<e , there exist c,dβˆˆπ–Ίπ—(𝐁n)=X1 such that c≀b and dβ‰°b , as desired.\ Next we consider the case where Aβ‰ {0,1} . Recall from the first part of the proof that {Xa:aβˆˆπ–Ίπ—(𝐀)} is a partition of 𝖺𝗍(𝐁n) . Therefore, 𝖺𝗍𝐁n(b)βŠ†π–Ίπ—(𝐁n)=⋃{Xa:aβˆˆπ–Ίπ—(𝐀)} . Suppose, with a view to contradiction, that for every aβˆˆπ–Ίπ—(𝐀) we have XaβŠ†π–Ίπ—πn(b) or Xaβˆ©π–Ίπ—πn(b)=βˆ… . Then
𝖺𝗍𝐁n(b)=⋃{Xa:aβˆˆπ–Ίπ—(𝐀) and XaβŠ†π–Ίπ—πn(b)}.
It follows that
b=⋁𝖺𝗍𝐁n(b)=⋁⋃{Xa:aβˆˆπ–Ίπ—(𝐀) and XaβŠ†π–Ίπ—πn(b)}=⋁{⋁𝖺𝗍𝐁n(a):aβˆˆπ–Ίπ—(𝐀) and XaβŠ†π–Ίπ—πn(b)}=⋁{aβˆˆπ–Ίπ—(𝐀):XaβŠ†π–Ίπ—πn(b)},
where the first equality holds by \eqref{Eq : tricks for An : Beth completion : 4} and bβ‰ 1 (the latter follows from bβˆ‰A ), the second by \eqref{Eq : at(b) in terms of X_a}, the third by the definition of Xa , and the fourth follows from \eqref{Eq : tricks for An : Beth completion : 4} because aβ‰ 1 (the latter holds because aβˆˆπ–Ίπ—(𝐀) and Aβ‰ {0,1} ). But this is a contradiction to the assumption that bβˆ‰A . Therefore, there exists aβˆˆπ–Ίπ—(𝐀) such that βˆ…βŠŠXaβˆ©π–Ίπ—πn(b)⊊Xa . Consequently, we can choose c∈Xaβˆ©π–Ίπ—πn(b) to obtain c∈Xa such that c≀b and d∈Xaβˆ’π–Ίπ—πn(b) such that dβ‰°b . Thus, in both cases, there exist aβˆˆπ–Ίπ—(𝐀) and c,d∈Bn with
c,d∈Xa,cβˆˆπ–Ίπ—πn(b), and dβ‰°b.
Then let Οƒ:𝖺𝗍(𝐁n)→𝖺𝗍(𝐁n) be a permutation such that
Οƒ[Xa]=Xa for every aβˆˆπ–Ίπ—(𝐀) and Οƒ(c)=d.
Notice that Οƒ exists because c,d∈Xa by the first item of (\ref{Eq : proper Beth completion : sigma fixes the partition : new}). Recall that 𝐁n=𝐀n[β„’β„±n] . Thus, we can consider the automorphism Οƒ*:𝐀n→𝐀n defined in \cref{Prop : proper Beth completion : the auto sigma}, which by Prop.~9.5 CKMIMP is also an automorphism of 𝐁n . Therefore, in order to complete the proof, it only remains to show that Οƒ*(b)β‰ b and Οƒ*(a)=a for every a∈A .
We begin by proving that
Οƒ*(b)=⋁σ[𝖺𝗍𝐁n(b)]β‰₯Οƒ(c)=d.
The first step in the above display holds by the definition of Οƒ* and b<e<1 , 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 Οƒ*(b)β‰ b .
Lastly, we will prove that Οƒ*(a)=a for every a∈A . Consider a∈A . If a=1 , then Οƒ*(a)=a by the definition of Οƒ* . Then we consider the case where aβ‰ 1 . We will prove that
Οƒ*(a)=Οƒ*(⋁𝐀𝖺𝗍𝐀(a))=Οƒ*(⋁𝐁n𝖺𝗍𝐀(a))=⋁𝐁nΟƒ*[𝖺𝗍𝐀(a)]=⋁pβˆˆπ–Ίπ—π€(a)𝐁n(⋁𝐁nΟƒ[𝖺𝗍𝐁n(p)])=⋁pβˆˆπ–Ίπ—π€(a)𝐁n(⋁𝐁n𝖺𝗍𝐁n(p))=⋁𝐁n𝖺𝗍𝐀(a)=⋁𝐀𝖺𝗍𝐀(a)=a.
The above equalities are justified as follows: the first and the last hold by \eqref{Eq : tricks for An : Beth completion : 4} and aβ‰ 1 , the second and the second to last because 𝐀≀𝐁n , 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 p≀a<1 implies pβ‰ 1 , the fifth by the left hand side of (\ref{Eq : proper Beth completion : sigma fixes the partition}), and the sixth because p≀a<1 implies p≀e , whence (\ref{Eq : tricks for An : Beth completion : 4}) guarantees that p=⋁𝐁n𝖺𝗍𝐁n(p) . Thus, we conclude that Οƒ*(a)=a for every a∈A .
(\ref{item : proper Beth completion : automorphisms : 2}): Consider a pair of embeddings g,h:𝐀→𝐁n . As g and h are homomorphisms of bounded lattices, we have g(0)=h(0)=0 and g(1)=h(1)=1 . Therefore, if A={0,1} , we have g=h and we are done letting i be the identity map on Bn .
Then we may assume that Aβ‰ {0,1} , that is, {0,1}⊊A . Since g,h:𝐀→𝐁n are embeddings, both g[𝐀] and h[𝐀] are subalgebras of 𝐁n containing at least an element a other than 0 and 1 . Then they must also contain Β¬a and, therefore, e=a∨¬a∈g[𝐀]∩h[𝐀] by \eqref{Eq : tricks for An : Beth completion : 2}. As e is the second largest element of 𝐁n and g and h are embeddings of lattices, we obtain that 𝐀 possesses a second largest element e* such that g(e*)=h(e*)=e . Moreover, 0<e*<1 because e* is the second largest element to 𝐀 and Aβ‰ {0,1} . If A={0,e*,1} , we have g=h and we are done letting i be the identity map on Bn .
Then we may assume that Aβ‰ {0,e*,1} , that is, {0,e*,1}⊊A . We rely on the following series of observations.
ClaimΒ 6
We have g[𝖺𝗍(𝐀)]βˆͺh[𝖺𝗍(𝐀)]βŠ†{a∈Bn:0<a<e} .
proof}[Proof of the Claim]
By symmetry it suffices to show that g[𝖺𝗍(𝐀)]βŠ†{a∈Bn:0<a<e} . To this end, consider aβˆˆπ–Ίπ—(𝐀) . Then a>0 . Moreover, since e* is the second largest element of 𝐀 and 𝐀 contains an element other than 0,e* , and 1 , from aβˆˆπ–Ίπ—(𝐀) it follows that a<e* . Therefore, 0<a<e* . Since g is a embedding of bounded lattices, we obtain 0=g(0)<g(a)<g(e*) . As we already established g(e*)=e , we conclude that 0<g(a)<e .
ClaimΒ 7
For every aβˆˆπ–Ίπ—(𝐀) we have |𝖺𝗍𝐁n(g(a))|=|𝖺𝗍𝐁n(h(a))| .
Proof.
[Proof of the Claim] Recall that 𝐀n has n atoms by definition. As 𝐁n is an expansion of 𝐀n , we obtain that 𝐁n has n atoms as well. Then consider a∈Bnβˆ’{0,e,1} and observe that |𝖺𝗍𝐁n(a)|≀nβˆ’1 because |𝖺𝗍𝐁n(a)|=n by \eqref{Eq : tricks for An : Beth completion : 4} would imply aβ‰₯e . Recall that β„’β„±n=β„’βˆͺ{β„“f:fβˆˆβ„±n} . Therefore, from \cref{Cor : proper Beth completion : fnk is extendable} and β„“fk,n𝐁n=fk,n𝐀n it follows that for every m≀nβˆ’1 ,
|𝖺𝗍𝐁n(a)|=m⇔for every 0<k≀nβˆ’1 we have β„“fk,n𝐁n(a)={1if m≀k;eif mβ‰₯k+1.
To prove the statement of the claim, consider aβˆˆπ–Ίπ—(𝐀) . By Claim \ref{Claim : proper Beth completion : automorphism : 1} we have 0<g(a),h(a)<e . Then |𝖺𝗍𝐁n(g(a))| is a positive integer m≀nβˆ’1 . In view of (\ref{Eq : proper Beth completion : automorphisms : 2}), for every positive k≀nβˆ’1 ,
β„“fk,n𝐁n(g(a))={1if m≀k;eif mβ‰₯k+1.
Since g:𝐀→𝐁n is an embedding such that g(e*)=e and g(1)=1 , this yields that for every positive k≀nβˆ’1 ,
β„“fk,n𝐀(a)={1if m≀k;e*if mβ‰₯k+1.
As h:𝐀→𝐁n is also an embedding such that h(e*)=e and h(1)=1 , we obtain that for every positive k≀nβˆ’1 ,
β„“fk,n𝐁n(h(a))={1if m≀k;eif mβ‰₯k+1.
Together with (\ref{Eq : proper Beth completion : automorphisms : 2}), this yields |𝖺𝗍𝐁n(h(a))|=m .
ClaimΒ 8
For every a,bβˆˆπ–Ίπ—(𝐀) ,
if aβ‰ b, then 𝖺𝗍𝐁n(g(a))βˆ©π–Ίπ—πn(g(b))=βˆ…=𝖺𝗍𝐁n(h(a))βˆ©π–Ίπ—πn(h(b)).
Proof.
[Proof of the Claim] Suppose that aβ‰ b . By symmetry it suffices to show that 𝖺𝗍𝐁n(g(a))βˆ©π–Ίπ—πn(g(b))=βˆ… . From aβ‰ b and a,bβˆˆπ–Ίπ—(𝐀) it follows that aβˆ§π€b=0 . Consequently, g(a)∧𝐁ng(b)=0 because g:𝐀→𝐁n is an embedding. Therefore, we conclude that 𝖺𝗍𝐁n(g(a))βˆ©π–Ίπ—πn(g(b))=βˆ… .
In view of Claims \ref{Claim : proper Beth completion : automorphism : 2} and \ref{Claim : proper Beth completion : automorphism : 3} there exists a permutation Οƒ:𝖺𝗍(𝐁n)→𝖺𝗍(𝐁n) such that
Οƒ[𝖺𝗍𝐁n(h(a))]=𝖺𝗍𝐁n(g(a)) for every aβˆˆπ–Ίπ—(𝐀).
As 𝐁n=𝐀n[β„’β„±n] , the map Οƒ can also be viewed as a permutation of 𝖺𝗍(𝐀n) . Consequently, \cref{Prop : proper Beth completion : the auto sigma} yields an automorphism Οƒ*:𝐀n→𝐀n , which by Prop.~9.5 CKMIMP is also an automorphism of 𝐁n . To conclude the proof, it only remains to show that g=Οƒ*∘h , for in this case we can take i=Οƒ* .
From the assumption that g,h , and Οƒ* are homomorphisms of bounded lattices it follows that g(1)=h(1)=Οƒ*(1)=1 , whence g(1)=Οƒ*(h(1)) . Therefore, it suffices to show that g(a)=Οƒ*(h(a)) for every a∈Aβˆ’{1} . We will prove that for every a∈Aβˆ’{1} ,
g(a)=g(⋁𝐀𝖺𝗍𝐀(a))=⋁𝐁ng[𝖺𝗍𝐀(a)]=⋁bβˆˆπ–Ίπ—π€(a)𝐁n⋁𝐁n𝖺𝗍𝐁n(g(b))=⋁bβˆˆπ–Ίπ—π€(a)𝐁n⋁𝐁nΟƒ[𝖺𝗍𝐁n(h(b))]=⋁bβˆˆπ–Ίπ—π€(a)𝐁nΟƒ*(h(b))=Οƒ*(h(⋁𝐀𝖺𝗍𝐀(a)))=Οƒ*(h(a)).
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 aβ‰ 1 , the second and the second to last because g,h , 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 g=Οƒ*∘h . \end{proof}
Finalizing the proof of the fact that 𝖑(n) is a congruence preserving Beth companion of 𝕍(𝐀n) (\cref{Thm : proper Beth completion : B(n) is the companion}) requires some further investigation of the variety 𝖑(n) and its properties. While 𝕍(𝐀n) lacks the amalgamation property for every nβ‰₯3 (see Thm.~2 Mak77), this property holds in the pp expansion 𝖑(n) of 𝕍(𝐀n) , 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 π–ͺrfsi is defined as π–ͺrfsi* .} (see also Thm.\ 3 GLAP), together with the observation that 𝖑(n) has the congruence extension property for each nβ‰₯3 .
Given a quasivariety π–ͺ , let
π–ͺrfsi*=π–ͺrfsiβˆͺ{π€βˆˆπ–ͺ:𝐀 is trivial}.
TheoremΒ 6
Let π–ͺ be a quasivariety with the relative congruence extension property such that π–ͺrfsi is closed under nontrivial subalgebras. Then π–ͺ has the amalgamation property if and only if π–ͺrfsi* has the amalgamation property.
To show that 𝖑(n) has the congruence extension property for each nβ‰₯3 , 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 ΞΈ=Ο•β†ΎA . 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 ΞΈ=Ξ·β†ΎA . Recall from Prop.~12.13 CKMIMP that π‚βˆˆπ–ͺ[β„’β„±] implies π–’π—ˆπ—‡π–¬(𝐂)=π–’π—ˆπ—‡π–ͺ(𝐂↾ℒπ–ͺ) , whence Ξ·βˆˆπ–’π—ˆπ—‡π–¬(𝐂) . This yields Ξ·β†ΎBβˆˆπ–’π—ˆπ—‡π–¬(𝐁) and ΞΈ=(Ξ·β†ΎB)β†ΎA because 𝐀≀𝐁≀𝐂 and ΞΈ=Ξ·β†ΎA . Hence, we are done letting Ο•=Ξ·β†ΎB .
PropositionΒ 8
For every nβ‰₯3 the variety 𝖑(n) has the congruence extension property.
Proof.
We recall that every variety of Heyting algebras has the congruence extension property. In particular, 𝕍(𝐀n) has the congruence extension property for every nβ‰₯3 . Therefore, \cref{Prop : CEP preserved in pp exp} yields that the pp expansion 𝖑(n) of 𝕍(𝐀n) has the congruence extension property.
PropositionΒ 9
For every nβ‰₯3 the variety 𝖑(n) has the amalgamation property.
Proof.
Recall from \cref{Prop : proper Beth completion : B(n) has only the CEP} that the variety 𝖑(n) has the congruence extension property. Moreover, 𝖑(n)fsi 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 𝖑(n) has the amalgamation property, it suffices to show that 𝖑(n)fsi* has the amalgamation property. To this end, consider a pair of embeddings h1:𝐀→𝐁 and h2:𝐀→𝐂 with 𝐀,𝐁,π‚βˆˆπ–‘(n)fsi* . We need to find a pair of embeddings g1:𝐁→𝐃 and g2:𝐂→𝐃 with πƒβˆˆπ–‘(n)fsi* such that g1∘h1=g2∘h2 .
We have two cases depending on whether 𝐀 is trivial or nontrivial. First, suppose that 𝐀 is trivial. As 𝖑(n)fsi 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 𝖑(n)fsi has a trivial subalgebra. Since 𝐀 embeds into 𝐁 and 𝐂 , this yields 𝐁,π‚βˆ‰π–‘(n)fsi . Therefore, 𝐁 and 𝐂 are trivial because 𝐁,π‚βˆˆπ–‘(n)fsi* . Consequently, 𝐀,𝐁 , and 𝐂 are all trivial and the embeddings h1:𝐀→𝐁 and h2:𝐀→𝐂 are isomorphisms. Therefore, we may assume that 𝐀=𝐁=𝐂 and that h1 and h2 are the identity map i on A . Hence, letting 𝐃=𝐀 and g1=g2=i , we are done.
Next we consider the case where 𝐀 is nontrivial. Since 𝐀 embeds into 𝐁 and 𝐂 , we obtain that 𝐁 and 𝐂 are also nontrivial. Together with 𝐁,π‚βˆˆπ–‘(n)fsi* , this yields 𝐁,π‚βˆˆπ–‘(n)fsi . Recall from \cref{Prop : B(n) : proper Beth completion : arithmetical} that 𝖑(n)fsi=π•€π•Š(𝐁n) , whence 𝐁,π‚βˆˆπ•€π•Š(𝐁n) . Therefore, we may assume that 𝐁=𝐂=𝐁n and that h1 and h2 are embeddings of 𝐀 into 𝐁n . By Proposition \ref{Prop : proper Beth completion : automorphisms}(\ref{item : proper Beth completion : automorphisms : 2}) there exists iβˆˆπ–Ίπ—Žπ—(𝐁n) such that h1=i∘h2 . Let 𝐃=𝐁n , g2=i , and g1 the identity map on Bn . Clearly, g1,g2:𝐁n→𝐁n are embeddings such that g1∘h1=h1=i∘h2=g2∘h2 .
We are now ready to prove \cref{Thm : proper Beth completion : B(n) is the companion}.
Proof.
Recall that 𝖑(n) is a pp expansion of 𝕍(𝐀n) . Moreover, since 𝕍(𝐀n) has the congruence extension property, we can apply Thm.~12.4(ii) CKMIMP, obtaining that 𝖑(n) is congruence preserving. Hence, by Thm.~11.6 CKMIMP it will be enough to prove that 𝖑(n) 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 𝖑(n) is an arithmetical variety with the amalgamation property. Therefore, in view of Cor.~7.16 CKMIMP, it will be enough to show that every π‚βˆˆπ–‘(n)fsi lacks proper 𝖑(n) -epic subalgebras. To this end, consider π€β‰€π‚βˆˆπ–‘(n)fsi with 𝐀≀𝐂 proper. Then there exists b∈Cβˆ’A . Moreover, we may assume that 𝐂≀𝐁n by Proposition \ref{Prop : B(n) : proper Beth completion : arithmetical}, whence 𝐀≀𝐂≀𝐁n .
Let i be the identity map on 𝐁n . As iβˆˆπ–Ύπ—‡π–½(𝐁n) and b∈C , to conclude the proof, it will be enough to find some hβˆˆπ–Ύπ—‡π–½(𝐁n) such that hβ†ΎA=iβ†ΎA and h(b)β‰ i(b) . For, by considering the restrictions of h and i to 𝐂≀𝐁n , we obtain that 𝐀≀𝐂 is not 𝖑(n) -epic, as desired.
We have two cases: either eβˆ‰A or e∈A . First, suppose that eβˆ‰A . Since 𝐀≀𝐁n , we have 𝐀↾ℒ≀(𝐁n)β†Ύβ„’=𝐀n . Together with eβˆ‰A and \eqref{Eq : tricks for An : Beth completion : 2}, this yields A={0,1} . Then 0<b because bβˆ‰A . Let aβˆˆπ–Ίπ—πn(b) and consider the map h:𝐁n→𝐁n defined for every c∈Bn as
h(c)={1if a≀c;0if aβ‰°c.
Since hβˆˆπ–Ύπ—‡π–½(𝐀n) and 𝐁n=𝐀n[β„’β„±n] , from Prop.~9.5 CKMIMP it follows that hβˆˆπ–Ύπ—‡π–½(𝐁n) . Moreover, aβˆˆπ–Ίπ—πn(b) and the definition of h imply h(b)=1 . Then h(b)β‰ b because bβˆ‰A={0,1} . Thus, h,i:𝐁n→𝐁n are homomorphisms such that h(b)β‰ b=i(b) and hβ†ΎA=iβ†ΎA (the latter because A={0,1} and both h and i preserve the constants 0 and 1 ).
Lastly, we consider the case where e∈A . As 𝐀≀𝐂 is proper and 𝐂≀𝐁n , there exists b∈Cβˆ’(Aβˆͺ{e})βŠ†Bnβˆ’(Aβˆͺ{e}) . By Proposition \ref{Prop : proper Beth completion : automorphisms}(\ref{item : proper Beth completion : automorphisms : 1}) there also exists hβˆˆπ–Ίπ—Žπ—(𝐁n) such that bβ‰ h(b) and a=h(a) for every a∈A . Thus, h,i:𝐁n→𝐁n are homomorphisms such that hβ†ΎA=iβ†ΎA and h(b)β‰ b=i(b) .
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 𝖑(n) is a congruence preserving Beth companion of 𝕍(𝐀n) by Theorem \ref{Thm : proper Beth completion : B(n) is the companion}, it will be enough to show that 𝖑(n) is not equational. Suppose the contrary, with a view to contradiction. Then let a be an atom of 𝐁n and consider 𝐂=𝖲𝗀𝐁n(a) . The following is an immediate consequence of the definition of 𝐂 .
ClaimΒ 9
The universe of 𝐂 is {0,a,Β¬a,e,1} . Moreover, the Heyting algebra reduct of 𝐂 is isomorphic to 𝐀2 with minimum 0 , maximum 1 , second largest element e , and atoms a and Β¬a .
As a is an atom of 𝐁n and 𝐀n shares its bounded lattice reduct with 𝐁n , the number of atoms of 𝐀n below a is 1 . Since 𝐀n has nβ‰₯3 atoms, from (\ref{Eq : tricks for An : Beth completion : 5}) it follows that the number of atoms of 𝐀n below Β¬a is nβˆ’1β‰₯3βˆ’1β‰₯2 . Therefore, from \cref{Cor : proper Beth completion : fnk is extendable} it follows that β„“f1,n𝐁n(a)=1 and β„“f1,n𝐁n(Β¬a)=e . As 𝐂≀𝐁n , we obtain
β„“f1,n𝐂(a)=1andβ„“f1,n𝐂(Β¬a)=e.
Recall from the assumptions that 𝖑(n) is equational. Therefore, by Rem.~11.12(vi) CKMIMP it is faithfully term equivalent relative to 𝕍(𝐀n) to a Beth companion 𝖬 of 𝕍(𝐀n) induced by implicit operations defined by conjunctions of equations. By Thm.~10.4 CKMIMP the Beth companion 𝖬 is of the form 𝕍(𝐀n)[β„’β„±*] with β„±βŠ†π–Ύπ—‘π—eq(𝕍(𝐀n)) and β„’β„±* an β„± -expansion of the language β„’ of Heyting algebras. Furthermore, recall that 𝖑(n) is a variety by \cref{Prop : B(n) : proper Beth completion : arithmetical}. Therefore, from Rem.~11.12(v) CKMIMP it follows that the class 𝕍(𝐀n)[β„’β„±*] is also a variety.
Let Ο„ and ρ be the maps witnessing the fact that 𝖑(n) and 𝕍(𝐀n)[β„’β„±*] are faithfully term equivalent relative to 𝕍(𝐀n) . We may assume that for every πƒβˆˆπ–‘(n) ,
Ο„(𝐃)βˆˆπ•(𝐀n)[β„’β„±*] and 𝐃↾ℒ=Ο„(𝐃)β†Ύβ„’.
As 𝐂≀𝐁nβˆˆπ–‘(n) and 𝖑(n) is a variety by \cref{Prop : B(n) : proper Beth completion : arithmetical}, we have π‚βˆˆπ–‘(n) . Then Ο„(𝐂)βˆˆπ•(𝐀n)[β„’β„±*] by the left hand side of (\ref{Eq : proper Beth completion : f on A is asymmetric : 23}). Consequently, there exists πƒβˆˆπ•(𝐀n) 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 𝐀2 with atoms a and Β¬a 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 a and Β¬a , thus obtaining an automorphism Οƒ*:𝐃→𝐃 with
Οƒ*(a)=Β¬a and Οƒ*(1)=1.
Moreover, from Ο„(𝐂)=𝐃[β„’β„±*] it follows that 𝐂=ρτ(𝐂)=ρ(𝐃[β„’β„±*]) . Together with (\ref{Eq : proper Beth completion : f on A is asymmetric : 1}), this implies
ρ(β„“f1,n)𝐃[β„’β„±*](a)=1 and ρ(β„“f1,n)𝐃[β„’β„±*](Β¬a)=e.
Recall from Prop.~10.22(ii) CKMIMP that there exists gβˆˆπ–Ύπ—‘π—pp(𝕍(𝐀n)) such that
ρ(β„“f1,n)𝐃[β„’β„±*]=g𝐃.
Together with the left hand side of (\ref{Eq : proper Beth completion : f on A is asymmetric : 3}), this yields g𝐃(a)=1 . As the implicit operation g is preserved by homomorphisms, we can apply the automorphism Οƒ* of 𝐃 in (\ref{Eq : proper Beth completion : f on A is asymmetric : 2}) to deduce
g𝐃(Β¬a)=g𝐃(Οƒ*(a))=Οƒ*(g𝐃(a))=Οƒ*(1)=1
and, therefore, ρ(β„“f1,n)𝐃[β„’β„±*](Β¬(a))=1 by \eqref{Eq : g = rho-ell-f}. Since 1β‰ e , this contradicts the right hand side of (\ref{Eq : proper Beth completion : f on A is asymmetric : 3}). Hence, we conclude that 𝖑(n) is a congruence preserving Beth companion of 𝕍(𝐀n) that is not equational.

References

[4]Β 
L.~Carai, M.~Kurtzhals, and T.~Moraschini. The theory of implicit operations. Available on arXiv, 2025.
Exit Reading PDF XML


Table of contents
  • Introduction
  • A variety with a pp expansion that is a proper quasivariety
  • A nonequational congruence preserving Beth companion
  • References

Export citation

Copy and paste formatted citation
Placeholder

Download citation in file


Share


RSS

  • About Publisher
Powered by PubliMill  •  Privacy policy