Find a predicate form in prenex normal form which is logically equivalent to using the equivalences:
Here we only have one quantifier to be shifted to the front, so we can use equivalence number 12 to get
Is this right? Because we are only justified in using this equivalence if the variable y doesn not occur free in , but we don't know that since y doesn't not appear in the scope of any quantifiers in it...
In our case the variables are not distinct so we can't apply the equivalcences straight away, so we have to change bound variables first so that we can move quantifiers past the free variables:
Now, I'm a bit confused about the negation, but I applied equivalence number 4
Now we apply equivalence number 3
I would appreciate it if anyone could correct me.
You captured y in Agxy. The quantified y in the conclusion has to be renamed first.
Did I derive it correctly correct? It looks like it's in the prenex normal form since it's in the form (B being a predicate form with no quantifiers and is any quantifier).