Understanding the logic of "unique existence" proofs

Question

I am learning the lean/mathlib system for automatically checking proofs, and was genuinely surprised that to prove unique existence, the structure there forces us to separately prove these properties:

• uniqueness
• existence

Surely, uniqueness already implies existence?

---

Example

Consider the condition $x-2=3.$

First, I simply try $x=5$ without worrying about how I found this "witness". Since $x=5 \implies x-2=5-2=3,$ I have shown that the condition is satisfied by this solution. I can see that this shows the existence of a solution, but doesn't show there are no more.

Next, I apply a series of algebraic manipulations on the given condition, and I may arrive at a set of solutions. I arrive at a single solution: $x-2=3 \implies x-2+2=3+2 \implies x=5.$ If the condition were a quadratic, then the algebraic manipulations would lead me to two solutions.

Hence, I have shown that the condition leads to a unique solution (which automatically proves existence), and I didn't need to separately show existence and uniqueness.

1. For this example, am I correct that proving existence is redundant?
2. If so, then is this just for such simple cases?

Answer 1

Another example

Consider the even numbers, $2\mathbb Z:=\{\ldots,-4,-2,0,2,4,\ldots\}.$ I can easily prove that if there exists a multiplicative unit in this set, then it is unique:

Let $1'$ and $1''$ be multiplicative units in $2\mathbb Z,$ i.e. for all $x\in\mathbb Z$ we have $1'\cdot x=x\cdot 1'=x$ and $1''\cdot x=x\cdot 1''=x.$ Then $1'=1'\cdot 1''=1'',$ i.e. a multiplicative unit is unique.

But I haven't here proved that there is such an element in $2\mathbb Z.$ Indeed, there is actually no such element in $2\mathbb Z.$

Answer 2

I think 'uniqueness' is a bit ambiguous. Some will say that uniqueness means 'exactly one', whereas others will say it means 'at most one'. In math, we typically mean the latter, but I think our intuition would go with the former. But yeah, if it's the latter, then you'll still need to prove existence, since 'at most one' is consistent with there being no solutions at all.

Answer 3

Don Hatch left a comment that I agree with: my initial response blurred the distinction between:

• There exists at most one solution.

• There exists a unique solution.

I regard this as a mistake on my part. I have edited my answer to correct this mistake.

---

Consider the statement:

$$x - 2 = 3 \implies x = 5. \tag1 $$

(1) above, which is a true statement, merely asserts that if a solution exists then it must be unique. However, (1) above does not assert that any solution exists.

Worded differently, (1) above asserts that there is at most one solution, but does not assert that there is at least one solution.

More explicitly, (1) above asserts that if there exists a value $~x = x_0~$ that satisfies the equation $~x-2 = 3,~$ then the only possible value for $~x_0~$ is the value $~x_0 = 5.~$

Now consider the statement:

$$x = 5 \implies x - 2 = 3. \tag2 $$

(2) above, which is also a true statement, merely asserts that there exists at least one solution. However, (2) above does not assert that there is at most one solution.

More explicitly, (2) above asserts that if $~x_0 = 5,~$ then $~x = x_0~$ is a satisfying value to the equation $~x - 2 = 3.~$

However, (2) above does not exclude the possibility that there might be other satisfying values $~x_0~$ to the equation $~x - 2 = 3,~$ besides the value $~x_0 = 5.$

---

As other responses have discussed, there is ambiguity around the word uniqueness.

Prior to my editing this answer, I (in effect) indicated that statement (1) above is asserting uniqueness. My intention however, was that statement (1) is asserting that there is at most one solution.

After thinking about it, my (subjective) view is that asserting that an equation has a unique solution is equivalent to making both of the following assertions.

• The equation has at most one solution.

• The equation has at least one solution.

Answer 4

to prove unique existence, the structure there forces us to separately prove these properties:

• uniqueness
• existence

More accurately, the conjunction of the properties

1. at most one; i.e., not more than one (conditional uniqueness)
2. at least one; i.e., existence

is equivalent to the property

• exactly one, i.e., uniqueness ("unique existence" basically means this).

Surely, uniqueness already implies existence?

Yes.

Example

Consider the condition $x-2=3.$

I arrive at a single solution: $x-2=3 \implies x-2+2=3+2 \implies x=5.$

Here, you've proven that there is at most one solution (Property 1: there is a unique solution, if it exists). Note that this step by itself shows only that $x=5$ is a candidate solution, which may turn out to be extraneous, in which case the given condition actually has no solution.

Note also that in this part, uniqueness has not actually been proven.

Since $x=5 \implies x-2=5-2=3,$ I have shown that the condition is satisfied by this solution. I can see that this shows the existence of a solution

Here, you've proven that there is at least one solution (Property 2: there exists a solution).

So, I have shown that the condition leads to a unique solution (which automatically proves existence), and I didn't need to separately show existence and uniqueness.

More simply: your previous two steps together entails the required conclusion: that there is exactly one solution (there is a unique solution).

1. For this example, am I correct that proving existence is redundant?

Your proof of uniqueness already contains a proof of existence.

2. If so, then is this just for such simple cases?

No.

If the condition were a quadratic, then the algebraic manipulations would lead me to two solutions.

Manipulating a quadratic equation needn’t give rise to two (real) solutions: the manipulation $$x^2+2=0\implies (x^2+2)(x^3-4x)=0\implies x=-2,0,2$$ has created 3 solutions (all extraneous).

---

Addendum

I disagree that between "exactly one" and "at most one", the word "unique" means the latter (and I cannot find any source to substantiate this claim). After all, $∃_{=1}$ is called the uniqueness quantifier, and every element of a function's domain is said to have a unique mapping.

Further counteracting any unequivocal claim that in mathematical writing the word "unique" doesn't mean "exactly one": 1, 2, 3, 4.

Answer 5

Your particular example is special in that linear equations always have (existence) a single (unique) answer. But of course, things can be more complicated:

If $x$ is a real number and it has a multiplicative inverse, that inverse is unique.

Suppose that $y$ and $z$ are each multiplicative inverses of $x$. Then $$y = y \cdot 1 = y \cdot (xz) = (yx)\cdot z = 1 \cdot z = z,$$ so that $$y = z,$$ with the proviso that we already know that $1$ is the multiplicative identity and that multiplication of real numbers is associative.

But of course, not every real number has a multiplicative inverse.

Many times, an existence proof has non-reversible steps (or at least, steps that are not reversible in a unique way). How do you differentiate between your steps showing that $x-2=3$ has a unique solution and that $x^2 = 9$ does not? Ok, we all know that taking square roots introduces a complication (i.e. they are not precisely reversible), but in general, many problems are solved by nonreversible processes. Showing that $x^2 = 9$ has a solution only requires me to exhibit $x = 3$. But of course, we know that solution is not unique.

As a more "regular" algebraic situation, consider the two system of equations $$\begin{align*} x + y &= 5\\ x-y &= 3\\ \end{align*}$$ which has only the solution $x = 4, y = 1$.

However, the system $$\begin{align*} x + y &= 5\\ 2x+2y &= 10\\ \end{align*}$$ also has $x = 4, y = 1$ as a solution, along with infinitely many others. The person who solves the first system might choose a solution path that happens to prove existence and uniqueness at the same time. However, I can solve the first system by simply exhibiting $(4,1)$ as a solution and then claiming that since the lines defined by the system have distinct slopes, they must intersect in only one point. That is as valid of a proof of existence and uniqueness as going through the more typical algebra to deduce $(4,1)$ is the only solution.

Answer 6

Uniqueness implies existence in everyday parlance, but not in mathematics.

This is awkward to speak about in ordinary natural language, because any obvious phrasing of the uniqueness property already implicitly presumes existence. For example, if someone says that for a given constant $a$, $ax + 1 = 0$ “has a unique real solution”, removing the word “unique” gives you a statement of existence of a solution. Even just the definite article “the” carries an implicit assumption of existence. This is related to how we often tend to have trouble accepting vacuous statements as true: Gricean maxims are essentially one big licence to assume “you probably wouldn’t tell me this if it were useless” (while talking about non-existent things is presumed useless), so an ordinary-language claim like “all unicorns are blue” is usually taken to imply unicorns exist, and “the solution is unique” is taken to imply a solution exists.

