arXiv subjects

Toshiyasu Arai

Publications and source records attributed to Toshiyasu Arai.

At least 37 records · Page 2Linked to original sources

arXiv2018

Proof-theoretic strengths of weak theories for positive inductive definitions

In this paper the lightface $Π^{1}_{1}$-Comprehension axiom is shown to be proof-theoretically strong even over $\mbox{RCA}_{0}^{*}$, and we calibrate the proof-theoretic ordinals of weak fragments of the theory $\mbox{ID}_{1}$ of positive inductive definitions over natural numbers. Conjunctions of negative and positive formulas in the transfinite induction axiom of $\mbox{ID}_{1}$ are shown to be weak, and disjunctions are strong. Thus we draw a boundary line between predicatively reducible and impredicative fragments of $\mbox{ID}_{1}$.

math.LO↗

arXiv2018

Hydras for $ω_{1}$

In this paper we introduce a hydra battle. Each hydra will eventually die out, but the fact is not provable in a set theory with urelements of natural numbers and the assumption that `there exists an uncountable regular ordinal'.

math.LO↗

arXiv2018

Cut-elimination for $ω_{1}$

In this paper we calibrate the strength of the soundness of a Kripke-Platek set theory with the axioms of Infinity and Π_{1}-Collection with the assumption that`there exists an uncountable regular ordinal' in terms of the existence of ordinals.

math.LO↗

arXiv2017

Derivatives of normal functions and omega-models

In this note the well-ordering principle for the derivative of normal functions on ordinals is shown to be equivalent to the existence of arbitrarily large countable coded omega-models of the well-ordering principle for the function.

math.LO↗

arXiv2017

Cut-eliminability in second order logic calculi

In this paper we propose a semantics in which the truth value of a formula is a pair of elements in a complete Boolean algebra. Through the semantics we can unify largely two proofs of cut-eliminability (Hauptsatz) in classical second order logic calculus, one is due to Takahashi-Prawitz and the other by Maehara.

math.LO↗

arXiv2017

Proof search in multi-succedent sequent calculi for intuitionistic logic under the Schuette's schema

Following G. Mints(Kluwer 2000 and draft 2013), we present terminating and bicomplete proof searches in multi-succedent sequent calculi for intuitionistic propositional logic, fragments of intuitionistic predicate logic and full intuitionistic predicate logic in the spirit of Schuette's schema.

math.LO↗

arXiv2016

Cut-elimination for SBL

In this paper we give a terminating cut-elimination procedure for a logic calculus SBL. SBL corresponds to the second order arithmetic Pi^{1}_{2}-Separation and Bar Induction.

math.LO↗

arXiv2015

$omega_{1}$ under $Pi_{1}$-Collection

We describe a proof-theoretic bound on $Sigma_{2}$-definable countable ordinals in Kripke-Platek set theory with $Pi_{1}$-Collection and the existence of $omega_{1}$.

math.LO↗

arXiv2014

Predicatively computable functions on sets

Inspired from a joint work by A. Beckmann, S. Buss and S. Friedman, we propose a class of set-theoretic functions, predicatively computable functions. Each function in this class is polynomial time computable when we restrict to finite binary strings.

math.LO↗

arXiv2014

Lifting proof theory to the countable ordinals II: second-order indescribable cardinals

We show that the existence of a Pi^{1}_{N}-indescribable cardinal over the Zermelo-Fraenkel's set theory ZF is proof-theoretically reducible to iterations of Mostowski collapsings and lower Mahlo operations. Furthermore we describe a proof-theoretic bound on definable countable ordinals whose existence is provable from the existence of second order indescribable cardinals over ZF.

math.LO↗

arXiv2013

A polynomial time complete disjunction property in intuitionistic propositional logic

We extend the polynomial time algorithms due to Buss and Mints(APAL 1999) and Ferrari, Fiorentini and Fiorino(LPAR 2002) to yield a polynomial time complete disjunction property in intuitionistic propositional logic.

math.LO↗

arXiv2013

Lifting up the proof theory to the countables : Zermelo-Fraenkel set theory

We describe the countable ordinals in terms of iterations of Mostowski collapsings. This gives a proof-theoretic bound of definable countable ordinals in the Zermelo-Fraenkel's set theory ZF.

math.LO↗

arXiv2013

Conservations of first-order reflections

The set theory KP$Π_{N+1}$ for $Π_{N+1}$-reflecting universes is shown to be $Π_{N+1}$-conservative over iterations of $Π_{N}$-recursively Mahlo operations for each $N\geq 2$.

math.LO↗

arXiv2013

Proof theory of weak compactness

We show that the existence of a weakly compact cardinal over the Zermelo-Fraenkel's set theory is proof-theoretically reducible to iterations of Mostowski collapsings and Mahlo operations.

math.LO↗

arXiv2011

Introducing the hardline in proof theory

In this paper we expound some basic ideas of proof theory for theories of ordinals such that there are many stable ordinals below the ordinals.

math.LO↗

arXiv2011

A sneak preview of proof theory of ordinals

This talk is a sneak preview of the project, 'proof theory for theories of ordinals'. Background, aims, survey and furture works on the project are given. Subsystems of second order arithmetic are embedded in recursively large ordinals and then the latter are analysed. We scarcely touch upon proof theoretical matters.

math.LO↗

arXiv2010

Quick cut-elimination for strictly positive cuts

In this paper we show that the intuitionistic theory for finitely many iterations of strictly positive operators is a conservative extension of the Heyting arithmetic. The proof is inspired by the quick cut-elimination due to G. Mints. This technique is also applied to fragments of Heyting arithmetic.

math.LO↗

arXiv2010

Proof theory for theories of ordinals III: $Π_{N}$-reflection

This paper deals with a proof theory for a theory of $Π_{N}$-reflecting ordinals using a system of ordinal diagrams. This is a sequel to the previous one(APAL 129)in which a theory for $Π_{3}$-reflection is analysed proof-theoretically.

math.LO↗