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.
|Titolo:||Formative processes with applications to the decision problem in set theory: I. Powerset and singleton operators|
|Data di pubblicazione:||2002|
|Citazione:||Formative processes with applications to the decision problem in set theory: I. Powerset and singleton operators / CANTONE D; OMODEO E.G; URSINO P. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 172:2(2002), pp. 165-201.|
|Appare nelle tipologie:||1.1 Articolo in rivista|