Homework 08 - Due 23 April or until professor or teaching assistant solves it (whichever comes later)
(Problem 7.10 at the end of Chapter 7 of Calculus of Computation Textbook.)
Consider a language that contains some terms whose values are interpreted as integers (to be concrete, the language of Presburger arithmetic, or the BAPA language). Consider formulas interpreted over some theory that has an effective quantifier elimination algorithm . Then show that there is an algorithm for solving optimization problems such as
where denotes a term of the language whose value is an integer, and where is an arbitrary formula in language . The meaning of solution for constraints is the following. Let . Then the solution is an element of such that
- if then
- if then contains arbitrarily large elements (for each integer , there exists such that )
- if then and
Your answer will show, given , how to solve optimization problems for any theory that has quantifier elimination. For example, taking Presburger arithmetic, we can solve linear optimization problems such as
Taking BAPA as a theory with QE, we can solve problems such as finding
By generalizing the objective function to reals, we can solve non-linear but polynomial optimization problems using quantifier elimination over reals.
Consider language and the theory where is the set of following axioms (axioms of linear order):
Observe that these axioms are true in the structures of integers, natural numbers, and rational numbers, where is interpreted as the usual less-than-equal relation on such numbers.
Describe an algorithm that, given a sentence in this language, decides whether . Explain why your algorithm is correct.
If you cannot solve the problem in its entirety, write observations that you could obtain. You are allowed (but not required) to use any references (books, papers) that you can find (but it may be easier to solve the problem on your own). You must cite any references that you used. You need not write down in great detail explanations of simple facts, but if you omit any proof steps make sure that they indeed simple.
Solution (added afterwards):
Somewhat related papers:
- A. Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fund. Math., 49:129–141, 1961.
- H Lauchli. A decision procedure for the weak second-order theory of linear order (1968), In Contributions to Mathematical Logic, Proceedings of Logic Colloquium Hanover
- Françoise Maurin, Ehrenfeucht games and ordinal addition, 1998. (We show in this paper that the theory of ordinal addition of any fixed ordinal ω^α, with α less than ω^ω, admits a quantifier elimination. This in particular gives a new proof for the decidability result first established in 1965 by R. Büchi using transfinite automata. Our proof is based on the Ehrenfeucht games, and we show that quantifier elimination go through generalized power.