Coexact completion of profinite Heyting algebras and uniform interpolation
This work provides foundational insights into the algebraic and topos-theoretic structures of Heyting algebras, which is incremental for researchers in mathematical logic and category theory.
The paper demonstrates that the sheaf representation of finitely presented Heyting algebras is algebraically equivalent to profinite completion, and shows that uniform interpolation properties generalize to profinite Heyting algebras as consequences of the internal logic of the K-topos.
This paper shows that the sheaf representation of finitely presented Heyting algebras constructed by Ghilardi and Zawadowski is, from an algebraic perspective, equivalent to the construction of profinite completion. We show that the dual category of profinite Heyting algebras is an infinitary extensive regular category, and its ex/reg-completion is exactly the aforementioned sheaf topos, which we refer to as the K-topos. We show how certain properties of uniform interpolation can be generalised to the context of arbitrary profinite Heyting algebras, and are consequences of the internal logic of the K-topos. Along the way we also establish various topos-theoretic properties of the K-topos.