“The consistency of intensional Martin-Löf type theory with formal Church’s thesis, a game-semantic approach”
Lunedì 21 Settmbre 2020, ore 16:30 - Zoom - Norihiro Yamada (University of Minnesota)
Abstract
In this talk, I will show that intensional Martin-Löf type theory is consistent with formal Church’s thesis, which solves a problem in type theory and constructive mathematics open for a while. My proof is based on game semantics, a particular kind of mathematical semantics of logic and computation, and the proof utilizes some characteristic feature of game semantics in a fundamental way. Rather than the technical details, the talk will focus on sketching the following main points: 1. Introduction to intensional Martin-Löf type theory and formal Church’s thesis; 2. Why the consistency problem is difficult; 3. The proof idea.
