首页/论文/2007.08094

arXiv 2007.080942020-07-28math.LOcs.LO

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

Norihiro Yamada

英文摘要：

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.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

On Church's Thesis in Cubical Assemblies

We show that Church's thesis, the axiom stating that all functions on the naturals are computable, does not hold in the cubical assemblies model of cubical type theory. We show that nevertheless Church's thesis is consistent with univalent type theory by constructing a reflective subuniverse of cubical assemblies where it holds.

2019-05-08cs.LOmath.LO

关于无限计算的丘奇-图灵命题

Towards a Church-Turing-Thesis for Infinitary Computations

我们考虑的问题是，是否有一个无限类似的丘奇图灵命题。为此，我们认为，有一个直观的概念，超限可计算性，并建立一个规范的模型，称为理想化代理机（$IAM$），这将是等同于强度的顺序图灵机定义的P。

2013-07-24math.LO

基本商完备化、丘奇论题与分划装配

Elementary Quotient Completions, Church's Thesis, and Partioned Assemblies

本文通过将有效拓扑斯与装配拟拓扑斯统一视为基于分划装配的Lawvere学说的基本商完备化，解释了二者所满足的丘奇论题形式差异的根源。

2019-06-21math.LO

Unconstrained Church-Turing thesis cannot possibly be true

University of Michigan（密歇根大学）

The Church-Turing thesis asserts that if a partial strings-to-strings function is effectively computable then it is computable by a Turing machine. In the 1930s, when Church and Turing worked on their versions of the thesis, there was a robust notion of algorithm. These traditional algorithms are known also as classical or sequential. In the original thesis, effectively computable meant computable by an effective classical algorithm. Based on an earlier axiomatization of classical algorithms, the original thesis was proven in 2008. Since the 1930s, the notion of algorithm has changed dramatica…

2019-01-15cs.CLcs.DScs.LO

归纳形式拓扑、丘奇论题和选择公理的可实现性语义

A realizability semantics for inductive formal topologies, Church's Thesis and Axiom of Choice

本文为扩展了归纳形式拓扑、丘奇论题和选择公理的极简主义基础理论意向层（mtt）提出了一种Kleene可实现性语义，并在Aczel构造性集合论CZF加正则扩展公理中形式化该语义，以证明其一致性。

2021-05-26math.LO

算术丘奇论题下的范式与一致反射

Normal Forms and Uniform Reflection under the Arithmetical Church Thesis

本研究在算术丘奇论题下细化二阶算术的解析分层，得到更精细区分量词交替的范式，并以此证明Frittaion分离定理中的选择假设不可省略。

2026-08-05math.LO

更多相关论文收起更多论文

Turing-Church thesis, constructve mathematics and intuitionist logic

At a first glance the Theory of computation relies on potential infinity and an organization aimed at solving a problem. Under such aspect it is like Mendeleev theory of chemistry. Also its theoretical development reiterates that of this scientific theory: it makes use of doubly negated propositions and its reasoning proceeds through ad absurdum proofs; a final, universal predicate of equivalence of all definitions of a computations is translated into an equality one, and at the same time intuitionist logic into classical logic. Yet, the last step of this development of current theory includes…

2021-01-13math.LO

Parametric Church's Thesis: Synthetic Computability without Choice

In synthetic computability, pioneered by Richman, Bridges, and Bauer, one develops computability theory without an explicit model of computation. This is enabled by assuming an axiom equivalent to postulating a function $ϕ$ to be universal for the space $\mathbb{N}\to\mathbb{N}$ ($\mathsf{CT}_ϕ$, a consequence of the constructivist axiom $\mathsf{CT}$), Markov's principle, and at least the axiom of countable choice. Assuming $\mathsf{CT}$ and countable choice invalidates the law of excluded middle, thereby also invalidating classical intuitions prevalent in textbooks on computability. On the o…

2021-12-22cs.LOmath.LO

Means-fit effectivity

Historically, the notion of effective algorithm is closely related to the Church-Turing thesis. But effectivity imposes no restriction on computation time or any other resource; in that sense, it is incompatible with engineering or physics. We propose a natural generalization of it, means-fitting effectivity, which is effectivity relative to the (physical or abstract) underlying machinery of the algorithm. This machinery varies from one class of algorithms to another. Think for example of ruler-and-compass algorithms, arithmetical algorithms, and Blum-Shub-Smale algorithms. We believe that mea…

2020-02-20cs.LOmath.LO

基本交互式算法：预览

Basic interactive algorithms: Preview

University of Michigan（密歇根大学）

