具有结构归纳的形式数学系统的进一步结果和例子

Further results and examples for formal mathematical systems with structural induction

Matthias Kunik

备注：: 43 pages. arXiv admin note: text overlap with arXiv:2005.04951

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

在前一篇文章“包括结构归纳原理的形式数学系统”中，我们提出了一个形式数学系统的统一理论，包括与形式语法密切相关的递归系统，包括谓词演算以及形式归纳原理。在本文中，我们提出了一些进一步的结果和例子，以说明这个理论是如何工作的。

英文摘要：

In the former article "Formal mathematical systems including a structural induction principle" we have presented a unified theory for formal mathematical systems including recursive systems closely related to formal grammars, including the predicate calculus as well as a formal induction principle. In this paper we present some further results and examples in order to illustrate how this theory works.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

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

继续探索

相关论文

包含结构归纳原理的形式数学系统

Formal Mathematical Systems including a Structural Induction Principle

我们提出了一个统一的理论，正式的数学系统，包括递归系统密切相关的正式文法，包括谓词演算以及正式的归纳原则。我们引入递归系统产生递归的术语列表之间的关系，考虑的基本对象。递归系统由公理和特定的推理规则组成，公理是一种特殊的无量词正角公式。它的扩展到正式的数学系统，导致一个正式的结构归纳的基本递归系统的公理。这种方法提供了一些新的表现定理，而不使用人工和困难的解释技术。在这个框架内，我们还将推导出哥德尔第一和第二不完全性定理的一般类公理化的形式数学系统的版本。

2021-12-20math.LO

康托尔的非等势性定理，归纳式证明

Cantor's Non-Equinumerosity Theorems, Inductively

Harish and Bina Shah School of AI and Computer Science, Plaksha University（普拉克斯哈大学人工智能与计算机科学学院）

该论文面向不同阶段读者，分别用数学归纳法和超限归纳法证明康托尔的相关非等势性定理，需用到选择公理与序数概念，部分证明或为首次提出并与旧结果对比。

2026-08-26math.LO

与$PA$等价的理论的证明图式--论保守性反思原则的益处

Proof Schemata for Theories equivalent to $PA$: on the Benefit of Conservative Reflection Principles

归纳通常形式化为LK演算的规则或公理扩展。虽然这种对微积分的扩展简单而优雅，但证明转换和分析可能相当困难。具有归纳规则的理论，例如皮亚诺算术，没有{ \em Herbrand}定理。在这项工作中，我们扩展了现有的元理论形式主义，所谓的证明图式，递归公式的归纳特别适合于证明分析，皮亚诺算术。这种关系在\PA和另一种证明形式主义之间提供了一个有意义的保守反射原则。证明图式已被证明有一个变种的Herbrand定理的经典逻辑，可以提升到我们的新的形式主义相当于原始的递归算术的子系统。

2018-04-01math.LO

康托空间上的开归纳原理与近似扇定理

The Principle of Open Induction on Cantor space and the Approximate-Fan Theorem

本文在直觉主义逆数学框架中研究康托空间上的开归纳原理与近似扇定理，证明前者蕴含扇定理但不可逆推，并给出两者的若干等价命题。

2023-11-02math.LO

Peano算术中$\mathbb{N}$的归纳原理之间的关系

Implications between Induction Principles for $\mathbb{N}$ in Peano Arithmetic

在关于自然数的入门书籍中，一种常见的断言--通常留给读者作为练习--是关于$\mathbb{N}$（正则/普通，完备/强）的某些归纳形式彼此等价，并且等价于良序原则。这意味着，如果P1和P2是这些原则中的两个，那么，在所有其他通常采用的自然数集合的假设下（例如，除了归纳公理以外的佩亚诺公理），P1蕴涵P2，反之亦然。在本文中，我们表明，一个合理的形式化，皮亚诺算术的基础上，这些原则之间的一些所谓的影响，只有当一个额外的，独立的条件是假设，即：每一个非零的自然数是一个继任者。这个条件是正规归纳原理的一个推论，而不是其他归纳原理的推论。因此，有必要回顾归纳原则与$\mathbb{N}$中类似陈述之间的所有目前公认的含义。从一个列表中的9个属性，通常被认为是归纳原则（或等效），我们确定所有有效的和“几乎有效”的影响，它们之间，以及反驳所有无效的影响由反例，其中包括类似于皮亚诺模型的结构，但不一定满足皮亚诺的归纳公理，并有一个顺序关系充分从属于零和后继者。最后，我们将讨论如果我们弱化关于序关系的假设，什么可以被证明，什么不能被证明。本文的目的是阐明需要更加谨慎时，声称之间的等价性归纳原则$\mathbb{N}$。

2021-11-21math.LO

关于Kotlarski定理的一个加强

On a strengthening of Kotlarski's theorem

Kotlarski定理（见H.科特拉斯基有限归纳和满意度类。《数理逻辑季刊》，第32卷，第31-34页，1986年，第531- 544页。）在$WKL_0$中正式化。

2016-12-21math.LO

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

利用性质省略导出MIZAR数学库中证明的隐式假设

Eliciting implicit assumptions of proofs in the MIZAR Mathematical Library by property omission

Center for Artificial Intelligence（人工智能中心）；New University of Lisbon（里斯本新大学）

当使用交互式定理证明器进行形式化证明时，经常会发生关于数学概念的额外背景知识（声明性或过程性）被采用而形式化器没有显式地调用它，以帮助形式化器专注于证明的相关细节。在产生和研究形式化的数学论证的背景下，这种机制显然是有价值的。但我们可能并不总是希望压制背景知识。为了某些目的，尽可能精确地知道在形式证明中隐含地使用了什么背景知识是很重要的。在本文中，我们描述了在MIZAR数学库的正式数学证明上进行的一个实验，以引出一类隐含使用的背景知识：函数和关系的性质（例如，交换性、不对称性等）。

2011-09-03cs.AIcs.LOmath.LO