Game semantics of universes in Martin-Löf type theory (Preprint)

  <Reference List>
Type: Preprint
National /International: International
Title: Game semantics of universes in Martin-Löf type theory
Publication Date: 2025-09-18
Authors: - Norihiro Yamada
Abstract:

We extend game semantics of Martin-Löf type theory to a cumulative hierarchy of universes. This extension fulfils game semantics of all standard types in Martin-Löf type theory for the first time in the literature. More broadly, its contribution to mathematical semantics, constructive mathematics and foundations of mathematics is that it is the first intensional model of universes, showing that it is possible to interpret universes by finitary computational steps. In contrast, extensional models of universes, e.g., realisability and domain models, were given more than 30 years ago. As a result, the powerful combinatorial method of game semantics becomes available for the study of universes and types generated by them. We illustrate this advantage by applying the game semantics to show the independence of Markov's principle from Martin-Löf type theory with universes. A challenge in obtaining game semantics of universes comes from a conflict between identity types and universes: Naive game semantics of the encoding of identity types by universes yields a decision procedure on the equality between functions, contradicting recursion theory. We conquer this challenge by novel games for universes whose strategies encode games for identity types without deciding the equality. In this way, we encode extensionally undecidable types effectively by intensional computations.

Institution: DMUC 25-31
Online version: http://www.mat.uc.pt...prints/eng_2025.html
Download: Not available
 
© Centre for Mathematics, University of Coimbra, funded by
Science and Technology Foundation
Powered by: rdOnWeb v1.4 | technical support