本文预览了基本交互式算法的公理化工作，回顾了基本算法的公理化及其在证明 Church-Turing 论题中的作用，并探讨了概率、非确定性和量子算法等扩展概念与预言机基本算法的关联。

2025-08-07cs.CLcs.LOmath.LO

带Church论题和选择公理的归纳与余归纳拓扑生成

Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice

本研究通过将mTTcind+CT+AC的一致性归结为CZF+REA，证明了在最小主义框架中添加余归纳定义不增加一致性强度，并给出了两种解释路径。

2022-11-11math.LO

An interpretation of the Sigma-2 fragment of classical Analysis in System T

We show that it is possible to define a realizability interpretation for the $Σ_2$-fragment of classical Analysis using Gödel's System T only. This supplements a previous result of Schwichtenberg regarding bar recursion at types 0 and 1 by showing how to avoid using bar recursion altogether. Our result is proved via a conservative extension of System T with an operator for composable continuations from the theory of programming languages due to Danvy and Filinski. The fragment of Analysis is therefore essentially constructive, even in presence of the full Axiom of Choice schema: Weak Church's …

2015-01-29cs.LOmath.LO

Realizability Semantics for Quantified Modal Logic: Generalizing Flagg's 1985 Construction

A semantics for quantified modal logic is presented that is based on Kleene's notion of realizability. This semantics generalizes Flagg's 1985 construction of a model of a modal version of Church's Thesis and first-order arithmetic. While the bulk of the paper is devoted to developing the details of the semantics, to illustrate the scope of this approach, we show that the construction produces (i) a model of a modal version of Church's Thesis and a variant of a modal set theory due to Goodman and Scedrov, (ii) a model of a modal version of Troelstra's generalized continuity principle together …

2016-03-01math.LO

Lifschitz Realizability as a Topological Construction

We develop a number of variants of Lifschitz realizability for CZF by building topological models internally in certain realizability models. We use this to show some interesting metamathematical results about constructive set theory with variants of LLPO including consistency with unique Church's thesis, consistency with some Brouwerian principles and variants of the numerical existence property.

2018-06-26math.LO

Higher-Order Functions and Brouwer's Thesis

Extending Martín Escardó's effectful forcing technique, we give a new proof of a well-known result: Brouwer's monotone bar theorem holds for any bar that can be realized by a functional of type $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$ in Gödel's System T. Effectful forcing is an elementary alternative to standard sheaf-theoretic forcing arguments, using ideas from programming languages, including computational effects, monads, the algebra interpretation of call-by-name $λ$-calculus, and logical relations. Our argument proceeds by interpreting System T programs as well-founded dialogue tree…

2021-04-19cs.LOmath.LO

An extensional Kleene realizability semantics for the Minimalist Foundation

We build a Kleene realizability semantics for the two-level Minimalist Foundation MF, ideated by Maietti and Sambin in 2005 and completed by Maietti in 2009. Thanks to this semantics we prove that both levels of MF are consistent with the (Extended) formal Church Thesis CT. MF consists of two levels, an intensional one, called mTT and an extensional one, called emTT, based on versions of Martin-Löf's type theory. Thanks to the link between the two levels, it is enough to build a semantics for the intensional level to get one also for the extensional level. Hence here we just build a realizabil…

2015-05-05math.LO

扩展、省略类型和标准系统

Expansions, omitting types, and standard systems

递归饱和和辉煌是算术模型中的两个重要概念。Kaye、Kossak和Kotlarski引入了算术饱和的概念，并认为递归饱和可能不像最初假设的那样严格。在这篇论文中，我们给出了递归饱和的变化的进一步的例子，所有这些都与类似于辉煌的可扩展性属性有关。然而，可扩展性比辉煌性更强，并且以某种方式暗示着扩展不仅满足一个理论，而且省略了一个类型。我们推测，这种可扩展性的一个特殊版本实际上相当于算术饱和。我们证明了这些性质中的另一个等价于β-饱和。我们还介绍了递归饱和的一个变体，它在标准谓词的上下文中是有意义的，并且相当于一定量的普通饱和。本文还研究了所有忽略某个类型p（x）的模型的理论。我们定义了一个证明系统，它证明一个句子当且仅当它在所有省略类型p（x）的模型中为真。讨论了这类证明系统的复杂性，并给出了在特殊意义下具有高复杂性的一些理论和类型的显式例子。最后，我们对斯科特的问题做了一个小小的评论。在Martin公理的假设下，证明了具有可数链条件的在算术理解下闭的基数<2^{ \aleph_0 }的Scott集是PA的某个模型的标准系.然而，我们不知道是否存在这样的不可数Scott集。

2004-10-25math.LO