Let V be the cumulative set theoretic hierarchy, generated from the
empty set by taking powers at successor stages and unions at limit
stages and, following [2], let the primitive language of set theory be
the first order language which contains binary symbols for equality
and membership only. Despite the existence of
∀∀-formulae in the primitive language, with two free
variables, which are satisfiable in V but not by finite sets ([5]),
and therefore of ∃∃∀∀ sentences of the
same language, which are undecidable in ZFC without the Axiom of
Infinity, truth in V for
∃*∀∀-sentences of the
primitive language, is decidable ([1]). Completeness of ZF
with respect to such sentences follows.