CS550 Exercises 5 Solution

Exercises 5
Exercise 1 (Quantifier Elimination in PA). Apply quantifier elimination as seen in the Lectures to the following formulas:
• ∃x,y.2x + 3y < 7 ∧ x < y
• ∃x,y.2x + 3y < 7 ∧ y < x
• ∃x,y.3x + 3y < 8 ∧ 8 < 3x + 2y
• ∃x,y.x = 2y ∧ ∃z.x = 3z
Exercise 2 (Satisfiability algorithm for Presburger arithmetic). Consider the formula F(x) given by
F(x) = ^ ai < x ∧ ^ x < bj ∧ ^ Ki|(x + ti).
i=1 j=1 i=1
1. Assume all ai,bj,ti are integer constants. Give an algorithm that, given any formula of the form above, returns:
• a value for x, if such value exists, and
• “UNSAT” if no such value exists
2. Give a recursive algorithm that, given a formula in the above form returns
• one map from variables to integers for which formula evaluates to true, if such a map exists, and
• “UNSAT” if no such map exists.
Exercise 3 (Quantifier elimination for rationals). In this exercise we will devise a quantifier elimination method for rational numbers. We consider formulas over the signature (Q,<,≤,=,+,−), i.e. with constant symbols among Q, interpreted over the standard structure of rational numbers.
1. Show that for any formula F, there exists a formula F1 such that
F ⇐⇒ Q1x1,...,Qnxn,Qn+1y.F1
1
Where Qi are either ∃ or ¬∃, i.e. existential quantifiers that can be separated by negations and where F1 is built only from (∧,∨,Q,<,= ,+,−,k · ). In particular it is quantifier-free and contains no negation! 2. Do we need to add the divisibility relation as in the PA case? Why?
3. Show that there exist a formula F2 such that F1 ⇐⇒ F2 and every atom of F2 is of the form:
t < y
or
y < t
for some term t
4. Show that there exists a formula F3 that is quantifier-free such that
(∃y.F2) ⇐⇒ F3
Hint: Picture a graph of the truth value of F2 as a function of y. How often can the truth value change? Is it possible to test F2 in some finite number of intervals only?
Exercise 4 (PA without divisibility). Show that Presburger Arithmetic without the divisibility relationship does not admit quantifier elimination with the following steps:
1. Find a quantified formula of one free variable F(y) such that F(y) is true for infinitely many positive integers and false for infinitely many positive integers. I.e., SF = {n ∈ N|F(n)} is infinite and N SF is infinite.
2. Show that for any quantifier-free formula of one free variable G(y), either SG is finite or N SG is finite.
3. Conclude.
Exercise 5 (Structure of sets). Consider the structure (P(N),⊆,= ∩,∪, c) whose base set is the set of all sets of natural numbers and where c denotes complement. Is it possible to eliminate quantifiers from arbitrary first order formulas on this structure? For example, ∃B.A ⊆ B ∧ B ⊆ C is equivalent to A ⊆ C. Show a quantifier elimination procedure, or give an example of a quantified first-order logic formula that has no equivalent formula without quantifiers, and prove it.
2