Two simple models for linear set theory
Masaru Shirahata · 1995
In this paper, we give two fairly simple models of set theory with the unrestricted comprehension based on linear logic. The first model is the extension of the idea of Boolean valued models to linear logic. The second model interprets the occurrences of terms and formulas, allowing the interpretations of different occurrences of the same term to be different sets. The soundness of the latter is guaranteed due to the cut-elimination theorem and the absence of contraction. 1 Introduction In this paper, we give two fairly simple models of set theory with the unrestriected comprehension based on linear logic (for the proof-theoretic study, see [3, 4, 5, 6, 7, 8, 9]) The first model is the extension of the idea of Boolean-valued models to linear logic. The second model interprets the occurrences of terms and formulas, allowing the different interpretations for the two occurrences of the same term. We show the completeness for the first model, and only the soundness for the second. Komori ...