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
关键词
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
相关论文
共 22 条
[1]  
Aczel P., 2000, NOTES CONSTRUCTIVE S, V40
[2]  
Aczel P., 1988, CSLI Lecture Notes, V14
[3]  
Aczel P., 1978, LOGIC C, V77, P55
[4]  
[Anonymous], 1985, Foundations of Constructive Mathematics
[5]  
[Anonymous], 1999, Perspectives in Mathematical Logic
[6]  
[Anonymous], LOGIC C
[7]  
BEESON M, 1979, PAC J MATH, V84, P1
[8]  
Feferman, 1975, LECT NOTES MATH, P87, DOI [DOI 10.1007/BFB0062852, 10. 1007/BFb0062852]
[9]  
Finsler P., 1926, MATH Z, V25, P673
[10]   SET THEORETIC FOUNDATIONS FOR CONSTRUCTIVE ANALYSIS [J].
FRIEDMAN, H .
ANNALS OF MATHEMATICS, 1977, 105 (01) :1-28