GNU Aris Manual: pr

Next: ii, Previous: nq, Up: Predicate Rules [Contents]

6.3.7 Prenex

3x(P(x) ^ Q(a)) <=> 3x(P(x)) ^ Q(a)
Vx(P(x) ^ Q(a)) <=> Vx(P(x)) ^ Q(a)
3x(P(x) v Q(a)) <=> 3x(P(x)) v Q(a)
Vx(P(x) v Q(a)) <=> Vx(P(x)) v Q(a)

The Prenex Laws are used to move quantifiers to the start of the sentence.

Prenex uses only one reference, and, being an equivalence rule, can be used on any part of the sentence.