BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Heyting Algebras and Higher-Order Logic - Prof. Andrew M Pitts (Un
 iversity of Cambridge)
DTSTART:20250519T120000Z
DTEND:20250519T130000Z
UID:TALK229879@talks.cam.ac.uk
CONTACT:Dr Meven Lennon-Bertrand
DESCRIPTION:Every logical theory gives rise to a Lindenbaum-Tarski algebra
  of truth values\, whose underlying set is the theory's sentences quotient
 ed by provability in the theory. For theories in classical first-order log
 ic\, the algebras that arise are exactly all possible Boolean algebras. Fo
 r theories in intuitionistic first-order logic\, they are all possible Hey
 ting 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 kn
 ow which Heyting algebras can be the Lindenbaum-Tarski algebra of a higher
 -order theory.\n\nMy attempt to resolve this question more than 30 years a
 go failed\, but produced the consolation prize of a very surprising proper
 ty of intuitionistic logic that has subsequently been called "uniform inte
 rpolation". I will explain the connection between Heyting algebras of high
 er order theories and uniform interpolation and tell you something of what
  has followed in the pursuit of this open question.
LOCATION:FS07\, Computer Laboratory
END:VEVENT
END:VCALENDAR