First-Order Logic with Isomorphism
Dimitris Tsementzis: Rutgers University
Location: Hill 705
Date & time: Monday, 20 February 2017 at 5:00PM - 5:11PM
We describe an extension of the syntax and proof system of first-order logic that has a natural semantics in the Univalent Foundations. This allows us to carry out a model theory in which mathematical structures are formalized in terms of homotopy types, just as in traditional model theory they are formalized in terms of sets. After defining the system, we will outline the relevant soundness and completeness results and sketch some applications.
This talk is based on the paper here: (https://arxiv.org/abs/1603.03092) and relevant slides can be found here: (http://rci.rutgers.edu/~dt506/HMT.online.version.pdf).