Application of formative processes to the decision problem in set theory
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.
The authors retain all rights to the original work without any restrictions.
License for Published Contents
"Le Matematiche" published articlesa are distribuited with Creative Commons Attribution 4.0 International. You are free to copy, distribute and transmit the work, and to adapt the work. You must attribute the work in the manner specified by the author or licensor (but not in any way that suggests that they endorse you or your use of the work).
License for Metadata
"Le Matematiche" published articles metadata are dedicated to the public domain by waiving all publisher's rights to the work worldwide under copyright law, including all related and neighboring rights, to the extent allowed by law.
You can copy, modify, distribute and perform the work, even for commercial purposes, all without asking permission.
No Fee Charging
No fee is required to complete the submission/review/publishing process of authors paper.
