Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
add comment

1 Answer

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).

share|improve this answer
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
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.