Decision procedures for elementary sublanguages of set theory
Tóm tắt
In this paper we prove the decidability of the class of unquantified formulae of set theory involving the operators ϕ, ∪, ∩, \, {·}, pred
< and the predicates =, ∈,
$$ \subseteq $$
, Finite, where pred
<(s) denotes the collection of all sets having rank strictly less than the rank of s. This work generalizes and combines earlier results published in the same series of papers.
Tài liệu tham khảo
Cantone, D., ‘Decision procedures for elementary sublanguages of set theory. X. Multilevel syllogistic extended by the singleton and powerset operators’, J. Symb. Comp. — Special issue (to appear). New Trends in Automated Mathematical Reasoning-Proceedings.
Cantone, D., Cutello, V. and Ferro, A., ‘Decision procedures for elementary sublanguages of set theory. XIV. Three languages involving rank related constructs’, in Int. Symp. on Symbolic and Algebraic Computation (to appear).
Cantone, D., Ferro, A., Micale, B. and Sorace, G., ‘y∈x}’, Comm. Pure App. Math. 40, 37–77 (1987).
Cantone, D. and Schwartz, J. T., ‘Decision procedures for elementary sublanguages of set theory. XI. Multilevel syllogistic extended by some elementary map constructs’, J. Symb. Comp. — Special issue (to appear). New Trends in Automated Mathematical Reasoning-Proceedings.
Jech, T. J., Set Theory, Academic Press, New York (1978).
Vaught, R. L., Set Theory. An Introduction, Birkhauser, Boston (1985).