BRICS RS-98-30 C. Butz: Finitely Presented Heyting Algebras BRICS

Basic Research in Computer Science

Finitely Presented Heyting Algebras

Carsten Butz BRICS Report Series RS-98-30 ISSN 0909-0878 November 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/98/30/

Finitely Presented Heyting Algebras

Carsten Butz^{∗}

October 15, 1998

Abstract

In this paper we study the structure of finitely presented Heyting algebras. Using algebraic techniques (as opposed to techniques from proof-theory) we show that every such Heyting algebra is in fact co-Heyting, improving on a result of Ghilardi who showed that Heyting algebras free on a finite set of generators are co-Heyting. Along the way we give a new and simple proof of the finite model property. Our main technical tool is a representation of finitely presented Heyting algebras in terms of a colimit of finite distributive lattices. As applications we construct explicitly the minimal join-irreducible elements (the atoms) and the maximal join-irreducible elements of a finitely presented Heyting algebras in terms of a given presentation. This gives as well a new proof of the disjunction property for intuitionistic propositional logic.

Unfortunately not very much is known about the structure of Heyting algebras, although it is understood that implication causes the complex structure of Heyting algebras. Just to name an example, the free Boolean algebra on one generator has four elements, the free Heyting algebra on one generator is infinite.

Our research was motivated a simple application of Pitts’ uniform interpolation theorem [11]. Combining it with the old analysis of Heyting algebras free on a finite set of generators by Urquhart [13] we get a faithful functor

J: HA_{f.p.}^{op} → PoSet,

∗BRICS, Basic Research in Computer Science, Centre of the Danish National Research Foundation, Computer Science Department, Aarhus University, Ny Munkegade, DK–8000 Århus C, Denmark, butz@brics.dk.

sending a finitely presented Heyting algebra to the partially ordered set of its join-irreducible elements, and a map between Heyting algebras to its leftadjoint restricted to join-irreducible elements. We will explore on the induced duality more detailed in [5].

Let us briefly browse through the contents of this paper: The first section recapitulates the basic notions, mainly that of the implicational degree of an element in a Heyting algebra. This is a notion relative to a given set of generators. In the next section we study finite Heyting algebras. Our contribution is a simple proof of the finite model property which names in particular a canonical family of finite Heyting algebras into which we can embed a given finitely presented one.

In Section 3 we recapitulate the standard duality between finite distributive lattices and finite posets. The ‘new’ feature here is a strict categorical formulation which helps simplifying some proofs and avoiding calculations. In the following section we recapitulate the description given by Ghilardi [8] on how to adjoin implications to a finite distributive lattice, thereby not destroying a given set of implications. This construction will be our major technical ingredient in Section 5 where we show that every finitely presented Heyting algebra is co-Heyting, i.e., that the operation (−) \ (−) dual to implication is defined. This result improves on Ghilardi’s [8] that this is true for Heyting algebras free on a finite set of generators.

Then we go on analysing the structure of finitely presented Heyting algebras in Section 6. We show that every element can be expressed as a finite join of join-irreducibles, and calculate explicitly the maximal join-irreducible elements in such a Heyting algebra (in terms of a given presentation). As a consequence we give a new proof of the disjunction property for propositional intuitionistic logic. As well, we calculate the minimal join-irreducible elements, which are nothing but the atoms of the Heyting algebra.

Finally, we show how all this material can be used to express the category of finitely presented Heyting algebras as a category of fractions of a certain category with objects morphism between finite distributive lattices.

Acknowledgements: Part of the results of this paper were presented at the 65th Peripatetic Seminar on Sheaves and Logic in Århus, November 1997, and at a talk at Utrecht University in March 1998. I would like to thank Anders Kock, who patiently watched this paper growing.

1 Implicational degree

The object of study in this paper are Heyting algebras. For example, the free Heyting algebra on a set of generators X is (isomorphic to) the set of equivalence classes of terms with free variables among elements of X. Here the terms are freely generated by the grammar

terms(X) x(∈ X) | ⊤ | ⊥ | t ∧ t′ | t ∨ t′ | t → t′ ,

and the equivalence relation is provability in intuitionistic propositional logic, that is, t and t′ are equivalent if ⊢_{i} t ↔ t′. (We refer to [6] for a possible axiomatisation.) We use the usual abbreviations ¬t for t → ⊥ and t ↔ t′ for (t → t′) ∧ (t′ → t), the latter we already used above. The free Heyting algebra on a set of generators X is denoted HA[X]. In case X is a finite set (a tuple x̄) we write as well HA[x̄]. We assume that the reader is familiar with the notions of finitely generated algebras, finitely presented algebras, and finite algebras. With morphisms the structure preserving maps we have the corresponding full inclusions of categories

HA_{fin} ↪ HA_{f.p.} ↪ HA_{f.g.} ↪ HA .

We warn the reader that we usually confuse a term and the element denoted by it in the free Heyting algebra. Only if absolutely necessary we denote equivalence classes of terms by [t].

The implicational degree of a term t is defined by recursion:

degx̄(⊤) = degx̄(⊥) = degx̄(x_{i}) = 0,

degx̄(t_{1}(x̄) ∧ t_{2}(x̄)) = degx̄(t_{1}(x̄) ∨ t_{2}(x̄)) = max{degx̄(t_{1}(x̄)), degx̄(t_{2}(x̄))},

degx̄(t_{1}(x̄) → t_{2}(x̄)) = 1 + max{degx̄(t_{1}(x̄)), degx̄(t_{2}(x̄))}.

If the set of variables is clear from the context we write deg(t).

The implicational degree of an element h ∈ HA[x̄] is the minimum over all degrees of terms t that represent h. For example, in HA[x̄] we have (identifying a term with the equivalence class it represents (!))

degx̄(x_{1} ∧ (x_{2} → x_{3})) = 1,
degx̄(x_{1} → x_{1}) = 0 = degx̄(⊤),
degx̄(x_{1} ∧ (x_{1} → x_{2})) = 0 = degx̄(x_{1} ∧ x_{2}).

The elements of implicational degree ≤ n form a finite distributive sub-lattice Dn ; x̄ of HA[x̄], so that we get a sequence

