2020/07/16 by Norihiro Yamada, Yamada, Norihiro
Computer Science · #Advanced Database Systems and Queries #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2007.08094
openalex publication_date 2020/07/16 · openalex created_date 2024/04/11 · openalex updated_date 2026/07/28
We prove consistency of intensional Martin-Löf 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 à 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 ξ-rule). We overcome this point and prove the consistency by novel realizability à la game semantics, which is based on the author's previous work.