کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4661674 1633451 2015 36 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
A new model construction by making a detour via intuitionistic theories II: Interpretability lower bound of Feferman's explicit mathematics T0T0
ترجمه فارسی عنوان
ساخت مدل جدید با ساختن یک مسیر انحرافی از طریق نظریه های شهودی II: کران پایین تر تعادلی از ریاضیات T0T0 صریح Feferman
کلمات کلیدی
ریاضیات صریح Feferman؛ ساخت یک مسیر انحرافی از طریق نظریه شهودی؛ قابلیت تفسیر؛ بازنمایی درختی مجموعه؛ قابلیت اجرا احاطه ای
موضوعات مرتبط
مهندسی و علوم پایه ریاضیات منطق ریاضی
چکیده انگلیسی

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 T0T0 of explicit mathematics (but only when formulated on classical logic) with a concrete interpretation of the subsystem Σ21-AC+(BI) of second order arithmetic inside T0T0. Whereas a lower bound proof in the sense of proof-theoretic reducibility or of ordinal analysis 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 [37], 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.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 166, Issues 7–8, July–August 2015, Pages 800–835
نویسندگان
,