Ordinal notation systems corresponding to Friedman's linearized well-partial-orders with gap-condition
在这篇文章中,我们研究是否添加免费的θ函数形成一个规范的符号系统的线性版本的弗里德曼的良好的偏序与所谓的间隙条件在一个有限集的标签。令人惊讶的是,我们可以证明这是两个标签的情况,但不是两个以上的标签。为此,我们确定了序数小于$\varepsilon_0$的无加法θ函数的符号系统的序型。我们进一步证明了Friedman序的极大序型可以通过基于特定的二元θ函数的某种序数记号系统得到。
2015-05-06 math.LO
Deducibility and Independence in Beklemishev's Autonomous Provability Calculus
Beklemishev基于可证代数的自治展开为Feferman-Schütte序数$Γ_0$引入了一个序数记号系统。在本文中,我们提出的逻辑$\textbf{BC}$(为微积分)。$\textbf{BC}$的语言将所述序数记号法系统扩展到严格肯定模态语言。因此,与其他可证明性逻辑不同,$\textbf{BC}$基于自包含签名,该自包含签名产生序数记号系统,而不是由先验给定的某个序数索引的模态。证明了该逻辑等价于$\textbf{RC}_{Γ_0}$,即等价于$\textbf{GLP}_{Γ_0}$的严格正片段.然后,我们定义了一个组合语句的基础上$\textbf{BC}$和证明它是独立的理论$\textbf{ATR}_0$的算术超限递归,一个理论的二阶算术远比皮亚诺算术更强大。
2020-08-31 math.LO
A simplified ordinal analysis of first-order reflection
本文给出了一阶反射的一个简化的序分析。基于$ψ$ -函数,介绍了一个序数记号系统$OT$. $L_{ω_{1}^{CK}}$上的可证$Σ_{1}$ -语句通过算子控制导子上的割消有界。
2019-07-12 math.LO
The Aurellion Function: A Recursive Fast-Growing Hierarchy Beyond Knuth Notation
本文提出Aurellion函数,一种基于Knuth上箭头记号的递归快速增长层级,证明其支配Peano算术中所有可证明全函数,并将其定位于证明论序数Γ₀附近,同时探讨超限扩展以连接大数构造与序数分析。
2025-06-05 math.LO
Extending the Veblen Function
本文定义了Veblen序数函数系统的维度扩展,通过多维数组迭代导数实现,并构建了相应的序数记号及转换算法。
2023-12-25 math.LO
Pure patterns of order 2
我们提供相互之间的经典序数记号的基本递归序同构,Skolem脱壳的基础上,和符号从纯粹的基本模式的相似顺序$2$,表明后者的特点证明理论的顺序片段$Π^1_1$ - $\mathrm{CA}_0$的二阶数论,或等价的集合论$\mathrm{KPl}_0$。作为推论,我们证明了Carlson关于$2$阶尊重森林的良拟序性的结果蕴涵了直到$\mathrm{KPl}_0$阶的超穷归纳法.我们希望我们的方法将有助于分析更强大的模式系统。
2017-10-05 math.LO
The Provably Total Set-Recursive Functions of KPl
Institute of Discrete Mathematics and Geometry, TU Wien(TU维也纳离散数学与几何研究所);Department of Philosophy, University of Barcelona(巴塞罗那大学哲学系)
通过相对化序数分析,刻画了KPl及其相关理论的可证全集合递归从ω函数。
2025-10-16 math.LO
Recursive Analogues of Shrewdness and Subtlety, with Applications to Fine Structure
本文分享稳定序数与精明基数的已知结果,并论证Σ₂-非可投射序数可作为与Jensen精细结构相关的精微基数的递归类比。
2024-07-08 math.LO
G_{δσ}-games and generalized computation
我们证明了在Cantor或Baire空间中$G_{δσ}$(也称为$Σ^{0}_{3}$)游戏的获胜策略的存在性与在更高的2型泛函中广义递归函数的存在性之间的等价性。(Such递归与某些超限计算模型相关联)。我们表明,除其他外,在这个意义上的收敛递归的指数集是一个完整的$\Game Σ_{3}^{0}$集:作为释义,这些游戏在这个水平上,是赢得了玩家I,基本上有相同的信息作为“停机问题”,这个概念的递归。此外,在这种博弈中,第一个参与者的策略在这个意义上是递归的。因此,我们建立了单调$\Game Σ^{0}_{3}$ -归纳算子的序数长度,并在可构造的层次结构中找到第一个序数。定理(a)下面的集合是递归同构的。(i)完整的ITTM-半递归的${eJ}$集,$H^{eJ}$ ;(ii)$Σ_{1}$ -$( L_{η_{0}} , \in ) $的理论,其中$η_{0}$是$\Game Σ_{3}^{0}$ -单调归纳的闭包序数;(iii)完整的$\Game Σ_{3}^{0}$整数集。(b)整数的ittm递归${eJ}$集合正是$L_{η_{0}}$的集合。
2015-09-30 math.LO
Well-Orderedness of the Bashicu Matrix System
本文证明了由BashicuHyudora创建的递归序数表示系统——Bashicu矩阵系统具有良序性。
2024-10-11 math.LO
Wellfoundedness proofs by means of non-monotonic inductive definitions II: first order operators
本文给出了$Π_N$ -反射序数的递归记法系统的良基性的两个证明。一种是基于$Π_{N-1}^0$归纳定义,另一种是基于区分类。
2010-05-12 math.LO
On the consistency of $P=NP$ with fragments of ZFC whose own consistency strength can be measured by an ordinal assignment
我们将可满足性问题中的$P<NP$假设表述为$Π^0_2$语句,从中我们可以构造一个部分递归函数$f_{\neg A}$,使得$f_{\neg A}$是全的当且仅当$P < NP$。然后,我们表明,如果$f_{\neg A}$是全的,那么它不是${\cal T}$ -可证明的全(其中${\cal T}$是ZFC的一个片段,充分扩展PA,其一致性是有序的)。因此,$P < NP$的否定,即$P = NP$,与那些${\cal T}$是一致的。
2000-06-10 math.LO
Realizing the totally unordered structure of ordinals
本文提出了用于分析经典集合论可实现性模型中序数的工具,通过定义 reish 算子构建递归名以计算序数,并证明 ε-完全有序集无法完全表示序数,同时提供了保留基数的方法。
2025-04-04 cs.LO math.LO
Compact totally separated types
本文利用拓扑学构造可有限时间穷尽搜索的无限类型(紧致类型),通过两种序数记号系统(Brouwer编码及其推广)衡量其逻辑复杂性,并证明相关性质在构造性设置中的限制,扩展至Martin-Löf类型论并形式化于Agda。
2026-11-13 cs.LO math.GN math.LO
Toward higher-order infinite time Turing machines: simulational $Γ$-machines
Institut Polytechnique de Paris, École Polytechnique(巴黎理工学院,巴黎综合理工学院);CNRS, Université Paris Cité and Sorbonne Université(法国国家科学研究中心,巴黎西岱大学与索邦大学);Université Sorbonne Paris Nord, LIPN, Institut Galilée(北巴黎索邦大学,LIPN,伽利莱研究所)
本文定义了一族满足特定约束的极限规则,构建了具有通用机器且可写序数与时钟序数上确界相匹配的高阶无限时间图灵机模型,并通过反例验证了约束的必要性。
2025-11-04 math.LO
Borel Ranks and Wadge Degrees of Context Free Omega Languages
我们表明,从拓扑的角度来看,考虑Borel和Wadge层次,1-计数器Büchi自动机具有相同的接受能力比图灵机配备一个Büchi接受条件。特别地,对于每一个非空递归序数α,都存在1-计数器Büchi自动机所接受的Sigma^0_α-完全和Pi^0_α-完全的上下文无关omega语言,并且上下文无关omega语言的Borel秩集的上确界是严格大于第一个非递归序数的序数γ ^[1_2]。这个令人惊讶的结果回答了H. Lescow和W. Thomas [无限计算的逻辑规范,在:“并发的十年”,LNCS 803,Springer,1994,第583-621页]。
2007-12-09 cs.GT cs.LO math.LO
Punctually Standard and Nonstandard Models of Natural Numbers
Novosibirsk State University(新西伯利亚国立大学);Innopolis University(因诺波利斯大学);Faculty of Mathematics and Informatics, Sofia University(索非亚大学数学与信息学院);Institute of Computer Science, Polish Academy of Sciences(波兰科学院计算机科学研究所);Faculty of Philosophy, University of Warsaw(华沙大学哲学系)
本文研究了自然数模型中原始递归函数的标准化问题,提出了‘准时标准性的基础’概念,并展示了有限生成结构的准时范畴性。
2026-03-11 cs.CC math.LO
Superintuitionistic predicate logics of linear frames: undecidability with two individual variables
该研究证明线性Kripke框架定义的超直觉谓词逻辑QLC的两变量片段不可判定,且相关序数框架逻辑非递归可枚举,通过改进铺砌问题描述方法和双标记技术实现仅用两变量的证明。
2025-10-02 math.LO
Complexities of Well-Quasi-Ordered Substructural Logics
本文利用序数索引快速增长复杂性类,对具有良拟序的子结构逻辑的可演绎性和可证明性问题进行全面分类,揭示了逻辑设计变化对算法行为的影响。
2025-04-30 cs.CC cs.LO math.LO
Hyperarithmetical Complexity of Infinitary Action Logic with Multiplexing
本文针对带多路复用的无穷动作逻辑$!^m\nabla \mathrm{ACT}_\omega$的可推导性问题,证明其在图灵归约下为$\Delta^0_{\omega^\omega}$-完全,确定其闭包序数为$\omega^\omega$,并给出相关片段的复杂度结果。
2023-12-09 cs.LO math.LO