Finitely Presented Heyting Algebras
DOI:
https://doi.org/10.7146/brics.v5i30.19436Resumé
In this paper we study the structure of finitely presented Heytingalgebras. 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 algebra 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 : HAop
f:p: ! PoSet; 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 nite Heyting algebras. Our contribution is a simple proof of the nite model property which names in particular a canonical family of nite Heyting algebras into which we can
embed a given finitely presented one.
In Section 3 we recapitulate the standard duality between nite distributive lattices and nite 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 nite 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 nitely presented
Heyting algebra is co-Heyting, i.e., that the operation (−) n (−) dual to implication is dened. 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.
Downloads
Publiceret
1998-01-30
Citation/Eksport
Butz, C. (1998). Finitely Presented Heyting Algebras. BRICS Report Series, 5(30). https://doi.org/10.7146/brics.v5i30.19436
Nummer
Sektion
Artikler
Licens
Authors who publish with this journal agree to the following terms:- Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).