Extending constructive operational set theory by impredicative principles

被引：4

作者：

Cantini, Andrea ^{[1
]}

机构：

[1] Univ Florence, Dipartimento Filosofia, I-50139 Florence, Italy

来源：

MATHEMATICAL LOGIC QUARTERLY | 2011年 / 57卷 / 03期

关键词：

Set; operation; partial combinatory logic; uniform comprehension; mu-operator; unbounded set quantifier; INDUCTIVE DEFINITIONS; STRENGTH;

D O I：

10.1002/malq.201010009

中图分类号：

O1 [数学];

学科分类号：

0701 ; 070101 ;

摘要：

We study constructive set theories, which deal with (partial) operations applying both to sets and operations themselves. Our starting point is a fully explicit, finitely axiomatized system ESTE of constructive sets and operations, which was shown in [10] to be as strong as PA. In this paper we consider extensions with operations, which internally represent description operators, unbounded set quantifiers and local fixed point operators. We investigate the proof theoretic strength of the resulting systems, which turn out to be (except for the description operator) impredicative (being comparable with full second-order arithmetic and the second-order mu-calculus over arithmetic). (C) 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim

引用

页码：299 / 322

页数：24

共 50 条

[1] Constructive set theory and Brouwerian principles
Rathjen, M
[J]. JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2005, 11 (12) : 2008 - 2033
[2] Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe
Tupailo, S
[J]. ANNALS OF PURE AND APPLIED LOGIC, 2003, 120 (1-3) : 165 - 196
[3] AXIOMS OF CHOICE IN IMPREDICATIVE SET-THEORY
MAREK, W
ZBIERSKI, P
[J]. BULLETIN DE L ACADEMIE POLONAISE DES SCIENCES-SERIE DES SCIENCES MATHEMATIQUES ASTRONOMIQUES ET PHYSIQUES, 1972, 20 (04): : 255 - &
[4] CONSTRUCTIVE SET-THEORY
MYHILL, J
[J]. JOURNAL OF SYMBOLIC LOGIC, 1975, 40 (03) : 347 - 382
[5] Choice principles in constructive and classical set theories
Rathjen, Michael
[J]. LOGIC COLLOQUIUM '02, 2006, 27 : 299 - 326
[6] Inaccessibility in constructive set theory and type theory
Rathjen, M
Griffor, ER
Palmgren, E
[J]. ANNALS OF PURE AND APPLIED LOGIC, 1998, 94 (1-3) : 181 - 200
[7] THE NON-FINITIZABILITY OF IMPREDICATIVE PRINCIPLES
WANG, H
[J]. BULLETIN OF THE AMERICAN MATHEMATICAL SOCIETY, 1950, 56 (05) : 465 - 465
[8] Rudimentary and arithmetical constructive set theory
Aczel, Peter
[J]. ANNALS OF PURE AND APPLIED LOGIC, 2013, 164 (04) : 396 - 415
[9] The natural numbers in constructive set theory
Rathjen, Michael
[J]. MATHEMATICAL LOGIC QUARTERLY, 2008, 54 (01) : 83 - 97
[10] Constructive toposes with countable sums as models of constructive set theory
Simpson, Alex
Streicher, Thomas
[J]. ANNALS OF PURE AND APPLIED LOGIC, 2012, 163 (10) : 1419 - 1436

← 1 2 3 4 5 →