Toshiyasu Arai

J-GLOBAL         Last updated: Mar 29, 2017 at 19:17
Toshiyasu Arai
Chiba U.
Graduate School of Science
Job title
Doctor of Science

Academic & Professional Experience

助手, 名古屋大学理学部数学科

Association Memberships


Published Papers

Intuitionistic fixed point theories over set theories
Toshiyasu Arai
Archives Mathematical Logic   54 531-553   Jul 2015   [Refereed]
Toshiyasu Arai
Archives for Mathematical Logic   54 471-485   May 2015   [Refereed]
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 stri...
Toshiyasu Arai
Journal of Mathematical Logic      Mar 2013   [Refereed]
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.
Toshiyasu Arai
Journal of Symbolic Logic   79(2) 325-354   Jun 2014   [Refereed]
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.
Toshiyasu Arai
Journal of Symbolic Logic   79(3) 814-825   Sep 2014   [Refereed]
The set theory KPTex for Tex-reflecting universes is shown to
be Tex-conservative over iterations of Tex-recursively Mahlo
operations for each Tex.
Toshiyasu Arai
Annals of the Japan Association for Philosophy of Science   20 29-47   Mar 2012   [Refereed]
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 th...
Toshiyasu Arai
Annals of Pure and Applied Logic   162(10) 807-815   Oct 2011   [Refereed]
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 techni...
Toshiyasu Arai
Archive for Mathematical Logic   50(3-4) 445-458   May 2011   [Refereed]
In this paper we show that the lengths of the approximating processes in
epsilon substitution method are calculable by ordinal recursions in an optimal
Toshiyasu Arai
Archives for Mathematical Logic   50(3-4) 395-409   May 2011   [Refereed]
In this note we will introduce a class of search problems, called nested
Polynomial Local Search (nPLS) problems, and show that definable NP search
problems, i.e., Tex-definable functions in Tex are characterized
in terms of the neste...
Toshiyasu Arai
Annals of Pure and Applied Logic   162 107-143   Dec 2010   [Refereed]
In this paper, we give two proofs of the wellfoundedness of recursive
notation systems for Tex-reflecting ordinals. One is based on
Tex-inductive definitions, and the other is based on distinguished

Books etc

新井 敏康
岩波書店   May 2011   ISBN:4000055364
Asian Logic Conference, 新井 敏康, Brendle J. (Jörg), 桔梗 宏孝, Chong Chi-Tat, Downey R. G. (Rod G.), 冯 琦, 小野 寛晰
World Scientific   2010   ISBN:9789814293013
新井 紀子, 新井 敏康
東京図書   Oct 2009   ISBN:4489020546


Toshiyasu Arai
   Jan 2017
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 ...
Toshiyasu Arai
   Jun 2016
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.
Toshiyasu Arai
   Mar 2016
In this paper the lightface Pi^{1}_{1}-Comprehension axiom is shown to be
proof-theoretically strong even over RCA_{0}^{*}, and we calibrate the
proof-theoretic ordinals of weak fragments of the theory ID_{1} of positive
inductive definitions over...
Toshiyasu Arai
   Aug 2015
In this paper we introduce a hydra game. Each hydra will eventually die out,
but the fact is not provable in Kripke-Platek set theory with Pi_{1}-Collection
and the assumption that `there exists an uncountable regular ordinal'.
Toshiyasu Arai
   Jun 2015
In this note we give a simplified ordinal analysis of first-order reflection.
An ordinal notation system Tex is introduced based on psi-functions, and a
wellfoundedness proof of it is done in terms of distinguished classes. Provable
Axiomatizing some small classes of set functions
Toshiyasu Arai
arXiv 1503.07982      Mar 2015
Toshiyasu Arai
   Sep 2014
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
Toshiyasu Arai
   Dec 2013
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.
Toshiyasu Arai
   Dec 2013
Following G. Mints(Kluwer 200 and draft 2013), we present a complete proof
search in multi-sequent calculi for intuitionistic propositional and pure
predicate logic in spirit of Schütte's schema(JSL 1960).
Toshiyasu Arai
   Apr 2011
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.
ゲーデルの無矛盾性証明 (総特集 ゲーデル) -- (数理論理学)
現代思想   35(3) 82-93   2007
Toshiyasu Arai, Naohi Eguchi
   Jul 2006
Bellantoni and Cook have given a function-algebra characterization of the
polynomial-time computable functions via an unbounded recursion scheme which is
called safe recursion. Inspired by their work, we characterize the
exponential-time computabl...
竹内の基本予想とは何か、何であるべきか : 50年に (証明論と計算論)
新井 敏康
数理解析研究所講究録   1442 1-7   Jul 2005
Toshiyasu Arai
   Sep 1998
In this paper we introduce a system AID (Alogtime Inductive Definitions) of
bounded arithmetic. The main feature of AID is to allow a form of inductive
definitions, which was extracted from Buss' propositional consistency proof of
Frege systems F....
From the Attic
数理解析研究所講究録   976 97-124   Feb 1997
Introducing the Hardline in Proof Theory
数理解析研究所講究録   976 135-145   Feb 1997
ニ階算術の諸公理AC, DC, CA, BIの関係 : Cut-Eliminationの初等的応用として(順序数の基本列と組合せ的原理の関係)
数理解析研究所講究録   771 1-76   Dec 1991
Cut-elimination for SBL
数理解析研究所講究録   669 16-43   Aug 1988
A Subsystem of Classical Analysis proper to Takeuti's Reduction Method for Tex-Analysis(LOGIC AND THE FOUNDATIONS OF MATHEMATICS)
数理解析研究所講究録   516 92-110   Mar 1984
竹内の基本予想とは何か, 何であるべきか-50年に

Conference Activities & Talks

Search problems in bounded arithmetics [Invited]
T. Arai
A Proof Theory Workshop   Mar 2010   
In germ [Invited]
T. Arai
Leeds Symposium on Proof Theory and Constructivism   Jul 2009   
Provably Tex and weakly descending chains of ordinals, [Invited]
T. Arai
Eleventh Asian Logic Conference   Jun 2009   
Proofs and sets [Invited]
T. Arai
International Workshop on Constructivism, Logic and Mathematics   2008   
Iterating the recursively Mahlo operations [Invited]
T. Arai
Logic Methodology, Philosophy of Science   2007   
無矛盾性証明について [Invited]
新井 敏康
科学基礎論学会秋の研究例会   2006   
Resolving the reflecting universes [Invited]
T. Arai
Berkeley Logic Colloquium   2006   
An expository survey on epsilon substitution method [Invited]
T. Arai
Asian Mathematical Congress   2005   
Epsilon substitution method for inductive definitions, [Invited]
T. Arai
ASL Annual meeting   2005   
Hilbertの第2問題に関する証明論の展開, [Invited]
新井 敏康
日本数学会総合講演   Sep 2004