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?

An orbit-finite signature $\Sigma$ is an orbit-finite set of symbols, together with an equivariant arity function to the set of natural numbers. An orbit-finite structure $\str S$ over $\Sigma$ is an orbit-finite domain together with an equivariant interpretation mapping from $\Sigma$ to relations over the domain, respecting the arities.

Pp-formulas over a signature $\Sigma$ are defined inductively:

If $R$ is a symbol of arity $n$ then $R(x_1,x_2,x_2,\ldots,x_n)$ is a pp-formula with free variables $\set{x_1,\ldots,x_n}$
If $\set{\phi_i}_{i\in I}$ is an orbit-finite family of pp-formulas, then $\bigwedge_{i\in I}\phi_i$ is a pp-formula with free variables $\bigcup_{i\in I}\textrm{FV}(\phi_i)$ , where $FV(\phi_i)$ are the free variables of the formula $\phi_i$ .
If $\psi$ is a a pp-formula and $A$ is an orbit-finite set, then $\exists^A \bar x.\psi$ is a pp-formula. Its free variables are the free variables of $\psi$ minus $\set{x_a:a\in A}$ .

The set of free variables of a pp-formula is always an orbit-finite set. A valuation in a structure $\str S$ is a finitely-supported mapping from the set of free variables to the domain of $\str S$ .

Semantics. Fix an orbit-finite structure $\str S$ . The semantics of a pp-formula $\phi$ with free variables $V$ is a set of valuations, $\phi[\str S]\subset \str S^V$ , defined as:

$\set{f: (f(x_1),\ldots,f(x_n))\in R}$ if $\phi=R(x_1,\ldots,x_n)$
$\set{f: \forall{i\in I}. f|_{FV(\phi_i)}\in\phi_i[\str S]}$ if $\phi=\bigwedge_{i\in I}\phi_i[\str S]$
$\set{f|_{FV(\phi)}: f\in \psi[\str S]}$ if $\phi=\exists^A\bar x. \psi[\str S]$

A pp-formula in prenex form is a formula of the form $\exists^A\bar x. \bigwedge_{i\in I}\phi_i$ , where $\phi_i$ is of the form $R(x_1,\ldots,x_n)$ .

Fact. For every pp-sentence $\phi$ in prenex form there exists an orbit-finite structure $\str S$ with the property (*):

$\str T\models \phi$ if and only if $\str T$ maps homomorphically to $\str S$ , for every structure $\str T.$

Conversely for every orbit-finite structure $\str S$ there is a prenex pp-formula $\phi$ with the property (*).

Proof. A sentence $\exists^A\bar x. \bigwedge_{i\in I}\phi_i$ is converted to the structure with universe $A$ , and such that the relation $R(a_1,\ldots,a_n)$ holds if and only if the predicate $R(x_{a_1},\ldots,x_{a_n})$ occurs in the formula.

Conversely, a structure $\str A$ is converted into a sentence $\exists^A\bar x.\bigwedge_{i\in I}\phi_i$ , where $A$ is the domain of $\str A$ , $I$ is the disjoint union of all relations of $\str A$ , and $\phi_i$ is the predicate $R(x_{a_1},\ldots,x_{a_n})$ if $i$ is the tuple $(a_1,\ldots,a_n)$ of the relation $R$ . $\square$

Fact. Over the ordered atoms $\str Q$ , the formula

$\bigwedge_{q\in\str Q} \exists z. R_q(z)$

(where for each $q\in\str Q$ , the symbol $R_q$ is a unary predicate) is not equivalent to any formula in prenex form.

Proof. For $n=1,2,\ldots$ , let us define a structure $\str T_n$ with domain $\str Q^{(n)}=\set{(q_1,\ldots,q_n):q_1<q_2<\ldots<q_n}$ and where for each $p\in\str Q$ , the interpretation of the symbol $R_p$ is the set $\set{\bar q\in\str Q^{(n)}: p=q_1}$ . Clearly, the structure $\str T_n$ satisfies the formula $\phi$ . However, it does not satisfy the formula $\exists^\str Qz.\bigwedge_{q\in\str Q} R_q(z_q)$ , which would be the natural candidate for a prenex-normal form equivalent to $\phi$ (obtained by Skolemization). This argument, however, does not show that $\phi$ is not equivalent to a formula in prenex form.

Suppose that $\phi$ is equivalent to a formula in prenex form. Then there exists an orbit-finite structure $\str S$ as described in the fact above. Assume that $\str S$ is equivariant (the argument in the general case is similar). Observe that since $\str S$ maps homomorphically to itself, it follows that $\str S$ satisfies the formula $\phi$ . On the other hand, since for each $n$ , $\str T_n$ satisfies the formula $\phi$ , it follows that $\str S$ maps to $\str T_n$ .

Let $f:\str S\to \str T_n$ be a finitely supported homomorphism to $\str T_n$ , where $n>m$ .

For $U,V\subset\str Q$ we write $U<V$ if $\forall_{u\in U}\forall_{v\in V}u<v$ .

Let $q_0$ be an element of $\str Q$ such that $\sup f<q_0$ . Since $\str S$ satisfies the formula $\phi$ , there exists an element $z_0$ such that $R_{q_0}(z_0)$ holds in $\str S$ . Let $\alpha$ be any automorphism of the atoms which maps $(q_0,z_0)$ to $(q,z)$ such that $q>\sup f$ .

What is $f(z)$ ? From equivariance of $\str S$ it follows that $R_{q}(z)$ holds. Therefore, $f(z)\in \str T_n$ is a tuple of the form

$f(z)=(r_1,r_2,r_3,\ldots,r_{n}),\quad\text{where }q=r_1<r_2<\ldots<r_{n}$

The support $\set{r_1,\ldots,r_n}$ of $f(z)$ is contained in $\sup f\cup \sup z$ . Since $\sup f<r_1<r_2<\ldots<r_m$ , it follows that actually $r_1,r_2,\ldots,r_n\in \sup z$ . But $\sup z$ has $m<n$ elements, a contradiction. $\square$