Existentially Closed Brouwerian Semilattices
Luca Carai Silvio Ghilardi




Interplay of dust alignment, grain growth and magnetic fields in polarization: lessons from the emission-to-extinction ratio
    L. Fanciullo, 1
        V. Guillet, 1	
	F. Boulanger, 1
          A. P. Jones 1
          
    
============================================================================================================================







date




 The variety of Brouwerian semilattices is amalgamable and locally finite, hence by well-known results <cit.>, it has a  model completion (whose models are the existentially closed structures). In this paper, we supply for such a model completion  a finite and rather simple axiomatization. 






§ INTRODUCTION
 

In algebraic logic some attention has been paid to the class of existentially closed structures in varieties coming from the algebraization of common propositional logics. In fact, there are relevant cases where such classes are elementary: this includes, besides the easy case of Boolean algebras, also Heyting algebras <cit.>, diagonalizable algebras <cit.> and some universal classes related to temporal logics <cit.>,<cit.>. However, very little is known about the related axiomatizations, with the remarkable exception of the 
case of the locally  finite amalgamable varieties of Heyting algebras recently investigated in <cit.> and of the simpler cases of posets and semilattices studied in <cit.>. In this paper, we use a 
methodology similar to <cit.> (relying on classifications of minimal extensions) in order to investigate the case of Brouwerian semilattices, i.e. the algebraic structures corresponding to the implication-conjunction fragment of intuitionistic logic. We 
obtain the finite axiomatization reported below, which is similar in spirit to the axiomatizations from <cit.> (in the sense that we also have kinds of `density' and 
`splitting' conditions). The main technical problem  we must face for this result (making axioms formulation slightly more complex and proofs much more involved) 

is the lack of joins in the language of Brouwerian semilattices. 


 



 §.§ Statement of the main result

The first researcher to consider the Brouwerian semilattices as algebraic objects in their own right was W. C. Nemitz in <cit.>.
A Brouwerian semilattice is a poset (P, ≤) having a greatest element (which we denote with 1),
inf's of pairs (the inf of { a,b } is called `meet' of a and b and denoted with a ∧ b)
and relative pseudo-complements (the relative pseudo-complement of a and b is denoted with a → b).
We recall that a→ b is characterized by the the following property: for every c ∈ P we have

    c ≤ a → b   iff   c ∧ a ≤ b.


Brouwerian semilattices can also be defined in an alternative way as algebras over the signature 1, ∧, →, subject to the following equations

    [                         a ∧ a=a                                              a ∧ (a → b)= a ∧ b;                   a ∧ b = b ∧ a                                                 b ∧ (a → b) = b;       a ∧ (b ∧ c) = (a ∧ b) ∧ c                                 a → (b ∧ c) = (a → b) ∧ (a → c);                        a ∧ 1= a                                                         a → a=1 ]

In case this equational axiomatization is adopted, the partial order ≤ is recovered via the definition
a ≤ b iff a ∧ b= a.

By a result due to Diego and McKay <cit.>, Brouwerian semilattices are locally finite (meaning that all finitely generated Brouwerian semilattices are finite); since they are also amalgamable, it follows <cit.> that the theory of Brouwerian semilattices has a model completion.
We prove that such a model completion 
is given by the above set of axioms for the theory of Brouwerian semilattices together with the three additional axioms (Density1, Density2, Splitting) below.


We use the shorthand a ≪ b to mean that a ≤ b and b → a=a.


[Density 1] For every c there exists an element b different from 1 such that b ≪ c. 


[Density 2] For every c,a_1,a_2,d such that a_1,a_2 ≠ 1, a_1 ≪ c, a_2 ≪ c and d → a_1=a_1, d → a_2=a_2 there exists an element b different from 1 such that:

    a_1 ≪ b 
    
    	a_2 ≪ b 
    
    	b ≪ c 
    
        d → b=b


[Splitting] For every a,b_1,b_2 such that 1 ≠ a ≪ b_1  b_2 there exist elements a_1 and a_2 different from 1 such that:

    b_1 ≥ a_1,   b_2 ≥ a_2 
        a_2 → a = a_1  
        a_1 → a = a_2 
        a_2 → b_1 = b_2 → b_1 
        a_1 → b_2 = b_1 → b_2




As testimony of the usefulness of this result, the following proposition shows some properties of the existentially closed Brouwerian semilattices that can be deduced from our investigation as an easy exercise.


Let L be an existentially closed Brouwerian semilattice. Then:


  * L has no bottom element.

  * If a,b ∈ L are incomparable, i.e. a ≰ b and b ≰ a, then the join of a and b in L does not exist.

  * There are no meet-irreducible elements in L.



The paper is structured as follows: Section <ref> gives the basic notions and definitions, in particular it describes the finite duality and characterizes the existentially closed structures by means of embeddings of finite extensions of finite sub-structures. In Section <ref> we investigate the minimal extensions and use them to give an intermediate characterization of the existentially closed structures. Section <ref> focuses on the axiomatization, it is split into two subsections: the first about the Splitting axiom and the second about the Density axioms. Finally, in Section <ref> we present and prove some properties of the existentially closed structures whose validity follows from this investigation.




§ PRELIMINARY BACKGROUND
 

A co-Brouwerian semilattice, CBS for short, is a structure obtained by reversing the order of a Brouwerian semilattice.

We will work with CBSes instead of Brouwerian semilattices.



A poset (P, ≤) is said to be a co-Brouwerian semilattice if it has a least element, which we denote with 0, and for every a,b ∈ P there exists the sup of { a,b }, which we call join of a and b and denote with a ∨ b, and the difference a - b satisfying for every c ∈ P

    a-b ≤ c    iff    a ≤ b ∨ c.

a ≪ b will mean that a ≤ b and b-a=b.
 

Clearly, there is also an alternative equational definition for co-Brouwerian semilattices (which we leave to the reader, because it is dual to the equational definition for Brouwerian semilattices given above).


Moreover, we will call co-Heyting algebras the structures obtained reversing the order of Heyting algebras. Obviously any co-Heyting algebra is a CBS.


Let A,B be co-Brouwerian semilattices.
A map f:A → B is a morphism of co-Brouwerian semilattices if it preserves 0, the join and difference of any two elements of A.


Notice that such a morphism  f is an order preserving map because, for any a,b elements of a co-Brouwerian semilattice, we have a ≤ b iff a ∨ b= b.



Let L be a CBS.

We say that g ∈ L is join-irreducible iff for every n ≥ 0 and b_1, …, b_n ∈ L, we have that

    g ≤ b_1 ∨…∨ b_n    implies   g ≤ b_i  for some  i=1, …, n.

Notice that taking n=0 we obtain that join-irreducibles are different from 0.



Let L be a CBS and g ∈ L. Then the following conditions are equivalent:


  * g is join-irreducible. 

  * g ≠ 0 and for any b_1,b_2 ∈ L we have that g ≤ b_1 ∨ b_2 implies g ≤ b_1 or g ≤ b_2. 

  * For every n ≥ 0 and b_1, …, b_n ∈ L we have that

 g = b_1 ∨…∨ b_n implies g = b_i for some i=1, …, n. 

  * g ≠ 0 and for any b_1,b_2 ∈ L we have that g = b_1 ∨ b_2 implies g = b_1 or g = b_2. 

  * g ≠ 0 and for any a ∈ L we have that g-a=0 or g-a=g. 




The implications <ref> ⇔ <ref>, <ref> ⇔ <ref> and <ref> ⇒ <ref> are straightforward. For the remaining ones see Lemma 2.1 in <cit.>.



Let L be a CBS and a ∈ L.

A join-irreducible component of a is a maximal element among the join-irreducibles of L that are smaller than or equal to a.


 
The following is a list of facts that might be used without explicit mention.

These identities hold in any CBS:

    0-a=0         a-0=a 
    
    (a-b) ∨ b=a ∨ b         (a-b) ∨ a= a 
    
    (a-b) ∨ (a-(a-b))=a         a-(a-(a-b))=a-b 
    
    (a_1 ∨⋯∨ a_n)-b=     (a_1-b)∨⋯∨ (a_n-b) 
      
    a-(b_1 ∨⋯∨ b_n)=     ((a-b_1)- ⋯ )-b_n

In particular

    (a-b)-c=(a-c)-b

Furthermore in any CBS:

    a ≤ b        iff     a-b=0 
    if   b ≤ c   then   b-a    ≤ c-a   and   a-c ≤ a-b

The following facts are true in any finite CBS:

    a = ⋁{join-irreducible components of  a  }
    
    a-b=  ⋁{ g   |   g     is a join-irreducible component of  a  such that  g ≰ b  }

Moreover, in a finite CBS, g is join-irreducible iff it has a unique predecessor, i.e. a maximal element among the elements strictly smaller than g, and in that case we denote it by g^- and it is equal to ⋁_a < g a.

Recall that a ≪ b means a ≤ b and b-a=b. Thus, in any finite CBS, a ≪ b if and only if a ≤ b and there are no join-irreducible components of b that are less than or equal to a. Finally, if g is join-irreducible then g^- ≪ g.



Let (P, ≤) be a poset. For any a ∈ P we define a = { p ∈ P   |   p ≤ a } and for any A ⊆ P we define A= ⋃_a ∈ A a. A subset D ⊆ P such that D=  D is called a downset, i.e. a downward closed subset, of P. The downsets a and A are called the downsets generated by a and A.

Given a poset P, the set of downsets of P denoted by 𝒟(P) has naturally a structure of CBS given by the usual inclusion of subsets. Joins coincide with the union of subsets and the zero element with the empty subset. It turns out that the difference of two downsets A,B ∈𝒟(P) is A-B=  (A ∖ B).

Note that if P is finite then also 𝒟(P) is. In that case any downset A ∈𝒟(P) is generated by the set of its maximal elements and for any A,B ∈𝒟(P) we have that A-B is the downset generated by the maximal elements of A that are not in B. Moreover the join-irreducibles of 𝒟(P) are the downsets of the form p for p ∈ P and the downsets generated by the maximal elements of a given downset are its join-irreducible components. Notice that this is not always the case when P is infinite.

Finally, when P is finite, for A,B ∈𝒟(P) satisfying A ≪ B means that A ⊆ B and A does not contain any maximal element of B. 




 §.§ Locally finiteness


 
The variety of CBSes is locally finite.


 We just sketch the proof 

first presented in <cit.>.


A CBS L is subdirectly irreducible iff L ∖{ 0 } has a least element, or equivalently L has a single atom, i.e. a minimal element different from 0.

Let L be subdirectly irreducible and u the least element of L ∖{ 0 }. Then L ∖{ u } is a sub-CBS of L. This implies that any generating set of L must contain u.

Moreover if L is generated by n elements then L ∖{ u } can be generated by n-1 elements. It follows that the cardinality of subdirectly irreducible CBSes generated by n elements is bounded by # F_n-1 +1 where F_m is the free CBS on m generators. Since # F_0=1 by induction we obtain that F_m is finite for any m because it is a subdirect product of a finite family of subdirectly irreducibles which are generated by m elements.



Computing the cardinality of F_m is a hard task. It is known that # F_0=1, # F_1=2, # F_2=18 and # F_3=623,662,965,552,330. The size of F_4 is still unknown. In <cit.> it is proved that the number of join-irreducible elements of F_4 is 2,494,651,862,209,437.

This shows that although the cardinality of the free CBS on a finite number of generators is always finite,  it grows very rapidly.




 §.§ Finite duality



Any finite CBS is a distributive lattice. 



 A finite CBS is complete, hence also co-complete, so it is a lattice.
The map a ∨ (-) preserves infima because it has a left adjoint given by (-) - a. Thus the distributive laws hold.




Every finite Brouwerian semilattice is a Heyting algebra but it is not true that every Brouwerian semilattices morphism among finite Brouwerian semilattices is a Heyting algebra morphism. 


The following theorem presents the finite duality result due to Köhler: 

 
The category 𝐂𝐁𝐒_fin of finite CBSes is dual to the category 𝐏 whose objects are finite posets and whose morphisms are partial mappings α:P → Q satisfying:
 

  * ∀ p,q ∈dom α if  p < q  then α(p) < α(q). 

  * ∀ p ∈dom α and ∀ q ∈ Q  if α(p) < q  then ∃ r ∈dom α such that  p < r  and α(r)=q. 



 The proof can be found in <cit.>. We just recall how the equivalence works.
To a finite poset P it is associated the CBS 𝒟(P) of downsets of P.

