Model completions and r-Heyting categories (Q1372155)

Using a syntactic version of Pitts' Theorem, the authors show in a first section that the first-order theory of Heyting algebras admits a model completion and that the opposite of the category of finitely represented Heyting algebras is a Heyting category. Following a brief recall of some notions concerning finitely represented algebras and the consideration of \(r\)-Heyting categories and their basic properties, a generalisation of the observation about Heyting algebras is proved in the next sections. Let \(T\) be an equational theory. Then the main result says that, under the assumption that the posets of regular subobjects of the opposite \({\mathbf T}\) of the category of locally presented \(T\)-algebras carry a Heyting algebra structure which is pullback-stable, \(T\) admits a model completion iff \({\mathbf T}\) is an \(r\)-Heyting category. The assumption above is equivalent to a conjunction of well-known notions from universal algebra. In an appendix it is shown that there are exactly 8 varieties of Heyting algebras whose theory admits a model completion.