Why are Bernays–Schönfinkel formulas only 'effectively' propositional? According to https://en.wikipedia.org/wiki/Bernays%E2%80%93Sch%C3%B6nfinkel_class

The Bernays–Schönfinkel class (also known as Bernays–Schönfinkel–Ramsey class) of formulas, named after Paul Bernays, Moses Schönfinkel and Frank P. Ramsey, is a fragment of first-order logic formulas where satisfiability is decidable.


It is the set of sentences that, when written in prenex normal form, have an ∃*∀* quantifier prefix and do not contain any function symbols.


This class of logic formulas is also sometimes referred as effectively propositional (EPR) since it can be effectively translated into propositional logic formulas by a process of grounding or instantiation.

Hang on. Existentially quantified variables not in the scope of universal quantifiers, translate during CNF conversion into constant symbols with no function arguments. And the definition specifies no function symbols. So it seems like that definition should specify just the propositional fragment of first-order logic. No 'effectively', no need for any process of grounding or instantiation.
What am I missing?
 A: The Bernays–Schönfinkel class is not the propositional fragment of first-order logic because the sentences in it are not propositional! They involve quantifiers and variables.
Now it's true that a sentence $\varphi$ in the Bernays–Schönfinkel class can be transformed into a propositional sentence $\widehat{\varphi}$: (1) introduce constant symbols as witnesses for the existential quantifiers, (2) replace the universal quantifiers by conjunctions over the constant symbols, and (3) replace atomic sentences with new proposition symbols. For example, $\exists x\exists y\forall z R(x,z)\lor R(y,z)$ becomes $(P_{R(c,c)}\lor P_{R(d,c)})\land (P_{R(c,d)}\lor P_{R(d,d)})$. This is the process that the wikipedia article refers to as "grounding or instantiation" and that (I think) you refer to as "CNF conversion".
The key point of this construction is that $\varphi$ and $\widehat{\varphi}$ are equisatisfiable: $\varphi$ has a model (in the sense of first-order logic) if and only if $\widehat{\varphi}$ has a model (in the sense of propositional logic). But it's not the case that $\varphi$ and $\widehat{\varphi}$ are equivalent - it's not even clear what this would mean, since they're sentences in different logics.
