“Joyal-Tierney and constructive model theory”
Martedì 28 Gennaio 2020, ore 14:30 - Aula 2AB45 - Henrik Forssell (U. of Stockholm)
Abstract
In the absence of the Gödel completeness theorem, constructive logicians frequently resort to sheaf theoretic methods for semantic proofs. The Joyal-Tierney representation theorem states that every sheaf topos, and thus the classifying topos of any geometric theory T, can be represented as the topos of equivariant sheaves on a localic groupoid (where, then, a point of the groupoid corresponds to a Tarski model of T). We revisit the Joyal-Tierney theorem from both a syntactical and semantic perspective, and connect it to certain formal space valued models used by Coquand, Sadocco, Sambin, and Smith.
