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.
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 ...
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...
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.
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.
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...
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...
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
way.
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.
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...
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'.
In this note we give a simplified ordinal analysis of first-order reflection.
An ordinal notation system is introduced based on psi-functions, and a
wellfoundedness proof of it is done in terms of distinguished classes. Provable
Sigma_{1}-sen...
In this note we axiomatize the classes of rudimentary functions, primitive
recursive functions, safe recursive set functions, and predicatively computable
functions.
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-theoret...
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.
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).
Annals of the Japan Association for Philosophy of Science vol.
20(2012), pp. 29-47 Feb 2011
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...
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.
Annals of Pure and Applied Logic vol.162(2011), pp. 807-815 Oct 2010
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...
This paper deals with a proof theory for a theory of -reflecting
ordinals using a system of ordinal diagrams. This is a sequel to the previous
one(APAL 129)in which a theory for -reflection is analysed
proof-theoretically.
Annals of Pure and Applied Logic vol.162 (2010), pp. 107-143 May 2010
In this paper, we give two proofs of the wellfoundedness of recursive
notation systems for -reflecting ordinals. One is based on -inductive definitions, and the other is based on distinguished
classes.
Archive for Mathematical Logic vol.50(2011), pp. 395-409 May 2010
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., -definable functions in are characterized
in terms of the neste...
Archive for Mathematical Logic vol.50(2011), pp. 445-458 May 2010
In this paper we show that the lengths of the approximating processes in
epsilon substitution method are calculable by ordinal recursions in an optimal
way.
Proofs, Categories and Computations,College Publications, (2010),
pp. 1-14 May 2010
In this paper we show that an intuitionistic theory for fixed points is
conservative over the Heyting arithmetic with respect to a certain class of
formulas. This extends partly the result of mine. The proof is inspired by the
quick cut-eliminatio...
Proceedings of the 11th Asian Logic Conference,World Scientific
(2012), pp. 1-21 May 2010
In this note we show that a set is provably in the fragment of arithmetic iff it is -provably in the class of -r.e. sets in the Ershov hierarchy for an , wh...
Proceedings of the thirteenth International Congress of Logic
Methodology, Philosophy of Science, 2009 May 2010
In this paper we address a problem: How far can we iterate lower recursively
Mahlo operations in higher reflecting universes? Or formally: How much can
lower recursively Mahlo operations be iterated in set theories for higher
reflecting universes?...
Following
faculty.chiba-u.jp
