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.
- Linear logic
- Set theory
ASJC Scopus subject areas
- History and Philosophy of Science