Prove 1 == 0 in Wolfram Language

Ideas
1

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!

1 Like
2

In[1]:= FindInstance[x^2 + 1 == 0, x]

Out[1]= {{x -> -I}}
1 Like
3

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

4

In[3]:= FindInstance[step1, x, Booleans]

Out[3]= {}
5

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!

1 Like
6

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}}
6 Likes
7

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.

2 Likes
8

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.

9

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