We give a complete proof that all 3-quantifier sentences in the primitive notation of set theory (∈, =), are decided in ZFC, and in fact in a weak fragment of ZF without the power set axiom. We obtain information concerning witnesses of 2-quantifier formulas with one free variable. There is a 5-quantifier sentence that is not decided in ZFC (see [2]).
@article{bwmeta1.element.bwnjournal-article-doi-10_4064-fm177-3-3,
author = {Harvey M. Friedman},
title = {Three-quantifier sentences},
journal = {Fundamenta Mathematicae},
volume = {177},
year = {2003},
pages = {213-240},
zbl = {1020.03044},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.bwnjournal-article-doi-10_4064-fm177-3-3}
}
Harvey M. Friedman. Three-quantifier sentences. Fundamenta Mathematicae, Tome 177 (2003) pp. 213-240. http://gdmltest.u-ga.fr/item/bwmeta1.element.bwnjournal-article-doi-10_4064-fm177-3-3/