论文标题
马丁 - 洛夫类型理论的游戏语义，第三部分：它与教会论文的一致性
Game semantics of Martin-Löf type theory, part III: its consistency with Church's thesis
论文作者
论文摘要
我们证明了强度马丁 - 洛夫类型理论（MLTT）与正规教会的论文（CT）的一致性，该论文至少十五年。证明一致性的困难在于，kleene的标准方法不起作用，尽管它验证了CT，但由于它没有建模MLTT，但它验证了CT。具体而言，可实现性不能验证MLTT的一致性规则（称为$ξ$ -rule）。我们克服了这一点，并通过新颖的“游戏语义”语义证明了一致性，该语义是基于作者以前的作品。
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.
