Christian Espíndola: Beth models for intuitionistic logic

The semantics of possible worlds for intuitionistic logic gives rise to Kripke models and its variant, Beth models. Although both semantics can be shown to be complete, we will see that the later has advantages over the former in the sense that with a weaker metatheory, they describe a wider variety of categorical models. In particular, we will discuss how to build, for every model in a Grothendieck topos, an elementarily equivalent Beth model, as well as the constructive aspects and applications of this.