On the free Heyting algebra extension of a Hilbert algebra

TL;DR

This paper constructs an explicit left adjoint functor from Heyting algebras to Hilbert algebras, clarifying their categorical relationship and extending prior work on free implicative semilattice extensions.

Contribution

It provides an explicit construction of the left adjoint functor, enhancing understanding of the categorical connection between Heyting and Hilbert algebras.

Findings

Explicit construction of the left adjoint functor.

Factorization through free implicative semilattice extension.

Clarification of categorical relationships between algebra classes.

Abstract

In this paper we provided an explicit construction for the left adjoint of the forgetful functor from the category of Heyting algebras to that of Hilbert algebras. This functor factorizes through the free implicative semilattice extension of a Hilbert algebra of Celani and Jansana [On the free implicative semilattice extension of a Hilbert algebra}. Mathematical Logic Quarterly 58, 3 (2012), 188--207].