Classicaly, primitive positive formulas form the smallest fragment of first-order logic which is closed under conjunction and existential quantification. Pp-formulas can be turned in to a normal form 
– this is due to Skolemization, i.e. the fact that 
can be turned into 
. In this case, Skolemization is a consequence of the axiom of finite choice.
We show that in the world with atoms, not every orbit-finite pp-formula can be converted into an equivalent one in prenex form. This is another demonstration of the failure of the axiom of choice.
This raises the question: what is the appropriate notion of a pp-formula, which does have normal forms?