首页/论文/1104.2744

arXiv 1104.27442011-04math.LO

非确定性归纳定义

Non-deterministic inductive definitions

Benno van den Berg

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

我们研究了一个新的证明原则的建设性Zermelo-Fraenkel集合论的背景下，我们将所谓的“非确定性归纳定义”。我们给正式拓扑的应用程序，以及这一原则的谓词理由。

英文摘要：

We study a new proof principle in the context of constructive Zermelo-Fraenkel set theory based on what we will call "non-deterministic inductive definitions". We give applications to formal topology as well as a predicative justification of this principle.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

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

继续探索

相关论文

用有界算术中的归纳定义刻画复杂类

Characterising Complexity Classes by Inductive Definitions in Bounded Arithmetic

著名的描述性特征的P和PSPACE重述的库克-阮风格的二阶有界算术。本文引入二阶有界算术上的归纳定义公理。我们表明，P可以捕获的公理的暴胀归纳定义，而PSPACE可以捕获的公理的非暴胀归纳定义。

2014-01-20math.LO

功能解释和归纳定义

Functional interpretation and inductive definitions

扩展哥德尔的\emph{Dialectica}解释，我们提供了一个功能的解释，经典理论的积极算术归纳定义，减少他们的理论有限型泛函定义使用超限递归良好的树。

2009-02-17math.LO

利用非单调归纳定义的良基性证明II：一阶算子

Wellfoundedness proofs by means of non-monotonic inductive definitions II: first order operators

本文给出了$Π_N$ -反射序数的递归记法系统的良基性的两个证明。一种是基于$Π_{N-1}^0$归纳定义，另一种是基于区分类。

2010-05-12math.LO

归纳定义系统ID_1的可证计算函数的简化刻画

A Simplified Characterisation of Provably Computable Functions of the System ID_1 of Inductive Definitions

我们提出了一个简化和流线型的可证明的全部可计算功能的理论ID_1的非迭代归纳定义的特征。的想法是简化采用的方法，运营商控制的衍生工具，最初介绍了由Wilfried Buchholz和后来申请的第二作者的一个特征证明总可计算功能的皮亚诺算术PA。

2012-05-13math.LO

正归纳定义的弱理论的证明理论强度

Proof-theoretic strengths of weak theories for positive inductive definitions

在本文中，光面$Π^{1}_{1}$ -概括公理被证明是证明理论上强，甚至在$\mbox{RCA}_{0}^{*}$，我们校准证明理论的弱片段的序数的理论$\mbox{ID}_{1}$的正归纳定义在自然数。证明了$\mbox{ID}_{1}$的超穷归纳法公理中正负公式的合取是弱的，而析取是强的.因此，我们在$\mbox{ID}_{1}$的谓词可约片段和非谓词片段之间划定了一条边界。

2018-02-20math.LO

弱决定性系统与算术拟归纳定义

Weak systems of determinacy and arithmetical quasi-inductive definitions

