Rectified prenex form conversion algorithm inconsistencies

Question

I've looked at these two different RPF conversion algorithms where the first step of each, say 1 and 1', states:

1.Remove all “$\to$”s using the fact that $\alpha\to\beta ≡ \neg\alpha\lor\beta.$
1'.Eliminate $\leftrightarrow$ using the law $A \leftrightarrow B ≡ (A \to B) \land (B \to A)$ on all subformulas of $X$.

Why should we care about $\to$ or $\leftrightarrow$ if neither the definition of a rectified formula nor the definition of the prenex form says anything about the logical connectives?

The formula of the form, say, $\forall x \exists y(Px \to Qy \leftrightarrow Rz)$ is still in RPF, right?

The two different algorithms only seem to confirm that we can skip the first step.

Answer 1

Correct !

The only possible explanation for this "weird" choice, is that the treatment of PNF is a pre-requisite for Resolution (see Ch.3, page 115-on) and resolution needs clauses.

But note that on Singh's book the procedure for "prenexing" does not ask to eliminate $\to$, but only $↔$.

The need to avoid $↔$ [see Exercise 2.14: Can you see why the procedure PrenForm eliminates $↔$ before rectifying the formula?] is connected to Theorem 2.13: in it there are no equivalences involving $↔$ to be used for "moving outside" the quantifiers.

Answer 2

Both of the algorithms you linked are of the "if a transform matches, then apply it" type of algorithm. Both are of the type "it doesn't matter what order you apply the transforms in, just keep applying any that match in any order".

You are correct to observe that the algorithms use 2 different sets of transforms. That does not imply that a transforms which only occur in 1 of the algorithms are unnecessary. For example, for the first algorithm, if you remove

$$A \implies B \triangleright \lnot A \lor B \tag{T1}$$

...then how will you transform $(\forall x ~ A) \implies B$ into PNF? You can't, unless you add 4 new rules:

$$(\forall x ~ A) \implies B \triangleright \exists x~(A \implies B) \tag{T2}$$ $$(\exists x ~ A) \implies B \triangleright \forall x~(A \implies B) \tag{T3}$$ $$A \implies (\forall x ~ B) \triangleright \forall x~(A \implies B) \tag{T4}$$ $$A \implies (\exists x ~ B) \triangleright \exists x~(A \implies B) \tag{T5}$$

Algorithm 1 has transform (T1), but not (T2) through (T5). Algorithm 2 has (T2) through (T5), but not (T1).

Neither algorithm has a rule for transforming $(\forall x~P) \text{ xor } Q$. Consequently, neither will put all formulas using xor into PNF. But you could add the rule $A \text{ xor } B \triangleright (A \land \lnot B) \lor (\lnot A \lor B)$ and you can now convert formulas involving xor to PNF.

The first algorithm doesn't have a method for converting formulas of the form $(\forall x~P) \iff Q$, but you can just copy that rule from the second algorithm, add it to the first, and then the first algorithm will also be able to transform formulas involving if-and-only-if.

Btw, note that some of the transforms assume a non-empty universe.