As part of a project aimed at the implementation of a proof-checker based on the set-theoretic formalism, the decision problem in set theory has been studied very intensively, starting in the late seventies. Several results have been produced in the first decade of research, giving rise to the novel field of computable set theory. At that point, it already was clear that to face the tremendous amount of technicalities involved in the combination of smaller decidable fragments into larger ones, new techniques were in order. Such techniques have recently emerged, by a careful analysis of the formation process of disjoint families of sets. This has led to the characterization of suitable decidable conditions for the satisfiability of set-theoretic formulae belonging to specific collections. In this paper we give an elementary introduction to the formative process technique and discuss some open problems.

Applications of formative processes to the decision problem in set theory

URSINO, PIETRO
2004

Abstract

As part of a project aimed at the implementation of a proof-checker based on the set-theoretic formalism, the decision problem in set theory has been studied very intensively, starting in the late seventies. Several results have been produced in the first decade of research, giving rise to the novel field of computable set theory. At that point, it already was clear that to face the tremendous amount of technicalities involved in the combination of smaller decidable fragments into larger ones, new techniques were in order. Such techniques have recently emerged, by a careful analysis of the formation process of disjoint families of sets. This has led to the characterization of suitable decidable conditions for the satisfiability of set-theoretic formulae belonging to specific collections. In this paper we give an elementary introduction to the formative process technique and discuss some open problems.
Satisfiability decision problem; satisfaction algorithm; Zermelo-Fraenkel set theory
D., Cantone; Ursino, Pietro
File in questo prodotto:
File Dimensione Formato  
DPU-LAST.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: DRM non definito
Dimensione 323.47 kB
Formato Adobe PDF
323.47 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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: http://hdl.handle.net/11383/20911
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact