Re: FindInstance puzzler
- To: mathgroup at smc.vnet.net
- Subject: [mg83759] Re: FindInstance puzzler
- From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
- Date: Fri, 30 Nov 2007 05:11:36 -0500 (EST)
- References: <20071129005504.373$Gf_-_@newsreader.com> <B8B71A2C-8F6D-42AB-9304-93AA3A41103B@mimuw.edu.pl>
> Resolve[ForAll[y, Element[y, Integers], Exists[x, Element[x,
> Integers],
> x^2 == y]]]
>
> ForAll[y, Element[y, Integers],
> Exists[x, Element[x, Integers], x^2 == y]]
>
> One could argue that this ought to be trivial since Integers are
> Reals and the answer for Reals is False. Indeed, this particular
> case and similar ones could be implemented in Mathematica by simply
> replacing Integers everywhere with Reals. If the answer is False for
> Reals so it must be for Integers.
I was very careless when I wrote the above (or my brain had ceased to
work). Of course the fact that we know that not every real has a real
square root it does not follow that not integer has an integer square
root. What does follow is that not every real has an integer square
root (otherwise it would have a real square root) but this can't be
determined by Resolve:
Resolve[ForAll[y, Element[y, Reals],
Exists[x, Element[x, Integers], x^2 == y]]]
ForAll[y, Element[y, Reals],
Exists[x, Element[x, Integers], x^2 == y]]
This still illustrates my point (arithmetical properties of integers
are hard to deal with for computers).
Andrzej Kozlowski
On 29 Nov 2007, at 17:58, Andrzej Kozlowski wrote:
>
> On 29 Nov 2007, at 14:55, David W. Cantrell wrote:
>
>> [Message also posted to: comp.soft-sys.math.mathematica]
>>
>> Andrzej Kozlowski <akoz at mimuw.edu.pl> wrote:
>>> On 28 Nov 2007, at 05:40, Adam Strzebonski wrote:
>>>
>>>> Andrzej Kozlowski wrote:
>>>>> *This message was transferred with a trial version of
>>>>> CommuniGate(tm) Pro*
>>>>> On 27 Nov 2007, at 17:05, Andrzej Kozlowski wrote:
>>>>>> Reduce[2*y*I*Sqrt[x] + 2*(y - I*Sqrt[x]) == 0, {x, y}, Reals]
>>>>> This should have been:
>>>>> In[17]:= Reduce[2*y*I*Sqrt[x] + 2*(y - y*I*Sqrt[x]) == 0,
>>>>> {x, y}, Reals]
>>>>> During evaluation of In[17]:= Reduce::nddc:The system 2 \
>>>>> [ImaginaryI] Sqrt[x] y+2 (y-\[ImaginaryI] Sqrt[x] y)\[LongEqual]0
>>>>> contains a nonreal constant 2 \[ImaginaryI]. With the domain \
>>>>> [DoubleStruckCapitalR] specified, all constants should be real. >>
>>>>> Out[17]= Reduce[2*I*Sqrt[x]*y + 2*(y - I*Sqrt[x]*y) == 0,
>>>>> {x, y}, Reals]
>>>>> but it other than that it does not change anything. Note that:
>>>>> Reduce[Simplify[2*y*I*Sqrt[x] + 2*(y - y*I*Sqrt[x]) == 0], {x, y},
>>>>> Reals]
>>>>> y==0
>>>>> What I really mean tto say is: wouldn't it be a litte better to
>>>>> first automatically apply Simplify in such situation to see if
>>>>> the =
>>>
>>>>> I's could be got rid of?
>>>>> Andrzej Kozlowski
>>>>
>>>> It think this behaviour is correct. Reduce should disallow any non-
>>>> real
>>>> subexpressions when the domain Reals is specified. The fact that it
>>>> cannot detect potentially non-real functions that cancel during
>>>> input
>>>> processing is more problematic, but hard to avoid.
>>>>
>>>> Adam Strzebonski
>>>
>>> Well yes, but... There are plenty of real valued functions for which
>>> it is hard to give an explicit expression not involving complex
>>> numbers.
>>
>> Agreed, but the function below is not a very good example since
>> it's just
>> Sqrt[Abs[Sin[x]]]. Does anyone know how to get Mathematica to make
>> that
>> simplification when x is real?
>>
>>> For example, the function
>>>
>>> g[x_] := Sec[(1/2)*Arg[I*Sin[x]]]*(Sqrt[I*Sin[x]] -
>>> I*Sqrt[Abs[Sin[x]]]*Sin[(1/2)*Arg[I*Sin[x]]])
>>>
>>> is always real valued for real x. In fact, Mathematica is able to
>>> show
>>> that this is so:
>>>
>>> ComplexExpand[Im[g[x]], TargetFunctions -> {Re, Im}]
>>> 0
>>>
>>> Moreover, Mathematica can even solve (well, almost) the following:
>>>
>>> Reduce[g[x] == 1 && Element[x, Reals], x]
>>>
>>> Reduce::ztest:Unable to decide whether numeric quantities {1/8 (-8
>>> tan-1(1-Power(<<2>>))-=CF=80)} are equal to zero. Assuming they
>>> are. >>
>>>
>>> Element[C[1], Integers] && (x == (1/2)*(4*Pi*C[1] - Pi) || x ==
>>> (1/2)*(4*Pi*C[1] + 3*Pi) || x == (1/2)*(4*Pi*C[1] + Pi))
>>>
>>> But even so, it won't even touch:
>>>
>>> Reduce[g[x] == 1, x,Reals]
>>
>> OTOH, Mathematica (at least version 5.2) does the following without
>> complaint:
>>
>> In[6]:= Reduce[Sqrt[Abs[Sin[x]]] == 1, x, Reals]
>>
>> Out[6]= Element[C[1], Integers] && (x == -(Pi/2) + 2*Pi*C[1] ||
>> x == (3*Pi)/2 + 2*Pi*C[1] || x == Pi/2 + 2*Pi*C[1])
>>
>> That result is obviously equivalent to just
>>
>> Element[C[1], Integers] && x == Pi/2 + Pi*C[1].
>>
>> I would guess that there might be an easy way to get
>> Mathematica to simplify Out[6] to something like
>> Element[C[1], Integers] && x == Pi/2 + Pi*C[1]. Is there such a way?
>>
>> David W. Cantrell
>
> I don't think there is any "general" way to "simplify" expressions
> like this because they involve integers (C[1]) and algorithms on
> which "symbolic deduction" is based, such as quantifier elimination,
> CAD etc, work over the reals (or the complexes). Of course some
> "simplifications" of this kind can be implemented using
> "heuristics" (and indeed, are in other places in Mathematica) but as
> this would be of limited use it seems to me unlikely to have been
> done.
>
> In a way it is somewhat counter-intuitive that "deduction" is so
> much harder when integers are involved rather than reals or
> complexes. Here is an illustration (although it has almost nothing
> to do with your question, it is meant to illustrate that "deduction"
> with integers is "hard" for computer programs)
>
> Mathematica can do this:
>
> Resolve[ForAll[y, Element[y, Reals], Exists[x, Element[x, Reals],
> x^2 == y]]]
> False
>
> and it also can do this:
>
> Resolve[ForAll[y, Element[y, Reals], Exists[x, Element[x, Complexes],
> x^2 == y]]]
> True
>
> But, perhaps surprisingly, it cannot do this:
>
> Resolve[ForAll[y, Element[y, Integers], Exists[x, Element[x,
> Integers],
> x^2 == y]]]
>
> ForAll[y, Element[y, Integers],
> Exists[x, Element[x, Integers], x^2 == y]]
>
> One could argue that this ought to be trivial since Integers are
> Reals and the answer for Reals is False. Indeed, this particular
> case and similar ones could be implemented in Mathematica by simply
> replacing Integers everywhere with Reals. If the answer is False for
> Reals so it must be for Integers. But as this would only work for a
> small subset of problems of this type it was (probably) felt not
> worth implementing.
> In your case, of course, the problem is not equivalent to one about
> Reals and, although something probably could be done to deal with
> such simple cases, I think it was also felt that the lack of general
> methods does not make doing this worth the effort.
> (Of course I am only guessing and it may even turn out that there is
> some clever way to do what you want. )
>
> Andrzej Kozlowski