Complexity assessments for decidable fragments of set theory. II: A taxonomy for ‘small’ languages involving membership

We carry on a long-standing investigation aimed at identifying fragments of set theory that are potentially useful in automated verification with proof-checkers, such as ÆtnaNova, based on the set-theoretic formalism. This note provides a complete taxonomy of the polynomial and the NP-complete fragments consisting of all conjunctions that involve, besides variables intended to range over the von Neumann set-universe, a collection of constructs drawn from the Boolean set operators ∪,∩, and the membership relators ∈ and ∈/. This is done in sight of combining the aforementioned taxonomy with one recently put together for analogous fragments involving, in place of the relators ∈ and ∈/, the Boolean relators ⊆, = and the predicates ‘· = ∅’ and ‘Disj(·, ·)’ (respectively meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’), along with their opposites.