Rodrigo ALMEIDA (University of Amsterdam) will give a talk on
Higher order uniform interpolation and Pitts problem
Abstract:
Given an elementary topos E, the lattice Sub_{E}(1) of its subterminal objects — called sometimes the `truth-values’ of E — always forms a Heyting algebra. In the early 80s, Andrew Pitts asked the following question: can every Heyting algebra H arise as Sub_{E}(1) for some elementary topos E? Despite work by Pitts, Pataraia, Jibladze and others, the full problem has remained unsolved. In this talk I will briefly survey what is known about this problem, and present some parts of an ongoing research project aimed at obtaining a (positive) solution to it. In particular I will introduce the concept of a “Pataraia doctrine”, with close connections to first-order hyperdoctrines with comprehension studied by Pitts (2004), show how they can be used to construct elementary toposes and present the key challenges of constructing such objects based on a given Heyting algebra. Lifting from Pitts original work on the subject, I will also introduce some notions of higher-order uniform interpolation, and the “Pitts implications” which tell how such properties arise in connection with this problem.
This talk reports on ongoing joint work with Marco Abbadini, Igor Arrieta, Daniel Otten and Lingyuan Ye.