Oskar Berndal: Type theoretic semantics for first order logic
Tid: Fr 2020-01-31 kl 10.00 - 11.00
Föreläsare: Oskar Berndal
Plats: Kräftriket, house 5, room 31
Whereas the semantics of first order logic are well-understood, many questions remain regarding the semantics of type theory. There is not even an established and unified notion of what precisely is a type theory.
In a recent work by Uemura, a general notion of type theories is proposed together with semantics for these type theories. The aim of this work is to present a type theory within this framework such that its semantics recovers the semantics for first order logic.
The main obstacle is the mismatch between what one takes as a morphism in the semantics: In first order logic one takes the functional relations whereas in type theory one essentially takes its terms. In order to bridge this gap we introduce terms for definite descriptions to the type theory.