A new model construction by making a detour via intuitionistic theories II: Interpretability lower bound of Feferman's explicit mathematics T0


Autoria(s): Sato, Kentaro
Data(s)

2015

Resumo

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.

Formato

application/pdf

application/pdf

Identificador

http://boris.unibe.ch/68827/1/sat15b.pdf

http://boris.unibe.ch/68827/8/1-s2.0-S0168007215000342-main.pdf

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(7-8), pp. 800-835. Elsevier 10.1016/j.apal.2015.04.002 <http://dx.doi.org/10.1016/j.apal.2015.04.002>

doi:10.7892/boris.68827

info:doi:10.1016/j.apal.2015.04.002

urn:issn:0168-0072

Idioma(s)

eng

Publicador

Elsevier

Relação

http://boris.unibe.ch/68827/

Direitos

info:eu-repo/semantics/openAccess

info:eu-repo/semantics/restrictedAccess

Fonte

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(7-8), pp. 800-835. Elsevier 10.1016/j.apal.2015.04.002 <http://dx.doi.org/10.1016/j.apal.2015.04.002>

Palavras-Chave #000 Computer science, knowledge & systems #510 Mathematics
Tipo

info:eu-repo/semantics/article

info:eu-repo/semantics/publishedVersion

PeerReviewed