An n -ary partial function on a set X is a function f : Y → X for some Y ⊆ X n . 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.

In other words, φ is functional in 𝖪 when

In this case, φ induces an n -ary partial function φ 𝐀 on each 𝐀 ∈ 𝖪 with domain

defined for every ⟨ a 1 , … , a n ⟩ ∈ 𝖽 𝗈 𝗆 ( φ 𝐀 ) as φ 𝐀 ( a 1 , … , a n ) = b , where b is the unique element of A such that 𝐀 ⊨ φ ( a 1 , … , a n , b ) . Consequently,

is an n -ary partial function on 𝖪 .

In elementary classes, implicit operations admit the following description (see Thm.~3.9 CKMIMP).

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).

Consider the linearly ordered Heyting algebra 𝐂 8 with universe

We consider the algebra 𝐀 obtained by endowing 𝐂 8 with a constant for the element a 5 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:

Our aim is to prove the following.

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 − { a 4 } is the universe of a subalgebra 𝐀 − { a 4 } of 𝐀 .

proof}[Proof of the Claim] As 𝐀 − { a 4 } is a subalgebra of 𝐀 , it suffices to prove the inclusion 𝕊 ( 𝐀 ) ⊆ { 𝐀 , 𝐀 − { a 4 } } , which amounts to 𝖲 𝗀 𝐀 ( ∅ ) = A ∖ { a 4 } . First, observe that 𝖲 𝗀 𝐀 ( ∅ ) contains the interpretations 0 , a 5 , and 1 of the constants. As

we conclude that 𝖲 𝗀 𝐀 ( ∅ ) contains a 1 , a 2 , a 3 , and a 6 as well. Hence, 𝖲 𝗀 𝐀 ( ∅ ) = A ∖ { a 4 } .

Proof.

[Proof of the Claim] It suffices to show that 𝖢 𝗀 𝐂 ( 1 , a ) is the monolith of 𝐂 . First, observe that 𝖢 𝗀 𝐂 ( 1 , a ) ∈ 𝖢 𝗈 𝗇 ( 𝐂 ) − { i d C } because a < 1 , where 1 is the maximum of 𝐂 . Then consider θ ∈ 𝖢 𝗈 𝗇 ( 𝐂 ) − { i d C } . As θ ≠ i d C , 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

is a congruence of 𝐀 − { a 4 } . Then let

Proof.

[Proof of the Claim] Observe that all 𝐀 , 𝐀 − { a 4 } , 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 𝕍 ( 𝐀 ) s i ⊆ ℍ 𝕊 ( 𝐀 ) . 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 𝐀 − { a 4 } are 𝐀 − { a 4 } 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 𝖢 𝗀 𝐀 ( a 6 , 1 ) = A × A . Observe that ⟨ 1 , 0 ⟩ = ⟨ a 4 * a 6 , a 4 * 1 ⟩ ∈ 𝖢 𝗀 𝐀 ( a 6 , 1 ) . As the lattice reduct of 𝐀 is a chain with extrema 0 and 1 , this guarantees that 𝖢 𝗀 𝐀 ( a 6 , 1 ) = A × A .

Lastly, we prove that, up to isomorphism, the only nontrivial homomorphic images of 𝐀 − { a 4 } are 𝐀 − { a 4 } and 𝐁 . By the definition of 𝐁 it will be enough to show that for every ϕ ∈ 𝖢 𝗈 𝗇 ( 𝐀 − { a 4 } ) ,

Consider ϕ ∉ { i d A − { a 4 } , θ } . Observe that the definition of θ and Claim \ref{Claim : new claim on B chain SI} guarantee that θ ⊊ ϕ . Therefore, there exist c , d ∈ A − { a 4 } such that ⟨ c , d ⟩ ∈ ϕ − θ . From the definition of θ it follows that

As c ≠ d and the lattice reduct of 𝐀 − { a 4 } is a chain, we can assume that c < d . From c < d , the right hand side of the above display, and the fact that a 6 is the second largest element of A − { a 4 } it follows that c < a 6 , whence c ≤ a 5 . Consequently,

