# Equality and Quantifiers

I am new to Mathematica and to Math. I do not study math in English, so please bear with me as I try to state my questions..

This is what I am trying to "solve":

$$∃!x : A(x) ⇔ ∃x : ¬A(x)$$

In words: "Is 'there is exactly one x for which the assertion A is true' equivalent to 'there is at least one x for which assertion A is not true' ?"

Referred to that I have questions:

• Is this something you would normally do with Mathematica?
• In the program I opened a "New Notebook" and typed in:

Equivalent[!Exists[x, a[x]], Exists[x, !a[x] ]]


and it - surprise! ;) - did not work. What have I done wrong ?

• How would the answer look like ?
• As far as I remember math quantifiers, "there i exactly one x..." is not one of them. They are either "For all x..." or "There is at least one x...". What You are looking for is a uniqueness quantification, but there's no such built-in function in Mathematica. Besides, negation of Exists[ ] results in ForAll[ ]. Commented Dec 13, 2013 at 15:07
• @WojciechSitkiewicz I guess it could be written as Exists[x, a[x]] && ForAll[{x,y}, a[x] && a[y] , x==y] or so
– ssch
Commented Dec 13, 2013 at 16:09

Based on ssch suggestion I have come up with a following code:

Equivalent[Exists[x, a[x]] && ForAll[{x, y}, a[x] && a[y], x == y],
Exists[x, ! a[x]]] // TautologyQ


False

Actually, ∃! is a standard for "there exists a unique ..." . However, the proposition is false. Consider A(x) where x is greater than 5. There exists lots of x for which x<=5. And surely there is not a unique x, for x>5.

To express ∃! in Mathematica one needs

Exists[x, A[x]] && ForAll[{a, b}, A[a] && A[b] \[Implies] a == b]


Then Mathematica can resolve

In[98]:= Equivalent[
Exists[x, A[x]] && ForAll[{a, b}, A[a] && A[b] \[Implies] a == b],
Exists[x, Not[A[x]]]] // TautologyQ

Out[98]= False


After doing this, I see that the full answer has already been provided.