Van den Berg - The Herbrand Topos

Category theory and topos theory can be used to provide semantic analogues of syntactic interpretations. For example, there is a topos, the effective topos, whose internal logic is given by number realizability. In this talk I will discuss another instance of this phenomenon. In earlier work together with Eyvind Briseid and Pavol Safarik we introduced a new realizability interpretation we dubbed "Herbrand realizability". In this talk I will explain the idea behind this interpretation and construct a new topos, the "Herbrand topos", whose internal logic coincides with Herbrand realizability.