Elimination of quantifier
∃
in
∃x ∈ ]a, b[ , φ
where
φ
a conjunction.
1. Moving predicates that does not depend on variable x
- If φ contains a predicate where x
does not appear, we can put this
predicate outside.
For instance, ∃x
∈ ]a, b[, (x2 + bx
= 0 and a = b + 1) can be transformed in a = b + 1 and ∃x,
(x2 + bx = 0).
- If there is no predicate where x appear,
then
the quantifier ∃ is eliminated. For instance, ∃x
∈
]a, b[ (a = b + 1)
is equivalent to (a = b + 1).
2. Simplification of the formula
The formula is of the form
∃x
∈ ]a, b[, P1 =
0 and P2 =
0 and .... Pn
= 0 and Q1 > 0
and Q2 > 0 and ...
Qk
> 0.