quantifier raising

There are a lot of logical equivalence rule that involves quantifiers. They are particular useful to convert a formula into Prenex normal form.

In general, if we have a two-place connective other than with a quantifier attached to one side, we can extract it to the front. The rules vary depending on the connective and the position of the quantifier.

More formally, Where contains no free occurrences of :

Note:

• For conjunction and disjunction, the quantifier can be moved to the front without changing
• For conditional, if we attached a quantifier to the antecedent, we need to change it to the other quantifier when we move it out