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?