and, therefore, ⟨ 1 , 0 ⟩ = ⟨ □ a 5 , □ 1 ⟩ ∈ ϕ . As before, this yields ϕ = ( A − { a 4 } ) × ( A − { a 4 } ) .

Consider the pp formula

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 𝕍 ( 𝐀 ) s i 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 𝕍 ( 𝐀 ) s i = 𝕀 ( { 𝐀 , 𝐀 − { a 4 } , 𝐁 } ) . As 𝐀 − { a 4 } ≤ 𝐀 , we have 𝕍 ( 𝐀 ) s i ⊆ 𝕀 𝕊 ( { 𝐀 , 𝐁 } ) . 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

the definition of φ guarantees that 𝐀 ⊨ φ ( a , a 3 ) . Therefore, it only remains to show that b = a 3 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 ∈ { a 2 , a 5 , a 6 } . Together with ◇ [ A ] = { a 1 , a 3 , a 5 , 1 } and a + b = ◇ c , this implies a + b = a 5 From the definition of + it thus follows that b = a 3 , as desired.

Then we consider the case where a ≠ 0 . Since a + a 1 = a 1 = ◇ a 1 , the definition of φ guarantees that 𝐀 ⊨ φ ( a , a 1 ) . Therefore, it only remains to show that b = a 1 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 ∈ { a 1 , a 2 } . Together with ◇ [ A ] = { a 1 , a 3 , a 5 , 1 } and a + b = ◇ c , this implies a + b = a 1 From the definition of + it thus follows that b = a 1 .

Next we consider the case of 𝐁 = ( 𝐀 − { a 4 } ) / θ . Since 𝐀 − { a 4 } ≤ 𝐀 the definition of θ guarantees that for every a , b ∈ A − { a 4 } ,

Then let a ∈ A − { a 4 } . As before, we have two cases: either a = 0 or a ≠ 0 . First, suppose that a = 0 . Since

from ⟨ a 6 , 1 ⟩ ∈ θ it follows that

By the definition of φ this guarantees that 𝐁 ⊨ φ ( a / θ , a 6 / θ ) . Therefore, it only remains to show that b / θ = a 6 / θ for every b ∈ A − { a 4 } such that 𝐁 ⊨ φ ( a / θ , b / θ ) . Consider b ∈ A − { a 4 } such that 𝐁 ⊨ φ ( a / θ , b / θ ) . Let c ∈ A − { a 4 } be the element given by the right hand side of (\ref{Eq : Miriam new equation}). As a = 0 , we have a + 𝐀 b ∈ { a 2 , a 5 , a 6 } . Together with ◇ c ∈ ◇ [ A − { a 4 } ] = { a 1 , a 3 , 1 } , the right hand side of (\ref{Eq : Miriam new equation}) ensures that a + 𝐀 b = a 6 . By the definition of + we obtain b ∈ { a 6 , 1 } . As ⟨ a 6 , 1 ⟩ ∈ θ , we conclude that b / θ = a 6 / θ , as desired. Then we consider the case where a ≠ 0 . In this case, a + 𝐀 a 1 = a 1 = ◇ 𝐀 a 1 . Therefore, 𝐁 ⊨ φ ( a / θ , a 1 / θ ) by the definition of φ . It only remains to show that b / θ = a 1 / θ for every b ∈ A − { a 4 } such that 𝐁 ⊨ φ ( a / θ , b / θ ) . Consider b ∈ A − { a 4 } such that 𝐁 ⊨ φ ( a / θ , b / θ ) . As before, let c ∈ A − { a 4 } be the element given by right hand side of (\ref{Eq : Miriam new equation}). Since a ≠ 0 , we have a + 𝐀 b ∈ { a 1 , a 2 } . Together with ◇ c ∈ ◇ [ A − { a 4 } ] = { a 1 , a 3 , 1 } and the right hand side of (\ref{Eq : Miriam new equation}), it follows that a + 𝐀 b = a 1 . By the definition of + we obtain b = a 1 , whence b / θ = a 1 / θ .

