Investigating Definability in Propositional Logic via Sheaves on Grothendieck Topologies

We address definability questions in propositional intuitionistic logic via an embedding of the opposite of the category of finitely presented Heyting algebras into a suitable sheaf topos. The closure properties of such an embedding are established by combinatorial arguments relying on Ehrenfeucht-Fraissé games. Applications are given to model-completability, fixpoints definability, projectivity, and unification theory.