Representations and model theory of free Heyting algebras

In this thesis we study representations and general model theory of free Heyting algebras, free products of Heyting algebras, and several related constructions and concepts. In particular, we systematically employ duality theory to uncover the geometric structure of those properties, with a focus on the logical analysis of intuitionistic logic, and its extensions. The most direct outcomes of such a study concern the theory of normal forms and its applications, the study of translations between intuitionistic logic and its fragments, and the development of tools for other related systems such as bi-intuitionistic logic, or intuitionistic modal logic. This finds further uses in the theoretical analysis of properties like interpolation, or in the uniform development of coalgebraic semantics.
The representations developed in the first part of the thesis are then used to settle some open problems in the field, concerning the model theory of free Heyting algebras. These are twofold: the study of uniform bounds on the complexity of free algebras leads us to the concept of uniform local tabularity, where we settle a question by Shehtman over the equivalence between this concept and local tabularity. On the other hand, in studying higher-order extensions of intuitionistic logic, we are lead to a question of Andrew Pitts about which Heyting algebras arise as lattices of truth-values of elementary toposes, where we extend the class of algebras for which a solution is known.