Proof-theoretic conservations of weak weak intuitionistic constructive set theories

被引：1

作者：

Gordeev, Lev ^{[1
,2
]}

机构：

[1] Univ Tubingen, Tubingen, Germany

[2] Univ Ghent, B-9000 Ghent, Belgium

来源：

ANNALS OF PURE AND APPLIED LOGIC | 2013年 / 164卷 / 12期

关键词：

Classical and intuitionistic mathematical logic; Set theory; Proof theory; Constructive mathematics;

D O I：

10.1016/j.apal.2013.06.012

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

The paper aims to provide precise proof theoretic characterizations of Myhill-Friedman-style "weak" constructive extensional set theories and Aczel-Rathjen analogous constructive set theories both enriched by Mostowski-style collapsing axioms and/or related anti-foundation axioms. The main results include full intuitionistic conservations over the corresponding purely arithmetical formalisms that are well known in the reverse mathematics which strengthens analogous results obtained by the author in the 80s. The present research was inspired by the more recent Sato-style "weak weak" classical extensional set theories whose proof theoretic strengths are shown to strongly exceed the ones of the intuitionistic counterparts in the presence of the collapsing axioms. (C) 2013 Elsevier B.V. All rights reserved.

引用

页码：1274 / 1292

页数：19