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?
An orbit-finite signature is an orbit-finite set of symbols, together with an equivariant arity function to the set of natural numbers. An orbit-finite structure over is an orbit-finite domain together with an equivariant interpretation mapping from to relations over the domain, respecting the arities.
Pp-formulas over a signature are defined inductively:
- If is a symbol of arity then is a pp-formula with free variables
- If is an orbit-finite family of pp-formulas, then is a pp-formula with free variables , where are the free variables of the formula .
- If is a a pp-formula and is an orbit-finite set, then is a pp-formula. Its free variables are the free variables of minus .
The set of free variables of a pp-formula is always an orbit-finite set. A valuation in a structure is a finitely-supported mapping from the set of free variables to the domain of .
Semantics. Fix an orbit-finite structure . The semantics of a pp-formula with free variables is a set of valuations, , defined as:
A pp-formula in prenex form is a formula of the form , where is of the form .
Fact. For every pp-sentence in prenex form there exists an orbit-finite structure with the property (*):
if and only if maps homomorphically to , for every structure
Conversely for every orbit-finite structure there is a prenex pp-formula with the property (*).
Proof. A sentence is converted to the structure with universe , and such that the relation holds if and only if the predicate occurs in the formula.
Conversely, a structure is converted into a sentence , where is the domain of , is the disjoint union of all relations of , and is the predicate if is the tuple of the relation .
Fact. Over the ordered atoms , the formula
(where for each , the symbol is a unary predicate) is not equivalent to any formula in prenex form.
Proof. For , let us define a structure with domain and where for each , the interpretation of the symbol is the set . Clearly, the structure satisfies the formula . However, it does not satisfy the formula , which would be the natural candidate for a prenex-normal form equivalent to (obtained by Skolemization). This argument, however, does not show that is not equivalent to a formula in prenex form.
Suppose that is equivalent to a formula in prenex form. Then there exists an orbit-finite structure as described in the fact above. Assume that is equivariant (the argument in the general case is similar). Observe that since maps homomorphically to itself, it follows that satisfies the formula . On the other hand, since for each , satisfies the formula , it follows that maps to .
Let be a finitely supported homomorphism to , where .
For we write if .
Let be an element of such that . Since satisfies the formula , there exists an element such that holds in . Let be any automorphism of the atoms which maps to such that .
What is ? From equivariance of it follows that holds. Therefore, is a tuple of the form
The support of is contained in . Since , it follows that actually . But has elements, a contradiction.
Question. What is the appropriate notion of a pp-formula, which has normal forms? And what is the related notion of a homomorphism?