Re: problem with reduce

*To*: mathgroup at smc.vnet.net*Subject*: [mg100365] Re: [mg100347] problem with reduce*From*: Andrzej Kozlowski <akoz at mimuw.edu.pl>*Date*: Tue, 2 Jun 2009 06:41:39 -0400 (EDT)*References*: <200906011111.HAA26170@smc.vnet.net>

First the reason. This is an example of what is called "quantifier elimination" (in this case one eliminates the quantifier Exists). Algorithms for quantifier elimination exist only for polynomial formulas with real number coefficients (or more generally with coefficients in real closed fields). This was first shown by the Polish logician Alfred Tarski, although modern algorithms are much faster. However, there is no algorithm for quantifier elimination over the integers. It's not just that one is now known, we know that there cannot be any general algorithm. Mathematica can, however, do this in certain special cases by using heuristic methods. However, since everything in your system is linear, you can simply eliminate quantifiers over the reals and then add Simplify using the assumption that everything is an integer: sols=Simplify[Reduce[ Exists[{C[1], C[2]}, Element[{C[1], C[2]}, Reals] && C[1] >= 0 && C[2] >= 0 && i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] && jP == j - C[2]], {iP, jP}, Backsubstitution -> True], Element[C[1] | C[2] | i | j | N | iP | jP, Integers]] (N == 1 && i == 1 && iP == 1 && j == jP) || (N > 1 && 1 <= i <= N && iP == N && i + j == jP + N) Lets now try to check if these really satisfy the original conditions. First, the original conditions (over the Integers) were: cond = Exists[{C[1], C[2]}, Element[{C[1], C[2]}, Integers] && C[1] >= 0 && C[2] >= 0 && i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] && jP == j - C[2]]; It is easy to verify that the first solution N == 1 && i == 1 && iP == 1 && j == jP is a solution because now quantifier elimination over the integers has become trivial: Reduce[cond /. ToRules[sols[[1]]]] True In fact, you can simply what C[1] and C[2] must be, treating the condition as a linear system of equations and inequalities: Reduce[C[1] >= 0 && C[2] >= 0 && i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] && jP == j - C[2] && sols[[1]], {C[1], C[2], iP, jP}, Reals, Backsubstitution -> True] N == 1 && i == 1 && C[1] == 0 && C[2] == 0 && iP == 1 && jP == j From which you can see that C[1] and C[2] are both zero, and zero is, of course, an integer. So we are sure we have one solution: N == 1 && i == 1 && iP == 1 && jP==j In the other case, Reduce still cannot prove that a solution exists if we try quantifier eleimination, but you can simply again consider everything as a linear system and find C[1] and C[2]: Reduce[C[1] >= 0 && C[2] >= 0 && i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] && jP == j - C[2] && sols[[2]], {C[1], C[2], iP, jP}, Reals, Backsubstitution -> True] N > 1 && 1 <= i <= N && C[1] == i - 1 && C[2] == N - i && iP == N && jP == i + j - N This again shows you that provided both N and i are integers, C[1] and C[2] will also be integers, so the system has actually been solved over the integers. So the second solution you want can be written Element[N, Integers] && Element[i, Integers] && N > 1 && 1 <= i <= N && iP == N && jP == i + j - N Andrzej Kozlowski On 1 Jun 2009, at 20:11, olfa wrote: > Hi mathematica community, > I have to solve this example > In[88]:= Reduce[Exists[{C[1], C[2]}, > Element[{C[1], C[2]}, Integers] && C[1] >= 0 && C[2] >= 0 && > i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] && > jP == j - C[2]], {iP, jP}, Backsubstitution -> True] > > During evaluation of In[88]:= Reduce::nsmet: This system cannot be > solved with the methods available to \ > Reduce. >> > > I have observed that when I remove Element[{C[1], C[2]}, Integers] > && C > [1] >= 0 && C[2] >= 0 like that: > In[89]:= Reduce[ > Exists[{C[1], C[2]}, > i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] && > jP == j - C[2]], {iP, jP}, Backsubstitution -> True] > > it gives me an output which is: > > Out[89]= iP == N && jP == i + j - N > > > I need to keep the information that Element[{C[1], C[2]}, Integers] && > C[1] >= 0 && C[2] >= 0 but reduce tells me that it cannot solve this > system. why and how to deal with this problem? > thank you. >

**References**:**problem with reduce***From:*olfa <olfa.mraihi@yahoo.fr>