prenex

Alphabet

and	:	[form × form] ⟶ form
or	:	[form × form] ⟶ form
not	:	[form] ⟶ form
forall	:	[form → form] ⟶ form
exists	:	[form → form] ⟶ form

Variables

P	:	form
Q	:	form → form

Rules

and(P, forall(λx:form.Q · x))	⇒	forall(λx:form.and(P, Q · x))
or(P, forall(λx:form.Q · x))	⇒	forall(λx:form.or(P, Q · x))
and(forall(λx:form.Q · x), P)	⇒	forall(λx:form.and(Q · x, P))
or(forall(λx:form.Q · x), P)	⇒	forall(λx:form.or(Q · x, P))
not(forall(λx:form.Q · x))	⇒	exists(λx:form.not(Q · x))
and(P, exists(λx:form.Q · x))	⇒	exists(λx:form.and(P, Q · x))
or(P, exists(λx:form.Q · x))	⇒	exists(λx:form.or(P, Q · x))
and(exists(λx:form.Q · x), P)	⇒	exists(λx:form.and(Q · x, P))
or(exists(λx:form.Q · x), P)	⇒	exists(λx:form.or(Q · x, P))
not(exists(λx:form.Q · x))	⇒	forall(λx:form.not(Q · x))