By \cref{Claim : varphi in ext} the formula φ defines some f ∈ 𝖾 𝗑 𝗍 p p ( 𝕍 ( 𝐀 ) ) . Consider the f -expansion ℒ f of ℒ 𝕍 ( 𝐀 ) obtained by adding a new unary function symbol g f 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 − { a 4 } is the universe of a subalgebra 𝐂 of 𝐀 [ ℒ ℱ ] . Then from the definition of 𝖬 it follows that

Now recall that

As θ is a congruence of 𝐀 − { a 4 } = 𝐂 ↾ ℒ 𝕍 ( 𝐀 ) which, moreover, is compatible with the new operation g f 𝐂 = 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

Since ⟨ a 6 , 1 ⟩ ∈ θ and 𝐂 ↾ ℒ 𝕍 ( 𝐀 ) = 𝐀 − { a 4 } ≤ 𝐀 , this yields

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 g f 𝐃 [ ℒ ℱ ] = f 𝐃 , this yields

Therefore, g f 𝐂 / θ ( 0 / θ ) = 1 / θ 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}

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

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

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).}

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.

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.

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 𝕍 ( 𝐀 n ) f s i .

Proof.

By Proposition \ref{Prop : Jonsson lattice : easy} we have 𝕍 ( 𝐀 n ) f s i ⊆ ℍ 𝕊 ( 𝐀 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 ) f s i ⊆ ℍ 𝕊 ( 𝐀 n ) ⊆ 𝕍 ( 𝐀 n ) , this yields 𝕍 ( 𝐀 n ) f s i = 𝕀 ( 𝐀 0 , … , 𝐀 n ) . Lastly, the equality 𝕀 ( 𝐀 0 , … , 𝐀 n ) = 𝕀 𝕊 ( 𝐀 n ) is an immediate consequence of the definition of 𝐀 0 , … , 𝐀 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

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

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 :

Moreover, for every 𝐁 ≤ 𝐀 n and a ∈ B the following holds:

We also rely on the following properties that hold in every Heyting algebra. First, for every a 1 , … , a m ∈ A κ ,

Second, for every a , b ∈ A κ ,

Now, fix n ≥ 3 . For each positive m ≤ n − 1 let s m , n and d denote the terms

where x , z 1 m , … , z n + 1 m are variables. Then let ψ m , n ( x , y , z 1 m , … , z n + 1 m ) be the conjunction of the following formulas:

For each positive k ≤ n − 1 let γ k , n ( x , y , z 1 1 , … , z n + 1 1 , … , z 1 k , … , z n + 1 k , w 1 , … , w k ) be the formula

and define

Observe that φ k , n ( x , y ) is a pp formula for every n ≥ 3 and positive k ≤ n − 1 . We will prove the following.

Proof.

We begin by proving the implication from left to right. Suppose that 𝐀 n ⊨ φ k , n ( a , b ) . Then there exist c 1 1 , … , c n + 1 1 , … , c 1 k , … , c n + 1 k , d 1 , … , d k ∈ A n such that

and for every positive m ≤ k 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 m ≤ k ,

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 ,

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 d m = 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 c i m ∨ ¬ c i m = e for all positive m ≤ k and i ≤ n + 1 . By (\ref{Eq : tricks for An : Beth completion : 2}) this yields

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

The right hand side of the first line of the above display implies that the sets of atoms below each of the c i p 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 c i p . Consequently, there must be at least p + 1 distinct atoms below the join of c 1 p , … , c p + 1 p . 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,

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 c p + 2 p , … , c n + 1 p 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 c p + 2 p , … , c n + 1 p 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 c p + 2 p ∨ … ∨ c n + 1 p . Therefore, using \eqref{Eq : tricks for An : Beth completion : 4} we obtain

Together with (\ref{Eq : proper Beth completion : total 3}), this yields

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

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,

We will prove that the following holds: