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 SLet \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


Question. What is the appropriate notion of a pp-formula, which has normal forms? And what is the related notion of a homomorphism?


Leave a Reply

Your email address will not be published.

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>