Decidability of ∃*∀∀-sentences in HF
Bellè, D. ; Parlamento, F.
Notre Dame J. Formal Logic, Tome 49 (2008) no. 1, p. 55-64 / Harvested from Project Euclid
Text on Project Euclid
PDF
Alt PDF
Let HF be the collection of the hereditarily finite well-founded sets and let the primitive language of set theory be the first-order language which contains binary symbols for equality and membership only. As announced in a previous paper by the authors, "Truth in V for ∃*∀∀-sentences is decidable," truth in HF for ∃*∀∀-sentences of the primitive language is decidable. The paper provides the proof of that claim.
Publié le : 2008-01-15
Classification:  quantifiers,  decidability,  hereditarily finite sets,  03B25,  03E30,  03C62 
@article{1199649900,
     author = {Bell\`e, D. and Parlamento, F.},
     title = {Decidability of [?]<sup>*</sup>[?][?]-sentences in HF},
     journal = {Notre Dame J. Formal Logic},
     volume = {49},
     number = {1},
     year = {2008},
     pages = { 55-64},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1199649900}
}

Bellè, D.; Parlamento, F. Decidability of ∃*∀∀-sentences in HF. Notre Dame J. Formal Logic, Tome 49 (2008) no. 1, pp.  55-64. http://gdmltest.u-ga.fr/item/1199649900/