Tag Archives: pp-formula

Normalization of pp-formulas

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 \exists^\ast \bigwedge_i \phi_i – this is due to Skolemization, i.e. the fact that \bigwedge_i \exists x \phi_i can be turned into \exists x_1,\ldots,x_n \bigwedge \phi_i. 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?

Continue reading