Title: First-Order Logic with Isomorphism
Speaker: Dimitrios Tsementzis (Rutgers University)
Abstract: The Univalent Foundations (UF) is a proposed foundation for mathematics that takes as primitive a notion of space (rather than a notion of set). A logic for UF would be a formal system which expresses theories formalized in terms of spaces, just as first-order logic expresses theories formalized in terms of sets. After a quick introduction to UF, I will proceed to develop such a logic, and sketch a proof that it is sound and complete with respect to its spatial semantics.