Decision procedures for elementary sublanguages of set theory. III: Restricted classes of formulas involving the power set operator and the general set union operator
type: Item
instance of: scholarly article
title: Decision procedures for elementary sublanguages of set theory. III: Restricted classes of formulas involving the power set operator and the general set union operator
zbMATH Open document ID: 0542.03003
DOI: 10.1016/0196-8858(84)90007-1
author: Michael Breban
author: Alfredo Ferro
published in: Advances in Applied Mathematics
publication date: 1984-01-01T00:00:00Z
review text: [For the preceding parts see Commun. Pure Appl. Math. 33, 599-608 (1980; Zbl 0453.03009) and ibid. 34, 177-195 (1981; Zbl 0465.03003).] From the authors' introduction: ''... we establish several decidability results concerning classes of unquantified set-theoretic formulae in the language consisting of \(=\), \(\in\), \(\subseteq\), \(\cup\), \(\cap\), -, \(\{ \}\) (singleton operation), pow (power set), and Un (general set union). More precisely we show that the class of all unquantified formulas containing no occurrence of Un and at most one occurrence of pow is decidable. We also show that decidability persists if no occurrence of Un and \(\{ \}\) is allowed, and at most two terms \(t_ 1\), \(t_ 2\) appear as arguments of the power set operator. Furthermore decidability of the class of all formulas containing no occurrence of the symbol pow and at most one occurrence of Un is established. Finally we show that the class of formulas containing no occurrence of \(\{ \}\) but in which the operators pow and Un appear only in the context \(x\subseteq pow(x)\), Un(x)\(\subseteq x\) (asserting x is a transitive set) or in the context \(x\not\subseteq pow(x)\), Un(x)\(\not\subseteq x\) (asserting x is not transitive) is decidable.''
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03E99
zbMATH DE Number: 3861117
zbMATH Keywords: decidability results
zbMATH Keywords: classes of unquantified set-theoretic formulae
zbMATH Keywords: power set
zbMATH Keywords: general set union
reviewed by: J. M. Plotkin
MaRDI profile type: Publication
full work available at URL: 0196-8858(84)90007-1
OpenAlex ID: W1977518772
cites work: Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions
cites work: Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
cites work: Q3905254
cites work: Sentences with three quantifiers are decidable in set theory
cites work: Set theory. With an introduction to descriptive set theory. Translation of the original Polish edition. 2nd, completely revised ed
cites work: Q5622181
description: scientific article; zbMATH DE number 3861117