Abstract

In this thesis, we develop four systems of set theory based on linear logic. All of those systems have the principle of unrestricted comprehension but they are shown to be consistent. The consistency proofs are given by establishing the cut-elimination theorems. ;Our first system of linear set theory SMALL is formulated in full linear logic, i.e., with exponentials. However we do not allow exponentials to appear inside of set terms. ;Secondly, we formulate a system of set theory in linear logic with infinitary additive conjunction and disjunction, instead of exponentials. This system is called AS$\sp\infty.$ ;Thirdly, we present the system of linear set theory LZF which is a conservative extension of Zermelo-Fraenkel set theory without the axiom of regularity or ZF$\sp-.$ The idea is to build up a linear set theory on top of ZF$\sp-$ in a style similar to SMALL. We establish a partial cut-elimination result for LZF, and derive from it that LZF is a conservative extension of ZF$\sp-,$ and therefore consistent relative to ZF$\sp-.$ ;Our last system of linear set theory AZF further extends LZF with weakening and the substitutivity principle, which are not available in LZF. ;In addition, we present the phase-valued model of linear set theory which is an extension of the Boolean-valued model of classical set theory. This only gives a model of linear set theory with the axiom of separation and not with the unrestricted comprehension. ;Finally, we explore possible applications of linear set theory, particularly to the foundations of category theory.