Decision procedures for elementary sublanguages of set theory: XIII. Model graphs,reflection and decidability |
| |
Authors: | Franco Parlamento Alberto Policriti |
| |
Affiliation: | (1) Dipartimento di Matematica e Informatica, Universitá di Udine, via Zanon 6, 31100 Udine, Italy;(2) Courant Institute of Mathematical Sciences, 251 Mercer Street, 10012 New York, NY, U.S.A. |
| |
Abstract: | Positive solutions to the decision problem for a class of quantified formulae of the first order set theoretic language based on , , =, involving particular occurrences of restricted universal quantifiers and for the unquantified formulae of , , =, {...}, , where {...} is the tuple operator and is a general choice operator, are obtained. To that end a method is developed which also provides strong reflection principles over the hereditarily finite sets. As far as finite satisfiability is concerned such results apply also to the unquantified extention of , , =, {...}, , obtained by adding the operators of binary union, intersection and difference and the relation of inclusion, provided no nested term involving is allowed. |
| |
Keywords: | Decidability reflection |
本文献已被 SpringerLink 等数据库收录! |
|