Conversion To prenex normal form with ∃xα ∨ ∀x(β)

Question

The algorithm I use is the one on this page

But does this algorithm actually handle the following 6 cases?

• ∀x(α) ∧ ∀x(β)
• ∀x(α) ∨ ∀x(β)
• ∃x(α) ∧ ∃x(β)
• ∃x(α) ∨ ∃x(β)
• ∀x(α) ∧ ∃x(β)
• ∀x(α) ∨ ∃x(β)

If not, what are the rules for the last 2 cases?

PS: If you know a URL to some code for conversion to prenex normal form, please let me knowsince I can't find any on the internet.

Answer 1

does this algorithm actually handle the following 6 cases?

Yes; use step 3 to rname the bound variables. E.g. for : $∀x(α) ∧ ∀x(β)$, rewrite it as :

$∀y(α) ∧ ∀x(β)$,

and then apply step 4 to get :

$∀y∀x(α ∧ β)$

because, after renaming, $x$ does not occur in $α$ nor $y$ in $β$.

See Prenex normal form.

---

The order of the quantifiers does not matter (in the "mixed" case) due to the renaming of bound variables.

Consider e.g.:

$∀x(α) ∨ ∃x(β)$.

After renaming, we get : $∀y(α) ∨ ∃x(β)$; then we apply step 4 to the left $∀y$ quantifier, getting : $∀y(α ∨ ∃x(β))$, due to the fact that $y$ does not occur in $β$.

Now forget about $∀y$ for a moment and apply again step 4 with $∃x$, getting :

$(α ∨ ∃x(β)) \equiv ∃x(α ∨ β)$

due to the fact that $x$ does not occur in $α$.

Now, we can "restore" $∀y$ to get :

$∀y∃x(α ∨ β)$.

The procedure is clearly symmetrical; thus, starting with $∃x$ we can get :

$∃x∀y(α ∨ β)$.