Stack Representation of First-order Intuitionistic Theories
Lingyuan Ye
There is a classical result of Pitts that propositional intuitionistic logic eliminates second order propositional quantifiers. Later, Ghilardi and Zawadowski have worked out a semantic proof of this by developing a sheaf representation of finitely presented Heyting algebras. The basic idea is to represent a Heyting algebra via its collection of models on finite Kripke frames, expressed in a suitable categorical and sheaf-theoretic language. Their representation allows them to show, among other things, that the algebraic theory of Heyting algebras has a model companion, and the quantifier elimination result also follows as a consequence. In this talk, I will briefly recall these classical result and show the possibility of extending these developments to a suitable class of first-order intuitionistic theories. In particular, I will explain how to construct higher sheaf representation of first-order intuitionistic theories, and discuss some possible outcomes.