JAIST Logic@JAIST

A Realizability Model for Type Theory

  • Keiko Nakata
  • Institute of Cybernetics, Tallinn University of Technology
  • Web site
Date: 2014/07/07 (Mon) 13:30 to 15:00
Place: JAIST IS school seminar room I45
Group: Logic Unit
We construct a realizability model for a Martin-Löf dependent type theory for the study of consistency and unprovability. We closely follow the approach of Coquand and Spiwack and take (equivalence classes of) the terms of the untyped lambda calculus extended with constants as the domain. The domain model naturally gives rise to a realizability model.

We use the realizability interpretation to prove unprovability in the type theory of the equivalence of Noetherian sets and streamless sets, two classically equivalent definitions of finite sets. Any Noetherian set is streamless, but the converse implication is unprovable in the type theory. For the latter result, we use (the functional version of) Markov's principle and a non-classical axiom ¬Πn:N.(H n)+¬(H n) for a halting predicate H, both of which have realizers.

(Joint work with Marc Bezem and Thierry Coquand)