Coexact completion of profinite Heyting algebras and uniform interpolation
2026-04-09 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors explain that a previous way of representing certain logical structures called Heyting algebras (by Ghilardi and Zawadowski) is basically the same as another process known as profinite completion. They explore properties of the category formed by these profinite Heyting algebras, showing it has nice mathematical features, and identify a related sheaf structure called the K-topos. They also show that some logical interpolation properties, which help connect formulas, naturally arise from the internal logic of this K-topos. Along the way, they describe additional properties of the K-topos using topos theory.
Heyting algebraSheaf representationProfinite completionProfinite Heyting algebraTopos theoryK-toposCategory theoryUniform interpolationEx/reg-completionInternal logic
Authors
Lingyuan Ye
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.