TY - JOUR
T1 - Truncation and Semi-Decidability Notions in Applicative Theories
JF - The Journal of Symbolic Logic
Y1 - 2018
A1 - Gerhard Jäger
A1 - Timtej Rosebrock
A1 - Kentaro Sato
AB - BON+ is an applicative theory and closely related to the first order parts of the standard systems of explicit mathematics. As such it is also a natural framework for abstract computations. In this article we analyze this aspect of BON+ more closely. First a point is made for introducing a new operation τN , called truncation, to obtain a natural formalization of partial recursive functions in our applicative framework. Then we introduce the operational versions of a series of notions that are all equivalent to semi- decidability in ordinary recursion theory on the natural numbers, and study their mutual relationships over BON+ with τN .
VL - 83
UR - http://www.iam.unibe.ch/ltgpub/2016/jarosa16.pdf
IS - 03
ER -
TY - JOUR
T1 - A new model construction by making a detour via intuitionistic theories I: Operational set theory without choice is $\Pi$1-equivalent to KP
JF - Annals of pure and applied logic
Y1 - 2015
A1 - Kentaro Sato
A1 - Rico Zumbrunnen
AB - We introduce a version of operational set theory, OST?, without a choice operation, which has a machinery for {$Δ$}0{$Δ$}0 separation based on truth functions and the separation operator, and a new kind of applicative set theory, so-called weak explicit set theory WEST, based on Gödel operations. We show that both the theories and Kripke?Platek set theory KPKP with infinity are pairwise {$\Pi$}1{$\Pi$}1 equivalent. We also show analogous assertions for subtheories with ?-induction restricted in various ways and for supertheories extended by powerset, beta, limit and Mahlo operations. Whereas the upper bound is given by a refinement of inductive definition in KPKP, the lower bound is by a combination, in a specific way, of realisability, (intuitionistic) forcing and negative interpretations. Thus, despite interpretability between classical theories, we make ?a detour via intuitionistic theories?. The combined interpretation, seen as a model construction in the sense of Visser's miniature model theory, is a new way of construction for classical theories and could be said the third kind of model construction ever used which is non-trivial on the logical connective level, after generic extension à la Cohen and Krivine's classical realisability model.
PB - Elsevier
VL - 166
UR - http://www.iam.unibe.ch/ltgpub/2014/sz14.pdf
ER -
TY - JOUR
T1 - A new model construction by making a detour via intuitionistic theories II: Interpretability lower bound of Feferman's explicit mathematics T0
JF - Annals of pure and applied logic
Y1 - 2015
A1 - Kentaro Sato
AB - We partially solve a long-standing problem in the proof theory of explicit mathematics or the proof theory in general. Namely, we give a lower bound of Feferman?s system T0 of explicit mathematics (but only when formulated on classical logic) with a concrete interpretat ion of the subsystem {$Σ$}12-AC+ (BI) of second order arithmetic inside T0. Whereas a lower bound proof in the sense of proof-theoretic reducibility or of ordinalanalysis was already given in 80s, the lower bound in the sense of interpretability we give here is new. We apply the new interpretation method developed by the author and Zumbrunnen (2015), which can be seen as the third kind of model construction method for classical theories, after Cohen?s forcing and Krivine?s classical realizability. It gives us an interpretation between classical theories, by composing interpretations between intuitionistic theories.
PB - Elsevier
VL - 166
UR - http://www.iam.unibe.ch/ltgpub/2015/sat15b.pdf
ER -
TY - JOUR
T1 - Full and hat inductive definitions are equivalent in NBG
JF - Archive for Mathematical Logic
Y1 - 2015
A1 - Kentaro Sato
AB - A new research project has, quite recently, been launched to clarify how different, from systems in second order number theory extending ACA 0, those in second order set theory extending NBG (as well as those in n + 3-th order number theory extending the so-called Bernays?Gödel expansion of full n + 2-order number theory etc.) are. In this article, we establish the equivalence between {$Δ$}10{$\backslash$}bf-LFP and {$Δ$}10{$\backslash$}bf-FP, which assert the existence of a least and of a (not necessarily least) fixed point, respectively, for positive elementary operators (or between {$Δ$}n+20{$\backslash$}bf-LFP and {$Δ$}n+20{$\backslash$}bf-FP). Our proof also shows the equivalence between ID 1 and {\^{ }}ID1, both of which are defined in the standard way but with the starting theory PA replaced by ZFC (or full n + 2-th order number theory with global well-ordering).
PB - Springer
VL - 54
UR - http://www.iam.unibe.ch/ltgpub/2015/sat15a.pdf
ER -
TY - JOUR
T1 - Forcing for Hat Inductive Definitions in Arithmetic – One of the Simplest Applications of Forcing –
JF - Mathematical Logic Quarterly
Y1 - 2014
A1 - Kentaro Sato
AB - By forcing, we give a direct interpretation of $\widehat{\mathsf{ID}}_\omega$ into Avigad's $\mathsf{FP}$. To the best of the author's knowledge, this is one of the simplest applications of forcing to ``real problems''.
VL - 60
UR - http://www.iam.unibe.ch/ltgpub/2014/sat14.pdf
ER -
TY - JOUR
T1 - From hierarchies to well-foundedness
JF - Archive for Mathematical Logic
Y1 - 2014
A1 - Dandolo Flumini
A1 - Kentaro Sato
PB - Springer Berlin Heidelberg
VL - 53
UR - http://www.iam.unibe.ch/ltgpub/2014/fs14.pdf
ER -
TY - JOUR
T1 - Relative predicativity and dependent recursion in second-order set theory and higher-order theories
JF - The Journal of Symbolic Logic
Y1 - 2014
A1 - Kentaro Sato
VL - 79
UR - http://www.iam.unibe.ch/ltgpub/2012/sat12.pdf
ER -