Game semantics of Martin-L\"of type theory, part III: its consistency with Church's thesis

TL;DR

This paper establishes the consistency of intensional Martin-Löf type theory with Church's thesis using a novel game semantics approach, addressing longstanding challenges in formal verification.

Contribution

It introduces a new realizability method based on game semantics to prove the consistency of MLTT with Church's thesis, overcoming previous limitations.

Findings

Proves consistency of MLTT with Church's thesis

Develops a novel game semantics-based realizability method

Addresses limitations of traditional realizability approaches

Abstract

We prove consistency of intensional Martin-L\"of type theory (MLTT) with formal Church's thesis (CT), which was open for at least fifteen years. The difficulty in proving the consistency is that a standard method of realizability \`{a} la Kleene does not work for the consistency, though it validates CT, as it does not model MLTT; specifically, the realizability does not validate MLTT's congruence rule on pi-types (known as the $\xi$-rule). We overcome this point and prove the consistency by novel realizability \`{a} la game semantics, which is based on the author's previous work.