A linear conservative extension of zermelo-fraenkel set theory

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.