Decision procedures for elementary sublanguages of set theory. III: Restricted classes of formulas involving the power set operator and the general set union operator (Q795031)

[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.''