A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions (Q477206)

In an earlier article [LIPICS -- Leibniz Int. Proc. Inform. 12, 129--143 (2011; Zbl 1247.03013)], \textit{D. Cantone} et al. studied the quantified fragment of set theory \(\forall^{\pi}_{0}\). In this fragment, there are only set variables, and there are terms of the form \([x,y]\) for ordered pairs; the operator \(\bar{\pi}\) computes the collection of non-pair elements of its argument. The predicates \(=\) and \(\in\) can only occur in atoms off the form \(x=y\), \(x\in \bar{\pi}(y)\) and \([x,y]\in z\). The formulas of \(\forall^{\pi}_{0}\) are built from atoms using propositional connectives and bounded quantifications of the form \((\forall x\in \bar{\pi}(y))\) and \((\forall [x,y]\in z)\); nesting of quantifiers is not allowed. Significantly for the article under review, the satisfiability problem for \(\forall^{\pi}_0\) formulas was shown to be decidable in the cited article. In the present paper, the authors consider a fragment \(\forall^{\pi}_{0,2}\) which has a two-sorted language with variables \(\{x, y,\dots\}\) for sets and variables \(\{f,g,\dots\}\) for maps. The atoms are of the form \(x\in y, [x,y]\in f, x=y\) and \(f=g\). The formulas of \(\forall^{\pi}_{0,2}\) are built from atoms using propositional connectives and bounded quantifications of the form \((\forall x\in y), (\exists x\in y), (\forall [x,y]\in f)\) and \((\exists [x,y]\in f)\), where certain nestings are forbidden. The authors show that the satisfiability problem for \(\forall^{\pi}_{0,2}\) can be reduced to the satisfiability problem for \(\forall^{\pi}_{0}\) and is thus decidable. Moreover, they show that it is decidable in non-deterministic exponential time. For the restricted class of formulas \((\forall^{\pi}_{0,2})^{\leq h}\), where \(h\) is a non-negative integer and quantifier prefix length is bounded by \(h\), they show the satisfiability problem is NP-complete. Here are some further results: (1) The authors introduce a description logic \(\mathcal{DL} (\forall^{\pi}_{0,2})\), and they show that the consistency problem for \(\mathcal{DL} (\forall^{\pi}_{0,2})\)-knowledge bases is NP-complete. (2) The language \(\forall^{\pi}_{0}\) is more expressive than that of \(\forall^{\pi}_{0,2}\). (3) Any extension of \(\forall^{\pi}_{0,2}\) in which one can express any of the following: \(x\subseteq \text{dom}(f),\; x\subseteq\text{range}(f),\; h\subseteq f\circ g, \;y\subseteq f[x]\) has an undecidable satisfiability problem.