Transfinite iteration functionals and ordinal arithmetic

Fast-collapsing theories

Reinhardt's conjecture, a formalization of the statement that a truthful knowing machine can know its own truthfulness and mechanicalness, was proved by Carlson using sophisticated structural results about the ordinals and transfinite induction just beyond the first epsilon number. We prove a weaker version of the conjecture, by elementary methods and transfinite induction up to a smaller ordinal.

Well-orders in the transfinite Japaridze algebra

This paper studies the transfinite propositional provability logics $\glp_Λ$ and their corresponding algebras. These logics have for each ordinal $ξ< Λ$ a modality $\la α\ra$. We will focus on the closed fragment of $\glp_Λ$ (i.e., where no propositional variables occur) and \emph{worms} therein. Worms are iterated consistency expressions of the form $\la ξ_n\ra \ldots \la ξ_1 \ra \top$. Beklemishev has defined well-orderings $<_ξ$ on worms whose modalities are all at least $ξ$ and presented a calculus to compute the respective order-types. In the current paper we present a generalization of t…

Predicative collapsing principles

We show that arithmetical transfinite recursion is equivalent to a suitable formalization of the following: For every ordinal $α$ there exists an ordinal $β$ such that $1+β\cdot(β+α)$ (ordinal arithmetic) admits an almost order preserving collapse into $β$. Arithmetical comprehension is equivalent to a statement of the same form, with $β\cdotα$ at the place of $β\cdot(β+α)$. We will also characterize the principles that any set is contained in a countable coded $ω$-model of arithmetical transfinite recursion resp. arithmetical comprehension.

Discrete Transfinite Computation

We describe various computational models based initially, but not exclusively, on that of the Turing machine, that are generalized to allow for transfinitely many computational steps. Variants of such machines are considered that have longer tapes than the standard model, or that work on ordinals rather than numbers. We outline the connections between such models and the older theories of recursion in higher types, generalized recursion theory, and recursion on ordinals such as $α$-recursion. We conclude that, in particular, polynomial time computation on $ω$-strings is well modelled by severa…

Euclidean integers, Euclidean ultrafilters, and Euclidean numerosities

We introduce axiomatically the ring $\bf{Z}_κ$ of the Euclidean integers, that can be viewed as the ``integral part" of the field $\mathbb{E}$ of Euclidean numbers of [4], where the transfinite sum of ordinal indexed $κ$-sequences of integers is well defined. In particular any ordinal might be identified with the transfiite sum of its characteristic function, preserving the so called natural operations. The ordered ring $\bf{Z}_κ$ may be obtained as an ultrapower of $\mathbb{Z}$ modulo suitable ultrafilters, thus constituting a \it{ring of nonstandard integers.} Most relevant is the \it{algebr…

Kreisel-Lévy-type theorems for Kripke-Platek and other set theories

We prove that, over Kripke-Platek set theory with infinity (KP), transfinite induction along the ordinal $ε_{Ω+1}$ is equivalent to the schema asserting the soundness of KP, where $Ω$ denotes the supremum of all ordinals in the universe; this is analogous to the result that, over Peano arithmetic (PA), transfinite induction along $ε_0$ is equivalent to the schema asserting the soundness of PA. In the proof we need to code infinitary proofs within KP, and it is done by using partial recursive set functions. This result can be generalised to KP + $Γ$-separation + $Γ$-collection where $Γ$ is any …

序数上的一种高级算术

A higher arithmetic on the ordinals

研究序数上的无限二元运算序列，给出序数标准算术与自然数超运算的共同扩展。

Transfinite Modal Logic: a Semi-quantitative Explanation for Bayesian Reasoning

Bayesian reasoning plays a significant role both in human rationality and in machine learning. In this paper, we introduce transfinite modal logic, which combines modal logic with ordinal arithmetic, in order to formalize Bayesian reasoning semi-quantitatively. Technically, we first investigate some nontrivial properties of ordinal arithmetic, which then enable us to expand normal modal logic's semantics naturally and elegantly onto the novel transfinite modal logic, while still keeping the ordinary definition of Kripke models totally intact. Despite all the transfinite mathematical definition…

Models of transfinite provability logic

For any ordinal Λ, we can define a polymodal logic GLP(Λ), with a modality [ξ] for each ξ<Λ. These represent provability predicates of increasing strength. Although GLP(Λ) has no Kripke models, Ignatiev showed that indeed one can construct a Kripke model of the variable-free fragment with natural number modalities. Later, Icard defined a topological model for the same fragment which is very closely related to Ignatiev's. In this paper we show how to extend these constructions for arbitrary Λ. More generally, for each Θ,Λwe build a Kripke model I(Θ,Λ) and a topological model T(Θ,Λ), and show th…