To a 𝐏-morphism among finite posets it is associated the morphism of CBSes that maps a downset to the downset generated by its preimage. More explicitly, to a 𝐏-morphism f:P → Q is associated the morphism that maps a downset D of Q to f^-1(D)={ p∈ P|∃ p'≥ p  (p'∈dom f  & f(p')∈ D)}.

On the other hand, to a finite CBS L it is associated the poset of its join-irreducible elements.


The following proposition is easily checked:


Let P,Q be finite posets and f : P → Q a 𝐏-morphism. Let α be the associated morphism of CBSes. Then
 

  * α is injective if and only if f is surjective.

  * α is surjective if and only if dom   f = P and f is injective.



Duality results involving all Brouwerian semilattices can be found in the recent paper <cit.> due to G. Bezhanishvili and R. Jansana. Other dualities are described in <cit.> and <cit.>.



Using finite duality we can show that the variety of CBSes has the amalgamation property.

The amalgamation property for Brouwerian semilattices is the algebraic counterpart of a syntactic fact about the implication-conjunction fragment of intuitionistic propositional logic: the interpolation property. The proof that such fragment satisfies this property can be found in <cit.>.

 
The theory of CBSes has the amalgamation property.



First, we show that the pushout of given monomorphisms (= injective maps) m:L_0 → L_1 and n:L_0 → L_2 among finite CBSes is still formed by monomorphisms. Then we extend the result to the general case.

To do this, by finite duality, it is sufficient to show that the category 𝐏 has the coamalgamation property.

This means that, given two surjective 𝐏-morphisms among finite posets f:P → Q and g:R → Q there exist a finite poset S and two surjective 𝐏-morphisms f':S → R and g':S → P making the following diagram commute.


    S [r, "f'"] [d, "g'"']     R [d, "g"] 
    
    P [r, "f"']     Q


For any p ∈ P let q_1, …, q_n be the minimal elements of

    { f(a)   |   a ∈dom  f  and  a ≥ p }⊆ Q

it could be that n=0 when such set is empty. Define:

    S_p= { ({ p }, { r_1, …, r_n })   |   r_i ∈dom  g  and  g(r_i)=q_i  for  i=1, …,n }

Analogously for any r ∈ R let q_1, …, q_n be the minimal elements of

    { f(a)   |   a ∈dom  g  and  a ≥ r }⊆ Q

and define

    S_r= { ({ p_1, …, p_n }, { r })   |   p_i ∈dom  f  and  f(p_i)=q_i  for  i=1, …,n }

Let

    S_P= ⋃_p ∈ P S_p      S_R= ⋃_r ∈ R S_r

And take S= S_P ∪ S_R.

We can immediately observe that if p ∈dom  f then 

    S_p= { ({ p }, { r })   |   r ∈dom  g  and  f(p)=g(r) }.

And that

    S_P ∩ S_R= { ({ p }, { r })   |   p ∈dom  f,  r ∈dom  g   and  f(p)=g(r) }.

And finally that if ({ p }, { r_1, …, r_n }) ∈ S_p then the r_i's are two-by-two incomparable, indeed g is order preserving and the g(r_i)'s are incomparable since they are the minimal elements of a subset of Q. Thus the elements of the two components of any element of S are two-by-two incomparable.

We define an order on S in the following way:

let (A_1,A_2), (B_1,B_2) ∈ S where A_1,B_1 ⊆ P and A_2,B_2 ⊆ R, we define

    (A_1,A_2) ≤ (B_1,B_2)     iff       ∀  y ∈ B_1  ∃  x ∈ A_1  such that  x ≤ y 
       and
       ∀  y ∈ B_2  ∃  x ∈ A_2  such that  x ≤ y

This order relation is clearly reflexive.

It is antisymmetric, indeed let (A_1,A_2) ≤ (B_1,B_2) and (B_1,B_2) ≤ (A_1,A_2) then for any y ∈ B_1 there exists x ∈ A_1 such that x ≤ y and there exists z ∈ B_1 such that z ≤ x. Since the elements of B_1 are incomparable we get z=y and thus x=y. Therefore B_1 ⊆ A_1. Symmetrically we get A_1 ⊆ B_1 and then A_1=B_1. Reasoning similarly we get A_2=B_2 and then (A_1,A_2) = (B_1,B_2).

It is transitive, indeed let (A_1,A_2) ≤ (B_1,B_2) and (B_1,B_2) ≤ (C_1,C_2) then for any z ∈ C_1 there exists y ∈ B_1 such that y ≤ z and there exists x ∈ A_1 such that x ≤ y and hence also x ≤ z. Analogously for the second components. Therefore (A_1,A_2) ≤ (C_1,C_2).

Thus we have defined a partial order on S.

Take g':S → P and f':S → R as:

    dom  g' = S_P            dom  f' = S_R 
    
    g'({ p }, A_2)=p             f'(A_1, { r })=r

Then

    dom  f ∘ g'     = (g')^-1 (dom  f)  = { ({ p }, A_2)∈ S_P   |   p ∈dom  f }
        ={ ({ p }, { r })   |   p ∈dom  f,   r ∈dom  g  and  f(p)=g(r) }
        = (f')^-1 (dom  g)  = { (A_1, { r })∈ S_R   |   r ∈dom  g }
        = dom  g ∘ f'

and if p ∈dom  f,   r ∈dom  g  and  f(p)=g(r) then

    (f ∘ g')(({ p }, { r }))=f(p)=g(r)=(g ∘ f')(({ p }, { r }))

g' is surjective: indeed let p ∈ P and q_1, …, q_n be the minimal elements of { f(a)   |   a ∈dom  f  and  a ≥ p }, by surjectivity of g there exist r_1, …, r_n ∈dom  g such that g(r_i)=q_i, then ({ p }, { r_1, …, r_n }) ∈ S_p ⊆dom  g' and g'(({ p }, { r_1, …, r_n }))=p. Analogously for the surjectivity of f'.

It remains to show that g',f' are 𝐏-morphisms.

Let ({ p }, A), ({ p' }, B) ∈ S_P= dom  g' such that ({ p }, A) < ({ p' }, B), we show that p < p'.

Clearly p ≤ p' by the definition of the order on S.

Suppose that p=p', let q_1, …, q_n be the minimal elements of { f(a)   |   a ∈dom  f  and  a ≥ p }. Let A={ r_1, …, r_n } and B={ r_1', …, r_n' } be such that g(r_i)=g(r_i')=q_i for i=1, …,n. Then for any r_i' ∈ B there exists r_j ∈ A such that r_j ≤ r_i'. If r_j ≤ r_i' with j ≠ i then q_j=g(r_j) ≤ g(r_i')=q_i and this is absurd because the q_i's are incomparable. Therefore r_i ≤ r_i' for any i=1, …, n, if r_i < r_i' then q_i=g(r_i) < g(r_i')=q_i which is absurd. Thus r_i=r_i' and A=B, we have obtained a contradiction. Analogous for f'.

Therefore g',f' preserve the strict order.

Let ({ p }, A) ∈ S_P and p < p'.

Let q_1, …, q_n be the minimal elements of { f(a)   |   a ∈dom  f  and  a ≥ p } and q_1', …, q_m' be the minimal elements of { f(a)   |   a ∈dom  f  and  a ≥ p' }; since the latter set is included in the former and they are both finite we have that for any q_j' there exist q_i such that q_i ≤ q_j'.

Let A= { r_1, …, r_n } with g(r_i)=q_i. Since g is a 𝐏-morphism and for any q_j' there exists i such that g(r_i)=q_i ≤ q_j', there exists r_j' ∈dom  g such that r_i ≤ r_j' and g(r_j')=q_j'. Take B= { r_1', …, r_m' } then for any r_j' there exists r_i such that r_i ≤ r_j', therefore ({ p }, A) <  ({ p' }, B) ∈ S_P. Analogous for f'.

Thus f',g' are surjective 𝐏-morphisms and they coamalgamate f,g.

We now want to prove the general case: pushouts of monos along monos in the category of CBSes are monos.

Suppose m:L_0 → L_1 and n:L_0 → L_2 are monos and L_0,L_1,L_2 are CBSes. Since the variety is locally finite by Theorem <ref>, we can consider L_0,L_1,L_2 as filtered colimits of families of finite CBSes. Assume without loss of generality that L_1 ∩ L_2 =L_0 and m,n are inclusions, then we can consider the families indexed by 𝒫_fin(L_1 ∪ L_2) given for any finite subset S ⊆ L_1 ∪ L_2 by the sub-CBSes respectively of L_1,L_2 and L_0 generated respectively by S ∩ L_1, S ∩ L_2 and m^-1(S ∩ L_1) ∩ n^-1(S ∩ L_2)=S ∩ L_0. Then we can compute the pushouts of the restrictions of the monos for any index, the colimit of all these pushouts is a mono because each of them is a mono. Thus we have obtained that the pushout of m along n and the pushout of n along m  are monomorphisms.




 §.§ Existentially closed CBSes
 

In this subsection we want to characterize the existentially closed CBSes using the finite extensions of their finite sub-CBSes.


Let T be a first order theory and 𝒜 a model of T.

𝒜 is said to be existentially closed for T if for every model ℬ of T such that 𝒜⊆ℬ every existential sentence in the language extended with names of elements of 𝒜 which holds in ℬ also holds in 𝒜


The following proposition is well-known from textbooks <cit.>:


Let T be a universal theory. If T has a model completion T^*, then the class of models of T^* is the class of models of T which are existentially closed for T.


Thanks to the locally finiteness and the amalgamability, by an easy model-theoretic reasoning we obtain the following characterization of the existentially closed CBSes:

 
Let L be a CBS. L is existentially closed iff for any finite sub-CBS L_0 ⊆ L and for any finite extension C ⊇ L_0 there exists an embedding C → L fixing L_0 pointwise. 



First, we prove that if for any finite sub-CBS L_0 ⊆ L and for any finite extension C ⊇ L_0 there exists an embedding C → L fixing L_0 pointwise, then L is existentially closed.

Let D be an extension of L and ∃ x_1, …, x_m φ (x_1, …, x_m, a_1, …,a_n) an existential ℒ_L-sentence, where φ (x_1, …, x_m, a_1, …,a_n) is quantifier free and a_1, …, a_n ∈ L.

Suppose D ∃ x_1, …, x_m φ (x_1, …, x_m, a_1, …,a_n).

Let d_1, …, d_m be elements of D such that D φ (d_1, …, d_m, a_1, …,a_n).

Consider the sub-CBS L_0 ⊆ L generated by a_1, …, a_n and the sub-CBS C ⊆ D generated by d_1, …, d_m, a_1, …,a_n. They are both finite because they are finitely generated and the CBSes form a locally finite variety.

By hypothesis there exists an embedding C → L fixing L_0 pointwise.

Let d_1', …, d_m' be the images of d_1, …, d_m by this embedding. Thus L φ (d_1', …, d_m', a_1, …,a_n) because φ is quantifier free.

Therefore L ∃ x_1, …, x_m φ (x_1, …, x_m, a_1, …,a_n). It follows that L is existentially closed.

To prove the other implication, suppose L is existentially closed.

By amalgamation property there exists a CBS D amalgamating L and C over L_0.


    [row sep=tiny]
        L [rd]     
    
    L_0 [rd, hook] [ru, hook]        D  
        C [ru]

Let Σ be the set of quantifier free ℒ_C-sentences of the form c * c'=c” true in C where c,c',c”∈ C and * is either ∨ or -. Hence (C,Σ) is a finite presentation of C.

Now let c_1,…,c_r,a_1, …, a_n be an enumeration of the elements in C where the a_i's are the elements in L. We obtain the quantifier free ℒ_C-sentence σ(c_1,…,c_r,a_1, …,a_n) by taking the conjunction of all the sentences in Σ and all the sentences of the form (c = c') for every c,c' ∈ C such that c ≠ c'.

Clearly ∃ x_1, …, x_r σ(x_1,…,x_r,a_1, …,a_n) is an existential ℒ_L-sentence true in D. Since L is existentially closed, L ∃ x_1, …, x_r σ(x_1,…,x_r,a_1, …,a_n). Let c_1', …, c_r' ∈ L be such that L σ(c_1',…,c_r',a_1, …,a_n). The map C → L fixing L_0 pointwise and mapping c_i to c_i' is an embedding. Indeed it is injective and an homomorphism by definition of the sentence σ.




§ MINIMAL FINITE EXTENSIONS
 

In this section we focus on the finite extensions of CBSes. We are interested in particular to the minimal ones since any finite extension can be decomposed in a finite chain of minimal extensions. We will study minimal finite extensions by describing the properties of some elements which generate them. This investigation will lead us to another characterization of the existentially closed CBSes.

 
Let P be a poset, P_0 ⊆ P and ℱ a partition of P_0, let A,B ∈ℱ.

We say that A ≤ B iff there exist a ∈ A, b ∈ B such that a ≤ b.


 
Let P be a finite poset.

To give a surjective 𝐏-morphism f from P to any finite poset is equivalent, up to isomorphism, to give a partition ℱ of a subset of P such that:


  * for all A,B ∈ℱ we have that if A ≤ B and B ≤ A then A=B, 

  * for all A,B ∈ℱ and a ∈ A if A ≤ B then there exists b ∈ B such that a ≤ b,

  * for all A ∈ℱ we have that all the elements of P in A are two-by-two incomparable.





Given a surjective 𝐏-morphism f : P → Q, the partition ℱ of dom  f ⊆ P is obtained by taking the collection of the fibers of f. 
ℱ satisfies <ref> because f is order preserving and the order on Q is antisymmetric. Furthermore ℱ satisfies <ref> as a consequence of condition <ref> in the definition of 𝐏-morphism. Finally, ℱ satisfies <ref> because 𝐏-morphisms are strict order preserving.

On the other hand, given a partition ℱ of a subset P_0 of P satisfying the conditions <ref>, <ref> and <ref>, we obtain a poset Q by taking the quotient set of P_0 given by ℱ with the order defined in Definition <ref>. The partial map f : P → Q is just the projection onto the quotient.

Q is a poset: the order of Q is clearly reflexive, it is antisymmetric because ℱ satisfies <ref>. It is also transitive because if A ≤ B e B ≤ C then there exist a ∈ A,  b, b' ∈ B,  c ∈ C such that a ≤ b,  b' ≤ c; since <ref> holds, there exist c' ∈ C such that b ≤ c', hence a ≤ c' and A ≤ C. The projection f is order preserving, it is a 𝐏-morphism because <ref> holds and it is obviously surjective.

It remains to show that a surjective 𝐏-morphism f:P → Q differs by an isomorphism to the projection onto the quotient defined by the partition given by the fibers of f. This follows from the fact that for any a,b ∈dom  f it is f(a) ≤ f(b) iff f^-1(f(a)) ≤ f^-1(f(b)) (notice that f^-1(f(a)) is the element of ℱ containing a). Indeed if f(a) ≤ f(b), since f is a 𝐏-morphism, there exists b' such that a ≤ b' and f(b')=f(b), therefore since a ≤ b' it is f^-1(f(a)) ≤ f^-1(f(b)). The other direction of the implication holds because f is order preserving.


 
Let P,Q be finite posets and  f : P → Q a surjective 𝐏-morphism (or equivalently: let ℱ satisfy conditions <ref>, <ref> and <ref> of Proposition <ref>). We say that f (or ℱ) is minimal if #P=#Q+1.



If ℱ is minimal, then at most one element of ℱ is not a singleton.


 
Let f:P → Q be a surjective 𝐏-morphism between finite posets. Let n = #P-#Q. Then there exist Q_0, … , Q_n with Q_0=P, Q_n=Q and f_i:Q_i-1→ Q_i which are minimal surjective 𝐏-morphisms for i=1,…,n such that f= f_n ∘⋯∘ f_1. 




Let R = dom  f, we can decompose f=f”∘ f' where f”:R → Q is just the restriction of f on its domain and f':P → R is the partial morphism with domain R that acts as the identity on R.

The morphism f”:R → Q is a total morphism[Since it is a total map, its dual preserves the maximum downset and intersections of downsets. Therefore it is dual to a co-Heyting algebras morphism.], we prove by induction on # R-#Q that it can be decomposed in a chain of minimal surjective 𝐏-morphisms.

Suppose # R-#Q>1 and let us consider the partition ℱ of R given by the fibers of f”. Let x ∈ P be minimal among the elements of R that are not in a singleton of ℱ. Let G be the element of ℱ containing x, then #G > 1 and all the elements of R inside G are incomparable to each other.

Let Q_n-1 be the quotient of R defined by the refining of ℱ in which G is substituted by { x } and G \{ x }, we name this new partition ℱ'.

The projection onto the quotient π:R → Q_n-1 is a 𝐏-morphism because ℱ' satisfies the conditions <ref>, <ref> and <ref> of Proposition <ref>. Indeed, it satisfies <ref> and <ref> because ℱ satisfies them and the elements in G are incomparable. To show that <ref> holds it is sufficient to show that for the pairs of sets in ℱ' in which exactly one of the two is { x } or G \{ x } because ℱ satisfies <ref> and { x } and G \{ x } are incomparable.

Let A ∈ℱ be different from { x } and G \{ x }.

If { x }≤ A then <ref> holds because { x } is a singleton.

If A ≤{ x } then there exists a ∈ A such that a ≤ x, hence A is a singleton by minimality of x, therefore <ref> holds.

If G \{ x }≤ A then we have that G ≤ A, thus for any y ∈ G \{ x } there exists y' ≥ y such that y' ∈ A.

If A ≤ G \{ x } it is A ≤ G thus for any y ∈ A there exists y' ≥ y such that y'=x or y' ∈ G \{ x }. Suppose there exists y ∈ A such that there is no y' ≥ y such that y' ∈ G \{ x }: then x ≥ y, by minimality of x it has to be A= { y } then A ≰ G \{ x }, this is absurd.

Therefore π:R → Q_n-1 is a surjective total 𝐏-morphism and we can apply the inductive hypothesis on π.

Then it suffices to show that the order-preserving map f_n:Q_n-1→ Q induced by f” is a 𝐏-morphism, because in that case it is obviously surjective and minimal. But this is easy to show because the fibers of f_n are all singletons except one and because f” is a 𝐏-morphism.

It remains to decompose f', to do that just enumerate the elements of P ∖ R= { p_1, …, p_k } and let f_1 ' :R ∪{ p_1 }→ R be the partial morphism with domain R that acts as the identity on R. Then construct f_2 ' : R ∪{ p_1,p_2 }→ R ∪{ p_1 } in the same way and so on until p_k.



We say that a proper extension L_0 ⊆ L of finite CBSes is minimal if there is no intermediate proper extension L_0 ⊊ L_1 ⊊ L.



An extension L_0 ⊆ L of finite CBSes is minimal iff the surjective 𝐏-morphism that is dual to the inclusion is minimal.



Let f : P → Q be a surjective 𝐏-morphism with #P=#Q+1. And suppose there exist two surjective 𝐏-morphisms g_1 :P → R and g_2 : R → Q such that f=g_2 ∘ g_1, being g_1 and g_2 surjective #R must be equal to #P or #Q. In the former case the domain of g_1 must be all P and the relative fiber partition could only be the one formed exclusively by singletons because of cardinality, in the latter case the same holds for g_2. So either g_1 or g_2 has to be an isomorphism of posets.

Hence if we have two consecutive extensions that form an inclusion whose dual is minimal, then the dual of one of the two extensions is an isomorphism and so the relative extension is the identity.

The other implication follows easily from Theorem <ref>.




By Definition <ref> it follows immediately that there are two different kinds of minimal surjective 𝐏-morphisms between finite posets.

We call a minimal surjective 𝐏-morphism of the first kind when there is exactly one element outside its domain and thus the restriction of such map on its domain is bijective and therefore an isomorphism of posets (any bijective 𝐏-morphism is an isomorphism of posets). Some of these maps are dual to co-Heyting algebras embeddings but some are not.

We call a minimal surjective 𝐏-morphism of the second kind when it is total, i.e. there are no elements outside its domain, and thus there is exactly a single fiber which is not a singleton and it contains exactly two elements. The maps of the second kind are dual to co-Heyting algebras embeddings.

Figures <ref> and <ref> show some examples of minimal surjective 𝐏-morphisms and relative extensions of CBSes.

We call a finite minimal extension of CBSes either of the first or of the second kind if the corresponding minimal surjective 𝐏-morphism is respectively of the first or of the second kind.

Therefore, a finite minimal extension of CBSes of the first kind preserves the join-irreducibility of all the join-irreducibles in the domain. Indeed, since the corresponding 𝐏-morphism is an isomorphism when restricted on its domain, we have that the downset generated by the preimage of a principal downset is still principal.

A finite minimal extension of CBSes of the second kind preserves the join-irreducibility of all the join-irreducibles in the domain except one which becomes the join of the two new join-irreducible elements in the codomain. Indeed, the corresponding 𝐏-morphism is total and all its fibers are singletons except one, this implies that the preimage of any principal downset is principal except for one whose preimage is a downset generated by two elements.






It turns out that we can characterize the finite minimal extensions of CBSes by means of their generators.

 
Let L_0 be a finite CBS and L an extension of L_0. We call an element x ∈ L primitive of the first kind over L_0 if the following conditions are satisfied:


  * x ∉ L_0 

and for any a join-irreducible of L_0:


  * a-x ∈ L_0, 

  * x-a = x  or  x-a = 0. 




 
Let L_0 be a finite CBS and L an extension of L_0.[Notice that we do not require L to be a finite CBS.]
If x ∈ L is primitive of the first kind over L_0 then the sub-CBS L_0 ⟨ x ⟩ of L generated by x over L_0 is a finite minimal extension of L_0 of the first kind.


Before proving Theorem <ref> we need the following lemma:

 
Let L_0 be a finite CBS, L an extension of L_0 and x ∈ L primitive of the first kind over L_0, then the two following properties hold:
 

  * ∀ a ∈ L_0    a-x ∈ L_0, 

  * ∀ a ∈ L_0    x-a = x  or  x-a = 0. 




Let a ∈ L_0 and a_1, …, a_n be its join-irreducible components in L_0, since L_0 is finite we have a=a_1 ∨⋯∨ a_n. To prove <ref> observe that

    a-x=(a_1-x) ∨⋯∨ (a_n-x)

which is an element of L_0 because it is join of elements of L_0 as a consequence of <ref> of Definition <ref>.

Furthermore to prove <ref> notice that

    x-a=x-(a_1 ∨⋯∨ a_n)=((x-a_1)- ⋯ )-a_n

and that <ref> of Definition <ref> implies that there are two possibilities: x-a_i=x for any i=1, …,n or x-a_i=0 for some i. In the former case we have x-a=x, in the latter suppose that i is the smallest index such that  x-a_i=0 then 

    x-a=((x-a_i)- ⋯ )-a_n=(0- ⋯ )-a_n=0.




Let L' be the sub ∨-semilattice of L generated by x over L_0, we show that L' actually coincides with L_0 ⟨ x ⟩.

L' is clearly finite, its elements are the elements of L_0 and the elements of the form a ∨ x with a ∈ L_0. It follows from <ref> and <ref> of Lemma <ref> that if 
 a,b,c,d ∈ L_0 ∪{ x } then (a ∨ b) -(c ∨ d) = (a-(c ∨ d) ) ∨ (b-(c ∨ d) )= ( (a-c )-d) ∨ ((b-c)-d) belong to L'. Therefore L'=L_0 ⟨ x ⟩.

We want to show that the join-irreducibles of L_0 ⟨ x ⟩ are exactly the join-irreducibles of L_0 and x.

x is a join-irreducible element of L_0 ⟨ x ⟩, indeed x ≠ 0 since by hypothesis x ∉ L_0 and suppose that x ≤ a ∨ b with a,b ∈ L_0 ⟨ x ⟩ and a,b ≱ x; therefore a and b must be elements of L_0 because they cannot be of the form c ∨ x with c ∈ L_0. It follows from <ref> of Lemma <ref> and a,b ≱ x that x-a = x-b = x and so 0=x-(a ∨ b )=  ( x-b)-a= x-a = x, this is absurd because x ≠ 0.

The join-irreducible elements of L_0 are still join-irreducible in L_0 ⟨ x ⟩. It is sufficient to show that for any g join-irreducible in L_0 if g ≤ a ∨ x with a ∈ L_0 then g ≤ a or g ≤ x. Notice that being L a CBS it is g= (g-x ) ∨ ( g-(g-x)) (see Remark <ref>), we also have by <ref> of Definition <ref> that g-x and g-(g-x) are in L_0. Then being g join-irreducible in L_0 we get g=g-x or g =   g-(g-x). In the latter case g-x= g-(g-(g-x))= g-g = 0 so g ≤ x. In the former case 0=g- (a ∨ x )  = (g-x)-a= g-a so g ≤ a.

Clearly if an element of the form x ∨ a with a ∈ L_0 is different from a and x it cannot be join-irreducible in L_0 ⟨ x ⟩. Also if an element of L_0 is not join-irreducible in L_0 it cannot be join-irreducible in L_0 ⟨ x ⟩. Hence the join-irreducible elements of L_0 ⟨ x ⟩ are exactly the join-irreducible elements of L_0 and x.

Therefore the extension L_0 ↪ L_0 ⟨ x ⟩ is minimal since L_0 ⟨ x ⟩ contains exactly one join-irreducible element more than L_0. Notice that L_0 ⟨ x ⟩ is a minimal extension of L_0 of the first kind because the join-irreducibility of all the join-irreducibles of L_0 is preserved.


 
Let L_0 be a finite CBS and L an extension of L_0.[Again we do not require L to be a finite CBS.]
We call a couple of elements (x_1,x_2) ∈ L^2 primitive of the second kind over L_0 if the following conditions are satisfied:


  * x_1,x_2 ∉ L_0 and x_1 ≠ x_2 

and there exists g join-irreducible element of L_0 such that:


  * g-x_1=x_2 and g-x_2=x_1, 

  * for any join-irreducible element a of L_0 such that a <g we have a-x_i ∈ L_0 for i=1,2. 




 
g in Definition <ref> is univocally determined by (x_1,x_2) since g= x_1 ∨ x_2.

Indeed, by property <ref> of Definition <ref> we have x_1 ≤ g, x_2 ≤ g and also g-(x_1 ∨ x_2)=(g-x_1)-x_2=x_2-x_2=0 that implies g ≤ x_1 ∨ x_2.


 
Let L_0 be a finite CBS and L an extension of L_0.
If (x_1,x_2) ∈ L^2 is primitive of the second kind over L_0 then the sub-CBS L_0 ⟨ x_1, x_2 ⟩ of L generated by { x_1,x_2 } over L_0 is a finite minimal extension of L_0 of the second kind.


Before proving Theorem <ref> we need the following lemma:

 
Let L_0 be a finite CBS, L an extension of L_0 and (x_1,x_2) ∈ L^2 primitive of the second kind over L_0, then the two following properties hold:
 

  * ∀ a ∈ L_0    a-x_i ∈ L_0  or  a-x_i = b ∨ x_j with b ∈ L_0 for { i,j } = { 1,2 }. 

  * ∀ a ∈ L_0     x_i-a = x_i  or  x_i-a = 0 for i=1,2. 




To show <ref> we first prove that if a ≠ g is join-irreducible in L_0, then a-x_i ∈ L_0. If a<g this is covered by the hypothesis <ref> of Definition <ref>. Now suppose that a is a join-irreducible element of L_0 such that a ≰ g then a-g=a because a is join-irreducible. Thus a=a-g ≤ a-x_i ≤ a since x_i ≤ g (because x_i=g-x_j ≤ g with i ≠ j) and thus a-x_i=a ∈ L_0 for i=1,2.

We now prove <ref> for all a ∈ L_0.

Let a ∈ L_0 and a_1, …, a_n be its join-irreducible components in L_0, since L_0 is finite we have a=a_1 ∨⋯∨ a_n. To prove <ref> we consider two cases: g is a join-irreducible component of a or g is not a join-irreducible component of a. In the former case, when g is a join-irreducible component of a, suppose a_1=g, then

    a-x_i=(g-x_i) ∨⋯∨ (a_n-x_i)=x_j ∨ (a_2-x_i) ∨⋯∨ (a_n-x_i)

with { i,j } = { 1,2 }, notice that (a_2-x_i) ∨⋯∨ (a_n-x_i) ∈ L_0 because it is join of elements of L_0 by what we have just proved. In the latter case, g is not a join-irreducible component of a, we have 

    a-x=(a_1-x) ∨⋯∨ (a_n-x)

which is an element of L_0 because it is join of elements of L_0 as a consequence of what we have just proved.

Furthermore, to prove <ref> notice that since g is join-irreducible in L_0 we have that for any a ∈ L_0 there are two cases to consider: g ≤ a or g-a=g. In the former case we have, since x_i ≤ g by <ref> of Definition <ref>, that x_i-a=0 for i=1,2 because x_i ≤ g ≤ a. In the latter case, since g-a=g, we have

    x_i-a=(g-x_j)-a=(g-a)-x_j=g-x_j=x_i

for { i,j } = { 1,2 }.




Let L' be the sub ∨-semilattice of L generated by { x_1,x_2 } over L_0.

As shown in Remark <ref> we have g= x_1 ∨ x_2. Also x_2 - x_1 = x_2 and x_1 - x_2 = x_1. Indeed x_2 - x_1= (g - x_1)  -x_1 =  g-x_1= x_2, the other case is symmetrical.

Hence by reasoning in a similar way as in the proof of Theorem <ref>, using properties <ref> and <ref> of Lemma <ref>, we get that L'=L_0 ⟨ x_1, x_2 ⟩.

We now want to show that the join-irreducibles of L_0 ⟨ x_1, x_2 ⟩ are exactly x_1,x_2 and the join-irreducibles of L_0 different from g.

First, notice that if an element of L_0 is not join-irreducible in L_0 it cannot be join-irreducible in L_0 ⟨ x_1, x_2 ⟩. Furthermore, the only elements of L_0 ⟨ x_1, x_2 ⟩ not in L_0 that could be join-irreducible in L_0 ⟨ x_1, x_2 ⟩ are x_1,x_2 because L_0 ⟨ x_1, x_2 ⟩ is the ∨-semilattice generated by { x_1,x_2 } over L_0.

We now show that x_1,x_2 are join-irreducible in L_0 ⟨ x_1, x_2 ⟩.

Suppose x_1 is not join-irreducible in L_0 ⟨ x_1,x_2 ⟩ and let y_1, …, y_r be its join-irreducible components. One of them must be x_2 because x_1 ∉ L_0 and we observed that all the join-irreducible elements of L_0 ⟨ x_1,x_2 ⟩ are in L_0 ∪{ x_1,x_2 }. But then x_2 ≤ x_1 and therefore, by what was shown above, 0=x_2-x_1=x_2 which is absurd because x_2 ∉ L_0.

The same reasoning holds for the join-irreducibility of x_1.

It remains to show that the only element join-irreducible of L_0 which is not join-irreducible in L_0 ⟨ x_1, x_2 ⟩ is g.

Observe that g is not join-irreducible in L_0 ⟨ x_1, x_2 ⟩ because g=x_1 ∨ x_2 and x_1,x_2 ≠ g since x_1,x_2 ∉ L_0.

Let b ∈ L_0 be join-irreducible in L_0 but not in L_0 ⟨ x_1, x_2 ⟩, let y_1, …, y_r be the join-irreducible components of b in L_0 ⟨ x_1, x_2 ⟩. From what we observed above it follows that the y_i's are in L_0 ∪{ x_1,x_2 } and since b is join-irreducible in L_0 at least one of them is not in L_0. We can suppose y_1=x_1, so x_1 ≤ b. This implies that g ≤ b, indeed one among y_2, …, y_r has to be x_2 because otherwise y_2 ∨⋯∨ y_r ∈ L_0 and being the y_i's the join-irreducible components of b we have that x_1= b-(y_2 ∨⋯∨ y_r ) must be in L_0, this is absurd. If g < b then b-g= b because b is join-irreducible in L_0 but in this case x_1=y_1 ≤ b=b-g ≤ b-x_1 = y_2 ∨⋯∨ y_r and this is not possible because the y_i's  are the join-irreducible components of b. This implies b=g.

Therefore the extension L_0 ↪ L_0 ⟨ x_1,x_2 ⟩ is minimal since the number of join-irreducibles of L_0 ⟨ x_1,x_2 ⟩ is greater by one than the number of the join-irreducibles of L_0.

Notice that L_0 ⟨ x_1,x_2 ⟩ is a minimal extension of L_0 of the second kind because the join-irreducibility of all but one of the join-irreducibles of L_0 is preserved.



 
Let L_0 be a finite CBS and L a finite minimal extension of L_0, then L is generated over L_0 either by a primitive element x ∈ L of the first kind over L_0 or by x_1,x_2 ∈ L forming a primitive couple (x_1,x_2) of the second kind over L_0.



Let f : P → Q be the surjective minimal 𝐏-morphism dual to the inclusion of L_0 into L. Recall that P and Q are respectively the posets of the join-irreducible elements of L and L_0.

We consider two cases:

The first case is when f is of the first kind, i.e. dom  f ≠ P and there exists only one element p ∈ P ∖dom  f. In this case, by minimality of f, the restriction of f on its domain is an isomorphism of posets. We want to prove that x=p is a primitive element of L of the first kind over L_0.

We observe that the downset p cannot be generated by the preimage of any downset in Q because p is not in the domain of f, therefore x ∉ L_0.

For any q ∈ Q let q' be the unique element of P in the preimage of q by f, then f^-1 ( q)= q' because f is a 𝐏-morphism. Hence if q' ≤ p then q'- p= ∅ and if q' ≰ p then q' - p= q'. This translates to the fact that for any a join-irreducible of L_0 we have a-x ∈ L_0 because both ∅ and q' are generated by the preimage of a downset of Q. Furthermore, for any q ∈ Q if p ≤ q' then p -  q'=∅ and if p ≰ q' then p- q'= p. Thus for any a join-irreducible of L_0 either x-a=0 or x-a=x.

The second case is when f is of the second kind, i.e. dom  f = P and only two elements p_1,p_2 have the same image by f, recall that p_1,p_2 are incomparable. We want to prove that x_1=p_1 and x_2=p_2 form a primitive couple of elements of L of the second kind over L_0.

x_1 ≠ x_2 and x_1,x_2 ∈ L_0 because the downsets p_1 and p_2 are distinct and neither of them is generated by the preimage of a downset in Q. Indeed, since f is a total map the preimages of downsets of Q are already downsets of P and any preimage contains p_1 iff it contains p_2.

Let f(p_1)=f(p_2)=g ∈ Q then f^-1(g)= { p_1, p_2 }, since f is total f^-1( g) is a downset and thus f^-1( g)=  f^-1( g). We have that f^-1( g)= p_1 ∪ p_2 because f is a 𝐏-morphism and therefore f^-1( g)- p_1= p_2 and f^-1( g)- p_2= p_1 because p_1 and p_2 are incomparable. Therefore g-x_1=x_2 and g-x_2=x_1.

Let q ∈ Q such that q <g and q' be the unique element of P in the preimage of q by f, then f^-1 ( q)= q' because f is a 𝐏-morphism. Hence if q' ≤ p then q'- p= ∅ and if q' ≰ p then q' - p= q'. Both ∅ and q' are generated by the preimage of a downset of Q. This means that for any a join-irreducible of L_0 such that a < g we have a-x_i ∈ L_0 for i=1,2.



Let L_0 be a finite CBS.

We call signature of the first kind in L_0 a couple (h,G) where h ∈ L_0 and G is a set of two-by-two incomparable join-irreducible elements of L_0 such that h < g for all g ∈ G. We allow G to be empty.

We call signature of the second kind in L_0 a triple (h_1,h_2,g) where h_1,h_2 ∈ L_0, g is a join-irreducible element of L_0 such that h_1 ∨ h_2 =g^- the unique predecessor of g in L_0.



 
Let L_0 be a finite CBS. To give a minimal finite extension either of the first or of the second kind of L_0 (up to isomorphism over L_0) is equivalent to give respectively:


  * A signature (h,G) of the first kind in L_0.

  * A signature (h_1,h_2,g) of the second kind in L_0.
 


Once again finite duality shows its usefulness. Indeed, we have the following lemma:

 
Let Q be a finite poset. To give a minimal surjective 𝐏-morphism f with codomain Q either of the first or of the second kind (up to isomorphism) is equivalent to give respectively:


  * D,U respectively a downset and an upsetof Q such that D ∩ U= ∅ and for any d ∈ D, u ∈ U we have d ≤ u. 

  * g ∈ Q and D_1,D_2 downsets of Q such that D_1 ∪ D_2=  g ∖{ g }. 

The definitions of upset and of the upset a generated by an element a are analogous to the definitions for the downsets replacing ≤ with ≥.




Let f:P → Q be a minimal surjective 𝐏-morphism.

If f is of the first kind and dom  f = P ∖{ x } take D=f( x ∖{ x }) and U=f( x ∖{ x }).

If f is of the second kind, i.e. dom  f = P, then there is exactly one g ∈ Q such that f^-1(g)={ x_1,x_2 } consisting of two elements of P. Take D_i= f( x_i ∖{ x_i }) for i=1,2.

On the other hand, given D,U as in <ref> ,we obtain a minimal surjective 𝐏-morphism f:P → Q by taking P= Q ⊔{ x } and extending the order of Q setting q < x iff q ∈ D and x < q iff q ∈ U for any q ∈ Q. Take dom  f= Q ⊂ P and f as the identity on its domain.

Given g ∈ Q, D_1,D_2 as in <ref> obtain a minimal surjective 𝐏-morphism f:P → Q taking P= Q ∖{ g }⊔{ x_1,x_2 } and extending the order of Q ∖{ g } setting q < x_i iff q ∈ D_i and x_i < q iff g < q for any q ∈ Q. Take dom  f= P and f maps x_1,x_2 into g and acts as the identity on Q ∖{ g }.

Now let f_1 : P_1 → Q and f_2 : P_2 → Q be two surjective 𝐏-morphisms to which are associated the same (D,U) or (D_1,D_2,g), we show that there exists an isomorphism of posets φ :P_1 → P_2 such that f_2 ∘φ= f_1.

Suppose f_1,f_2 are of the first kind and the same (D,U) is associated to both of them. Then dom  f_1 = P_1 ∖{ p_1 } and dom  f_2 = P_2 ∖{ p_2 }.
Being f_1,f_2 two 𝐏-morphisms which are isomorphisms when restricted on their domains, we can invert the restriction of f_2 and compose it with the restriction of f_1 to obtain an isomorphism of posets φ' : dom  f_1 →dom  f_2.

It remains to extend φ' to an isomorphism φ :P_1 → P_2, just set φ (p_1)=p_2; φ so defined is an isomorphism of posets, we need to show that it reflects and preserves the order of P_1. f_1 and f_2 map respectively the elements smaller than p_1 and p_2 into the same elements of Q and the elements greater than p_1 and p_2 into the same elements of Q by hypothesis. Hence φ' maps the elements smaller than p_1 into the elements smaller than p_2 and the elements greater than p_1 into the elements greater than p_2 and so does its inverse. It follows that φ is an isomorphism of posets.

Suppose f_1,f_2 are of the second kind and the same (D_1,D_2,g) is associated to both of them. Then f_1,f_2 are total, i.e. dom  f_1=P_1 and dom  f_2=P_2.
The orders restricted on P_1 \ f_1^-1(g) and P_2 \ f_2^-1(g) are both isomorphic to Q \{ g } with isomorphisms given by the restrictions of f_1,f_2, indeed given two elements a,b ∈ P_1 \ f_i^-1(g) it is f_i(a) ≤ f_i(b) iff a ≤ b because f_i is a 𝐏-morphism for i=1,2. Composing these two isomorphisms we obtain an isomorphism φ' : P_1 \ f_1^-1(g) → P_2 \ f_2^-1(g).

We now extend it to φ:P_1 → P_2.

Let f_i^-1(g)= { x_1,i, x_2,i} for i=1,2, we can suppose to have ordered the indices in such a way that f_i( x_j,i\{ x_j,i})=D_j for i,j=1,2. Clearly we extend φ' to φ defining φ(x_j,1)=x_j,2. It remains to show that φ is order preserving and reflecting.

Let p ∈ P_1 be such that p ∉{ x_1,1, x_2,1}.

Since f_1,f_2 are 𝐏-morphisms and f_i(x_j,i)=g we get x_j,2=φ(x_j,1) ≤φ(p) iff g ≤ f_2(φ(p))=f_1(p) iff x_j,1≤ p for j=1,2.

Furthermore it is p ≤ x_1,1 iff f_1(p) ∈ D_1 and p ≤ x_2,1 iff f_1(p) ∈ D_2, similarly it is φ(p) ≤ x_1,2 iff f_1(p)=f_2(φ(p)) ∈ D_1 and φ(p) ≤ x_2,2 iff f_1(p)=f_2(φ(p)) ∈ D_2.

Therefore φ is order preserving and reflecting.



We just need to translate Lemma <ref> in the language of CBSes using the finite duality:

A signature of the first kind (h,G) in L_0 corresponds to a couple (D,U) in P as in <ref> of Lemma <ref>. Indeed, by Köhler duality, downsets of P correspond to elements of L_0 and upsets of P correspond to the sets of their minimal elements, i.e. sets of two-by-two incomparable join-irreducible elements of L_0. The conditions D ∩ U = ∅ and ∀ d ∈ D, u ∈ U d ≤ u translate in the condition h < g for any g ∈ G.

A signature of the second kind (h_1,h_2,g) in L_0 corresponds to a triple (D_1,D_2,g) in P as in <ref> of Lemma <ref>. Indeed, h_1,h_2 ∈ L_0 correspond to the downsets D_1,D_2 and g join-irreducible of L_0 is an element of P (recall that P is the poset of the join-irreducibles of L_0). The condition that D_1 ∪ D_2 =  g ∖{ g } translates into h_1 ∨ h_2 = g^- since the predecessor g^- of g in L_0 corresponds to the downset g ∖{ g } of P.


Therefore signatures inside a finite CBS L_0 are like `footprints' left by the minimal finite extensions of L_0: any minimal finite extension of L_0 leaves a `footprint' inside L_0 given by the corresponding signature. On the other hand, given a signature inside L_0 we can reconstruct a unique (up to isomorphism over L_0) minimal extension of L_0 corresponding to that signature.


Since, by Theorems <ref>, <ref> and <ref>, minimal finite extension of a finite CBS L_0 are exactly the ones generated over L_0 either by a primitive element or by a primitive couple, to any element or couple primitive over L_0 it is associated a unique signature in L_0. This is exactly what the next definition and theorem talk about.


Let L_0 be a finite CBS and L an extension of L_0.

We say that a primitive element x ∈ L of the first kind over L_0 induces a signature of the first kind (h,G) in L_0 if for any a join-irreducible of L_0 we have that

    a < x  iff  a ≤ h    and    x < a  iff  g ≤ a  for some  g ∈ G

We say that a primitive couple (x_1,x_2) ∈ L^2 of the second kind over L_0 induces a signature of the second kind (h_1,h_2,g) in L_0 if g=x_1 ∨ x_2 and for any a join-irreducible of L_0 we have that

    a < x_i  iff  a ≤ h_i    for  i=1,2



 
Let L_0 be a finite CBS and L an extension of L_0.

A primitive element x ∈ L induces a signature (h,G) iff the extension L_0 ⊆ L_0 ⟨ x ⟩ corresponds to that signature.

A primitive couple (x_1,x_2) ∈ L^2 induces a signature (h_1,h_2,g) iff the extension L_0 ⊆ L_0 ⟨ x_1,x_2 ⟩ corresponds to that signature.



For a primitive element x of the first kind over L_0 to induce a signature (h,G) means that h is the predecessor of x in L_0 ⟨ x ⟩ and G is the set of the join-irreducibles of L_0 which are minimal among the ones that are strictly greater than x in L_0 ⟨ x ⟩. This is the same as saying that the signature (h,G) is associated to the extension L_0 ⊆ L_0 ⟨ x ⟩.

For a primitive couple (x_1,x_2) of the second kind over L_0 to induce a signature (h_1,h_2,g) means that h_i is the predecessor of x_i in L_0 ⟨ x_1,x_2 ⟩ for i=1,2. This is the same as saying that the signature (h_1,h_2,g) is associated to the extension L_0 ⊆ L_0 ⟨ x_1,x_2 ⟩.


It is sufficient to translate Lemma <ref> in the language of CBSes
Notice that conditions <ref>, <ref>, <ref> of Definition <ref> already imply that g ≤ a iff x_i < a for i=1,2. Indeed, if g ≤ a then x_i ≤ a since x_i ≤ g by condition <ref> of Definition <ref>, thus x_i < a since x_i ∉ L_0 by <ref> of Definition <ref>. On the other hand if x_i < a then g ≤ a because otherwise g-a=g, since g is join-irreducible of L_0, and this is impossible because x_i is a join-irreducible component of g in the extension (in the proof of Theorem <ref> it is shown that g=x_1 ∨ x_2 and x_1,x_2 are distinct, incomparable and join-irreducibles in the extension).




We have thus finally obtained an intermediate characterization of existentially closed CBSes:


A CBS L is existentially closed iff for any finite sub-CBS L_0 ⊆ L we have:


  * Any signature of the first kind in L_0 is induced by a primitive element x ∈ L of the first kind over L_0.

  * Any signature of the second kind in L_0 is induced by a primitive couple (x_1,x_2) ∈ L^2 of the second kind over L_0.




By the characterization of the existentially closed CBSes given in Theorem <ref> we have that a CBS L is existentially closed iff for any finite sub-CBS L_0 and for any finite extension L_0' of L_0 we have that L_0' embeds into L fixing L_0 pointwise. Since any finite extension of L_0 can be decomposed into a chain of minimal extensions, we can restrict to the case in which L_0' is a minimal finite extension of L_0. Then the claim follows from Theorem <ref> and Theorem <ref>.


Thanks to Theorem <ref> we already get an axiomatization for the class of the existentially closed CBSes, indeed the quantification over the finite sub-CBS L_0 can be expressed elementarily using an infinite number of axioms. But this axiomatization is clearly unsatisfactory: other than being infinite, it is not conceptually clear.



§ AXIOMS
 

In this section we will prove that the existentially closed CBSes are exactly the ones satisfying the Splitting, Density 1 and Density 2 axioms. Each subsection focuses on one axiom. We will use extensively the characterization of existentially closed CBSes given by Theorem <ref>. To show the validity of the axioms in any existentially closed CBS we will use the following lemma.

 
Let θ(x) and ϕ(x,y) be quantifier-free formulas in the language of CBSes. Assume that for every finite CBS L_0 and every tuple a of elements of L_0 such that L_0 θ(a), there exists an extension L_1 of L_0 which satisfies ∃yϕ(a,y).

Then every existentially closed CBS satisfies the following sentence:

    ∀x ( θ (x) ⟶∃yϕ(x,y))




Let L be an existentially closed CBS.

Let a=(a_1, …,a_n) ∈ L^n be such that L θ(a). Let L_0 be the sub-CBS of L generated by a_1, …, a_n, by local finiteness L_0 is finite. By hypothesis there exists an extension L_1 of L_0 and b=(b_1, …,b_m) ∈ L_1^m such that L_1 ϕ(a,b).

Denote by L_0' the sub-CBS of L_1 generated by b_1, …,b_m over L_0, it is a finite extension of L_0. By Theorem <ref> L_0' embeds into L fixing L_0 pointwise.

We thus get L ϕ(a,b') where b'=(b_1', …,b_m') ∈ L^m are the images of b_1, …,b_m by the embedding.

Therefore we have proved that:

    L ∀x ( θ (x) ⟶∃yϕ(x,y))






 §.§ Splitting axiom
 

[Splitting Axiom] For every a,b_1,b_2 such that b_1 ∨ b_2 ≪ a ≠ 0 there exist elements a_1 and a_2 different from 0 such that:

    a-a_1    = a_2 ≥ b_2 
     
         a-a_2    = a_1 ≥ b_1 
    
         b_2-a_1    =b_2-b_1 
    
         b_1-a_2    =b_1-b_2



Any existentially closed CBS satisfies the Splitting Axiom.



It is sufficient to show, by Lemma <ref>, that for any finite CBS L_0 and a,b_1,b_2 ∈ L_0 such that  b_1 ∨ b_2 ≪ a ≠ 0 there exists a finite extension L_0 ⊆ L with a_1,a_2 ∈ L different from 0 such that:

    a-a_1    = a_2 ≥ b_2 
     
         a-a_2    = a_1 ≥ b_1 
    
         b_2-a_1    =b_2-b_1 
    
         b_1-a_2    =b_1-b_2

Let Q be the poset dual to L_0 and A, B_1,B_2 its downsets corresponding to a, b_1,b_2.

We obtain a surjective 𝐏-morphism π :P → Q in the following way:

For any x ∈ Q such that x ∉ B_2 (respectively x ∉ B_1) let ξ_x,1 (respectively ξ_x,2) be a new symbol.

For any x ∈ Q such that x ∈ B_1 ∩ B_2 let ξ_x,0 be a new symbol.

Let P be the set of all these symbols, we define an order on P setting:

    ξ_y,j≤ξ_x,i   ⇔ y ≤ x  and { i,j }≠{ 1,2 }

Intuitively P is composed by a copy of B_1 ∪ B_2 and two copies of Q \ (B_1 ∪ B_2), one of the two copies is placed over B_1 and the other over B_2.

We define π :P → Q setting dom π =P and π(ξ_x,i)=x.

Let a_1, …,  a_r be the join-irreducible components of A, for any i we have a_i ∉ B_1 ∪ B_2 because by hypothesis B_1 ∪ B_2 ≪ A. Therefore π^-1( a_i)= ξ_a_i,1∪ξ_a_i,2

We take:

    A_1= ⋃_i=1^r ξ_a_i,1     and      A_2= ⋃_i=1^r ξ_a_i,2

We obtain π^-1(A)-A_1=A_2 and π^-1(A)-A_2=A_1, they are both not empty because r ≥ 1 and A is not empty.

Furthermore for any x ∈ B_1 ∪ B_2 we have that x ≤ a_i for some i. Therefore if x ∈ B_1 \ B_2 it is ξ_x,1≤ξ_a_i,1, if x ∈ B_2 \ B_1 it is ξ_x,2≤ξ_a_i,2, finally if x ∈ B_1 ∩ B_2 then ξ_x,0≤ξ_a_i,1 and ξ_x,0≤ξ_a_i,2. This implies that π^-1(B_1) ⊆ A_1 and π^-1(B_2) ⊆ A_2.

We now show that A_1 ∩ A_2 = π^-1 (B_1) ∩π^-1(B_2).

Let ξ∈ P, we show that ξ∈ A_1 ∩ A_2 iff ξ∈π^-1 (B_1) ∩π^-1(B_2).

If ξ∈π^-1 (B_1) ∩π^-1(B_2) then π(ξ) ∈ B_1 ∩ B_2, therefore ξ=ξ_x,0 and x ≤ a_i for some i. It implies that ξ_x,0≤ξ_a_i,1, thus ξ_x,0∈ A_1 and ξ_x,0≤ξ_a_i,2, therefore ξ_x,0∈ A_2 and ξ∈ A_1 ∩ A_2.

On the other hand if ξ∈ A_1 ∩ A_2 then there exist i,j such that ξ≤ξ_a_i,1 and ξ≤ξ_a_j,2. By definition of the order on P it has to be ξ=ξ_x,0 with x ∈ B_1 ∩ B_2, therefore ξ∈π^-1 (B_1) ∩π^-1(B_2).

Then

    π^-1 (B_1) ∩π^-1(B_2) ⊆ A_1 ∩π^-1 (B_2) ⊆ A_1 ∩ A_2 = π^-1 (B_1) ∩π^-1(B_2)

Therefore

    π^-1 (B_2)-A_1= π^-1 (B_2)-(A_1 ∩π^-1 (B_2)) 
        =π^-1 (B_2)-(π^-1 (B_1) ∩π^-1 (B_2))=π^-1 (B_2)-π^-1 (B_1)

Analogously we can show

    π^-1 (B_2)-A_1=π^-1 (B_2)-π^-1 (B_1)

Thus taking the embedding L_0 ↪ L dual to π and a_1,a_2 ∈ L corresponding to A_1,A_2 we have obtained what we were looking for.



 
If L is a CBS generated by a finite subset X then any join-irreducible element of L is a join-irreducible component in L of some element of X.



In any CBS the following identities hold:

    +
    	c-(a ∨ b)    = (c-a)-b 
    
    	(a ∨ b)-c    = (a-c) ∨ (b-c) 
    
    	c-0    =c 
    
    	0-c    =0

It follows by an easy induction that any term in the language of CBS is equivalent to a term of the form x_1 ∨⋯∨ x_n with x_1, … x_n containing only the difference symbol and variables. 

Notice that if an element x_1 ∨⋯∨ x_m with x_1, … x_m ∈ L is join-irreducible then it coincides with x_i for some i=1, …,m; thus any join-irreducible element g of L is the interpretation of a term t over the variables X containing only the difference symbol. This implies that g is the join of some join-irreducible components of the leftmost variable in t. Indeed, this can be proved by induction on the complexity of the term observing that if c_1, …, c_m are the join-irreducible components of an element c ∈ L then for any b ∈ L:

    c-b=(c_1 ∨⋯∨ c_m)-b=(c_1-b)∨⋯∨ (c_m-b)= ⋁_c_i ≰ b c_i

because c_i-b=0 or c_i-b=c_i, respectively, when c_i ≤ b or c_i ≰ b since the c_i's are join-irreducibles.



Thus g is the join of the join-irreducible components of some x ∈ X, so, since it is join-irreducible, it is a join-irreducible component of x. 








Lemma <ref> is not true for co-Heyting algebras.

Indeed, consider the inclusion L_0 ↪ L_1 of co-Heyting algebras described by Figure <ref>.
L_1 is generated by L_0 and a but b=a ∧ (1-a) is join-irreducible in L_1 and it is not a join-irreducible component of any element of L_0 or a.


Notice that the sub-CBS of L_1 generated by L_0 and a does not contain b as shown in Figure <ref>





 
Let L_0 be a finite sub-CBS of L and let L be generated by L_0 and a_1, …, a_n ∈ L.

If a_1, …, a_n are joins of join-irreducible components in L of elements of L_0then the surjective 𝐏-morphism φ: P → Q dual to the inclusion L_0 ↪ L is such that dom φ =P. In particular, the inclusion is also a co-Heyting algebras morphism, i.e. it preserves meets and 1.

For instance, this happens when we have that all the a_i's are of the kind a_i=b_i-c_i with b_i ∈ L_0 and c_i ∈ L. Indeed, in such case, the join-irreducible components in L of the a_i's are among those of b_i.



By Lemma <ref> all the join-irreducible elements of L are join-irreducible components in L of elements of L_0 or of a_1, …, a_n. Since, by hypothesis, a_1, …, a_n are joins of join-irreducible components of elements of L_0, any join-irreducible components of a_i is a join-irreducible component of a join-irreducible component of an element of L_0 and thus it is a join-irreducible component of an element of L_0. Therefore any join-irreducible element of L is a join-irreducible component in L of an element of L_0.

Suppose that there is x ∈ P such that x ∉dom φ, then x corresponds to a join-irreducible element of L which is not a join-irreducible component of any element of L_0. Indeed, if it is a join-irreducible component of a ∈ L_0 then x ∈ P would be a maximal element of the downset φ^-1 (A) where A ⊆ Q is the downset relative to a, but this is not possible since if x ∈φ^-1 (A) then x would be less than or equal to an element in φ^-1 (A) ⊆dom φ which would be different from x, this is absurd because x is maximal in φ^-1 (A). Therefore, dom φ=P because the existence of an element x ∉dom φ would imply the existence of a join-irreducible element of L which is not a join-irreducible component in L of any element of L_0, but this contradicts what we have proven in the first part of this proof.


 
Let L be a CBS and L_0 a finite sub-CBS of L, g be join-irreducible in L_0 and y_1,y_2 ∈ L be nonzero elements such that 

    g-y_1    = y_2 
     
         g-y_2    = y_1

Let also L_0 ⟨ y_1,y_2 ⟩ be the sub-CBS of L generated by L_0 and { y_1,y_2 }. We have that:


  * g=y_1 ∨ y_2,

  * any join-irreducible a of L_0 such that a ≰ g is still join-irreducible in L_0 ⟨ y_1,y_2 ⟩,

  * y_1,y_2 are distinct, not in L_0 and they are the join-irreducible components of g in L_0 ⟨ y_1,y_2 ⟩.




Notice that y_1 ∨ y_2=g because y_1 ≤ g and y_2 ≤ g and 

    g-(y_1 ∨ y_2)=(g-y_1)-y_2=y_2-y_2=0.

Furthermore y_1,y_2 ∉ L_0. 

Indeed, suppose that y_1 ∈ L_0, then y_2=g-y_1 ∈ L_0, since g is join-irreducible in L_0 and g=y_1 ∨ y_2, we have that g=y_1 or g=y_2, by hypothesis it follows respectively that y_2=0 or y_1=0, in both cases we have a contradiction because y_1,y_2 ≠ 0. Similarly, we obtain that y_2 ∉ L_0.

We also have that y_1 ≠ y_2. Indeed, suppose y_1=y_2, then g-y_1=y_1 implies that g=y_1=0 and this is absurd.
 
We now show that any join-irreducible a of L_0 such that a ≰ g is still join-irreducible in L_0 ⟨ y_1,y_2 ⟩.

Any element of L_0 ⟨ y_1,y_2 ⟩ is the join of repeated differences of y_1,y_2 and of join-irreducibles of  L_0 different from g, this is implied by the identities (<ref>) as noted in the proof of Lemma <ref>.

It is sufficient to show that for any x obtained as repeated differences of y_1,y_2 and join-irreducibles of  L_0 different from g we have a-x=a or a-x=0. This will ensures that a is join-irreducible in L ⟨ y_1,y_2 ⟩. 

Since x is obtained as repeated differences of y_1,y_2 and join-irreducibles a_1, …, a_n of L_0 different from g, there is a term t in the language of CBSes containing only - and variables expressing x as t(y_1,y_2,a_1, …,a_n). We prove that a-x=a or a-x=0 by induction on the length of t. If the length is 1, then x ∈{ y_1, y_2, a_1, …, a_n } 

If x ∈ L_0 then a-x=a or a-x=0 since a is join-irreducible of L_0. Moreover a-y_i=a for i=1,2. Indeed, a ≥ a-y_i ≥ a-g=a because a is a join-irreducible of L_0 such that a ≰ g. 

Suppose the length of t is greater than 1. If the leftmost element among the ones whose differences give x is y_i for i=1,2 then a-x=a because a=a-y_i ≤ a-x ≤ a.[Notice the following fact: if a term t in the language of CBSes only contains - (and variables) and z is the leftmost variable in t, then the inequality t ≤ z is valid in every CBS (this is established by an easy induction on the length of t).]

If the leftmost element among the ones whose differences give x is b join-irreducible of L_0 different from g. If b < g, since a ≰ g yields a ≰ b and thus a=a-b by join-irriducibility of a, we obtain that a=a-b ≤ a-x ≤ a. If b ≰ g 
we can obtain x with a smaller number of differences because we can apply the induction hypothesis to replace its subterm of the kind b-c with b or 0 (with b and c playing respectively the role previously played by a and x) and apply again the inductive hypothesis because x can be expressed by a term shorter than t.
 
Now we prove that y_1,y_2 are join-irreducibles of L_0 ⟨ y_1,y_2 ⟩. We show that for y_1, for y_2 is analogous.

Again, we show that for all x ∈ L_0 ⟨ y_1,y_2 ⟩ we have y_1-x=y_1 or y_1-x=0.
Let x be obtained as repeated differences of y_1,y_2 and join-irreducibles of  L_0 different from g as above and let us proceed by induction on the number of such differences.

First of all

    y_1-y_2=(g-y_2)-y_2=(g-y_2)=y_1.

Let x ∈ L_0, if g ≤ x then y_1-x ≤ y_1-g=0, if g ≠ x, namely g-x=g (recall that g is join-irreducible in L_0) then

    y_1-x=(g-y_2)-x=(g-x)-y_2=g-y_2=y_1.

If the leftmost element among the ones whose differences give x is y_i for i=1,2 then applying the inductive hypothesis, possibly many times, we obtain that x=0 or x=y_i and in either case y_1-x=0 or y_1-x=y_1.

Suppose the leftmost element among the ones whose differences give x is b join-irreducible of L_0 different from g. If b < g then 

    y_1=(g-y_2)=(g-b)-y_2=y_1-b ≤ y_1

and y_1=y_1-b ≤ y_1-x ≤ y_1.[Recall footnote <ref>.]

If b ≰ g we cannot have b=g because g is not join-irreducible, then using what we have proved above (that any join-irreducible b of L_0 such that b ≰ g is still join-irreducible in L_0 ⟨ y_1,y_2 ⟩) we obtain x=b or x=0 and in either case y_1-x=0 or y_1-x=y_1.

Finally, to prove that y_1,y_2 are the join-irreducible components of g in L_0 ⟨ y_1,y_2 ⟩, we simply have to notice that y_1 ≰ y_2 and y_2 ≰ y_1. Just observe that if y_1 ≤ y_2 then g=y_1 ∨ y_2 = y_2 ∉ L_0 which is absurd. Analogously it cannot be y_2 ≤ y_1.


 
Let L be a CBS satisfying the Splitting Axiom.

Then for any finite sub-CBS L_0 ⊆ L and for any signature (h_1,h_2,g) of the second kind in L_0 there exists a primitive couple (x_1,x_2) ∈ L^2 of the second kind over L_0 inducing such signature.




We follow this strategy: we use the Splitting Axiom to `split' g obtaining two elements, one over h_1 and another over h_2. When h_1=h_2 these two elements form a primitive couple that induces the signature (h_1,h_2,g), but unfortunately this is not true in general because these two elements may be too big. So we may have to `split' these two new elements too in order to obtain other elements which we may have to `split' again and again. This process has to stop after a finite number of steps, intuitively the more the element h_1 ∧ h_2 (the meet is taken inside L_0) is smaller that h_1 and h_2, the more the process lasts. Then we accurately partition the set of all these `shards' into two disjoint subsets and we take the joins of these two subsets. In this way we obtain two elements that form a primitive couple that induces the signature (h_1,h_2,g) and we are done.


The statement of the Theorem require that, according to the definition of primitive couple inducing a given signature, we need to do the following. Given h_1,h_2 ∈ L_0 and g join-irreducible of L_0 such that h_1 ∨ h_2 = g^-, we have to find x_1, x_2 ∈ L such that:


  * x_1 ≠ x_2 and x_1,x_2 ∉ L_0, 

  * g-x_1=x_2 and g-x_2=x_1 

and for any a join-irreducible of L_0:


  * if a <g then a-x_i ∈ L_0 for i=1,2, 

  * a < x_i iff a ≤ h_i for i=1,2. 

We recall that L_0 is a co-Heyting algebra because it is finite. In particular we can consider meets inside L_0 and they distribute with the joins.

Let n_i for i=1,2 the maximum length of chains of join-irreducible elements of L_0

    k_1 < k_2 < ⋯ <k_n_i

such that k_n_i≤ h_i and k_1 ≰ h_j with i ≠ j, or equivalently k_1 ≰ h_1 ∧ h_2 where the meet is taken inside L_0.

Let n=n_1+n_2.

Intuitively, the natural number n measures how much h_1 ∧ h_2 is smaller than h_1 and h_2.

We prove the claim by induction on n.

Case 1: n=0.

Then h_1 ∧ h_2=h_1=h_2=g^-. We denote h_1=h_2 by h.

Since h ≪ g, we can apply the splitting axiom to g,h,h, hence there exist elements x_1,x_2 ∈ L different from 0 such that:

    g-x_1    = x_2 ≥ h 
     
         g-x_2    = x_1 ≥ h

We now show that (x_1,x_2) is a primitive couple of the second kind and induces the signature (h_1,h_2,g):


  * As shown in Lemma <ref> we have that x_1 ≠ x_2 and x_1,x_2 ∉ L_0.

  * g-x_1=x_2 and g-x_2=x_1 follow directly from the splitting axiom, see (<ref>).

Let a be a join-irreducible element of L_0, then for i=1,2:


  * If a < g then a ≤ g^-= h thus a-x_i=0 because h ≤ x_i as a consequence of the splitting axiom, see (<ref>).

  * If a < x_i then a < g because x_i < g by (<ref>) and therefore a ≤ g^- =h.

	If a ≤ h then, since x_i ∉ L_0 and h ≤ x_i, we have a < x_i.  

Case 2: n>0.

Suppose that the claim is true for any m<n.

Since h_1 ∨ h_2 =g^- ≪ g, we can apply the splitting axiom to g,h_1,h_2, hence there exist elements y_1,y_2 ∈ L different from 0 such that:

    g-y_1    = y_2 ≥ h_2 
     
         g-y_2    = y_1 ≥ h_1 
    
    	 h_2-y_1    =h_2-h_1 
    
         h_1-y_2    =h_1-h_2

Let L_0 ⟨ y_1,y_2 ⟩ be the sub-CBS of L generated by L_0 and { y_1,y_2 }. By local finiteness L_0 ⟨ y_1,y_2 ⟩ is finite and thus a co-Heyting algebra.

Before continuing the proof we show a series of claims.

The two following triples are signatures of the second kind in L_0 ⟨ y_1,y_2 ⟩:

    (h_1,   h_2 ∧ y_1,   y_1)
    
    	(h_1 ∧ y_2,   h_2,   y_2)

where the meets are taken inside L_0 ⟨ y_1,y_2 ⟩.


By Lemma <ref> y_1,y_2 ∉ L_0 are join-irreducibles in L_0 ⟨ y_1,y_2 ⟩.

Moreover, in L_0 ⟨ y_1,y_2 ⟩ we have that:

    h_1 ∨ (h_2 ∧ y_1)    =y_1^- 
    
    	(h_1 ∧ y_2) ∨ h_2    =y_2^-

Indeed

    h_1 ∨ (h_2 ∧ y_1)=(h_1 ∨ h_2) ∧ (h_1 ∨ y_1)=(h_1 ∨ h_2) ∧ y_1

and we have that this coincides with y_1^-, the predecessor of y_1 in L_0 ⟨ y_1,y_2 ⟩. To show this, observe that, as a consequence of Lemma <ref>, the inclusion L_0 ↪ L_0 ⟨ y_1,y_2 ⟩ is dual to a surjective 𝐏-morphism φ:P → Q with dom φ= P. Recall that Q and P are the posets of the join-irreducibles respectively of L_0 and L_0 ⟨ y_1,y_2 ⟩. Notice that the preimage of an element q of Q, i.e. a join-irreducible element of L_0 consists of the join-irreducible components of such element inside L_0 ⟨ y_1,y_2 ⟩. This is a consequence of the fact that φ^-1(q) ⊆ P corresponds to q as element of L_0 ⟨ y_1,y_2 ⟩ and the set of maximal elements of  φ^-1(q) is exactly the preimage of q because φ preserves the strict order.

Then φ^-1(g)= { y_1, y_2 } because y_1,y_2 are the join-irreducible components  of g in L_0 ⟨ y_1,y_2 ⟩ by Lemma <ref>.

Notice that for any downset D ⊆ Q we have φ^-1(D)=φ^-1(D) because dom φ= P and  φ^-1(D) is a downset in the domain of φ.

Since φ^-1( g)=φ^-1( g)= y_1 ∪ y_2 we have:

    φ^-1( g ∖{ g })=φ^-1( g ∖{ g })=( y_1 ∪ y_2) ∖{ y_1,y_2 }

Thus (h_1 ∨ h_2)∧ y_1=g^- ∧ y_1 is equal to y_1^- because of the following equations

    ( y_1 ∪ y_2) ∖{ y_1,y_2 }∩ y_1 =  y_1 ∖{ y_1,y_2 }=  y_1 ∖{ y_1 }

To prove that (h_1 ∧ y_2) ∨ h_2 =y_2^- the reasoning is analogous.

Notice that h_1 ∧ h_2 is the same taken in L_0 and in L_0 ⟨ y_1,y_2 ⟩ because by Lemma <ref> the inclusion L_0 ↪ L_0 ⟨ y_1,y_2 ⟩ preserves meets.
 
For i=1,2 the maximum length of chains of join-irreducibles of L_0 ⟨ y_1,y_2 ⟩ less than or equal to h_i that are not less than or equal to h_1 ∧ h_2 is the same as n_i defined above (recall that n_i is defined taking the join-irreducibles of L_0).



Indeed, suppose there exists a chain of join-irreducibles in L_0 ⟨ y_1,y_2 ⟩

    k_1 < k_2 < ⋯ <k_r

such that k_r ≤ h_i and k_1 ≰ h_1 ∧ h_2. By Lemma <ref> there exist b_1, …, b_r join-irreducibles in L_0 such that k_t is a join-irreducible component of b_t in L_0 ⟨ y_1,y_2 ⟩ for t=1, …,r. So b_r -h_i ≠ b_r because k_r ≤ b_r but k_r ≰ b_r -h_i. Indeed b_r -h_i is the join of the join-irreducible components of b_r that are not smaller than or equal to h_i but k_r is a join-irreducible component of b_r such that k_r ≤ h_i. Since b_r is join-irreducible of L_0 and b_r-h_i ≠ b_r it would be b_r ≤ h_i. Similarly b_t ≤ b_t+1 because b_t-b_t+1≠ b_t and b_1 ≰ h_1 ∧ h_2 since k_1 ≰ h_1 ∧ h_2 and we would obtain a chain of join-irreducibles in L_0

    b_1 < b_2 < ⋯ <b_r

On the other hand, given a chain of join-irreducibles in L_0

    b_1 < b_2 < ⋯ <b_r

such that b_r ≤ h_i and b_1 ≰ h_1 ∧ h_2. We can take k_t join-irreducible component of b_t inside L_0 ⟨ y_1,y_2 ⟩ such that k_1 ≰ h_1 ∧ h_2 and k_t < k_t+1 because k_t is join-irreducible and b_t+1 is the join of its join-irreducible components. Clearly we obtain a chain of join-irreducibles in L_0 ⟨ y_1,y_2 ⟩

    k_1 < k_2 < ⋯ <k_r

such that k_r ≤ h_i and k_1 ≰ h_1 ∧ h_2.




Suppose there exists a chain of join-irreducibles in L_0 ⟨ y_1,y_2 ⟩

    k_1 < k_2 < ⋯ <k_r

such that k_r ≤ h_i and k_1 ≰ h_1 ∧ h_2. Let, as above, φ:P → Q the surjective total 𝐏-morphism dual to the inclusion L_0 ↪ L_0 ⟨ y_1,y_2 ⟩, then

    φ(k_1) < φ(k_2) < ⋯ < φ(k_r)

is a chain of join-irreducibles in L_0 such that φ(k_r) ≤ h_i and φ(k_1) ≰ h_1 ∧ h_2.



[We remind that 𝐏-morphisms preserve the strict order.]

On the other hand a chain of join-irreducibles in L_0

    b_1 < b_2 < ⋯ <b_r

such that b_r ≤ h_i and b_1 ≰ h_1 ∧ h_2 can be lifted to a chain of join-irreducibles of L_0 ⟨ y_1,y_2 ⟩

    k_1 < k_2 < ⋯ <k_r

such that φ(k_s)=b_s for s=1, …, r using the fact that φ is a surjective 𝐏-morphism, we obtain that k_r ≤ h_i and k_1 ≰ h_1 ∧ h_2.


If h_2 ≰ h_1 then the maximum length of chains of join-irreducibles of L_0 ⟨ y_1,y_2 ⟩ less than or equal to h_2 ∧ y_1 that are not less than or equal to h_1 ∧ h_2= h_1 ∧ (h_2 ∧ y_1) is strictly smaller than n_2 (notice that n_2 ≠ 0 because h_2 ≰ h_1).

When h_1 ≰ h_2 in the same way we obtain the analogous result switching y_1 with y_2 and h_1 with h_2.



Indeed, suppose there exists a chain of join-irreducibles in L_0 ⟨ y_1,y_2 ⟩

    k_1 < k_2 < ⋯ <k_n_2

such that k_n_2≤ h_2 ∧ y_1 and k_1 ≰ h_1 ∧ h_2. By Lemma <ref> there exist b_1, …, b_n_2 join-irreducibles in L_0 such that k_t is a join-irreducible component of b_t in L_0 ⟨ y_1,y_2 ⟩, this would imply as before that b_n_2≤ h_2 because b_n_2 -h_2 ≠ b_n_2 and b_n_2 is join-irreducible of L_0 and similarly, b_t ≤ b_t+1 because b_t-b_t+1≠ b_t and b_1 ≰ h_1 ∧ h_2 since k_1 ≰ h_1 ∧ h_2 and we would obtain a chain of join-irreducibles in L_0

    b_1 < b_2 < ⋯ <b_n_2

with b_n_2 not a join-irreducible component of h_2. Indeed, suppose b_n_2 is a join-irreducible component of h_2, since k_n_2 is a join-irreducible component of b_n_2 in L_0 ⟨ y_1,y_2 ⟩ we would obtain that k_n_2 is a join-irreducible component of h_2 in L_0 ⟨ y_1,y_2 ⟩, but k_n_2≤ y_1 and y_1 is not greater than or equal to any join-irreducible component of h_2 which is not less than or equal to h_1 ∧ h_2 because h_2 - y_1=h_2-h_1=h_2-(h_1 ∧ h_2).

We have used the fact that if L_0 ⊆ L_1 is an extension of finite CBS, a,b ∈ L_0 such that b is a join-irreducible component of a in L_0 and c ∈ L_1 is a join-irreducible component of b in L_1 then c is also a join-irreducible component of a in L_1. We have taken a=h_2, b=b_n_2 and c=k_n_2.

Since b_n_2 is join-irreducible in L_0 and b_n_2≤ h_2 there would exist a continuation of the chain given by b_n_2+1 join-irreducible component of h_2 in L_0, but this is absurd because n_2 is the maximum length of such chains.




Suppose there exists a chain of join-irreducibles in L_0 ⟨ y_1,y_2 ⟩

    k_1 < k_2 < ⋯ <k_n_2

such that k_n_2≤ h_2 ∧ y_1 and k_1 ≰ h_1 ∧ h_2. Notice that this chain is not empty because n_2 ≠ 0. We have that k_n_2 is not a join-irreducible component of h_2 in L_0 ⟨ y_1,y_2 ⟩. Indeed, k_n_2≤ y_1 and y_1 is not greater than or equal to any join-irreducible component of h_2 which is not less than or equal to h_1 ∧ h_2 because h_2 - y_1=h_2-h_1=h_2-(h_1 ∧ h_2). Thus there would exist a continuation of such chain given by k_n_2+1 join-irreducible component of h_2 in L_0 ⟨ y_1,y_2 ⟩, but this is absurd because we have proved in Claim 2 that n_2 is the maximum length of such chains.


We can now apply the inductive hypothesis, to do so we shall consider different cases.

Subcase 2.1: h_1,h_2 incomparables. First, we consider the case in which h_1 ≰ h_2 and h_2 ≰ h_1, i.e. h_1,h_2 are incomparable.

What we have proved in Claim 3 implies that the sum of the lengths of the chains considered above for either of the two signatures (<ref>) is strictly smaller than n. Therefore we can apply the inductive hypothesis on both the two signatures (<ref>) considered inside L_0 ⟨ y_1,y_2 ⟩ to obtain two primitive couples (y_11, y_12) ∈ L^2 and (y_21, y_22) ∈ L^2 of the second kind over L_0 ⟨ y_1,y_2 ⟩ such that they induce respectively the signatures (h_1, h_2 ∧ y_1, y_1) and (h_1 ∧ y_2,  h_2, y_2). This means that:


  * y_11≠ y_12 and y_11,y_12∉ L_0 ⟨ y_1,y_2 ⟩, 

  * y_1- y_11=y_12 and y_1- y_12=y_11 

and for any a join-irreducible of L_0 ⟨ y_1,y_2 ⟩:


  * if a<y_1 then a-y_1i∈ L_0 ⟨ y_1,y_2 ⟩ for i=1,2, 

  * a < y_11 iff a ≤ h_1 and a < y_12 iff a ≤ (h_2 ∧ y_1). 

furthermore


  * y_21≠ y_22 and y_21,y_22∉ L_0 ⟨ y_1,y_2 ⟩, 

  * y_2- y_21=y_22 and y_2- y_22=y_21 

and for any a join-irreducible of L_0 ⟨ y_1,y_2 ⟩:


  * if a<y_2 then a-y_2i∈ L_0 ⟨ y_1,y_2 ⟩ for i=1,2, 

  * a < y_21 iff a ≤ (h_1 ∧ y_2) and a < y_22 iff a ≤ h_2. 

Notice that properties <ref> of y_11, y_12 and <ref> of y_21, y_22 actually hold for any a ∈ L_0 ⟨ y_1,y_2 ⟩ since any element in a finite CBS is the join of join-irreducible elements. Observe also that for a ∈ L_0 we have a ≤ y_ij iff a < y_ij because y_ij∉ L_0.

We want to prove that x_1=y_11∨ y_21 and x_2=y_12∨ y_22 are the two elements of L we are looking for, i.e. (x_1,x_2) is a primitive couple of the second kind over L_0 inducing the signature (h_1,h_2,g).

First of all, we observe that

    y_1-y_2i=y_1    and    y_2-y_1i=y_2     for  i=1,2

Indeed,

    y_1=g-y_2=(g-y_2)-y_2=y_1-y_2 ≤ y_1-y_2i≤ y_1

the second equation is shown analogously. (<ref>) also shows that y_1-y_2=y_1 and y_2-y_1=y_2.

Moreover

    y_1i-y_2j=y_1i   and    y_2i-y_1j=y_2i    for  i,j=1,2

Indeed, 

    y_11=y_1-y_12=(y_1-y_2)-y_12=(y_1-y_12)-y_2=y_11-y_2 ≤ y_11 - y_21≤ y_11

and thus y_11 - y_21=y_11, the remaining cases are analogous.

Notice the following fact about the extensions generated by the y_ij's:

The two extensions of finite CBSes given by L_0 ⟨ y_1,y_2 ⟩⊆ L_0 ⟨ y_1,y_2,y_11,y_12⟩⊆ L_0 ⟨ y_ij  |   i,j=1,2 ⟩ are both minimal of the second kind. This implies that any b join-irreducible of L_0 ⟨ y_1,y_2 ⟩ different from y_1,y_2 is still join-irreducible in L_0 ⟨ y_ij  |   i,j=1,2 ⟩.


It suffices to prove that (y_21, y_22) is a primitive couple of the second kind over L_0 ⟨ y_1,y_2, y_11, y_12⟩.

First of all, as a consequence of Lemma <ref>, y_1,y_2 are join-irreducible in L_0 ⟨ y_1,y_2 ⟩, thus y_2 is join-irreducible in L_0 ⟨ y_1,y_2, y_11, y_12⟩.


  * y_21≠ y_22 by property <ref> of y_21, y_22.

	y_21,y_22∈ L ∖ L_0 ⟨ y_1,y_2, y_11, y_12⟩. Indeed, if y_21∈ L_0 ⟨ y_1,y_2, y_11, y_12⟩ then y_22=y_2-y_21∈ L_0 ⟨ y_1,y_2, y_11, y_12⟩ and vice versa. In that case y_2=y_21∨ y_22∈ L_0 ⟨ y_1,y_2, y_11, y_12⟩ with y_21, y_22≠ y_2 because they are not in L_0 ⟨ y_1,y_2 ⟩, but this is absurd because y_2 is join-irreducible.

  * y_2-y_21=y_22 and y_2-y_22=y_21 by property <ref> of y_21, y_22.

  * Since L_0 ⟨ y_1,y_2, y_11, y_12⟩ is a minimal finite extension of L_0 ⟨ y_1,y_2 ⟩, its join-irreducibles are y_11, y_12 and the join-irreducibles of L_0 ⟨ y_1,y_2 ⟩ except y_1. If a is a join-irreducible of L_0 ⟨ y_1,y_2, y_11, y_12⟩ such that a < y_2 then a is join-irreducible in L_0 ⟨ y_1,y_2 ⟩ because a ≠ y_11, y_12 since y_11, y_12≮ y_2: indeed y_1i-y_2=y_1i-(y_21∨ y_22)=(y_1i-y_21)-y_22=y_1i≠ 0 by (<ref>).  Thus a-y_2i∈ L_0 ⟨ y_1,y_2 ⟩ by property <ref> of of y_21, y_22.


Moreover, we observe that

    g-x_1=x_2    and    g-x_2=x_1

because thanks to equations (<ref>) we have:

    g-x_1=(y_1 ∨ y_2)-(y_11∨ y_21)=((y_1-y_21)-y_11) ∨ ((y_2 - y_11)-y_21)
    
    		=(y_1-y_11) ∨ (y_2-y_21)=y_12∨ y_22=x_2;

showing the second equation of (<ref>) is analogous.

We are now ready to show that (x_1,x_2) is a primitive couple of the second kind over L_0 inducing the signature (h_1,h_2,g).


  * Equations (<ref>) imply that g=x_1 ∨ x_2, thus if x_1=x_2 then x_1=g=0 but this is absurd because x_1,x_2 ≠ 0 since y_11, y_12, y_21, y_22≠ 0 because they are not in L_0.

Furthermore x_1,x_2 ∉ L_0; this is because g is join-irreducible in L_0 and g-x_1=x_2 and g-x_2=x_1 are different from 0 and g.

  * See equations (<ref>).

Let now a be a join-irreducible element of L_0 and i=1,2:


  * If a < g then a ≤ g^-=h_1 ∨ h_2 and a ≤ h_1 or a ≤ h_2
	
	
  * If a ≤ h_1 then a-x_1=0 because h_1 ≤ y_11≤ x_1 by property <ref> of y_11.
	
  * If a ≤ h_2 and a ≰ h_1 we want to prove that a-x_1=a.
		
		The join-irreducible components of a in L_0 ⟨ y_1,y_2 ⟩ coincide with the join-irreducible component of a in L_0 ⟨ y_ij  |   i,j=1,2 ⟩.
		
		
		Since a is the join of its join-irreducible components in L_0 ⟨ y_1,y_2 ⟩, it is sufficient to prove that any join-irreducible component b of a in L_0 ⟨ y_1,y_2 ⟩ is join-irreducible in L_0 ⟨ y_ij  |   i,j=1,2 ⟩. We have b ≠ y_1,y_2 because b ≤ h_2 and y_1,y_2 ≰ h_2 since if y_i ≤ h_2 then 0=y_i -h_2=(g-y_j)-h_2=(g-h_2)-y_j=g-y_j=y_i  with i ≠ j which is absurd. Thus by Claim 4 we have that b is also join-irreducible in L_0 ⟨ y_ij  |   i,j=1,2 ⟩.
		
		Since a is join-irreducible of L_0 and a ≰ h_1 it is a-h_1=a. For any b join-irreducible component of a in L_0 ⟨ y_1,y_2 ⟩ we have b ≰ h_1 because a-h_1=a means that h_1 is not greater than or equal to any join-irreducible component of a. Since b ≰ h_1 and in particular b ≰ h_1 ∧ y_2 then property <ref> of y_11 and property <ref> of y_21 imply that b ≰ y_11, y_21. Therefore b ≰ y_11∨ y_21=x_1 because b is join-irreducible in L_0 ⟨ y_ij  |   i,j=1,2 ⟩. This implies that a-x_1=a because x_1 is not greater than or equal to any join-irreducible component of a in L_0 ⟨ y_ij  |   i,j=1,2 ⟩.

	For a-x_2 the property is checked in an analogous way.
	

  * If a ≤ h_i then a < y_ii≤ x_i by property <ref> of y_11 and property <ref> of y_22

	If a < x_1 then a < g by (<ref>) and a ≤ h_1 ∨ h_2=g^-. Let b be a join-irreducible component of a in L_0 ⟨ y_1,y_2 ⟩. We claim that b ≤ h_1. We have that b is join-irreducible in L_0 ⟨ y_1,y_2 ⟩ and b ≠ y_1,y_2 because  b < x_ 1 and y_1,y_2 ≮ x_1. Indeed, by equations (<ref>), we have:
	
    y_2-x_1=(y_2-y_21)-y_11=y_22-y_11=y_22≠ 0 
    
    	y_1-x_1=(y_1-y_11)-y_21=y_12-y_21=y_12≠ 0

	Suppose b ≰ h_1, then by property <ref> of y_11 we would get b ≮ y_11, furthermore b ≰ h_1 ∧ y_2 and by property <ref> of y_21 we would get b ≮ y_21. Then b would also be join-irreducible in L_0 ⟨ y_ij  |   i,j=1,2 ⟩ (see Claim 4). Therefore b ≮ y_11∨ y_21=x_1 but this is absurd. Thus for any b join-irreducible component of a we have b ≤ h_1 and hence a ≤ h_1.
 
	For x_2 the reasoning is analogous

Subcase 2.2: h_1,h_2 comparables. The remaining cases are when h_1 < h_2 or h_2 < h_1 since h_1=h_2 only occurs when n=0.

We now consider the case h_1 < h_2, for h_2 < h_1 the reasoning is analogous.

In this case, by equations (<ref>), we have y_2^-=(h_1 ∧ y_2) ∨ h_2=h_2 in L_0 ⟨ y_1,y_2 ⟩. Notice that we can apply the inductive hypothesis only on the first signature in (<ref>) because h_2 ≰ h_1 but it is not true that h_1 ≰ h_2. Then we obtain the existence of y_11,y_12 with the same properties <ref>, <ref>, <ref>, <ref> as in the previous subcase. We define x_1 = y_11 and x_2=y_12∨ y_2.

We want to prove that x_1,x_2 form a primitive couple (x_1,x_2) of the second kind over L_0 inducing the signature (h_1,h_2,g).

We have

    g-x_1=x_2    and    g-x_2=x_1

because

    g-x_1=(y_1 ∨ y_2)-y_11=(y_1-y_11) ∨ (y_2-y_11)=y_12∨ y_2=x_2 
    
    g-x_2=(y_1 ∨ y_2)-(y_12∨ y_2)=((y_1-y_2)-y_12) ∨ ((y_2-y_2)-y_12)=
    
    y_1-y_12=y_11=x_1

We have used that y_2 -y_11=y_2, it is proven in the same way as (<ref>) above.


  * Equations (<ref>) imply g=x_1 ∨ x_2, thus if x_1=x_2 then x_1=g=0 but this is absurd because x_1,x_2 ≠ 0 since y_11, y_12, y_2 ≠ 0 because they are not in L_0.

Furthermore x_1,x_2 ∉ L_0 since g is join-irreducible in L_0 and g-x_1=x_2 and g-x_2=x_1 are different from 0 and g.

  * See equations (<ref>).

Let now a be a join-irreducible element of L_0:


  * If a < g then a ≤ g^-= h_1 ∨ h_2=h_2.
	
	
  * If a ≤ h_1 then a-x_1=0 because h_1 ≤ y_11=x_1, moreover a ≤ h_1 < h_2 ≤ y_2 < x_2 imply a-x_2=0.
	
  * If a ≤ h_2 and a ≰ h_1 clearly a-x_2=0 because a ≤ h_2 ≤ y_2 ≤ x_2. We want to prove that a-x_1=a.
		
		The join-irreducible components of a in L_0 ⟨ y_1,y_2 ⟩ coincide with the join-irreducible components of a in L_0 ⟨ y_1,y_2, y_11, y_12⟩.
		
		
		Since a is the join of its join-irreducible components in L_0 ⟨ y_1,y_2 ⟩, it is sufficient to prove that any join-irreducible component b of a in L_0 ⟨ y_1,y_2 ⟩ is join-irreducible in L_0 ⟨ y_1,y_2, y_11, y_12⟩. Pick such a,b. We have b ≠ y_1 because b ≤ h_2 and y_1 ≰ h_2. Notice that y_1 ≰ h_2 since y_1 ≤ h_2 would imply 0=y_1-h_2=(g-y_2)-h_2=(g-h_2)-y_2=g-y_2=y_1 which is absurd. Then we have that b is also join-irreducible in L_0 ⟨ y_1,y_2, y_11, y_12⟩, this follows from the fact that L_0 ⟨ y_1,y_2, y_11, y_12⟩ is a minimal extension of L_0 ⟨ y_1,y_2 ⟩ of the second kind, which implies that the join-irreducibles in L_0 ⟨ y_1,y_2 ⟩ different from y_1 are still join-irreducible in L_0 ⟨ y_1,y_2, y_11, y_12⟩.
		
		Since a is join-irreducible of L_0 and a ≰ h_1 it is a-h_1=a. For any b join-irreducible component of a in L_0 ⟨ y_1,y_2 ⟩ we have b ≰ h_1 because a-h_1=a means that h_1 is not greater than or equal to any join-irreducible component of a. Since b ≰ h_1 by property <ref> of y_11 we have that b ≮ y_11=x_1, therefore b ≰ x_1 because b ≠ y_11 since y_11∉ L_0 ⟨ y_1,y_2 ⟩ . This implies that a-x_1=a because x_1 is not greater than or equal to any join-irreducible component of a in L_0 ⟨ y_1,y_2, y_11, y_12⟩.
	

  * By property <ref> of y_11 we have that a ≤ h_1 iff a < y_11=x_1.

	If a ≤ h_2 then a ≤ h_2 < y_2 ≤ x_2 since h_2=y_2^-.

	If a < x_2, since x_2 = y_12∨ y_2 ≤ y_1 ∨ y_2=g then a < g and a ≤ g^-=h_1 ∨ h_2=h_2.





 §.§ Density axioms


[Density 1 Axiom] For every c there exists b ≠ 0 such that c ≪ b


Any existentially closed CBS satisfies the Density 1 Axiom.



It is sufficient to show, by Lemma <ref>, that for any finite CBS L_0 and c ∈ L_0 there exists a finite extension L_0 ⊆ L with b ∈ L different from 0 such that c ≪ b.

Let P_0 be the finite poset dual to L_0 and C its downset corresponding to c.

Let P be the poset obtained by P_0 by adding a new maximum element m ∈ P such that m ≥ p for any p ∈ P_0 and φ:P → P_0 a surjective 𝐏-morphism such that dom φ=P_0 and it is the identity on its domain. Then C ≪ m and take as L the CBS dual to P and b ∈ L corresponding to m.


[Density 2 Axiom] For every c,a_1,a_2,d such that a_1,a_2 ≠ 0, c ≪ a_1, c ≪ a_2 and a_1-d=a_1, a_2-d=a_2 there exists an element b different from 0 such that:

    c ≪ b
     
         b ≪ a_1 
    
         b ≪ a_2 
    
         b-d=b



Any existentially closed CBS satisfies the Density 2 Axiom.



It is sufficient to show, by Lemma <ref>, that for any finite CBS L_0 and c,a_1,a_2,d such that a_1,a_2 ≠ 0, c ≪ a_1, c ≪ a_2 and a_1-d=a_1, a_2-d=a_2 there exists a finite extension L_0 ⊆ L with b ∈ L different from 0 such that c ≪ b, b ≪ a_1, b ≪ a_2 and b-d=b.

Let P_0 the poset dual to L_0 and C,A_1,A_2,D its downsets corresponding to c,a_1,a_2,d.

If C= ∅ choose two maximal elements α^1, α^2 respectively of A_1 and A_2 and obtain a poset P by adding a new element β to P_0 and setting for any x ∈ P:


  * β≤ x iff x=β or α^1 ≤ x or α^2 ≤ x.

	If α^1, α^2 are incomparable they become the only two successors of β in P, otherwise if e.g. α^1 ≤α^2 then α^1 is the only successor of β.

  * x ≤β iff x=β, i.e. β is minimal in P.

Define a surjective 𝐏-morphism φ:P → P_0 taking dom φ=P_0 and φ acting as the identity on its domain.
Take B= β, we have:


  * φ^-1(C)=∅≪ B,

  * B ≪φ^-1(A_1)=A_1 ∪{β},

  * B ≪φ^-1(A_2)=A_2 ∪{β},

  * B- φ^-1(D)=B.

	Indeed, since a_1-d=a_1 and a_2-d=a_2, D does not contain any maximal element of A_1 or A_2, in particular it does not contain α^1 or α^2

Take L the CBS dual to P and b ∈ L corresponding to B.

If C ≠∅ let γ_1, …, γ_n be the maximal elements of C.

Choose for any i=1, …,n two maximal elements α_i^1, α_i^2 respectively of A_1 and A_2 such that γ_i ≤α_i^1 and γ_i ≤α_i^2. Notice that they exist and γ_i ≠α_i^1, γ_i ≠α_i^2  because C ≪ A_1 and C ≪ A_2.

Obtain a poset P by adding new elements β_1, …, β_n to P_0 and setting for any x ∈ P:


  * β_i ≤ x iff x=β_i or α_i^1 ≤ x or α_i^2 ≤ x.

	If α_i^1, α_i^2 are incomparable they become the only two successors of β_i in P, otherwise if e.g. α_i^1 ≤α_i^2 then α_i^1 is the only successor of β_i.

  * x ≤β_i iff x=β or x ≤γ_i,

	i.e. γ_i is the unique predecessor of β_i in P.

Define a surjective 𝐏-morphism φ:P → P_0 taking dom φ=P_0 and φ acting as the identity on its domain.

Take B= β_1 ∪⋯∪β_n, we have:


  * φ^-1(C) ≪ B,

  * B ≪φ^-1(A_1)=A_1 ∪{β_1, …, β_n },

  * B ≪φ^-1(A_2)=A_2 ∪{β_1, …, β_n },

  * B- φ^-1(D)=B.

	Indeed D does not contain any maximal element of A_1 or A_2, in particular it does not contain α_i^1 or α_i^2 for any i=1, …,n.

Take L the CBS dual to P and b ∈ L corresponding to B.



Let L be a CBS satisfying the Splitting, Density 1 and Density 2 Axioms.

Then for any finite sub-CBS L_0 ⊆ L and for any signature (h,G) of the first kind in L_0 there exists a primitive element x ∈ L of the first kind over L_0 inducing such signature.




We follow this strategy: if G= ∅ we use the Density 1 Axiom to take an element m ∈ L greater than any element of L_0, then, thanks to the Splitting Axiom, using Theorem <ref> we `split' m into two elements, one over 1_L_0 the top element of L_0 and another over h. It turns out that this second element is primitive of the first kind and induces the signature (h, ∅).
If G is nonempty and G={ g_1, …, g_k } we suppose to have already found a primitive element y inducing the signature (h,{ g_1, …, g_k-1}). Then, using Theorem <ref> again, we `split' g_k into two elements g_k',g_k”, the first over h and the second over the predecessor of g_k. Finally, applying the Density 2 Axiom, we obtain an element of L in between h, g_k' and y. It turns out that this element is primitive of the first kind and induces the signature (h, G).


The statement of the Theorem require that, according to the definition of primitive element inducing a given signature, we need to do the following. Given h ∈ L_0 and G a set of join-irreducibles of L_0 such that h < g for any g ∈ G, we have to find x ∈ L such that:


  * x ∉ L_0 

and for any a join-irreducible of L_0:


  * a-x ∈ L_0, 

  * either x-a= x  or  x-a= 0, 

  * a < x iff a ≤ h and x < a iff g_i ≤ a for some i=1, …, k. 

The proof is by induction on k= # G.

Case k=0.

Let 1_L_0 be the maximum element of L_0, by Density 1 there exists 0 ≠ m ∈ L such that 1_L_0≪ m.

Then L_1=L_0 ∪{ m } is a sub-CBS of L. Indeed it is closed under taking joins and differences since for any a ∈ L_0 we have m > a and thus a-m=0 and m = m-1_L_0≤ m-a ≤ m, therefore m-a=m. Hence m is a join-irreducible of L_1. Furthermore it is clear that the join-irreducibles of L_1 are the join-irreducibles of L_0 and m.

(h,1_L_0,m) is a signature of the second kind in L_1, indeed h ∨ 1_L_0=1_L_0=m^-.

Thanks to the Splitting Axiom we can apply Theorem <ref> to the signature (h,1_L_0,m) in L_1 and obtain the existence of a primitive couple of the second kind (x_1,x_2) ∈ L^2 inducing such signature. 
Thus we have that there exist x_1,x_2 ∈ L such that:


  * x_1 ≠ x_2 and x_1,x_2 ∉ L_1, 

  * m-x_1=x_2 and m-x_2=x_1 

and for any c join-irreducible of L_1:


  * if c < m then c-x_i ∈ L_1 for i=1,2, 

  * c < x_1 iff c ≤ h and c < x_2 iff c ≤ 1_L_0. 

Recall that Lemma <ref> implies that for any c ∈ L_1:
 

  * c-x_i ∈ L_1 or c-x_i= b ∨ x_j for some b ∈ L_1 with { i,j } = { 1,2 }. 

  * x_i-c= x_i  or  x_i-c= 0 for i=1,2. 

Let x=x_1, it is the element we were looking for. Indeed we now show that x is a primitive element of the first kind over L_0 inducing the signature (h, ∅)


  * x ∉ L_0 since x=x_1 ∉ L_1 by property <ref> of x_1.

Let a be a join-irreducible of L_0. Then


  * a-x_1 ∈ L_0.
	 
	Indeed, from a ≤ 1_L_0 it follows (by property <ref> of x_2) a < x_2; then by <ref> either a-x_1 ∈ L_1 or a-x_1=b ∨ x_2 with b ∈ L_0. The latter is absurd because (for a < x_2) we would get x_2 > a ≥ a-x_1=b ∨ x_2 ≥ x_2. Then a-x_1 ∈ L_1, i.e. a-x_1 ∈ L_0 because m > a ≥ a-x_1.

  * x_1-a=x_1 or x_1-a=0 by property <ref>.

  * a < x_1 if and only if a ≤ h by property <ref> of x_1.

	x_1 ≮ a, because if x_1 < a then x_1 < 1_L_0 and so 0=x_1-1_L_0=(m-x_2)-1_L_0=(m-1_L_0)-x_2=m-x_2=x_1 which is absurd because x_1 ∉ L_1 by property <ref> of x_1.

Case k ≥ 1.

Suppose that G= { g_1, …, g_k }. By inductive hypothesis there exists a primitive element y ∈ L of the first kind over L_0 which induces the signature (h, { g_1, …, g_k-1}). This means that for any a join-irreducible of L_0:


  * y ∉ L_0, 

  * a-y ∈ L_0, 

  * either y-a= y  or  y-a= 0, 

  * a < y iff a ≤ h and y < a iff g_i ≤ a for some i=1, …, k-1. 

Recall that Lemma <ref> shows that the properties <ref> and <ref> actually hold for any a ∈ L_0.

Notice that g_k is still join-irreducible in the sub-CBS L_0 ⟨ y ⟩⊆ L generated by L_0 and y since L_0 ⊆ L_0 ⟨ y ⟩ is a minimal finite extension of the first kind by Theorem <ref>.

Since L satisfies the Splitting Axiom, we can apply Theorem <ref> to the signature (h,g_k^-, g_k) in L_0 ⟨ y ⟩. Notice that it is a signature of the second kind because h ∨ g_k^-= g_k^- ≪ g_k. Therefore, there exists a primitive couple of the second kind (g_k',g_k”) ∈ L^2 inducing such signature. Thus we have that there exist g_k',g_k”∈ L such that:


  * g_k',g_k”∉ L_0 ⟨ y ⟩ and g_k' ≠ g_k”, 

  * g_k-g_k'=g_k” and g_k-g_k”=g_k' 

and for any a join-irreducible of L_0 ⟨ y ⟩:


  * if a<g_k then a-g_k' ∈ L_0 ⟨ y ⟩ and a-g_k”∈ L_0 ⟨ y ⟩, 

  * a < g_k' iff a ≤ h and a < g_k” iff a ≤ g_k^-. 

Observe that property <ref> actually holds for any a ∈ L_0 ⟨ y ⟩ since any element in a finite CBS is the join of join-irreducible elements.

Apply the Density 2 Axiom on h,y,g_k',d where 

    d= ⋁{ b  join-irreducible of L_0 s.t.  b ≱ g_1, …, b ≱ g_k }.

We can apply it because:

h ≪ y since by property <ref> of y we have y-h=y because h ∈ L_0 and h < y.

h ≪ g_k' since h < g_k' and g_k'-h=(g_k-g_k”)-h=(g_k-h)-g_k”=g_k-g_k”=g_k'. Notice that g_k-h=g_k because g_k is join-irreducible in L_0. 

y-d=y since for any b join-irreducible in L_0 such that b ≱ g_1, …, b ≱ g_k we have y-b=y: otherwise, since y is join-irreducible in L_0 ⟨ y ⟩, it would be y-b=0 so b > y and then by property <ref> of y we would have b ≥ g_i for some i<k which is absurd.

g_k'-d=g_k' since 

    g_k = g_k-⋁{ b  join-irreducible of L_0 s.t.  b ≱ g_k }≤ g_k-d ≤ g_k

and g_k'-d=(g_k-g_k”)-d=(g_k-d)-g_k”=g_k-g_k”=g_k'.

Then by the Density 2 Axiom there exists 0 ≠ x ∈ L such that 

    h ≪ x,   x ≪ y,   x ≪ g_k'  and  x-d=x

x is the element we were looking for. Indeed, it is primitive of the first kind over L_0 and induces the signature (h,G):


  * We have x ∉ L_0 because if x ∈ L_0 then since x < y it would be x ≤ h by property <ref> of y but this is absurd because x ≠ 0 and h ≪ x.

Let a be a join-irreducible of L_0:


  * If a ≤ h then a-x=0 since h ≤ x by (<ref>).

	If a ≰ h then by property <ref> of g_k' we have a ≮ g_k'.
	
	
  * If a ≰ h and a ≠ g_k then a is still join-irreducible in L_0 ⟨ y,g_k',g_k”⟩ (since L_0 ⟨ y ⟩⊆ L_0 ⟨ y,g_k',g_k”⟩ is a minimal finite extension by Theorem <ref>), thus a-g_k'=a. Therefore a-x=a because a=a-g_k' ≤ a-x ≤ a since x ≤ g_k'.
	
  * If a=g_k then by x ≪ g_k' (see (<ref>))
	
    g_k-x=(g_k' ∨ g_k”)-x=(g_k'-x) ∨ (g_k”-x )=g_k' ∨ ((g_k-g_k')-x)
    
         =g_k' ∨ (g_k-(g_k' ∨ x)) =g_k' ∨ (g_k-g_k')=g_k' ∨ g_k”=g_k.

	

  * If a ≥ g_i for some i=1, …,k then:
	
	
  * If i ≠ k then a ≥ y ≥ x and x-a=0 by property <ref> of y and (<ref>).
	
  * If i=k then a ≥ g_k ≥ g_k' ≥ x and x-a=0.
	
	If a ≱ g_i for any i=1,…,k then a ≤ d and x-a=x since x=x-d ≤ x-a ≤ x

  * If a < x then a < g_k' and thus a ≤ h by property <ref> of g_k'.

	If a ≤ h then a < x because h <x by (<ref>).

	If x <a and a ≱ g_1, …, a ≱ g_k, then a ≤ d and x=x-d ≤ x-a =0 which is absurd, thus g_i ≤ a for some i=1, …,k.

	If g_i ≤ a for some i=1, …,k then:
	
	
  * If i ≠ k then, since y < g_i by property <ref> of y, we have x <y < g_i ≤ a and thus x < a.
	
  * If i=k then x < g_k' <g_k ≤ a and thus x<a.
	





§ PROPERTIES OF EXISTENTIALLY CLOSED CBSES
 

From our investigation we can easily obtain some properties of the existentially closed CBSes:



If L is an existentially closed CBS, then L does not have a maximum element.



Since L satisfy the Density 1 Axiom for any c ∈ L there exists an element b ≠ 0 such that c ≪ b and therefore c <b. This implies that there cannot be a maximum element of L.



Let L be an existentially closed CBS and a,b ∈ L.

If a and b are incomparable, i.e. a ≰ b and b ≰ a, then there does not exist the meet of a and b in L.

Notice that if a ≤ b then the meet exists and it is a.



Denote by c the meet of a and b. Consider L_0 ⊆ L the sub-CBS generated by a,b,c. It is finite by local finiteness. c is the meet of a and b also in L_0.

Since a,b are incomparable there exist g_1,g_2 join-irreducible components in L_0 respectively of a and b such that g_1 ≰ b and g_2 ≰ a.

By Theorem <ref> taking h=0 ∈ L_0 we have that there exists x ∈ L ∖ L_0 such that for any d ∈ L_0:


  * d < x iff d=0,

  * x < d iff g_i ≤ d for i=1 or i=2.

We have that x ≰ c since  x ∉ L_0, g_1 ≰ c and g_2 ≰ c, therefore c <  c ∨ x. Notice that x < g_1 ≤ a and x < g_2 ≤ b, thus c ∨ x ≤ a and c ∨ x ≤ b. This implies that c cannot be the meet of a and b in L.




If L is an existentially closed CBS, then there are no join-irreducible elements of L.



Let g be a nonzero element of L. We can apply the splitting axiom on the triple g,0,0, then there exist g_1,g_2 ∈ L such that 

    g-g_1=g_2,    g-g_2=g_1   and   g_1,g_2 ≠ 0.

Since g_1,g_2 ≤ g and g-(g_1 ∨ g_2)=(g-g_1)-g_2=0 we have that g=g_1 
∨ g_2. Moreover g_1,g_2 ≠ g because g_1,g_2 ≠ 0. Therefore g cannot be join-irreducible because g=g_1 ∨ g_2 with g_1,g_2 ≠ g, recall that 0 is never join-irreducible.



alpha
 