为了证明Sigma^0_3决定性介于Pi^1_3-CA_0（甚至是Pi^1_3-光面可定义参数的Pi^1_2-CA_0（光面））和Delta^1_3-CA_0 + AQI之间，我们在L-层次中找到了各种Sigma^0_3-博弈的获胜策略。(Here“AQI”是二阶数论中的陈述，即任何输入上的每个算术准归纳定义都是稳定的）。

2009-05-26math.LO

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

算术归纳定义的循环证明

Cyclic proofs for arithmetical inductive definitions

该研究针对算术归纳定义的循环证明理论，通过元数学论证结合二阶算术中递归序数理论的形式化，证明了循环系统与归纳系统能力等价，解决了闭包序数超出元理论证明论序数的难题。

2023-06-14math.LO

有限非确定归纳定义的等价性

Equivalents of the finitary non-deterministic inductive definitions

我们给出了等价于van den Berg（2013）的非确定性归纳定义（NID）原理的一些片段的陈述，该原理在构造性集合论CZF的弱子系统中工作。我们表明，在建设性的拓扑结构，最初证明了使用NID的几个语句是等价的初等和有限NID。我们还表明，有限NID是等价于它的二进制片段和初等NID是等价于NID的双闭子集的概念的基础上的一个变种。我们的结果表明，证明这些陈述的建设性拓扑需要真正的扩展CZF的基本或有限NID。

2019-06-22math.LO

构造系统的证明论：归纳类型与单价性

Proof Theory of Constructive Systems: Inductive Types and Univalence

在费弗曼的工作中，显式数学和广义归纳定义理论起着核心作用。本文的一个目的是描述与马丁-洛夫类型理论和建设性Zermelo-Fraenkel集合论的连接。证明论有助于更深入地理解构造性数学的不同框架之间的关系。一些减少是已知的，只有通过序理论的特征。本文还讨论了Voevodsky的univalence公理的强度。另一个目标是在直觉显式数学的框架内研究广义归纳定义的直觉理论的强度，这超出了马丁-洛夫类型理论的范围。

2018-01-05math.LO

算术直觉归纳定义与直觉循环证明的等价性

Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic

循环证明系统为我们提供了另一种表示归纳定义和有效证明搜索的方法。2011年，Brotherston和Simpson证明了经典循环证明系统的可证明性与马丁-洛夫归纳定义的经典系统的可证明性之间的等价性。本文研究直觉逻辑中的猜想。本文首先指出，FOSSACS 2017年论文的反模型表明直觉逻辑的猜想一般是错误的。然后证明了直觉逻辑的猜想在算术下成立，即直觉循环证明系统与Martin-Lof归纳定义的直觉系统在都包含Heyting算术HA时的可证性相同。为此，本文还证明了HA证明了归纳法的Podelski-Rybalchenko定理和归纳法的Kleene-Brouwer定理。这些结果立即为同一作者在LICS 2017论文中提出的经典逻辑算术下的猜想提供了另一个证明。

2017-12-10cs.LOmath.LO

带归纳定义的一阶逻辑循环证明中切割消除的失败

The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions

本文证明带归纳定义的一阶逻辑循环证明系统中切割消除不成立，通过构造一个必须依赖切割规则才能证明的相继式实例，证实了该系统无法消除切割的猜想。

2024-02-15cs.LOmath.LO

非单调归纳定义的无穷与循环相继式演算

An Infinitary and a Cyclic Sequent Calculus for Non-Monotone Inductive Definitions

KU Leuven（荷语鲁汶大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）

本文为 FO(ID) 逻辑中的非单调归纳定义形式化了无限下降原理，通过扩展 LKID{\omega} 和 CLKID{\omega} 得到相继式演算 SCFO(ID)-inf 和 SCFO(ID)-cyc，并证明了可靠性、完备性、消割及与 SCFO(ID) 的关系。

2026-09-23cs.LOmath.LO

依赖类型论中归纳与共归纳定义的拓扑解读

A topological reading of inductive and coinductive definitions in Dependent Type Theory

本文在依赖类型论中用共归纳生成的正性关系刻画共归纳谓词，并联系良基树的形式覆盖拓扑解释，全部证明已在 Agda 中形式化。

2024-04-04cs.LOmath.LO

Frege系统的有界算法AID

Bounded arithmetic AID for Frege system

本文介绍一个有界算术系统AID（Alogtime Inductive Definitions）. AID的主要特征是允许一种形式的归纳定义，这是从Buss对Frege系统F的命题一致性证明中提取出来的。我们证明了AID证明了F的可靠性，反之，AID中的任何一个B^b_0-定理都会产生布尔语句，而F具有多重证明。进一步，我们定义了AID + Δ b^_0 - CA与P. Clote方程系统ALV的量化理论QALV之间的Δ b_1-忠实解释.因此ALV也证明了F.

1998-09-30math.LO

三次Agda中的三个等价序数记号系统

Three Equivalent Ordinal Notation Systems in Cubical Agda

我们提出了三个序数记号系统表示序数低于$\varepsilon_0$在类型理论，使用最近的类型理论的创新，如互感归纳的定义和更高的归纳类型。我们展示了如何序数算术可以开发这些系统，以及他们如何承认一个超穷归纳法原则。我们证明了所有三个符号系统是等价的，这样我们就可以使用单价原理在它们之间传输结果。我们所有的建筑都在立方体的阿格达中实现。

2020-01-02math.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

在具有有限极限的$(\infty,1)$-范畴中的高阶归纳类型

Higher inductive types in $(\infty,1)$-categories

本文在具有有限极限的$(\infty,1)$-范畴中定义高阶归纳类型，证明相关范畴有限可展示且初始对象存在，并证明初始对象的全局截面函子保持高阶归纳类型。

2024-10-23cs.LOmath.CTmath.LO

关于Tarski的不动点定理

On Tarski's fixed point theorem

提出并研究了完全格上抽象归纳定义的概念。作为应用，我们得到了Tarski的不动点定理的一个构造性和预言性的形式.

2014-07-18math.LO

贝叶斯算子对布尔代数的扩充：在确定性贝叶斯逻辑定义中的应用

Extension of Boolean algebra by a Bayesian operator; application to the definition of a Deterministic Bayesian Logic

这项工作有助于领域的布尔代数和贝叶斯概率，提出了一个代数扩张的布尔代数，实现了一个操作的贝叶斯条件推理，并在此操作下关闭。从Lewis的工作（Lewis' triviality）开始，人们就知道在事件空间中构造这样的条件算子是不可能的。然而，这项工作提出了一个答案，补充刘易斯的平凡，建设的条件运营商以外的空间的事件，从而导致一个代数扩张。特别地，证明了定义在布尔代数上的任何概率都可以按照条件概率的乘法定义，扩张到它的代数扩张上.本文最后在此代数扩张的基础上引入了一个新的二值逻辑，并得到了它的基本性质。

2011-12-15cs.AIcs.LOmath.LO

多重代数与非确定语义在次协调逻辑中的应用

Multialgebras and Non-Deterministic Semantics applied to Paraconsistent Logics

本文的工作主要分为两个方面：在多重代数理论中，我们主要关注自由生成对象在其范畴中的新定义，以及这个范畴如何等价于另一个以偏序代数为对象的范畴;然后，我们使用非确定性语义，特别是那些我们命名为限制N矩阵，关于次协调逻辑和处理不相容性的自然概念的新表示的一些系统，它概括了不一致性。

2022-06-21math.LO

通过限制归纳谓词的元数来恢复循环证明系统中消切性质的研究

A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates

本文研究循环证明系统中消切性质失效的原因，证明即使将语言限制为一元归纳谓词和一元函数，消切性质在简单循环证明系统中仍不成立，改进了先前需三元谓词的反例。

2025-03-05cs.LOmath.LO