An open mapping theorem for finitely copresented Esakia spaces

TL;DR

This paper proves an open mapping theorem for dual spaces of finitely presented Heyting algebras, providing a new semantic proof of the uniform interpolation theorem in intuitionistic logic using duality theory.

Contribution

It introduces a new open mapping theorem for finitely copresented Esakia spaces and offers a simplified, self-contained proof of uniform interpolation without sheaves or game semantics.

Findings

Established an open mapping theorem for duals of finitely presented Heyting algebras

Provided a new semantic proof of uniform interpolation in intuitionistic logic

Simplified proof technique avoiding sheaves and game semantics

Abstract

We prove an open mapping theorem for the topological spaces dual to finitely presented Heyting algebras. This yields in particular a short, self-contained semantic proof of the uniform interpolation theorem for intuitionistic propositional logic, first proved by Pitts in 1992. Our proof is based on the methods of Ghilardi & Zawadowski. However, our proof does not require sheaves nor games, only basic duality theory for Heyting algebras.