Sato, Kentaro (2015). A new model construction by making a detour via intuitionistic theories II: Interpretability lower bound of Feferman's explicit mathematics T0. Annals of pure and applied logic, 166(78), pp. 800835. Elsevier 10.1016/j.apal.2015.04.002

Text
sat15b.pdf  Submitted Version Available under License Publisher holds Copyright. Download (436kB)  Preview 

Text
1s2.0S0168007215000342main.pdf  Published Version Restricted to registered users only Available under License Publisher holds Copyright. Download (907kB)  Request a copy 
We partially solve a longstanding 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 Σ12AC+ (BI) of second order arithmetic inside T0. Whereas a lower bound proof in the sense of prooftheoretic 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.
Item Type:  Journal Article (Original Article) 

Division/Institute:  08 Faculty of Science > Institute of Computer Science (INF) > Logic and Theory Group (LTG) 08 Faculty of Science > Institute of Computer Science (INF) 
UniBE Contributor:  Sato, Kentaro 
Subjects:  000 Computer science, knowledge & systems 500 Science > 510 Mathematics 
ISSN:  01680072 
Publisher:  Elsevier 
Language:  English 
Submitter:  Florian Ranzi 
Date Deposited:  21 May 2015 13:14 
Last Modified:  25 May 2015 04:13 
Publisher DOI:  10.1016/j.apal.2015.04.002 
BORIS DOI:  10.7892/boris.68827 
URI:  http://boris.unibe.ch/id/eprint/68827 