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

OMODEO, EUGENIO;
2002

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.
http://www.sciencedirect.com/science/article/pii/S0890540101930962
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11368/1696333
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? ND
social impact