A linear conservative extension of zermelo-fraenkel set theory

Research output: Contribution to journalArticle

3 Citations (Scopus)


In 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 formulais 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.

Original languageEnglish
Pages (from-to)361-392
Number of pages32
JournalStudia Logica
Issue number3
Publication statusPublished - 1996
Externally publishedYes



  • Linear logic
  • Set theory

ASJC Scopus subject areas

  • Logic

Cite this