A linear conservative extension of zermelo-fraenkel set theory

Research output: Contribution to journalArticle

3 Citations (Scopus)

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 languageEnglish
Pages (from-to)361-392
Number of pages32
JournalStudia Logica
Volume56
Issue number3
Publication statusPublished - 1996
Externally publishedYes

Fingerprint

Cut-elimination
Set Theory
Sequent Calculus
Linear Logic
Term
Axiom
Regularity
Partial
Imply
Theorem
Conservative Extension
Zermelo
Abstraction

Keywords

  • Linear logic
  • Set theory

ASJC Scopus subject areas

  • Logic

Cite this

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

In: Studia Logica, Vol. 56, No. 3, 1996, p. 361-392.

Research output: Contribution to journalArticle

@article{b36b7ebfd0f044a69546390267a96158,
title = "A linear conservative extension of zermelo-fraenkel set theory",
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.",
keywords = "Linear logic, Set theory",
author = "Masaru Shirahata",
year = "1996",
language = "English",
volume = "56",
pages = "361--392",
journal = "Studia Logica",
issn = "0039-3215",
publisher = "Springer Netherlands",
number = "3",

}

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 -