# Unique normal form of formulae of predicate calculus?

Is there a unique normal form for each formula of predicate calculus?

I am aware of prenex normal forms of predicate calculus and of disjunctive and conjunctive normal forms of propositional calculus. But what is the name of the combination of the two, i.e. the formula is in prenex normal form and the (quantifier-free) matrix is in - say - disjunctive normal form?

Can uniqueness always be achieved by a optimal choice of variables and sorting and arrangement of the literals of the disjunctive normal form (given that the variables and the relation and function symbols are lexicographically sorted) and elimination of double negation?

Example: The intended unique normal form of

$(\forall x_2) \neg R_2 (x_2) \rightarrow \Big((\exists x_1)\neg\neg R_3(x_1) \wedge R_1(x_1,x_2) \Big)$

should be (not quite sure)

$(\forall x_1)(\exists x_2)\big(R_1 (x_2,x_1) \vee R_2(x_1)\big) \wedge \big( R_2(x_1) \vee R_3 (x_2) \big)$

What is the complexity of finding such normal forms?

-

I would like to point out that the problem of uniqueness of a formula is non-trivial even in propositional logic. Eg. (p→q)∧(q→r)∧(r→p) is equal to (¬p∨q)∧(¬q∨r)∧(¬r∨p) and also to (¬p∨r)∧(¬r∨q)∧(¬q∨p).

-
To me, the only criterion for achieving uniqueness seems to be "lexicographic order"in which (¬p∨q)∧(¬q∨r)∧(¬r∨p) is smaller than (¬p∨r)∧(¬r∨q)∧(¬q∨p), but even smaller is (¬p∨q)∧(p∨¬r)∧(¬q∨r) - depending on the handling of ¬ and the logical connectives. But a permutation of the sentence variables might yield even smaller formulas. –  Hans Stricker Jan 24 '11 at 16:04