Searcharxiv⌕ Search

arXiv subjects

Toshiyasu Arai

Publications and source records attributed to Toshiyasu Arai.

At least 19 recordsLinked to original sources
arXiv2023

Well-foundedness proof for $Π^{1}_{1}$-reflection

In the lecture notes it is shown that an ordinal $ψ_Ω(\varepsilon_{\mathbb{S}^{+}+1})$ is an upper bound for the proof-theoretic ordinal of a set theory ${\sf KP}ω+(M\prec_{Σ_{1}}V)$. In this note we show that ${\sf KP}ω+(M\prec_{Σ_{1}}V)$ proves the well-foundedness up to $ψ_Ω(ω_{n}(\mathbb{S}^{+}+1))$ for each $n$.

math.LO↗
arXiv2023

Lectures on Ordinal Analysis

This is a lecture notes for a mini-course in Department of Mathematics, Ghent University, 14 Mar.-25 Mar. 2023.

math.LO↗
arXiv2023

Provably well-founded strict partial orders

In this note we show through infinitary derivations that each provably well-founded strict partial order in ${\rm ACA}_{0}$ admits an embedding to an ordinal$<\varepsilon_{0}$.

math.LO↗
arXiv2022

Wellfoundedness proof with the maximal distinguished set

In arXiv:2208.12944 it is shown that an ordinal $\sup_{N<ω}ψ_{Ω_{1}}(\varepsilon_{Ω_{\mathbb{S}+N}+1})$ is an upper bound for the proof-theoretic ordinal of a set theory ${\sf KP}\ell^{r}+(M\prec_{Σ_{1}}V)$. In this paper we show that a second order arithmetic $Σ^{1-}_{2}\mbox{-CA}+Π^{1}_{1}\mbox{-CA}_{0}$ proves the wellfoundedness up to $ψ_{Ω_{1}}(\varepsilon_{Ω_{\mathbb{S}+N+1}})$ for each $N$. It is easy to interpret $Σ^{1-}_{2}\mbox{-CA}+Π^{1}_{1}\mbox{-CA}_{0}$ in ${\sf KP}\ell^{r}+(M\prec_{Σ_{1}}V)$.

math.LO↗
arXiv2020

Two remarks on proof theory of first-order arithmetic

In this note let us give two remarks on proof-theory of PA. First a derivability relation is introduced to bound witnesses for provable $Σ_{1}$-formulas in PA. Second Paris-Harrington's proof for their independence result is reformulated to show a `consistency' proof of PA based on a combinatorial principle.

math.LO↗
arXiv2019

Mahlo classes for first-order reflections

In this note we axiomatize the $Π_{k+1}$-consequences in the set theory ${\sf KP}Π_{N}$ for $Π_{N}$-reflecting universes in terms of iterations of $Π_{i}$-recursively Mahlo operations for $1\leq k\leq i<N$.

math.LO↗
arXiv2019

A simplified ordinal analysis of first-order reflection

In this note we give a simplified ordinal analysis of first-order reflection. An ordinal notation system $OT$ is introduced based on $ψ$-functions. Provable $Σ_{1}$-sentences on $L_{ω_{1}^{CK}}$ are bounded through cut-elimination on operator controlled derivations.

math.LO↗
arXiv2019

Predicatively unprovable termination of the Ackermannian Goodstein process

The classical Goodstein process gives rise to long but finite sequences of natural numbers whose termination is not provable in Peano arithmetic. In this manuscript we consider a variant based on the Ackermann function. We show that Ackermannian Goodstein sequences eventually terminate, but this fact is not provable using predicative means.

math.LO↗
arXiv2019

Proof-theoretic strengths of the well ordering principles

In this note the proof-theoretic ordinal of the well-ordering principle for the normal functions ${\sf g}$ on ordinals is shown to be equal to the least fixed point of ${\sf g}$. Moreover corrections to the previous paper are made.

math.LO↗
arXiv2018

Grzegorczyk sequence

Natural numbers are represented by Grzegorczyk functions. The representation is implicit in the technique of H. Friedman. An iterated base-shift in the representation with subtracting 1 yields a sequence, Grzegorczyk sequence. It is shown that the termination of the sequence is independent from the first order arithmetic PA. We follow M. Rathjen in the proof of the independence.

math.LO↗
arXiv2018

Hydra games for recursively Mahlo operations

A hydra game is proposed, and the fact that every hydra eventually die out is shown to be equivalent (over a weak arithmetic) to the 1-consistency of set theory KPM for recursively Mahlo universes.

math.LO↗