Studia Logica 56 (3):361 - 392 (1996)
AbstractIn this paper, we develop the system LZF of set theory with the unrestricted comprehension in full linear logic and show that LZF is a conservative extension of ZF– i.e., the Zermelo-Fraenkel set theory without the axiom of regularity. We formulate LZF as a sequent calculus with abstraction terms and prove the partial cut-elimination theorem for it. The cut-elimination result ensures the subterm property for those formulas which contain only terms corresponding to sets in ZF–. This implies that LZF is a conservative extension of ZF– and therefore the former is consistent relative to the latter.
Similar books and articles
An axiom schema of comprehension of zermelo–fraenkel–skolem set theory.Johannes Heidema - 1990 - History and Philosophy of Logic 11 (1):59-65.
A1 is not a conservative extension of s4 but of S.Michiro Kondo - 1989 - Journal of Philosophical Logic 18 (3):321 - 323.
The origins of zermelo's axiomatization of set theory.Gregory H. Moore - 1978 - Journal of Philosophical Logic 7 (1):307 - 329.
On interpretations of bounded arithmetic and bounded set theory.Richard Pettigrew - 2009 - Notre Dame Journal of Formal Logic 50 (2):141-152.
Added to PP
Historical graph of downloads
Citations of this work
On arithmetic in the Cantor- Łukasiewicz fuzzy set theory.Petr Hájek - 2005 - Archive for Mathematical Logic 44 (6):763-782.
The Trend of Logic and Foundation of Mathematics in Japan in 1991 to 1996.Yuzuru Kakuda, Kanji Namba & Nobuyoshi Motohashi - 1997 - Annals of the Japan Association for Philosophy of Science 9 (2):95-110.
References found in this work
The Semantics and Proof Theory of Linear Logic.Arnon Avron - 1988 - Theoretical Computer Science 57 (2):161-184.
A consistent theory of attributes in a logic without contraction.Richard B. White - 1993 - Studia Logica 52 (1):113 - 142.