Henrik Forssell: The coherent definability theorem by locales of models
Time: Wed 2022-11-23 10.00 - 12.00
Location: Albano house 1, floor 3, Room U (Kovalevsky)
Participating: Henrik Forssell, Oslo Metropolitan University
Abstract
In his PhD Thesis, Johan Lindberg gave an explicit description of the Joyal-Tierney representation theorem in terms of locales of models of geometric theories. We revisit this description and show an example application of it by giving a constructive formulation and proof of the Definability Theorem for coherent logic (Elephant, D3.5.1).