Logic seminar: Andrew Pitts
| Dates: | 30 April 2025 |
|---|
| Times: | 15:00 - 16:00 |
|---|
| What is it: | Seminar |
|---|
| Organiser: | Department of Mathematics |
|---|
| Who is it for: | University staff, External researchers, Adults, Alumni, Current University students |
|---|
|
Title: Heyting Algebras and Higher-Order Logic
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.
Travel and Contact Information
Find event
Frank Adams 1
Alan Turing Building
Manchester
