Herbrand-satisfiability of a Quantified Set-theoretic Fragment *

Abstract

In the last decades, several fragments of set theory have been studied in the context of Computable Set Theory. In general, the semantics of set-theoretic languages differs from the canonical first-order semantics in that the interpretation domain of set-theoretic terms is fixed to a given universe of sets. Because of this, theoretical results and various machinery developed in the context of first-order logic could be not easily applicable in the set-theoretic realm. Recently, the decidability of quantified fragments of set theory which allow one to explicitly handle ordered pairs has been studied, in view of applications in the field of knowledge representation. Among other results, a NEXPTIME decision procedure for satisfiability of formulae in one of these fragments, ${\forall }_0^{\pi }$ , has been devised. In this paper we exploit the main features of such a decision procedure to reduce the satisfiability problem for the fragment ${\forall }_0^{\pi }$ to the problem of Herbrand satisfiability for a first-order language extending it. In addition, it turns out that such a reduction maps formulae of the Disjunctive Datalog subset of ${\forall }_0^{\pi }$ into Disjunctive Datalog formulae.