But in formal logic, you can actually talk about uniqueness without having it imply existence. That is to say, you can establish that any two elements of the set are equal without proving the set contains any elements at all – and in fact it may very well be actually empty.

Consider this definition: a function $f : X \to Y$ is weakly constant if and only if

$$ \forall a \in X : \forall b \in X : f(a) = f(b) $$

This is a statement of uniqueness of the… umm… err… uniqueness of any potential value in the range of $f$. But it will be also (vacuously) true if the range of $f$ is empty, which happens when $X$ is empty, and therefore $f$ is an empty function. (You think it’s wrong? Then show us the $a$ and $b$ for which $f(a) \ne f(b)$.) A definition of a constant function implying uniqueness and existence would be

$$ \exists a \in X : \forall b \in X : f(a) = f(b) $$

under which an empty function is not considered constant.

Answer 7

Surely, uniqueness already implies existence?

No. Uniqueness and existence are independent of one another.

Existence and uniqueness are often stated in the form:

$~~~~~~\exists a: [P(a) \land \forall b:[P(b)\implies a=b]] $

Equivalently and more useful in this context, it can be restated as the conjunction:

$~~~~~~\forall a,b: [P(a) \land P(b) => a=b]~~\land ~~ \exists a: P(a) $

The leftmost term (uniqueness) means there exists at most one $x$ such that $P(x)$.

The rightmost term (existence) means there exists at least one $x$ such that $P(x)$.

Each term is independent of the other, e.g. it is possible that there exist at most one $x$ such that $P(x)$ is true (uniqueness holds), and there exists no $x$ such that $P(x)$ is true (existence does not hold).

Answer 8

The idea that uniqueness doesn't imply existence makes a little more sense when we have a family of equations where some have solutions and some don't, and we want to say that for the ones that do have a solution it is unique. This is often important in systems of differential equations as well as in linear algebra, but as a simple example we can say that the solutions to $\frac{1}{1 + e^{-x}} = A$ are unique, since the left-hand side is an injective function.

It is true that the more exact language would be to say that solutions are unique where they exist, but when it comes to the proofs themselves a typical uniqueness proof starts by assuming the existence of a solution, and then showing that there cannot be a second distinct solution, which means we wind up proving $\textrm{solution exists} \implies \textrm{solution is unique}$. As a result, the proof is still true in the case where there are no solutions, because $F \implies T$ is taken to be true.

Answer 9

Surely, uniqueness already implies existence?

In the context of binary relations on a set, you can have uniqueness without existence. Consider the following for example:

$~~~~~~X=\{0,1,2\}$

$~~~~~~f=\{(1,0), (2,1)\} \subset X^2$

By inspection, we have uniqueness:

$~~~~~~\forall a,b,c \in X:[(a,b)\in f~ \land ~(a,c)\in f \implies b=c]$

We do not, however, have existence:

$~~~~~~\neg \forall a\in X: \exists b\in X: (a,b) \in f$

$~~~~~~a=0~$ being the counter-example

Answer 10

Problem: What is the largest real number?

Let $z$ denote the largest real number, that is, $z\geq x$ for all real $x$. Clearly, $z$ is unique: If there is another $\hat{z}$ which would be the largest real number, we have $x\leq z$ and $x\leq\hat{z}$ for all $x\in\mathbb{R}$. Thus, $z\leq\hat{z}$ and $\hat{z}\leq z$. and Hence, $z=\hat{z}$.

Hence, we have shown uniqueness, but not existence.

---

Your example may be a bit confusing because it is so simple, since by very few manipulations you arrive at $x=5$, which obviously exists and is unique.

I should also note that in many cases (e.g., solutions of diferential equations), uniqueness is actually much easier to show that existence. So it is not uncommon for math courses to prove uniqueness first.