发表机构
Recognition Physics Institute; Department of Mathematics, Faculty of Science and Mathematics, University of Niš（识别物理研究所; 尼什大学科学与数学学院数学系）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究提出δ-演算，构造无选择数塔，分类ℕ_δ的加法幺半群识别商，明确分类所需非构造性原则，结果在Lean 4中形式化。
AI 中文摘要
令δ表示区分的本原行为，形式上实现为有限记录的单步扩展r ↦ Sr。我们研究归纳生成的δ-轨道及其一阶算术表示ℕ_δ。对应的δ-演算是基于签名{0,S,+,·}的直觉主义一阶证明系统。每个推导附带一个台账，记录排中律、有限全知原则、马尔可夫原则以及对量化公式的归纳的使用情况。最后一项不影响推导是否为强制的。若一个闭公式在强制片段中可推导，则它在标准模型中为真。从δ出发，我们构造一个无选择的数塔δ ⇝ ℕ_δ ↪ ℤ_δ ↪ ℚ_δ。元理论数系统ℕ、ℤ和ℚ各自都有一个显式注入到ℕ_δ中。我们还对加法幺半群(ℕ_δ,+,0)的识别商进行分类。假设排中律成立，则每个识别子要么是单射，要么具有核同余≡_{i,p}，对应唯一的一对i≥0、p≥1。在非单射情形下，商同构于有限单生成幺半群M(i,p)。我们用该台账来衡量此分类的“代价”，确定每种形式需要哪些非构造性原则：若同余可判定且给出一对不同的相关元素，则分类是强制的；若同余可判定且不等于相等，则需要马尔可夫原则；对于任意同余，这种二分法需要排中律。反向蕴含表明，后两种“代价”无法降低。主要结果已在Lean 4中形式化。
英文摘要
Let $δ$ denote the primitive act of distinction, formally realized as the one-step extension $r\mapsto Sr$ of a finite record. We prove that the $δ$-orbit is initial among $δ$-algebras: every $δ$-algebra admits a unique structure-preserving map from the orbit. The map is injective when the successor operation is injective and the base point is not a successor. If the $δ$-algebra also satisfies induction for all predicates, the map is bijective and gives the unique isomorphism with the generated $δ$-orbit. The $δ$-calculus is an intuitionistic first-order proof system over the signature $\{0,S,+,\cdot\}$. Each derivation carries a ledger recording the use of the law of excluded middle, the limited principle of omniscience, Markov's principle, and induction on quantified formulas. Every closed formula derivable in the forced fragment is true in the standard model. Starting from $δ$, we construct the choice-free number tower $δ\leadsto \mathbb{N}_δ\hookrightarrow \mathbb{Z}_δ\hookrightarrow \mathbb{Q}_δ$. The metatheoretic systems $\mathbb{N}$, $\mathbb{Z}$, and $\mathbb{Q}$ each admit an explicit injection into $\mathbb{N}_δ$. Under the law of excluded middle, every recognizer is either injective or has kernel congruence $\equiv_{i,p}$ for a unique pair $i\geq0$, $p\geq1$. In the noninjective case, the quotient is a finite monogenic monoid $M(i,p)$. A decidable congruence together with an explicit pair of distinct related elements implies the classification without additional nonconstructive principles. For a decidable congruence different from equality, Markov's principle is needed. For an arbitrary congruence, the dichotomy requires the law of excluded middle. The reverse implications show that the last two prices are exact. They are distinct from the syntactic ledger of derivations in the $δ$-calculus.
