Message Boards Message Boards

1
|
8514 Views
|
8 Replies
|
11 Total Likes
View groups...
Share
Share this post:

Prove 1 == 0 in Wolfram Language

Posted 5 years ago

Consider the following code:

step1 = Exists[x, x \[Element] Complexes, x^2 + 1 == 0];
    Resolve[step1]
    Reduce[step1, x]
    FullSimplify[step1, x]
    FindInstance[step1, x, Complexes]

giving

True
True
True
{{x -> 0}}

Telling us that 1==0 and True==False.

Inactivate[Evaluate@step1[[3]], Equal] /. x -> 0
Activate[%]

giving

1 == 0
False

Voila!

8 Replies
Exists[x, x \[Element] Complexes, x^2 + 1 == 0]

evaluates (with some prodding) to True. Then FindInstance[True, x] finds an instance of the variable x that makes True true.

POSTED BY: Gianluca Gorni

Paradox: Nothing can make False true, but False makes everything true. Go figure.

POSTED BY: Daniel Lichtblau

The variable x inside the quantifier is local to the quantifier. It is not the same as the global variable x specified in FindInstance. The statement

Exists[x, x \[Element] Complexes, x^2 + 1 == 0]

does not have any free variables. It is a true sentence, so the input to FindInstance is equivalent to FindInstance[True, x]. True is satisfied by any value of x, in particular by x->0.

A quantifier variable is bound to the nearest enclosing quantifier. For instance, the formula form below contains four different variables named x, one free, three bound to different quantifiers. Variables specified in the second argument of FindInstance are interpreted as free variables of its first argument.

In[1]:= form = x==17 && ForAll[x, x>2, x^2>4 && Exists[x, x>0, x<1 && ForAll[x,
x<0, x^2>0]]];

In[2]:= FindInstance[form, x]
Out[2]= {{x -> 17}}
POSTED BY: Adam Strzebonski

Thanks Adam, that explains it. It was not appropriate for me to use FindInstance in that way in that case. However it does show that form of Exists in the details for FindInstance, but the example does have free variables. And the Exists page does say that the x variable is localized. It's connecting a slightly subtle point across pages. It might help if there was a note in the Details section of FindInstance that stated that variables should be free variables in expr but not the localized variable x.

I don't even understand how to interpret the intended semantics of

 FindInstance[
  Exists[x, x \[Element] Complexes, x^2 + 1 == 0], x, Complexes]

but certainly the output {{x -> 0}} is bizarre.

Hope you've reported this to WRI tech support!

POSTED BY: Murray Eisenberg
POSTED BY: Frank Kampas
In[1]:= FindInstance[x^2 + 1 == 0, x]

Out[1]= {{x -> -I}}
POSTED BY: Frank Kampas

I know what the correct mathematical answer is, but I was practicing using Exists and FindInstance, which should also work.

Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Reply Preview
Attachments
Remove
or Discard

Group Abstract Group Abstract