MacNeille and hyper-MacNeille completions of Heyting algebras

Frederik Möllerström Lauridsen

(Joint work with John Harding)

Recently Ciabattoni, Galatos, and Terui have introduced a new notion of completion of residuated lattices which they call the hyper-MacNeille completion. This type of completion plays a central role in their work on establishing the admissibility of the cut-rule in certain types of hypersequent calculi for substructural logics.

In this talk we will focus on describing the hyper-MacNeille completion of Heyting algebras. We show that the hyper-MacNeille completion and the MacNeille completion coincide for so-called centrally supplemented Heyting algebras. That is, Heyting algebras with order-duals being Stone lattices. In fact, we show that any Heyting algebra A has a centrally supplemented extension S(A) such that the hyper-MacNeille completion of A is isomorphic to the MacNeille completion of S(A). These centrally supplemented extensions turn out to be the order-duals of the 1-Stone extensions originally introduced by Davey in 1972.