ArTS Archivio della ricerca di Trieste
ArTS è il sistema di gestione integrata dei dati della ricerca adottato dall' Università degli Studi di Trieste
EnglishThis 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 |
| Autori: | |
| Data di pubblicazione: | 2002 |
| Rivista: | |
| 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. |
| Handle: | http://hdl.handle.net/11368/1696333 |
| Digital Object Identifier (DOI): | http://dx.doi.org/10.1006/inco.2001.3096 |
| URL: | http://www.sciencedirect.com/science/article/pii/S0890540101930962 |
| Appare nelle tipologie: | 1.1 Articolo in Rivista |
