Hyper-MacNeille Completions of Heyting algebras

TL;DR

This paper introduces the hyper-MacNeille completion for Heyting algebras, characterizes it algebraically via centrally supplemented extensions, and proves its closure properties within finitely generated varieties.

Contribution

It provides an algebraic description of hyper-MacNeille completions and demonstrates their closure in finitely generated Heyting algebra varieties.

Findings

Hyper-MacNeille completion equals MacNeille of the centrally supplemented extension.

Finitely generated varieties of Heyting algebras are closed under hyper-MacNeille completions.

Connections established between centrally supplemented extensions and Boolean products.

Abstract

A Heyting algebra is supplemented if each element $a$ has a dual pseudo-complement $a^+$, and a Heyting algebra is centrally supplement if it is supplemented and each supplement is central. We show that each Heyting algebra has a centrally supplemented extension in the same variety of Heyting algebras as the original. We use this tool to investigate a new type of completion of Heyting algebras arising in the context of algebraic proof theory, the so-called hyper-MacNeille completion. We show that the hyper-MacNeille completion of a Heyting algebra is the MacNeille completion of its centrally supplemented extension. This provides an algebraic description of the hyper-MacNeille completion of a Heyting algebra, allows development of further properties of the hyper-MacNeille completion, and provides new examples of varieties of Heyting algebras that are closed under hyper-MacNeille completions. In particular, connections between the centrally supplemented extension and Boolean products allow us to show that any finitely generated variety of Heyting algebras is closed under hyper-MacNeille completions.