### Abstract

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 language | English |
---|---|

Pages (from-to) | 361-392 |

Number of pages | 32 |

Journal | Studia Logica |

Volume | 56 |

Issue number | 3 |

Publication status | Published - 1996 |

Externally published | Yes |

### Fingerprint

### Keywords

- Linear logic
- Set theory

### ASJC Scopus subject areas

- Logic

### Cite this

*Studia Logica*,

*56*(3), 361-392.

**A linear conservative extension of zermelo-fraenkel set theory.** / Shirahata, Masaru.

Research output: Contribution to journal › Article

*Studia Logica*, vol. 56, no. 3, pp. 361-392.

}

TY - JOUR

T1 - A linear conservative extension of zermelo-fraenkel set theory

AU - Shirahata, Masaru

PY - 1996

Y1 - 1996

N2 - 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.

AB - 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.

KW - Linear logic

KW - Set theory

UR - http://www.scopus.com/inward/record.url?scp=0003540818&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0003540818&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0003540818

VL - 56

SP - 361

EP - 392

JO - Studia Logica

JF - Studia Logica

SN - 0039-3215

IS - 3

ER -