Premium
Extending constructive operational set theory by impredicative principles
Author(s) -
Cantini Andrea
Publication year - 2011
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.201010009
Subject(s) - constructive , mathematics , operator (biology) , set (abstract data type) , constructive proof , calculus (dental) , set theory , algebra over a field , point (geometry) , order (exchange) , discrete mathematics , computer science , pure mathematics , process (computing) , programming language , medicine , biochemistry , chemistry , geometry , dentistry , repressor , finance , transcription factor , economics , gene
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 μ–calculus over arithmetic). © 2011 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim