This paper introduces formative processes, composed by transitive partitions. Given a family F of sets, a formative process ending in the Venn partition Sigma of F is shown to exist. Sufficient criteria are also singled out for a transitive partition to model (via a function from set variables to unions of sets in the partition) all set-literals modeled by Sigma. On the basis of such criteria a procedure is designed that mimics a given formative process by another where sets have finite rank bounded by C (\Sigma\), with C a specific computable function. As a by-product, one of the core results on decidability in computable set theory is rediscovered, namely the one that regards the satisfiability of unquantified set-theoretic formulae involving Boolean operators, the singleton-former, and the powerset operator. The method described (which is able to exhibit a set-solution when the answer is affirmative) can be extended to solve the satisfiability problem for broader fragments of set theory.
Formative processes with applications to the decision problem in set theory: I. Powerset and singleton operators
CANTONE, Domenico;URSINO P.
2002-01-01
Abstract
This paper introduces formative processes, composed by transitive partitions. Given a family F of sets, a formative process ending in the Venn partition Sigma of F is shown to exist. Sufficient criteria are also singled out for a transitive partition to model (via a function from set variables to unions of sets in the partition) all set-literals modeled by Sigma. On the basis of such criteria a procedure is designed that mimics a given formative process by another where sets have finite rank bounded by C (\Sigma\), with C a specific computable function. As a by-product, one of the core results on decidability in computable set theory is rediscovered, namely the one that regards the satisfiability of unquantified set-theoretic formulae involving Boolean operators, the singleton-former, and the powerset operator. The method described (which is able to exhibit a set-solution when the answer is affirmative) can be extended to solve the satisfiability problem for broader fragments of set theory.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.