Heyting Algebras and Higher-Order Logic

Add to your list(s) Download to your calendar using vCal

• Prof. Andrew M Pitts (University of Cambridge)
• Monday 19 May 2025, 13:00-14:00
• FS07, Computer Laboratory.

If you have a question about this talk, please contact Dr Meven Lennon-Bertrand.

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.

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• FS07, Computer Laboratory
• tcw57’s list

Note that ex-directory lists are not shown.