Penn Arts & Sciences Logo

Logic and Computation Seminar

Monday, April 18, 2022 - 3:30pm

Steve Awodey

Carnegie Mellon University


University of Pennsylvania

online - link available upon request

Recent joint work [1] with Nicola Gambino and Sina Hazratpour is presented.  Kripke-Joyal semantics extends the basic Kripke semantics for intuitionistic propositional logic (IPL) and first-order logic (IFOL) to the higher-order logic used in topos theory (IHOL).  It provides a systematic way to interpret propositions of IHOL into any Grothendieck topos and to test them for validity under the interpretation.  We extend the interpretation to the dependent type theory of Martin-Löf (MLTT), using the formalism of natural models [2].  A Kripke completeness theorem for MLTT is also given.  Prior cases of presheaf semantics for MLTT are subsumed, including the presheaf models of homotopy type theory (HoTT) of Voevodsky et al. and Coquand et al. 


[1] Steve Awodey, Nicola Gambino, Sina Hazratpour, Kripke-Joyal forcing for type theory and uniform fibrations, arXiv:2110.14576, 2021.


[2] Steve Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer Science, pp. 241–286, 2016.