Coexact completion of profinite Heyting algebras and uniform interpolation
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866908956843048960 |
|---|---|
| author | Ye, Lingyuan |
| author_facet | Ye, Lingyuan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_08267 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Coexact completion of profinite Heyting algebras and uniform interpolation Ye, Lingyuan Logic Logic in Computer Science Category Theory 06D20, 03C40, 03B20 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. |
| title | Coexact completion of profinite Heyting algebras and uniform interpolation |
| topic | Logic Logic in Computer Science Category Theory 06D20, 03C40, 03B20 |
| url | https://arxiv.org/abs/2604.08267 |