Given this well formed first order logic form:
$\forall x (\mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(x,y)) \Rightarrow (\forall x \ \mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \forall x \ \mathcal A_2^2(x,y))$
Where $\mathcal A_i^j$ is the $i$-th predicate of arity $j$ and $\mathcal f_i^j$ is the $i$-th functional letter of arity $j$
I have to take it in Prenex Normal Form.
My notes give this rules of transformation:
- $\lnot \forall x \ \mathcal A \equiv \exists x \ \lnot \mathcal A$
- $\lnot \exists x \ \mathcal A \equiv \forall x \ \lnot \mathcal A$
- $\forall x \mathcal \ A(x) \land \mathcal B \equiv \forall y (\mathcal A[y/x] \land \mathcal B)$
- $\exists x \ \mathcal A(x) \land \mathcal B \equiv \exists y (\mathcal A[y/x] \land \mathcal B)$
- $\forall x \ \mathcal A(x) \lor \mathcal B \equiv \forall y (\mathcal A[y/x] \lor \mathcal B)$
- $\exists x \ \mathcal A(x) \lor \mathcal B \equiv \exists y (\mathcal A[y/x] \lor \mathcal B)$
- $\forall x \ \mathcal A(x) \Rightarrow \mathcal B \equiv \exists y (\mathcal A[y/x] \Rightarrow \mathcal B)$
- $\exists x \ \mathcal A(x) \Rightarrow \mathcal B \equiv \forall y (\mathcal[y/x] \Rightarrow \mathcal B)$
- $\mathcal B \Rightarrow \forall x \mathcal \ A(x) \equiv \forall y (\mathcal B \Rightarrow \mathcal[y/x]) $
- $\mathcal B \Rightarrow \exists \mathcal \ A(x) \equiv \exists y (\mathcal B \Rightarrow \mathcal A[y/x])$
Where:
- $\mathcal A(x)$ is a formula with free occurences of $x$, and $y$ is a variable such that the term $y$ is free for $x$ in $\mathcal A(x)$ and $y$ doesn't have any free occurrence in $\mathcal B$
- $\mathcal A[y/x]$ is the formula obtained substituting every free occurrence of $x$ with $y$
- $\mathcal B$ is any well formed formula
(The notes also say that if $\mathcal B$ doesn't contain free occurrences of $x$ the change of the variable name isn't needed.)
I'm wondering if:
$\forall x (\mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(x,y)) \Rightarrow (\forall x \ \mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \forall x \ \mathcal A_2^2(x,y)) \equiv$
(using rule n. 5)
$\forall x (\mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(x,y)) \Rightarrow \forall x \ (\mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \forall x \ \mathcal A_2^2(x,y)) \equiv$
(using rule n.5)
$\forall x (\mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(x,y)) \Rightarrow \forall x \forall \nu \ (\mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(\nu,y)) \equiv$
(using rule n.9)
$\forall x( \forall x (\mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(x,y)) \Rightarrow \forall \nu(\mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(\nu,y))) \equiv$
(using rule n.9)
$\forall \nu(\forall x (\forall x (\mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(x,y)) \Rightarrow \mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(\nu,y))) \equiv$
(using rule n.7)
$\forall \nu(\forall x (\exists t ((\mathcal A_1^2(t,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(x,y)) \Rightarrow \mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(\nu,y)))) \equiv$
$\forall \nu \forall x \exists t ((\mathcal A_1^2(t,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(x,y)) \Rightarrow \mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(\nu,y))$
is a correct PNF of the starting formula.
I think the first three passages are okay, because they are the same of my notes, but from the 4th passage onwards my notes apply other transformation rules arriving to the PNF formula:
$\exists x \forall w \forall \nu ((\mathcal A_1^2(x,\mathcal f_1^2(y,z)) \lor \mathcal A_2^2(x,y)) \Rightarrow (\mathcal A_1^2(w, \mathcal f_1^2(y,z)) \lor \mathcal A_2^2(\nu, y)))$
I'm also suspicious about that $\forall x( \forall x (\mathcal A_1^2 ...$ in my 4-th passage, is it possible and correct to have two $\forall x$ which are totally the same (referring to the exactly same variable) in a formula?
Can anyone tell me if my procedure was correct and, eventually, explain me the details of my mistakes?