\xymatrix{D0 ; x̄ \ar@{^{(}->}[r] & D1 ; x̄ \ar@{^{(}->}[r] & … \ar@{^{(}->}[r] & Dn ; x̄ \ar@{^{(}->}[r] & … & HA[x̄].}

We speak as well about the standard filtration of HA[x̄] (by finite distributive lattices).

A Heyting algebra H is finitely generated (f.g.) if there exists a finite set h̄ in H so that any element in H can be expressed as a term in h̄. Equivalently, H is finitely generated if there is a surjective morphism χ: HA[x̄] ↠ H. Writing E_{χ}^{n} for the image of Dn ; x̄ under the map χ, we get a diagram of finite distributive lattices as follows:

\xymatrix{D0 ; x̄ \ar@{^{(}->}[r] \ar@{->>}[d]_{χ^{0}} & D1 ; x̄ \ar@{^{(}->}[r] \ar@{->>}[d]_{χ^{1}} & … \ar@{^{(}->}[r] & Dn ; x̄ \ar@{^{(}->}[r]^{α^{n,n+1}} \ar@{->>}[d]_{χ^{n}} & Dn+1 ; x̄ \ar@{^{(}->}[r] \ar@{->>}[d]_{χ^{n+1}} & … & HA[x̄] \ar@{->>}[d]^{χ} \\ E_{χ}^{0} \ar@{^{(}->}[r] & E_{χ}^{1} \ar@{^{(}->}[r] & … \ar@{^{(}->}[r] & E_{χ}^{n} \ar@{^{(}->}[r]_{β^{n,n+1}} & E_{χ}^{n+1} \ar@{^{(}->}[r] & … & H}  (1)

The maps into HA[x̄] or H are denoted α^{n,∞}: Dn ; x̄ → HA[x̄], respectively β^{n,∞}: E_{χ}^{n} → H. We call the sequence {E_{χ}^{i}}_{i≥0} the standard filtration of H, induced by the surjective map χ (or by the elements h̄ = χ(x̄)). Elements in E_{χ}^{n} \ E_{χ}^{n−1} are said to have degree n, and we write degh̄(e) = deg_{χ}(e) = n for this degree. Diagram (1) will be our main tool for analysing the structure of H.

Next we define the rank of a set of generators (or of a surjection χ as above): It is the minimum of implicational degrees of terms, needed to express H as a quotient HA[x̄]/(t^{j}(x̄) = s^{j}(x̄))_{J}. Formally it becomes as follows:

Definition 1.1 The rank of χ (or of the set of generators h̄), rank_{χ}(H) (or rankh̄(H)) is defined as

min{r | ∃t^{j}(x̄), s^{j}(x̄): deg(t^{j}), deg(s^{j}) ≤ r & H ≅ HA[x̄]/(t^{j}(x̄) = s^{j}(x̄))_{J}}.

Note that H is finitely presented (f.p.) if and only if rank_{χ}(H) is finite. As we will see, the rank of a presentation is an important number related to the structure of H.^{1} Example 1.2 The rank of the trivial representation χ = id: HA[x̄] → HA[x̄] is 0 since HA[x̄] ≅ HA[x̄]/(⊤ = ⊤). Of more interest is the following example: Fix Dn ; x̄ in HA[x̄]. Dn ; x̄, as a finite distributive lattice, is in particular a Heyting algebra. The implication is given by a →_{Dn ; x̄} b = ⋁{c ∈ Dn ; x̄ | a ∧ c ≤_{Dn ; x̄} b}, which is a finite suprema. The generators x̄ ∈ HA[x̄] are of degree 0, so lie in Dn ; x̄. Of course, Dn ; x̄ is generated as a Heyting algebra by x̄ ∈ Dn ; x̄. Therefore, there is a surjective map of Heyting algebras, defined by

1There is a different notion of rank available: Since any quotient just considered can be written in the form H ≅ HA[x̄]/(γ(x̄) = ⊤), i.e., is obtained by forcing one element γ(x̄)

equal to ⊤, we could define the rank of a presentation as the degree of this element. The two ranks differ by at most one, and each of them has its advantages and disadvantages.

π^{n}: HA[x̄] ↠ Dn ; x̄,  x̄ ∈ HA[x̄] ↦ x̄ ∈ Dn ; x̄.

The rank of this presentation is n + 1: Indeed, what we have to say is what happens to a term t(x̄) of degree n + 1, which becomes an element in Dn ; x̄, to be expressed by a term of degree ≤ n. (Strictly speaking we only showed that the rank is bounded by n + 1. Using that the free Heyting algebra on one generator is infinite ([1], pp. 182–185, [10], p. 35) one shows that the rank equals n + 1.)

The above example shows slightly more: π^{n} ↾ Dn ; x̄, which is the composite

\xymatrix{Dn ; x̄ \ar@{^{(}->}[r]_{α^{n,∞}} & HA[x̄] \ar@{->>}[r]_{π^{n}} & Dn ; x̄,}

say as a map of distributive lattices, is the identity on Dn ; x̄. This shows that the family of maps {π^{n}: HA[x̄] ↠ Dn ; x̄}_{n} is jointly injective. Equivalently, we have the embedding

HA[x̄] ↪ ∏_{n} Dn ; x̄

of HA[x̄] into the product of finite Heyting algebras.^{2} This is commonly known as the finite model property (here of free Heyting algebras on a finite set of generators). As is well known, this holds more generally for all finitely presented Heyting algebras. The usual proof uses the completeness theorem of intuitionistic propositional logic with respect to Kripke models, and then one has to show that finite Kripke models suffice (see for example [6]). We will give a simple algebraic proof in the next section.

2As Mai Gehrke has pointed out we get slightly more: The embedding gives a representation of HA[x̄] as a subdirect product of subdirectly irreducible algebras, the latter since in each Dn ; x̄ the top element is join-irreducible. In the general case of Proposition 2.1 we have to replace each E_{χ}^{n} by the product ∏_{p∈J (E_{χ}^{n})} E_{χ}^{n}/p (where J (E_{χ}^{n}) is the set of all join-irreducible elements of E_{χ}^{n}) to get a representation of a finitely presented Heyting algebra as a subdirect product of subdirectly irreducible algebras.

2 Finite Heyting algebras and the finite model property

In this section our fixed data is a representation χ: HA[x̄] ↠ H of some finitely presented Heyting algebra H. Associated we have the sequence of finite distributive lattices E_{χ}^{n}, each of which is in particular a finite Heyting algebra.

Proposition 2.1 (The finite model property.) Any finitely presented Heyting algebra H embeds into a product of finite ones. Even more: For n ≥ rank_{χ}(H) there are canonical morphisms of Heyting algebras γ^{n}: H ↠ E_{χ}^{n} and the family of these is jointly injective.

Proof. Fix a presentation H ≅ HA[x̄]/(t^{i}(x̄) = s^{i}(x̄))_{i∈I} where the degrees of the terms s^{i} and t^{i} are bounded by rank_{χ}(H) for all i ∈ I. Heyting algebra morphisms γ^{n}: H → E_{χ}^{n} correspond to elements ē ∈ E_{χ}^{n} satisfying t^{i}(ē) = s^{i}(ē) for all i ∈ I. Obviously, ē = x̄ ∈ E_{χ}^{n} will do the job, provided n ≥ rank_{χ}(H) since t^{i}(ē) = t^{i}[x̄] = [t^{i}(x̄)] = [s^{i}(x̄)] = s^{i}(ē). The family of these maps is jointly injective. □

We want to show that these distributive lattices E_{χ}^{n} are related by various maps. For this we first need a definition:

Definition 2.2 For n ≥ 0 and a set of variables x̄ we define the following term (in which the meet is indexed by all terms t of degree n + 1):

Δ^{n}(x̄) = ⋀ {t(x̄) ↔ δ_{t}(x̄)| deg(t) = n+1, deg(δ_{t}) ≤ n and Dn ; x̄ ⊧ t(x̄) ↔ δ_{t}(x̄)}.

(Here Dn ; x̄ is again the set of elements of degree bounded by n in the free Heyting algebra HA[x̄].)

We note that, being honest, Δ^{n}(x̄) is defined only up to provable equivalence (although we could fix a representative for this equivalence class of formulae). By definition (see Example 1.2), Dn ; x̄ ≅ HA[x̄]/Δ^{n}(x̄). Clearly, deg(Δ^{n}(x̄)) ≤ n + 2. So we can view Δ^{n}(x̄) as an element in Dm ; x̄, m ≥ n + 2, and there is thus a canonical map of Heyting algebras Dm ; x̄/Δ^{n}(x̄) → Dn ; x̄, which is easily seen to be a bijection. We conclude that for all n and all m ≥ n + 2 there is a map of Heyting algebras (the quotient map composed with the isomorphism above)

π^{m,n}: Dm ; x̄ → Dn ; x̄.

As well, it follows that Δ^{n}(x̄) ⊢_{i} Δ^{m}(x̄) for m ≥ n + 2.

The following proposition allows us to give a presentation of E_{χ}^{n} in terms of a presentation of H and of Dn ; x̄. Here the tensor stands for the usual tensor product of algebras, which is also known as push-out or as free amalgamated product.

Proposition 2.3 For n > rank_{χ}(H) there is an isomorphism E_{χ}^{n} ≅ H⊗_{HA[x̄]} Dn ; x̄. As a consequence, for m ≥ n + 2 the square on the right is a push-out square of Heyting algebras as well:

\xymatrix{HA[x̄] \ar@{->>}[r]^{π^{m}} \ar@{->>}[d]_{χ} & Dm ; x̄ \ar@{->>}[r]^{π^{m,n}} \ar@{->>}[d]^{χ^{m}} & Dn ; x̄ \ar@{->>}[dr]^{χ^{n}} \\ H \ar@{->>}[r] & E_{χ}^{m} \ar@{->>}[rr] &  & E_{χ}^{n} ≅ H ⊗_{HA[x̄]} Dn ; x̄}

We note that, in particular, χ^{n} for n > rank_{χ}(H) is a morphism of (finite) Heyting algebras.

Proof. It is clearly enough to prove the first statement. We fix again a presentation of H of minimal degree, i.e., H ≅ HA[x̄]/(t^{i}(x̄) = s^{i}(x̄))_{i∈I} where deg(t^{i}), deg(s^{i}) ≤ rank_{χ}(H) for all i ∈ I. We write Ψ(x̄) for ⋀_{I}(t^{i}(x̄) ↔ s^{i}(x̄)), a term of degree ≤ rank_{χ}(H) + 1.

Fix now n > rank_{χ}(H) and consider the push-out square

[figure: HA[x̄]; π^{n}; χ; Dn ; x̄; ≅; HA[x̄]/Δ^{n}(x̄); HA[x̄]/Ψ(x̄); ≅; H; H ⊗_{HA[x̄]} Dn ; x̄; ≅; HA[x̄]/Ψ(x̄) ∧ Δ^{n}(x̄)]

(Being more precise, the push-out is given as the quotient of Heyting algebras HA[x̄, x̄′]/(Ψ(x̄) = ⊤, Δ^{n}(x̄′) = ⊤, x̄ = x̄′). We already did some simplifications.) Since Dn ; x̄ → H ⊗_{HA[x̄]} Dn ; x̄ is surjective the composite

E_{χ}^{n} ↪ H ↠ H ⊗_{HA[x̄]} Dn ; x̄

is surjective as well. Let us show that it is injective: Take a, b ∈ E_{χ}^{n} and suppose they become equal in the tensor product H ⊗_{HA[x̄]} Dn ; x̄. Choosing polynomials a(x̄) and b(x̄) of degree ≤ n for a and b, this means that

Δ^{n}(x̄), Ψ(x̄) ⊢_{i} a(x̄) ↔ b(x̄).

Hence Δ^{n}(x̄) ⊢_{i} (Ψ(x̄) ∧ a(x̄)) → b(x̄) or [Ψ(x̄) ∧ a(x̄)]_{Dn ; x̄} ≤ [b(x̄)]_{Dn ; x̄}. By our assumption on n, deg(Ψ(x̄) ∧ a(x̄)) ≤ n, but Dn ; x̄ collapses only elements of degree > n, so that in fact [Ψ(x̄)∧a(x̄)]_{HA[x̄]} ≤ [b(x̄)]_{HA[x̄]}. Finally, since Ψ(x̄) becomes ⊤ in H we deduce [a(x̄)]_{H} ≤ [b(x̄)]_{H} and thus [a(x̄)]_{E_{χ}^{n}} ≤ [b(x̄)]_{E_{χ}^{n}}, since both a(x̄) and b(x̄) represent elements lying already in E_{χ}^{n}, a subset of H. The other inequality follows from a symmetric argument.

Moreover, one checks directly that along these isomorphisms the map

Dn ; x̄ → E_{χ}^{n} ≅ H ⊗_{HA[x̄]} Dn ; x̄ is really χ^{n}. □

Lemma 2.4 Let φ: H → H′ be a morphism of Heyting algebras with H′ finite, χ: HA[x̄] ↠ H a presentation of the finitely presented Heyting algebra H. Then there is a minimal n = n(φ) such that φ factors through some Heyting algebra morphism γ^{n}: H ↠ E_{χ}^{n}.

Proof. Using Proposition 2.3 it is enough to consider the case where H is the free Heyting algebra HA[x̄] and χ = id. Then it is enough to look at a surjection φ: HA[x̄] ↠ H′, which then gives rise to a presentation of H′. Since H′ is finite the induced sequence of elements of degree ≤ n becomes stationary,

\xymatrix{E_{φ}^{n} \ar@{^{(}->}[r]^{≅} & E_{φ}^{n+1} \ar@{^{(}->}[r]^{≅} & ⋯ & ⋯ & ≅ H′,}

for n big enough. Then the bottom map in Lemma 2.3 becomes an isomorphism, and φ^{n}: Dn ; x̄ → E^{n} ≅ H′ is a Heyting algebra morphism from Dn ; x̄ onto H′. Since φ factors through some γ^{n}: HA[x̄] → Dn ; x̄ there is certainly a minimal n where this happens. □

3 Duality for finite distributive lattices

For an element p ≠ ⊥ in a distributive lattice D, the following are equivalent:

— p = a ∨ b implies p = a or p = b; and

— p ≤ a ∨ b implies p ≤ a or p ≤ b.

Elements with this property are called join-irreducible. J (D) denotes the set of all join-irreducible elements of D, which inherits a partial order from D. Dually, we have the notion of meet-irreducibles and the partially ordered set M(D).

The construction of J (D) (or M(D)) is in no way functorial in D, unless…

Lemma 3.1 Let α: D → D′ be a map of distributive lattices. If the left adjoint α_{!} of α exists, it preserves join-irreducibles of D′ and yields a map

J (α) = α_{!} ↾ J (D′): J (D′) → J (D).

Dually, if the right adjoint α_{∗} exists, it preserves meet-irreducibles. □

Thus, after restricting to appropriate sub-categories of DLat we get (contravariant) functors to PoSet. In particular, there are two functors

J , M: DLat_{fin}^{op} ⇉ PoSet_{fin}.

Proposition 3.2 The two functors J and M are naturally isomorphic. Both induce an equivalence between the opposite of the category of finite distributive lattices and the category of finite partial orders. On the 2– categorical level both functors reverse the order: if α ≤ β: D ⇉ D′ then J (β) ≤ J (α): J (D′) ⇉ J (D); and similar for M.

Proof. The proposition just restates the well known fact that a finite distributive lattice is completely determined by its join-irreducible elements. See for example [7] for details. As well it is well known that for a finite distributive lattice D the posets J (D) and M(D) are order isomorphic, via

γ_{D}: J (D) → M(D), p ↦ ⋁{D\ ↑ p} = ⋁^{D}{J (D)\ ↑ p}.

(γ_{D}(p) is the unique element in D satisfying ↓ γ_{D}(p) = D\ ↑ p.) From this explicit description it follows easily that for α: D → D′ the diagrams

\xymatrix{J (D′) \ar[r]^{γ_{D′}} \ar[d]_{α_{!}} & M(D′) \ar[r]^{γ_{D′}^{−1}} \ar[d]_{α_{∗}} & J (D′) \ar[d]^{α_{!}} \\ J (D) \ar[r]_{γ_{D}} & M(D) \ar[r]_{γ_{D}^{−1}} & J (D)}

commute. This means exactly that γ is a natural isomorphism.

Finally, suppose that α, β: D ⇉ D′ and α ≤ β. Then, by adjointness and monotonicity, id ≤ αα_{!} ≤ βα_{!}, so that β_{!} ≤ α_{!}: D′ → D, and of course this inequality holds as well if both maps are restricted to join-irreducible elements in D′. □

Any finite distributive lattice is both a Heyting algebra and a co–Heyting algebra. The latter means that there is a binary operation (−) \ (−) (‘supplement’) determined completely by

a \ b ≤ c iff a ≤ b ∨ c.

A map α: D → D′ preserves implication iff J (α) is open, i.e., if p ≤ α_{!}(q) in J (D) implies there exists q′ ≤ q in J (D′) so that p = α_{!}(q′). For dual reasons, α is a morphism of co-Heyting algebras iff M(α) is co-open (α_{∗}(m) ≤ n in M(D) implies there exists an m′ ≥ m so that α_{∗}(m′) = m). Using the natural isomorphisms above, α preserves (−) \ (−) iff J (α) is co-open, that is, if α_{!}(q) ≤ p in J (D) implies there exists q′ ∈ J (D′), q ≤ q′ and α_{!}(q′) = p. For the record:

Lemma 3.3 Let α: D → D′ be a map between finite distributive lattices. Then α is a morphism of Heyting algebras if and only if J (α) is an open map; while α is a morphism of co-Heyting algebras iff M(α) is co-open, which in turn is equivalent to J (α) being co-open. □

4 Adjoining implications

We go back to the ‘standard’ filtration of a Heyting algebra by finite distributive lattices, see diagram (1). At first sight, none of the maps involved is open, i.e., is a morphism of Heyting algebras. (Of course, χ is open and we know already from Proposition 2.3 that χ^{n} is open if n is large enough.) But at least all the maps in this diagram come close to being open: All displayed maps are morphisms of distributive lattices, and in addition, for example α^{n,m} preserves implication between elements in the image of any α^{k,n} (k < n), and similarly, each χ^{n} preserves implications between elements in the image of α^{k,n}. It seems worthwhile to study more detailed this situation.

Definition 4.1 Let g: D′ → D be a morphism between distributive lattices. We suppose that D has implications between elements in the image of g.

A morphism of distributive lattices f: D → L is called g–open if (i) L has implications between elements in the image of f; and if (ii) f preserves implications between elements in the image of g, i.e.,

f(g(d′_{1}) →_{D} g(d′_{2})) = fg(d′_{1}) →_{L} fg(d′_{2}), for all d′_{1}, d′_{2} ∈ D′.

At least if D′ and D are finite there is no doubt that there is a minimal g-open map r^{g}: D → D^{g} so that any other g-open map f: D → L will factor as f^{g} ∘ r^{g} for a unique r^{g}–open map f^{g}: D^{g} → L. This D^{g} is a quotient of the free distributive lattice DLat[x_{d_{1},d_{2}} | d_{1}, d_{2} ∈ D] ⊗^{DLat} D, where x_{d_{1},d_{2}} is adjoined to represent the implication between d_{1} and d_{2}. So D^{g} is the set of formal expressions

⋀_{i=0}^{n} ⋁_{j∈J_{i}}(d_{1}^{i,j} → d_{2}^{i,j}), d_{1}^{i,j}, d_{2}^{i,j} ∈ D,

modulo some equations. We see as well that r^{g} is always an inclusion.

Example 4.2 Consider the standard filtration of the free Heyting algebra in a finite set of generators, (extended by one more term to the left)

\xymatrix{D^{−1} \ar@{^{(}->}[r]^{α^{−1,0}} & D0 ; x̄ \ar@{^{(}->}[r]^{α^{0,1}} & D1 ; x̄ \ar@{^{(}->}[r]^{α^{1,2}} & … & Dn ; x̄ \ar@{^{(}->}[r]^{α^{n,n+1}} & Dn+1 ; x̄ \ar@{^{(}->}[r] & … & HA[x̄]}

Here D^{−1} is the two-point lattice {0, 1}, and Dn ; x̄ is the distributive lattice of elements of implicational degree less or equal to n in the free Heyting algebra HA[x̄]. From the sketched description above it should be clear that, for example,

Dn+2 ; x̄ ≃ (Dn+1 ; x̄)^{α^{n,n+1}},

and the canonical map r^{α^{n,n+1}} is in this case just the inclusion α^{n+1,n+2}.

In case that g is a map between finite distributive lattices, there is an explicit description of the join-irreducible elements of D^{g} in terms of the join-irreducibles of D and the map J (g): J (D) → J (D′) due to S. Ghilardi. Since it is of vital importance for us, we will recapitulate its description, and refer the reader for a proof of its properties to [8].

Call a subset S ⊂ J (D) J (g)-open (or simpler: g_{!}–open) if for all s ∈ S and all p ∈ J (D)

p ≤ s implies ∃s′ ∈ S(s′ ≤ s & g_{!}(p) = g_{!}(s′)) .

Using duality, a subset S ⊂ J (D) is J (g)–open iff the dual map of distributive lattices D ↠↓ S is g–open. Then

J (D^{g}) = {S ⊂ J (D) | S is rooted and J (g)–open}.

(Here rooted means having a largest element.) The canonical map r^{g}: D → D^{g} is induced by its dual, r_{!}^{g} ↾ J (D^{g}) = J (r^{g}): J (D^{g}) → J (D), sending a rooted subset S ⊂ J (D) to its root. Given the dual of a g-open map J (f): J (L) → J (D) (f: D → L a g-open map between finite distributive lattices), the canonical map f^{g}: D^{g} → L is given by

J (f^{g}): J (L) → J (D^{g}), q ↦ {J (f)(q′) | q′ ≤ q}.

The point here is, as observed by Ghilardi, that J (r^{g}) has a right adjoint left inverse J (r^{g})_{∗}, sending p ∈ J (D) to the downward closure of p in J (D), i.e., to the set ↓^{J (D)} p.

On the level of distributive lattices this means that besides r^{g}: D → D^{g} there is another map of distributive lattices D^{g} → D. This map has to be the right adjoint r_{∗}^{g} of r^{g}. (This follows from Proposition 3.2: Writing s for the map of distributive lattics D^{g} → D we know that r_{!}^{g} ⊣ s_{!}, i.e., r_{!}^{g}s_{!} ≤ id_{J (D)} and id_{J (D′)} ≤ s_{!}r_{!}^{g}. Using duality, which reverses the order, we deduce sr^{g} ≥ id_{D} and id_{D^{g}} ≥ r^{g}s, which means that r^{g} is left-adjoint to s.^{3}) We deduce that since the lattices involved are finite, r_{∗}^{g} has another right adjoint r_{∗∗}^{g}. Moreover, since the left adjoint of a map of distributive lattices preserves join-irreducibles, r^{g} preserves join-irreducibles and in fact, the map J (r^{g})_{∗}, sending p ∈ J (D) to its downward closure, has to be the restriction of r^{g} to join-irreducibles in D. Finally, we see that J (r^{g}) is co-open, so that r^{g} is a map of co-Heyting algebras. We summarise this in the following proposition:

Proposition 4.3 (Ghilardi, see [8].) Let g: D′ → D be a morphism between finite distributive lattices. There exists a (unique) finite distributive lattice D^{g} together with a g-open map r^{g}: D ↪ D^{g}, so that any g-open map of lattices f: D → L (where L may be infinite) factors uniquely as f^{g} ∘ r^{g}, for f^{g}: D^{g} → L an r^{g}-open map. r^{g} is a map of co-Heyting algebras. Its right adjoint r_{∗}^{g}: D^{g} → D is a map of distributive lattices so that r^{g} preserves join-irreducible elements. Moreover, r_{∗}^{g} ∘ r^{g} = id_{D}. □

3There is a more conceptual argument for the fact that r_{∗}^{g} is a map of distributive lattices which is slightly more illuminating: Since id_{D} is g-open there exists an r^{g}-open map s: D^{g} → D satisfying s ∘ r^{g} = id_{D}. Since D^{g} is generated by the elements of the form d →_{D^{g}} d′ for d, d′ ∈ D it follows that r^{g} ∘ s ≤ id_{D^{g}} (using that r^{g} ∘ s is a map of distributive lattices so that r^{g}s(d → d′) ≤ r^{g}s(d) → r^{g}s(d′)) and s is right adjoint to r^{g}.

As mentioned before D^{g} is the set of formal expressions ⋀_{I} ⋁_{J}(d_{1}^{i,j} → d_{2}^{i,j}), d_{1}^{i,j}, d_{2}^{i,j} ∈ D, modulo some equivalence relation.

We note that r_{∗}^{g} is r^{g}-open: Indeed, it is a map of distributive lattices, and if d, d′ ∈ D then (we supress r^{g})

r_{∗}^{g}(d →_{D^{g}} d′) = ⋁{d ∈ D | p ≤_{D^{g}} d → d′}
= ⋁{d ∈ D | p ∧ d ≤_{D^{g}} d′}
= ⋁{d ∈ D | p ∧ d ≤_{D} d′}
= d →_{D} d′ .

Thus r_{∗}^{g} is the unique lifting of the g-open map id_{D}: D → D. One should note, however, that r_{∗}^{g} does not preserve arbitrary implications.

It remains the question which element is represented by the g_{!}-open S ⊂ J (D).

Lemma 4.4 For a g_{!}-open subset S ⊂ J (D) we have S ≤ p → γ_{D}(p) if and only if p ∉ S so that the g_{!}-open S represents the join-irreducible element S = ⋀_{p∉S}(p → γ_{D}(p)) in J (D^{g}) ⊂ D^{g}. Moreover, γ_{D^{g}}(S) = ⋁_{p∈S}(p → γ_{D}(p)).

Proof. Assuming the first part we clearly have S ≤ ⋀_{p∉S}(p → γ_{D}(p)). For the other inequality, if T ∈ J (D^{g}) is an arbitrary join-irreducible element such that for all p ∉ S the inequality T ≤ p → γ_{D}(p) holds, then p ∉ S implies p ∉ T by the first part, so that T ⊂ S and thus T ≤ S. (We note that this equation is already mention in [8].)

To verify the second identity of the lemma we have for p ∈ S that S ≰ p → γ_{D}(p), so p → γ_{D}(p) ≤ γ_{D^{g}}(S) which proves one inequality. For the other if S ≰ T in J (D^{g}) then there exists some p ∈ S so that p ∉ T, and T ≤ p → γ_{D}(p). Since γ_{D^{g}}(S) = ⋁^{D^{g}}(J (D^{g})\ ↑ S) we get the other inequality.

It remains to prove that (in D^{g}) for all S ∈ J (D^{g}), p ∈ J (D),

S ≤ p → γ_{D}(p) if and only if p ∉ S.  (2)

For this we work in D^{g} =↓ J (D^{g}).

From left to right suppose that S ∧p ≤ γ_{D}(p), i.e., ↓ S∩ ↓ r^{g}(p) ⊂ ⋃_{p≰p′} ↓ r^{g}(p′). If p ∈ S then S∩ ↓^{J (D)} p is g_{!}-open, so it is in J (D^{g}), and contained in ↓ S∩ ↓ r^{g}(p) so that S∩ ↓^{J (D)} p ⊆↓^{J (D)} p′ for some p′ such that p ≰ p′, a contradiction and p ∉ S. Conversely, if p ∉ S then take an arbitrary T in ↓ S∩ ↓ r^{g}(p), i.e., T ⊂ S∩ ↓ p. Because p is not in S there is some p′ strictly less than p so that T ⊂↓ p′, and T ∈↓ r^{g}(p′). Since p ≰ p′ the inequality follows. □

In the next section we will iterate the construction of adding implications infinitely many times. Here we take a look at what happens in the second step, that is, we consider the situation

[figure: D′; g; D; r^{g}; D^{g}; (D^{g})^{r^{g}}; D^{0}; r^{0,1}; D^{1}; r^{1,2}; D^{2}]  (3)

The following lemma is a valuable tool for calculating maps. We use the description of join-irreducibles of D^{1} and D^{2} as above.

Lemma 4.5 A rooted subset 𝔖 ⊂ J (D^{1}) is r_{!}^{0,1}-open (and therefore represents a join-irreducible element in D^{2} if and only if for all S ∈ 𝔖, S = {root(S′) | S′ ⊂ S and S′ ∈ 𝔖}.

(We remind the reader that elements of J (D^{1}) are rooted subsets of J (D^{0}), being g-open. Thus root(S′) = r_{!}^{0,1}(S′).)

Proof. Suppose 𝔖 ⊂ J (D^{1}) is r_{!}^{0,1}-open and fix S ∈ 𝔖 arbitrary. For s ∈ S we have S∩ ↓^{J (D^{0})} s ≤ S, and this set is g-open (i.e., in J (D^{1})) since S is. By r_{!}^{0,1}-openness of 𝔖 there is S′ ⊂ S, S′ in 𝔖, so that r_{!}^{0,1}(S′) = r_{!}^{0,1}(S∩ ↓ s). But root(S′) = r_{!}^{0,1}(S′) = root(S∩ ↓ s) = s, the latter because s ∈ S.

The other direction is trivial. □

As an application of the lemma we show existence of a Heyting algebra morphism γ^{2,0}: D^{2} → D^{0}. On the level of join-irreducibles it is given by

γ_{!}^{2,0}: J (D^{0}) → J (D^{2}), p ↦ {↓ p′ | p′ ≤ p}.

Clearly, γ_{!}^{2,0} is monotone and well-defined by Lemma 4.5.

Lemma 4.6 The map γ^{2,0}: D^{2} → D^{0} is a surjective morphism of Heyting algebras satisfying γ^{2,0} ∘ r^{1,2} = r_{∗}^{0,1}. As maps of posets, r_{∗}^{0,2} ≤ γ^{2,0} ≤ r_{!}^{0,2}.

Proof. Obviously, γ_{!}^{2,0} is injective (which implies that its dual is surjective). To show that it is open assume 𝔄 ⊂ γ_{!}^{2,0}(p), for p ∈ J (D^{0}) and 𝔄 ⊂ J (D^{1}) rooted and r_{!}^{0,1}-open. Then each set in 𝔄 is of the form ↓ p′ for some p′ ≤ p. In particular, root(𝔄) =↓ a for some a ≤ p. Lemma 4.5 now shows that 𝔄 = {↓ a′ | a′ ≤ a} = γ_{!}^{2,0}(a).

For the identity, we have to show that r^{0,1} = r_{!}^{1,2} ∘ γ_{!}^{2,0}: J (D^{0}) → J (D^{1}). But r_{!}^{1,2}γ_{!}^{2,0}(p) = root(γ_{!}^{2,0}(p)) =↓ p = r^{0,1}(p). Finally note that γ^{2,0} ∘ r^{0,2} = γ^{2,0} ∘ r^{1,2} ∘ r^{0,1} = r_{∗}^{0,1} ∘ r^{0,1} = id, so that the inequalities follow by applying γ^{2,0} to the inequalities r^{0,2}r_{∗}^{0,2} ≤ id ≤ r^{0,2}r_{!}^{0,2}. □

Let us remark that we already saw these morphisms of Heyting algebras, namely as quotient maps

Dn+2 ; x̄ → Dn ; x̄

(see the discussion before Lemma 2.3 and Example 4.2).

5 A representation theorem

In this section we iterate the construction of the previous one. We consider a map of finite distributive lattices α^{−1,0}: D^{−1} → D^{0} to get a sequence

\xymatrix{D^{−1} \ar[r]^{α^{−1,0}} & D^{0} \ar@{^{(}->}[r]^{α^{0,1}} & D^{1} \ar@{^{(}->}[r]^{α^{1,2}} & … & D^{n} \ar@{^{(}->}[r]^{α^{n,n+1}} & D^{n+1} \ar@{^{(}->}[r] & …}

of distributive lattices, with D^{n+1} = (D^{n})^{α^{n−1,n}} for n ≥ 0. The colimit of this sequence (in the category of distributive lattices) is denoted HA[α^{−1,0}: D^{−1} → D^{0}] or simply HA[α^{−1,0}].

Proposition 5.1 HA[α^{−1,0}] is a bi-Heyting algebra. As a Heyting algebra, it has the universal property that Heyting algebra maps HA[α^{−1,0}] → H correspond to α^{−1,0}-open maps (of distributive lattices) D^{0} → H. In particular, HA[α^{−1,0}] is a finitely presented Heyting algebra.

Proof. It is clear that the colimit is a bi-Heyting algebra (i.e., both a Heyting and a co-Heyting algebra). Denoting equivalence classes in the colimit by [a], the supplement of [a] and [b], for a ∈ D^{n} and b ∈ D^{m}, is given by [α^{n,k}(a) \_{D^{k}} α^{m,k}(b)], where k is the maximum of n and m. Their implication is given by [α^{n,k+1}(a) →_{D^{k+1}} α^{m,k+1}(b)].

To show the universal property, denote the canonical maps D^{n} → HA[α^{−1,0}] by α^{n,∞}. Since HA[α^{−1,0}] is a cone on the sequence of distributive lattices, the identities α^{n,∞} = α^{m,∞} ∘ α^{n,m} hold.

Let now γ: HA[α^{−1,0}] → H be arbitrary. If a, b ∈ D^{n} (n ≥ −1), then

γα^{n+1,∞}(α^{n,n+1}(a) →_{D^{n+1}} α^{n,n+1}(b))

= γ(a → b)
= γa →_{H} γb
= (γα^{n+1,∞})α^{n,n+1}(a) →_{H}
(γα^{n+1,∞})α^{n,n+1}(b).

Thus, γ ∘ α^{n+1,∞} is α^{n,n+1}-open, in particular,

γ̄ = γ ∘ α^{0,∞}: D^{0} → H

is α^{−1,0}-open. By the uniqueness of the lifting in Proposition 4.3, γ is uniquely determined by γ̄. By the same proposition, any such α^{−1,0}-open map γ̄: D^{0} → H lifts to a sequence of maps γ^{i}: D^{i} → H and thus to a map γ: HA[α^{−1,0}] → H. The properties of the lifting ensure that γ is a morphism of Heyting algebras.

It is now clear from the universal property that HA[α^{−1,0}] is finitely presented. We note that, in particular, α^{0,∞}(D^{0}) is a set of generators of HA[α^{−1,0}]. □

The following proposition shows that we captured all finitely presented Heyting algebras.

Proposition 5.2 (Representation of finitely presented Heyting algebras.) Let H be some finitely presented Heyting algebra and choose a presentation χ: HA[x̄] ↠ H of H. Then

H ≅ HA[β^{n,n+1}: E_{χ}^{n} ↪ E_{χ}^{n+1}],

where n ≥ rank_{χ}(H), and E_{χ}^{n} (respectively E_{χ}^{n+1}) is the set of elements of implicational degree ≤ n (of degree ≤ n + 1) in H.

Proof. We will give explicitly the isomorphism. Fix the data of the proposition, and a presentation H ≅ HA[x̄]/(s^{i}(x̄) = t^{i}(x̄))_{i∈I} where the degrees of the occurring terms s^{i} and t^{i} are bounded by rank_{χ}(H) for all i ∈ I.

The identity map HA[β^{n,n+1}] → HA[β^{n,n+1}] corresponds to a β^{n,n+1}-open map γ: E_{χ}^{n+1} → HA[β^{n,n+1}]. The generators of H, the elements x̄, are in E_{χ}^{0}, and by our assumption on n,

s^{i}(γ(x̄)) = γ(s^{i}(x̄)) = γ(t^{i}(x̄)) = t^{i}(γ(x̄)),

for all terms s^{i}, t^{i} occurring in the presentation of H, so that we get a morphism of Heyting algebras

H → HA[β^{n,n+1}],  x̄ ↦ γ(x̄).

By the universal property of HA[β^{n,n+1}] there is a map HA[β^{n,n+1}] → H, induced by the β^{n,n+1}-open inclusion β^{n+1,∞}: E_{χ}^{n+1} → H. Since by construction

\xymatrix{HA[β^{n,n+1}] \ar[r] & H \\ E_{χ}^{n+1} \ar@{^{(}->}[u]^{γ} \ar@{-->}[ur]_{β^{n+1,∞}}}

commutes we get that this second map sends γ(x̄) to β^{n+1,∞}(x̄) = x̄ ∈ H, and the two maps are inverse to each other. □

Example 5.3 The free Heyting algebra on a finite set of generators HA[x̄] can be described as HA[α^{−1,0}: D^{−1} → D0 ; x̄], where D^{−1} is again the two element distributive lattice, while D0 ; x̄ is the lattice of elements of implicational degree 0 in HA[x̄]. Equivalently, D0 ; x̄ is the free distributive lattice on the set of generators x̄, i.e., D0 ; x̄ = DLat[x̄].

Corollary 5.4 Every finitely presented Heyting algebra is co-Heyting. □

Corollary 5.5 A finitely presented Heyting algebra that is as well a finitely generated co-Heyting algebra is finite.

Proof. If H ≅ HA[α^{−1,0}: D^{−1} ↪ D^{0}] as a Heyting algebra then the co-Heyting algebra generators (finitely many) are all contained in some D^{n}. But the sub-co-Heyting algebra of H generated by D^{n} is D^{n} so that the inclusion α^{n,∞}: D^{n} → H is an isomorphism. □

The above corollary shows as well that the dual operations (−) \ (−) and ∼ (−) = ⊤ \ (−) are not definable in terms of the Heyting operations in case that H is infinite.

Corollary 5.6 (Rauszer [12].) Bi-intuitionistic logic is conservative over intuitionistic logic.

Proof. Algebraically this just says that the canonical map from the free Heyting algebra on countably many generators into the free bi-Heyting algebra on this set of generators is an inclusion. For this it is certainly enough to verify this statement for the canonical map of Heyting algebras from the free Heyting algebra on a finite set of generators x̄ to the free bi-Heyting algebra on this set of generators

HA[x̄] → biHA[x̄].

But by Proposition 5.2 and Proposition 5.1 this map has a (bi-Heyting) retraction biHA[x̄] ↠ HA[x̄]. □

After this representation we start analysing the structure of finitely presented Heyting algebras in the next section. (We turn this construction into a functor in Section 8.) But first we show that the maps β^{n,n+1} are good ones, sharing all the properties of the α^{n,n+1}.

Lemma 5.7 For n > rank_{χ}(H), there is a canonical isomorphism E_{χ}^{n+2} ≅ (E_{χ}^{n+1})^{β^{n,n+1}}, and β^{n+1,n+2} is the canonical inclusion E_{χ}^{n+1} ↪ (E_{χ}^{n+1})^{β^{n,n+1}}.

Proof. We consider the diagram

[figure: E^{n}; E^{n+1}; E^{n+2}; ⋯; H; F^{n}; γ^{n,n+1}; F^{n+1}; F^{n+2}; γ^{n+2,n+3}; ⋯; H; id; (F^{n+1})^{γ^{n,n+1}}; ⋯]

where all possible squares commute (the vertical surjections are induced by the universal property of the γ’s). By induction one shows that E^{i} ≅ F^{i}. For the induction step just note that in both cases, elements in (?)^{i+1} are exactly those elements of H of the form ⋀_{J} ⋁_{K}(a_{jk} →_{H} b_{jk}), for a_{jk}, b_{jk} in (?)^{i}. □

At the beginning of this section we defined HA[α^{−1,0}] as the colimit of a sequence of distributive lattices. But there are more maps of distributive lattices around: Each right adjoint α_{∗}^{n,n+1} is a map of distributive lattices. For each n ≥ 0 there is a morphism of Heyting algebras γ^{n+2,n}: D^{n+2} → D^{n} (Lemma 4.6), which altogether gives the following picture, where all displayed maps are in DLat. An ‘o’ indicates that the map is open (a morphism of Heyting algebras), a ‘c’ that it is co-open.

[figure: D^{0}; α^{0,1}; c; α_{∗}^{0,1}; D^{2}; γ^{2,0}; o; α^{2,3}; c; α_{∗}^{2,3}; D^{4}; γ^{4,2}; o; ···; HA[α^{−1,0}]; D^{−1}; α^{−1,0}; D^{1}; α^{1,2}; c; α_{∗}^{1,2}; D^{3}; γ^{3,1}; o; α^{3,4}; c; α_{∗}^{3,4}; ⋯; γ^{5,3}; o]

Here the ‘inner’ triangles commute, i.e., γ^{n+2,n}α^{n+1,n} = α_{∗}^{n,n+1}, for all n ≥ 0. We use the notation γ^{m,n} for the composite of the Heyting algebra morphisms D^{m} → D^{n}, which is only defined if m−n is even. There are as well surjective Heyting algebra morphisms (n ≥ 0)

γ^{∞,n}: HA[α^{−1,0}] ↠ D^{n},

induced by the α^{−1,0}-open map α^{0,n}: D^{0} → D^{n}, which is the identity if n = 0. Clearly, γ^{n,m}γ^{∞,n} = γ^{∞,m}, since both behave the same on generators.

The set D^{0} is a subset of HA[α^{−1,0}] and as a Heyting algebra, HA[α^{−1,0}] is generated by D^{0}. With respect to these generators D^{n} is exactly the set of elements of implicational degree ≤ n in HA[α^{−1,0}]. Each finite Heyting algebra D^{n} (n ≥ 0) is the quotient of HA[α^{−1,0}] by a unique element Δ^{n}. The same argument as in the case of free Heyting algebras (see Example 1.2) proves that Δ^{n} has degree n + 2 (i.e., Δ^{n} ∈ D^{n+2}), and of course

D^{n+2}/Δ^{n} ≅ D^{n},

so that we identify (again) γ^{n+2,n}: D^{n+2} → D^{n} as a quotient map in the canonical way. But since Δ^{n} ∈ D^{m} for all m ≥ n + 2 there are Heyting algebra morphisms D^{m} → D^{n} for all m ≥ n + 2 (and not only for those m such that m − n is even). The following lemma describes them explicitly:

Lemma 5.8 For each n ≥ 0, γ^{n+2,n}α_{∗}^{n+2,n+3}: D^{n+3} → D^{n} is a morphism of Heyting algebras. Moreover, γ^{n+2,n}α_{∗}^{n+2,n+4} = γ^{n+4,n}.

Proof. After shifting the indices we may assume n = 0. The map of distributive lattices γ^{2,0}α_{∗}^{2,3} is induced by the map of posets

α^{2,3}γ_{!}^{2,0}: J (D^{0}) → J (D^{3}), p ↦↓^{J (D^{2})} γ_{!}^{2,0}(p).

We must show that this map is open. For this note first that ↓^{J (D^{2})} γ_{!}^{2,0}(p) = γ_{!}^{2,0}(↓ p) = {γ_{!}^{2,0}(p′) | p′ ≤ p}, by openness of γ_{!}^{2,0}. So take 𝔸 ⊂ α^{2,3}γ_{!}^{2,0}(p) in J (D^{3}) arbitrary. By the just made remark we know that there is a subset A of ↓ p so that

𝔸 = {γ_{!}^{2,0}(a′) | a′ ∈ A}.

In particular, 𝔄 = root(𝔸) = γ_{!}^{2,0}(a) for some a ∈ A.

By Lemma 4.5, γ_{!}^{2,0}(a) = {root(𝔅) | 𝔅 ⊂ 𝔄 and 𝔅 ∈ 𝔸}, i.e., for all b ≤ a there is some 𝔅 ∈ 𝔸, 𝔅 ⊂ 𝔄 and

↓ b = root(𝔅).

Since root(γ_{!}^{2,0}(a′)) =↓ a′ we deduce, using the fact that 𝔅 is of the form γ_{!}^{2,0}(a′) for some a′, that 𝔅 = γ_{!}^{2,0}(b) ∈ 𝔸 for all b ≤ a. Therefore, γ_{!}^{2,0}(↓ a) = {γ_{!}^{2,0}(b) | b ≤ a} ⊂ 𝔸 and since root(𝔸) = γ_{!}^{2,0}(a) we get equality, so that α^{2,3}γ_{!}^{2,0} is open.

For the equality note that, by Lemma 4.6, γ^{2,0}α_{∗}^{2,4} = γ^{2,0}α_{∗}^{2,3}α_{∗}^{3,4} = γ^{2,0}γ^{4,2}α^{3,4}α_{∗}^{3,4} = γ^{4,0}. □

6 The structure of finitely presented Heyting algebras

In this section we use our particular representation of finitely presented Heyting algebras to obtain information about their structure. Again, notations refer to diagram (1).

The first part of the following proposition is known for Heyting algebras, free on a finite set of generators (see for example [13]).

Proposition 6.1 In the finitely presented Heyting algebra H, any element can be expressed as the finite join of join-irreducibles. Even more, if h ∈ H is of degree ≤ n, then h is the union of join-irreducibles each of which has degree ≤ n too, provided that n > rank_{χ}(H).

Proof. Since h has degree ≤ n, it lives in E_{χ}^{n}. But E_{χ}^{n} is finite, so that h is the finite union of elements in J (E_{χ}^{n}). Finally, the inclusion β^{n,∞}: E_{χ}^{n} → H preserves join-irreducibles by Lemma 5.7. □

If an element h ∈ H admits some representation h = ⋁_{I} p_{i}, p_{i} ∈ J (H), then it admits a unique minimal such.^{4} Here minimal refers to p_{i} ≤ p_{i′} implies p_{i} = p_{i′}. Indeed, from some representation one obtains a minimal by taking the maximal elements in the set {p_{i} | i ∈ I}. Given two such minimal representations, say ⋁_{I} p_{i} = h = ⋁_{J} q_{j}, we deduce by join-irreducibility p_{i} ≤ q_{j(i)} and then q_{j(i)} ≤ p_{k(i)}, for each i ∈ I. Now p_{i} = q_{j(i)} (= p_{k(i)}) by minimality of the representation.

Obviously, the minimal representation of ⊤_{H} yields a set of maximal elements in J (H). We can calculate this set even better.

Proposition 6.2 J (H) has finitely many maximal and finitely many minimal elements. If H ≅ HA[g: D^{−1} → D^{0}] then the maximal elements are those of J (D^{0}) (in the colimit), the minimal ones are the minimal elements in J (D^{1}).

Proof. We look at the beginning of the sequence which defines the Heyting algebra H ≅ HA[g: D^{−1} → D^{0}], i.e., at

[figure: D^{−1}; g; D^{0}; r^{g}; (D^{0})^{g}; ((D^{0})^{g})^{r^{g}}; ⋯; D; r^{0,1}; D^{1}; r^{1,2}; D^{2}; ⋯]

From the construction it is clear that each S ∈ J (D^{1}) is contained in ↓ root(S), so only sets of the form ↓ p, p ∈ J (D), can be maximal. They are maximal exactly if p was maximal in J (D). Since ↓ p = r^{0,1}(p) we get as well that r^{0,1} (and in fact, all r^{n,n+1} in the infinite iteration above) preserve and reflect maximal elements. Therefore, J (H) is set of equivalence classes in the colimit of the maximal elements of J (D^{0}).

Next, we look at the minimal elements: In general, if p is minimal in J (D) then r^{0,1}(p) =↓ p = {p} is minimal in J (D^{1}), that is, all the maps r^{n,n+1} preserve minimal elements.

Now suppose that 𝔄 ∈ J (D^{2}) is minimal. Then 𝔄 can be only a singleton set {A} (otherwise, 𝔄∩ ↓ A′ ⊊ 𝔄 contradicting minimality), so that A = root(𝔄) = r_{!}^{1,2}(𝔄). By Lemma 4.5, A = {root(A′) | A′ ⊂ A, A′ ∈ 𝔄}, so that A is a singleton set as well, A = {p} for p = root(A). But any one-element set is minimal, so A is minimal in J (D^{1}), and 𝔄 =↓ A = r^{1,2}(A). □

4A note aside: It seems that G. Birkhoff [3] was the first to observe the uniqueness of a finite irredundant representation. An observation trivial in these days.

Example 6.3 (Maximal and minimal elements in HA[x̄].) We consider the free Heyting algebra HA[x̄] on a finite set of generators, which is as mentioned several times HA[α^{−1,0}: {0, 1} ↪ DLat[x̄]] i.e., the defining sequence for HA[x̄] looks like

\xymatrix{\{0, 1\} \ar@{^{(}->}[r]_{α^{−1,0}} & DLat[x̄] \ar@{^{(}->}[r]_{α^{0,1}} & D1 ; x̄ \ar@{^{(}->}[r] & D2 ; x̄ \ar@{^{(}->}[r] & ⋯}

On the level of join irreducibles we have the sequence

\xymatrix{1 & J (D^{0}) \ar@{^{(}->}[r] \ar@{->>}[l] & J (D1 ; x̄) \ar@{^{(}->}[r] \ar@{->>}[l] & J (D2 ; x̄) \ar@{^{(}->}[r] \ar@{->>}[l] & ⋯ \ar@{->>}[l]}

Any one-element subset of J (D0 ; x̄) is α_{!}^{−1,0}-open, so they form exactly the minimal elements in J (D^{1}) and thus in the colimit. In particular, there are #Min(J (HA[x̄])) = #J (D0 ; x̄) many of them. Using disjunctive normal form, any element in D0 ; x̄ = DLat[x̄] has the form

⋁_{I} ⋀_{X_{i}⊂{x_{0},...,x_{n−1}}} X_{i}

(I = {∗} and X_{∗} = ∅ gives ⊤, while I = ∅ gives ⊥). Each of the elements ⋀ X for X ⊂ {x_{0}, …, x_{n−1}} is join-irreducible in D0 ; x̄, so that there are #P{x_{0}, …, x_{n−1}} = 2^{n} minimal elements in J (HA[x̄]). In fact, J (D0 ; x̄) ≅ P{x_{0}, …, x_{n−1}}, ordered by reverse inclusion.

Note that the minimal elements in J (HA[x̄]) are nothing but the atoms in HA[x̄], and this number was as well calculated in [2], Theorem 3.0(i).

There is exactly one maximal element in J (D0 ; x̄), namely ⊤. This means as well that in HA[x̄] there is one maximal join-irreducible element. This is of course the algebraic version of the disjunction property for intuitionistic propositional calculus:

⊢_{i} t_{1}(x̄) ∨ t_{2}(x̄) implies ⊢_{i} t_{1}(x̄) or ⊢_{i} t_{2}(x̄),

for all terms t_{1} and t_{2}.

The preceeding example holds slightly more generally.

Example 6.4 (The disjunction property.) A finitely presented Heyting algebra H has the disjunction property iff ⊤_{H} is join irreducible. Then H = HA[α^{−1,0}: D^{−1} → D^{0}] has the disjunction property if and only if D^{0} has.

Example 6.5 (Minimal elements in Heyting algebras, free on a distributive lattice.) The forgetful functor HA → DLat has a left adjoint, which sends a distributive lattice to the Heyting algebra freely generated by it.

A Heyting algebra H is free on a finite distributive lattice D iff H ≅ HA[α^{−1,0}: {0, 1} → D]. As in the example above, H has #J (D) many minimal join-irreducible elements. H has the disjunction property iff D has.

In Example 6.3 we calculated the number of atoms (the minimal joinirreducible elements) of HA[x̄]. The following Proposition 6.6 gives a more general way of calculating the number of atoms, and as a corollary we get an explicit description of the atoms of HA[x̄].

Proposition 6.6 For each finitely presented Heyting algebra H there is a canonical bijection between the set of atoms of a Heyting algebra, At(H), and the set of Heyting algebra morphisms from H to B = {⊥, ⊤}.

Proof. The atoms of a distributive lattice are exactly the maximal principal prime filters. Now prime filters F of the Heyting algebra H correspond to maps of distributive lattices ϕ: H → B under the correspondence F = ϕ^{−1}(⊤). Then F is principal if and only if ϕ has a left-adjoint ϕ_{!} (sending the top element of B to the generator of F). Finally, one easily checks that this generator is an atom if and only if the Frobenius identity ϕ_{!}(a ∧ ϕ(h)) = ϕ_{!}(a) ∧ h holds for all a ∈ B, h ∈ H, which is equivalent to say that ϕ preserves implication. To sum up, we proved that the atoms correspond to those Heyting algebra morphisms H → B that have a left adjoint. But any morphism of Heyting algebras H → B is surjective and clearly B is finitely presented over H (provided that H is finitely presented), so we deduce that such a map is actually a quotient map which always has both adjoints. (Note that we do not have to appeal to Pitts’ uniform interpolation theorem for this argument.) □

Corollary 6.7 The atoms in HA[x̄] are the elements

a_{A} = ⋀{x | x ∈ A} ∧ ⋀{¬x | x ∈ ∁A},

for A ∈ P(x̄).

Table 1: Number of join-irreducible elements

# of generators #J (D0 ; x̄)  #J (D1 ; x̄) #J (D2 ; x̄)
0  1  1  1
1  2  3  4
2  4  13  718
3  8  159  ?
4  16  33.337  ?
5  32  2.147.648.859  ?
6  64 9.223.372.049.740.171.909  ?

Proof. Given φ: HA[x̄] → B induced by x ∈ A ↦ 1 and x ∈ ∁A ↦ 0 the filter φ^{−1}(1) is the unique upward closed set ↑ a so that

\xymatrix{HA[x̄] \ar[r]^{φ} \ar@{->>}[d] & B \\ HA[x̄]/a \ar@{-->}[ur]^{≅}_{{A↦1 \atop ∁A↦0}}}

commutes, so that a has the form as stated in the corollary, and these are the atoms. □

Finally, let us say something on the size of the posets J (Dn ; x̄). Table 1 lists some numbers calculated using the following lemma. The values in case of two generators were independently calculated in [9].

Lemma 6.8 (i) J (D0 ; x̄) has 2^{n} elements.

(ii) If j(k) denotes the number of elements in J (D_{x_{1},...,x_{k}}^{1}) (or in J (D_{∅}^{1}) if k = 0) then j(n) can be calculated using the recursion

j(n) = 2^{(2^{n}−1)} + ∑_{k=0}^{n−1}(−1)^{(n−1)−k}\binom{n}{k}j(k).

Or in closed form, j(n) = ∑_{k=0}^{n} \binom{n}{k}2^{(2^{k}−1)}.

Proof. The first part holds since J (D0 ; x̄) is isomorphic to P(x̄). For the second, HA[∅] = {0, 1} and J (D_{∅}^{1}) = {1}. The recursion just counts rooted subsets in the poset P(x̄)^{op}. □

7 Prime formulae

We start with a well known observation:

Lemma 7.1 The following are equivalent for a finitely presented Heyting algebra H = HA[α^{−1,0}]:

(i) H has the disjunction property.

(ii) All D^{n} have the disjunction property.

(iii) The unique elements Δ^{n} ∈ D^{n+2} that satisfy H/Δ^{n} ≅ D^{n} are joinirreducible.

Proof. The first two equivalences are immediate, the others follow from the following straight forward lemma. □

Lemma 7.2 Consider a quotient map of Heyting algebras H ↠ H/h. Then h ∈ J (H) iff H/h has the disjunction property. □

Example 7.3 In Definition 2.2 we defined the terms Δ^{n}(x̄) which represent the unique elements in the free Heyting algebra HA[x̄] such that HA[x̄]/Δ^{n}(x̄) is isomorphic to the algebra of terms of implicational degree bounded by n, i.e., to Dn ; x̄. Since HA[x̄] has the disjunction property we deduce that Δ^{n}(x̄) is join-irreducible in H.

We want to say more about the elements Δ^{n}(x̄) ∈ HA[x̄]. In fact, we look at the more general situation of a Heyting algebra H ≅ HA[α^{−1,0}: D^{−1} → D^{0}] and Δ^{n} ∈ D^{n+2} the elements satisfying H/Δ^{n} ≅ D^{n}. In the sequel we use the order isomorphism γ_{D}: J (D) →^{≅} M(D) of a finite distributive lattice D.

Lemma 7.4 (i) Δ^{n} = ⋀{(p → m) → m | p ∈ J (D^{n}), m ∈ M(D^{n}), p ≰ m}.

(ii) Δ^{n} = ⋀{(p → γ_{D^{n}}(p)) → γ_{D^{n}}(p) | p ∈ J (D^{n})}.

Proof. Write π^{n} for the quotient H → D^{n}. As said before, all information contained in Δ^{n} is what happens to elements in D^{n+1}, i.e.,

Δ^{n} = ⋀{d ↔ π^{n}d | d ∈ D^{n+1}}.

As a lattice D^{n+1} is generated by elements of the form a → b (a, b ∈ D^{n}), and a is the join of join-irreducibles in D^{n}, and b is the meet of meet-irreducibles, so that

Δ^{n} = ⋀{(p → m) ↔ π^{n}(p → m) | p ∈ J (D^{n}), m ∈ M(D^{n}), p ≰ m}

(the pairs where p ≤ m do not contribute). But π^{n}(p → m) = p →_{D^{n}} m, which in case p ≰ m equals m since p →_{D^{n}} m ∧ p ≤ m. Finally, since (p → m) ↔ m = (p → m) → m the first equation follows.

For the second we note that by Lemma 4.4 the lattice D^{n+1} is generated by the elements p → γ_{D^{n}}(p) for p ∈ J (D^{n}). Since γ_{D^{n}}(p) is meet-irreducible and p ≰ γ_{D^{n}}(p) the same calculation as above proves the second equality. □

Example 7.5 From the explicit description of the free Heyting algebra on one generator (see for example [10], p. 35) one easily calculates that

Δ^{0}(x) = ¬¬x;
Δ^{1}(x) = ¬¬x → x;
Δ^{2}(x) = (¬¬x → x) → (x ∨ ¬x)

and for example Δ^{0}(x, y) = ¬¬(x ∧ y) ∧ (x → y) → y ∧ (y → x) → x. While these terms are easy to calculate we note that complexity increases dramatically. To calculate Δ^{2}(x, y) one has to know the poset J (D2 ; x̄), a poset with 718 elements (see Table 1).

Note that the inclusion D0 ; x̄ ↪ D_{x̄,ȳ}^{0} is induced on the level of joinirreducible elements by the projection P(x̄, ȳ) ↠ P(x̄), which is both open and co-open. Thus

D0 ; x̄ ↪ D_{x̄,ȳ}^{0},  x̄ ↦ x̄ ∈ D_{x̄,ȳ}^{0}

is a morphism of Heyting algebras (and co-Heyting) and Δ^{0}(x̄, ȳ) ⊢ Δ^{0}(x̄).

In contrast, the canonical map D_{x,y}^{1} ↪ D_{x,y,z}^{1} is not a morphism of Heyting algebras.

8 Functoriality

In this section, we turn the construction HA[α^{−1,0}: D^{−1} → D^{0}] into a functor. Let D denote the following sub-category of the arrow category DLat^{→}:

(i) Objects are morphisms α^{−1,0}: D^{−1} → D^{0} between distributive lattices (not necessarily finite) such that D^{0} has implications between elements in the image of α^{−1,0}.

(ii) An arrow f: (α^{−1,0}: D^{−1} → D^{0}) → (β^{−1,0}: E^{−1} → E^{0}) is a pair of morphisms (f^{−1}, f^{0}) of distributive lattices such that

\xymatrix{D^{−1} \ar[r]^{α^{−1,0}} \ar[d]_{f^{−1}} & D^{0} \ar[d]^{f^{0}} \\ E^{−1} \ar[r]_{β^{−1,0}} & E^{0}}

commutes, and where f^{0} is α^{−1,0}-open. (Note that this requires implicitly that E^{0} has implications between elements in the image of f^{0}.)

Given α^{−1,0}: D^{−1} → D^{0}, we consider the Heyting algebra HA[α^{−1,0}: D^{−1} → D^{0}], the Heyting algebra with the universal property that Heyting algebra morphisms HA[α^{−1,0}] → H correspond naturally to α^{−1,0}-open distributive lattice maps D^{0} → H. There is no doubt that HA[α^{−1,0}] exists: it is a quotient of the Heyting algebra freely generated by the lattice D^{0}, which in turn is a quotient of the free Heyting algebra on the set D^{0}. This shows as well that given α^{−1,0}, there is a canonical way to represent HA[α^{−1,0}], namely as the set of equivalence classes of an equivalence relation on the set of terms in the set of free variables D^{0}. This last observation is needed to turn our construction into a functor, and not just into a pseudo-functor.

Next we define HA[−] on arrows in D: Suppose we are given f = (f^{−1}, f^{0}): (α^{−1,0}: D^{−1} → D^{0}) → (β^{−1,0}: E^{−1} → E^{0}). By the universal property of HA[β^{−1,0}] there is a canonical β^{−1,0}-open map β^{0,∞}: E^{0} → HA[β^{−1,0}]. The composite β^{0,∞} ∘ f^{0}: D^{0} → HA[β^{−1,0}] is α^{−1,0}-open, so induces a map of Heyting algebras HA[f]: HA[α^{−1,0}] → HA[β^{−1,0}], and of course, the following diagram commutes:

\xymatrix{D^{0} \ar[r]^{α^{0,∞}} \ar[d]_{f^{0}} & HA[α^{−1,0}] \ar[d]^{HA[f]} \\ E^{0} \ar[r]_{β^{0,∞}} & HA[β^{−1,0}]}

The universal property of the Heyting algebras HA[−] guarantees that we obtain this way a functor.

Lemma 8.1 The functor HA[−]: D → HA is left adjoint to the inclusion functor i_{(−)}: HA → D, (i_{(−)} sends a Heyting algebra H to (id_{H}: H → H)). Moreover, HA[−] ∘ i_{(−)} ≅ id_{HA}.

Proof. There are natural bijections between the following data:

HA[α^{−1,0}] → H  in HA
α^{−1,0}-open maps D^{0} → H in DLat
maps [figure: D^{−1}; α^{−1,0}; H; D^{0}; H]  in D

which shows adjointness. Finally, given H in HA, id_{H}-open maps H → H′ are nothing but Heyting algebra morphisms H → H′, so that H ≅ HA[id_{H}].

□

We note that it follows from general category theory that the category HA can be obtained from D as a category of fractions (see for example [4], Section I.5.9).

After these general remarks we restrict ourselves to the full sub-category D_{fin} of D containing those objects α^{−1,0}: D^{−1} → D^{0} where D^{−1} and D^{0} are finite. Using Proposition 5.1 we get a functor

HA[−]: D_{fin} → HA_{f.p.},

up to isomorphism full on objects (Proposition 5.2). Note that in this case the right adjoint does not exist. Still, HA[−] so restricted is ‘full’ on arrows in the following liberate sense: Given φ: H → H′ in HA_{f.p.} there exists f: (α^{−1,0}) → (β^{−1,0}) in D_{fin} so that HA[α^{−1,0}] ≅ H, HA[β^{−1,0}] ≅ H′, and

[figure: HA[α^{−1,0}]; HA[f]; ≅; H; φ; HA[β^{−1,0}]; ≅; H′]

commutes.

Write Σ for the class of arrows in D_{fin} which are send by HA[−] to isomorphisms in HA_{f.p.}. It is clear that HA_{f.p.} is just the category of fractions of D_{fin}, inverting the arrows in Σ, that is, HA_{f.p.} ≅ D_{fin}[Σ^{−1}]. We leave it to the reader to show that Σ in fact admits a calculus of fractions:

Proposition 8.2 The class Σ of those arrows in D_{fin} which are sent to isomorphisms in HA_{f.p.} admits a calculus of fractions, and D_{fin}[Σ^{−1}] ≅ HA_{f.p.}.□

References

[1] R. Balbes and P. Dwinger. Distributive Lattices. University of Missouri Press, 1974.

[2] F. Bellissima. Finitely generated free Heyting algebras. J. Symbolic Logic, 51:152–165, 1986.

[3] G. Birkhoff. Lattice Theory. Amer. Math. Soc. Colloquium Publications, vol. 25, 1948.

[4] F. Borceux. Handbook of Categorical Algebra. Vol. 1, 2 and 3. Cambridge University Press, Cambridge 1994.

[5] C. Butz. Duality for finitely presented Heyting algebras. In preparation.

[6] D. van Dalen. Intuitionistic logic. In: Handbook of Philosophical Logic. Vol. III: Alternatives to Classical Logic. D. Gabbay and F. Guenther (eds.). D. Reidel Publishing Company, Dordrecht 1985.

[7] B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge University Press, Cambridge 1990.

[8] S. Ghilardi. Free Heyting algebras as bi-Heyting algebras. C. R. Math. Rep. Acad. Sci. Canada, 14:240–244, 1992.

[9] A. Hendriks. Computations in Propositional Logic. Ph.D. thesis, Amsterdam 1996.

[10] P. T. Johnstone. Stone Spaces. Cambridge University Press, Cambridge 1982.

[11] A. M. Pitts. On an interpretation of second order quantification in first order intuitionistic propositional logic. J. Symbolic Logic, 57:33–52, 1992.

[12] C. Rauszer. Semi-Boolean algebras and their applications to intuitionistic logic with dual operators. Fund. Math., 83:219-249, 1974.

[13] A. Urquhart. Free Heyting algebras. Algebra Univ., 3:94–97, 1973. 30

Recent BRICS Report Series Publications

RS-98-30 Carsten Butz. Finitely Presented Heyting Algebras. November 1998. 30 pp.

RS-98-29 Jan Camenisch and Markus Michels. Proving in Zero-Knowledge that a Number is the Product of Two Safe Primes. November 1998. 19 pp.

RS-98-28 Rasmus Pagh. Low Redundancy in Dictionaries with O(1) Worst Case Lookup Time. November 1998. 15 pp.

RS-98-27 Jan Camenisch and Markus Michels. A Group Signature Scheme Based on an RSA-Variant. November 1998. 18 pp. Preliminary version appeared in Ohta and Pei, editors, Advances in Cryptology: 4th ASIACRYPT Conference on the Theory and Applications of Cryptologic Techniques, ASIACRYPT ’98 Proceedings, LNCS 1514, 1998, pages 160–174.

RS-98-26 Paola Quaglia and David Walker. On Encoding pπ in mπ. October 1998. 27 pp. Full version of paper to appear in Foundations of Software Technology and Theoretical Computer Science: 18th Conference, FCT&TCS ’98 Proceedings, LNCS, 1998.

RS-98-25 Devdatt P. Dubhashi. Talagrand’s Inequality in Hereditary Settings. October 1998. 22 pp.

RS-98-24 Devdatt P. Dubhashi. Talagrand’s Inequality and Locality in Distributed Computing. October 1998. 14 pp.

RS-98-23 Devdatt P. Dubhashi. Martingales and Locality in Distributed Computing. October 1998. 19 pp.

RS-98-22 Gian Luca Cattani, John Power, and Glynn Winskel. A Categorical Axiomatics for Bisimulation. September 1998. ii+21 pp. Appears in Sangiorgi and de Simone, editors, Concurrency Theory: 9th International Conference, CONCUR ’98 Proceedings, LNCS 1466, 1998, pages 581–596.

RS-98-21 John Power, Gian Luca Cattani, and Glynn Winskel. A Representation Result for Free Cocompletions. September 1998. 16 pp.

RS-98-20 Søren Riis and Meera Sitharam. Uniformly Generated Submodules of Permutation Modules. September 1998. 35 pp.