Transitive Venn diagrams with applications to the decision problem in set theory.
Domenico Aldo Cantone, Eugenio Giovanni Omodeo, Pietro Ursino · 1999
This paper introduces the notions of transitive partition and of transitive Venn diagram of a collection of sets, and gives sufficient conditions in order that two transitive Venn diagrams satisfy a same family of set-theoretic literals. As a by-product, one of the core results on decidability in computable set theory is rediscovered, namely the one that regards the satis ability of unquantified set-theoretic formulae involving Boolean operators, the singleton-former, and the powerset operator. The method described is amenable to extensions able to deal with more general satisfiability decision problems for fragments of set theory.