算术超限递归之上的搜索问题

Searching problems above arithmetical transfinite recursion

本文研究算术超限递归之上介于 ATR₂ 与 C_{ω^ω} 之间的 Weihrauch 问题，证明康托空间单调算子不动点定理不可归约到 ATR₂，并引入 ω-模型反射 ATR₂^rfn 作为一类算术形式问题的上界，同时给出相对化最小不动点定理的线性层级。

Pi^0_1 ordinal analysis beyond first order arithmetic

In this paper we give an overview of an essential part of a Pi^0_1 ordinal analysis of Peano Arithmetic (PA) as presented by Beklemishev. This analysis is mainly performed within the polymodal provability logic GLP. We reflect on ways of extending this analysis beyond PA. A main difficulty in this is to find proper generalizations of the so-called Reduction Property. The Reduction Property relates reflection principles to reflection rules. In this paper we prove a result that simplifies the reflection rules. Moreover, we see that for an ordinal analysis the full Reduction Property is not neede…

Transfinite game values in infinite draughts

Infinite draughts, or checkers, is played just like the finite game, but on an infinite checkerboard extending without bound in all four directions. We prove that every countable ordinal arises as the game value of a position in infinite draughts. Thus, there are positions from which Red has a winning strategy enabling her to win always in finitely many moves, but the length of play can be completely controlled by Black in a manner as though counting down from a given countable ordinal.

算术归纳定义的循环证明

Cyclic proofs for arithmetical inductive definitions

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

The transfinite mean

We define a generalization of the arithmetic mean to bounded transfinite sequences of real numbers. We show that every probability space admits a transfinite sequences of points such that the measure of each measurable subset is equal to the frequency with which the sequence is in this subset. We include an argument suggested by Woodin that the club filter on $ω_1$ does not admit such a sequence of order type $ω_1$.

与$PA$序数分析相对应的带回溯选项的博弈

Games with backtracking options corresponding to the ordinal analysis of $PA$

本文利用源自证明复杂性与有界算术的博弈概念，通过直接见证论证，给出了皮亚诺算术$IΣ_{k}$片段序数分析的一个不依赖$ω$-逻辑切割消去的新证明。

线性逻辑中带有固定点的更广泛系统：证明论与复杂性

Wider systems for linear logic with fixed points: proof theory and complexity

本文提出了一种带有固定点的线性逻辑系统，通过证明论方法分析其复杂性，并证明了该系统在超算术层级的特定级别上的完备性。

Constructing Initial Algebras Using Inflationary Iteration

An old theorem of Adámek constructs initial algebras for sufficiently cocontinuous endofunctors via transfinite iteration over ordinals in classical set theory. We prove a new version that works in constructive logic, using "inflationary" iteration over a notion of size that abstracts from limit ordinals just their transitive, directed and well-founded properties. Borrowing from Taylor's constructive treatment of ordinals, we show that sizes exist with upper bounds for any given signature of indexes. From this it follows that there is a rich class of endofunctors to which the new theorem appli…

The structural complexity of models of arithmetic

We calculate the possible Scott ranks of countable models of Peano arithmetic. We show that no non-standard model can have Scott rank less than $ω$ and that non-standard models of true arithmetic must have Scott rank greater than $ω$. Other than that there are no restrictions. By giving a reduction via $Δ^{\mathrm{in}}_{1}$ bi-interpretability from the class of linear orderings to the canonical structural $ω$-jump of models of an arbitrary completion $T$ of $\mathrm{PA}$ we show that every countable ordinal $α>ω$ is realized as the Scott rank of a model of $T$.

On highly equivalent non-isomorphic countable models of arithmetic and set theory

It is well-known that the first order Peano axioms PA have a continuum of non-isomorphic countable models. The question, how close to being isomorphic such countable models can be, seems to be less investigated. A measure of closeness to isomorphism of countable models is the length of back-and-forth sequences that can be established between them. We show that for every countable ordinal alpha there are countable non-isomorphic models of PA with a back-and-forth sequence of length alpha between them. This implies that the Scott height (or rank) of such models is bigger than $α$. We also prove …

见证算术中的流

Witnessing Flows in Arithmetic

针对证明论序数机制无法精细处理弱算术理论及捕捉强理论中有界定义函数的问题，本文提出改进的序数分析机制以捕捉PA+超限归纳扩展理论中可证全的可行可定义有界函数，并通过游戏归约技术捕捉T²ₖ（或S²ₖ）中具有有界定义的函数。