Abstract

Every logical theory gives rise to a Lindenbaum-Tarski algebra of truth values, whose underlying set is the theory’s sentences quotiented by provability in the theory. For theories in classical first-order logic, the algebras that arise are exactly all possible Boolean algebras. For theories in intuitionistic first-order logic, they are all possible Heyting algebras. What happens when we move from first-order to higher-order? Higher-order logic allows quantification not only over individuals, but also over sets of individuals, sets of sets of individuals, and so on, for any finite order of iterating “sets of”. In the classical case, the Lindenbaum-Tarski algebras of higher-order theories are still all Boolean algebras. In the intuitionistic case, as far as I am aware, we do not know which Heyting algebras can be the Lindenbaum-Tarski algebra of a higher-order theory.

My attempt to resolve this question more than 30 years ago failed, but produced the consolation prize of a very surprising property of intuitionistic logic that has subsequently been called “uniform interpolation”. I will explain the connection between Heyting algebras of higher order theories and uniform interpolation and tell you something of what has followed in the pursuit of this open question.