A decision procedure for a sublanguage of set theory involving monotone additive and multiplicative functions, II. The multi-level case
AbstractMLSS is a decidable sublanguage of set theory involving the predicates membership, set equality, set inclusion, and the operators union, intersection, set difference, and singleton.
In this paper we extend MLSS with constructs for expressing monotonicity, additivity, and multiplicativity properties of set-to-set functions. We prove that the resulting language is decidable by reducing the problem of determining the satisfiability of its sentences to the problem of determining the satisfiability of sentences of MLSS.
In addition, we show an interesting model theoretic property of MLSS, the singleton model property, upon which our decidability proof is based. Intuitively, the singleton model property states that if a formula is satisfiable, then it is satisfiable in a model whose non-empty Venn regions are singleton sets.
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.