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

In this paper we address the decision problem for a two-sorted fragment of set theory with restricted quantification which extends the language studied in [4] with pair-related quantifiers and constructs. We also show that the decision problem for our language has a nondeterministic exponential-time complexity. However, in the restricted case of formulae whose quantifier prefixes have length bounded by a constant, the decision problem becomes NP-complete. In spite of such restriction, several useful set-theoretic constructs, mostly related to maps, are still expressible. We also argue that our restricted language has applications to knowledge representation, with particular reference to metamodeling issues. Finally, we compare our proposed language with two similar languages in terms of their expressivity and present some undecidable extensions of it, involving any of the domain, range, image, and map composition operators.