Coexact completion of profinite Heyting algebras and uniform interpolation

TL;DR

This paper links sheaf representations and profinite completions of finitely presented Heyting algebras, exploring their topos-theoretic properties and implications for uniform interpolation.

Contribution

It demonstrates the equivalence between sheaf representations and profinite completions of finitely presented Heyting algebras and analyzes the properties of the associated K-topos.

Findings

Dual category of profinite Heyting algebras is an infinitary extensive regular category.

The ex/reg-completion of this category is the K-topos.

Properties of uniform interpolation extend within the K-topos context.

Abstract

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.