Notes - Logic and Proof MT24, Quantifier elimination
Flashcards
@Define what it means for a theory $\pmb T$ to admit quantifier elimination.
For any formula of the form $\exists x F$ where $F$ is quantifier-free, there exists a quantifier-free formula $G$ with the same free variables and $\pmb T \models \exists x F \leftrightarrow G$.
A quantifier elimination procedure is not quite enough to show a theory $T$ is decidable. What else do you need, and once you have this, how can you use it to show a theory is decidable?
- You also need a procedure for determining whether or not $F \in \pmb T$ for a variable-free atomic formula $F$.
- Then to decide membership:
- Convert formula to prenex normal form.
- Eliminate all quantifiers.
- Check whether $F’ \in \pmb T$ using procedure.
@Justify why it suffices to show that you can eliminate an existential quantifier applied to a conjunction of literals to conclude that a theory has quantifier elimination.
- It suffices just to consider existential quantifiers since $\forall x F \leftrightarrow \lnot \exists x \lnot F$.
- It suffices just to consider conjunctions of literals since any formula $F$ can be put in DNF, and existential quantifiers distribute over disjunctions: $\exists x \bigvee^n _ {i = 1} \bigwedge^m _ {j = 1} L _ {i, j} \leftrightarrow \bigwedge^n _ {i = 1} \exists x \bigvee^m _ {j = 1} L _ {i, j}$.