the logic of "unique exists"

Stream: new members

[rzeta0]

Just started the section of Mechanics of Proof introducing "unique exists" proofs ∃!.

I am surprised by the logic of such proofs. It seem two things need to be proved:

• a "witness" so confirm there exists, say a
• a derivation that if any variable, say x, meets the conditions, it must be that x=a

My beginner brain tells me the first is redundant. Surely using agreed mathematical derivation steps to find x=a does both? Both meaning, show there exists, and what it is. It it were not unique, then the derivation would result in multiple solutions, eg for a quadratic equation have two solutions.

What am I missing?

[Henrik Böving]

Consider:

def f (x : Nat) : Prop := False

If you want to prove there exists exactly one n : Nat such that f n holds and you only do the second step you would get two nats n m : Nat and hn : f n hm : f m and be asked to prove n = m. Obviously this is false but hn : f n is the same as False so i have a proof of false and can thus close the goal, proving (according to your definition) that there exists exactly one n such that f n.

So no, it's not at all redundant

[Scott Carnahan]

If you don't show existence, then you have only showed that the set of satisfactory objects has size zero or one.

[Etienne Marion]

Another example, imagine you want to prove that there exists a unique prime and even number larger than 3. If x is such a number, it is prime and even so that you have x=2. But in fact such a number does not exist, you only prove that IF it exists, it would be equal to 2.

[Edward van de Meent]

rzeta0 said:

Surely using agreed mathematical derivation steps to find x=a does both?

in a sense, you are right. However, the devil lies in the details. i think in general, the "agreed mathematical derivation steps" for ∃! a, P a are of the form "supposing P a, we must have that Q a, and Q a indeed implies P a." in other words, the way this is typically done uses P a <-> Q a, where Q a eventually becomes something like a = 37 or the like, for which proving that ∃! a, Q a is highly trivial.

[Edward van de Meent]

so basically, you are right, except that "agreed mathematical derivation steps" in this context (for proving something like ∃! a, Q a) is different from those for just showing existance.

[Dan Velleman]

rzeta0 said:

Surely using agreed mathematical derivation steps to find x=a does both?

When proving a statement of the form ∃ x, P x, it is important to distinguish between (a) the steps you use to find x = a and (b) the steps you use in the proof of ∃ x, P x. Often the way you figure out this kind of proof is that you first, on scratch paper, assume that P x is true and then try to deduce from this what x must be. Sometimes you end up deducing an equation x = a. The steps in that derivation are what I called (a) above, and those steps do not appear in the proof of ∃ x, P x. Rather, to prove ∃ x, P x you simply start with use a (no need to explain how you came up with a) and then your goal is to prove P a--this is what I called (b) above. The proof of P a is often not the same as the steps in (a). For example, if P x is an equation involving x, then to prove P a you just have to verify that a satisfies the equation (perhaps just by doing some arithmetic), you don't have to solve the equation.

If you are trying to prove ∃! x, P x, rather than ∃ x, P x, then, as you described, the second half of the proof is to show that if you have any x such that P x, then you must have x = a. This is where you can use your reasoning from (a).

[rzeta0]

I'm struggling to understand all the replies.

So let's bring this to life with an example task.

---

Task
Show $\exists ! x : x -2 = 3$ for $x \in \mathbb{R}$. That is, show there exists a a unique $x$ such that $x-2=3$.

Solution
By applying agreed logical steps, in this case, adding 2 to both sides of the equality, and then simplifying using arithmetic, I arrive at $x=5$.

The steps have:

• led to me a single solution, a unique solution
• and the steps have identified what that solution is

I didn't need to "show there exists" separately. Where am I missing the first of the two steps, to "show there exists"?

---

Thoughts
Is it the case that with some problems, particularly the simple algebra ones I've seen, the derivation is sufficient as it shows both existence and what the value is - but that more sophisticated objects might need separate proofs?

I suspect there may be tasks where:

• IF there exists a solution, THEN it must be x=3
• There exists a solution (thus resolving the IF above).

I do value your replies, especially if they're aimed at beginners like me.

[Dan Velleman]

Here's one more example: Suppose you are trying to prove ∃! (x : Real), (x ^ 2 + x - 2) / (x ^2 - 1) = 1 (warning: this statement is actually false). You would probably start by solving the equation, and your first step might be to multiply through by x ^ 2 - 1, to get x ^2 + x - 2 = x ^ 2 - 1. Now you can cancel an x ^ 2 from both sides to get x - 2 = -1, and then add 2 to both sides to get x = 1. Perhaps you think the proof is done: you got a unique solution. But in fact, if you plug x = 1 into the original equation, you get 0 / 0 = 1, which is false. So in fact the equation has no solutions, and the statement is false.

[Eric Wieser]

rzeta0 said:

By applying agreed logical steps, in this case, adding 2 to both sides of the equality, and then simplifying using arithmetic, I arrive at x=5.

Great, you simplified your goal all the way to ∃! x, x = 5; but you still need to do the final step to prove this! While this is trivially true, that's not the same as it being true by definition, so you can't declare you're finished yet.

[rzeta0]

@Dan Velleman in your example, isn't the failure to "follow the agreed logical steps that preserve truth"? That is applying a logical operation "multiply both sides by $x^2 -1$ without declaring that $x^2-1 = 0$ is then excluded going forward ?

[rzeta0]

@Eric Wieser I think i'm getting closer to understanding . SO what is the final step I'm missing once I have ∃! x, x=5?

[Eric Wieser]

You don't "have" ∃! x, x=5, you have a goal of ∃! x, x=5. The things you have are your assumptions.

[Eric Wieser]

You might find it instructive to try and prove some very basic ExistsUnique statements in lean to gain intuition

[Eric Wieser]

if you think the definition is weird, try defining your own version MyExistsUniqu without condition 1, and try to prove the same results to see where things go wrong

[Dan Velleman]

rzeta0 said:

Task
Show ∃!x:x−2=3 for x∈R. That is, show there exists a a unique x such that x−2=3.
Solution
By applying agreed logical steps, in this case, adding 2 to both sides of the equality, and then simplifying using arithmetic, I arrive at x=5.

It depends on what you mean by "I arrive at x = 5." If you mean that you assumed that x - 2 = 3, added 2 to both sides, and deduced that x = 5, then you are not done. All you have shown is that IF x - 2 = 3 THEN x = 5; you still have to verify the reverse: IF x = 5 THEN x - 2 = 3, which you can do by plugging in 5 and verifying that 5 - 2 = 3.

In this case, there is another way to verify the second part: Adding 2 to both sides is reversible: you can subtract 2 from both sides of x = 5 to get x - 2 = 3. In general, if you use reversible steps when you are solving an equation, then you could think of yourself as proving both directions simultaneously--in this case, both IF x - 2 = 3 THEN x = 5 and also IF x = 5 THEN x - 2 = 3. The first of these shows that if anything satisfies the equation then it must be 5, and the second shows that 5 does satisfy the equation. I think this is the source of your confusion: you are assuming that you are going to be using reversible steps when you solve the equation, in which case you're right that you would be simultaneously proving both parts of the exists-unique statement. But you would have to prove that all of your steps are reversible to have a complete proof.

The mistake in my "proof" that ∃! (x : Real), (x ^ 2 + x - 2) / (x ^2 - 1) = 1 is that I used a step that was not reversible. There is nothing wrong with multiplying both sides of the equation by x ^ 2 - 1 to get x ^ 2 + x - 2 = x ^ 2 - 1; you can multiply both sides of an equation by 0 if you want to. However, this step is not reversible. To reverse it, you would have to divide both sides by x ^ 2 - 1, and that's not allowed if x ^ 2 - 1 = 0.

[Dan Velleman]

Here's a relevant theorem:

import Mathlib

theorem exists_unique_of_equiv_equal_witness
    {α : Type} {P : α → Prop} {a : α}
    (h : ∀ x, P x ↔ x = a) : ∃! x, P x := by
  use a
  constructor
  · apply (h a).mpr
    rfl
  · intro y h'
    exact (h y).mp h'

I don't know if there is a theorem like this in Mathlib, but if there is, then if you prove h : ∀ x, P x ↔ x = a, then you could apply the theorem to deduce ∃! x, P x. But notice that to prove ∀ x, P x ↔ x = a, you would probably start with intro x, and then you would have to prove P x ↔ x = a. Since this is an iff statement, you have to prove both directions. If you use logical steps to convert P x into x = a, you need to make sure those steps are reversible.

[rzeta0]

I think we're zooming into the root cause of my confusion:

Dan Velleman said:

It depends on what you mean by "I arrive at x = 5." If you mean that you assumed that x - 2 = 3, added 2 to both sides, and deduced that x = 5, then you are not done. All you have shown is that IF x - 2 = 3 THEN x = 5; you still have to verify the reverse: IF x = 5 THEN x - 2 = 3, which you can do by plugging in 5 and verifying that 5 - 2 = 3.

I think (i hope!) I am familiar with the idea that to prove $\iff$ I often need to prove both $\implies$ and $\impliedby$. I don't need to if I use reversible steps, eg $P \iff Q \iff R \iff S$ gives me $P \iff S$.

I'm trying to connect this idea to proving "exists a unique" - and the discussion suggests there is indeed a parallel, but I'm not seeing it.

Let me try:

• If I want to prove there exists a solution to $x-2=3$, not necsssarily unique, then I need to prove $x=5 \implies x-2=3$. There may be other solutions, but proving this implication doesn't confirm that, because it only confirms one solutions works.

• If I want to prove there is a unique solution to $x-2=3$, then I need to prove $x-2=3 \implies x=5$ and only $x=5$.

Imho the sequence of logical steps $x-2=3 \implies x-2+2 = 3+3 \implies x=5$ achieves that second bullet point. Note, these need not be reversible steps.

I keep looking at that last bullet and I keep interpreting it as also fulfilling the "there exists" requirement, because it finds $x=5$ which is a solution.

---

Let me try a different task:

Task: Show there exists only two solutions to $(x-1)(x-2)=0$.

Here I've generalised "unique solution" to "only n solutions".

To show there exists a solution, I can take $x=1$ without justifying where i got it, and show $x=1 \implies (x-1)(x-2) =0$.

To show there exist only two solutions I need to follow logical steps: $(x-1)(x-2)=0 \implies (x-1)=0 \lor (x-2)=0 \implies x=1 \lor x=2$. These need not be reversible steps.

Again, the last paragraph shows me there are only two solutions, and because there are two, it covers the case of showing at least one exists aka there exists.

[Yan Yablonovskiy]

@rzeta0 I think one of the issues is conflating what a verification or a proof entails in Lean. It might be the case you are thinking "if i find such an x, and prove any other y for the statement to be true we have y=x" -- this means youve surely witnessed such an x.

As others have pointed out, Lean is an implementation of calculus of constructions -- and as such its very flexible; and it is in fact possible in lean to coerce the elaborator to have the second part be true ASSUMING such an x. But it has not been witnessed yet.

This is also likely a nuance for this stronger version of existence, being that of unique existence.

Edit: Maybe , in terms of math and ignoring Lean details -- you may think of the second one as proving "if it exists, it is unique" rather than "there exists a unique". Because number 2 is not saying it exists and its unique, it simply asks whether, given it exists -- is it unique?

With that in mind, it shouldn't be hard to see why "if it exists, it is unique" doesnt guarantee it does exist.

[Daniel Weber]

rzeta0 said:

I think we're zooming into the root cause of my confusion:

Dan Velleman said:

It depends on what you mean by "I arrive at x = 5." If you mean that you assumed that x - 2 = 3, added 2 to both sides, and deduced that x = 5, then you are not done. All you have shown is that IF x - 2 = 3 THEN x = 5; you still have to verify the reverse: IF x = 5 THEN x - 2 = 3, which you can do by plugging in 5 and verifying that 5 - 2 = 3.

I think (i hope!) I am familiar with the idea that to prove $\iff$ I often need to prove both $\implies$ and $\impliedby$. I don't need to if I use reversible steps, eg $P \iff Q \iff R \iff S$ gives me $P \iff S$.

I'm trying to connect this idea to proving "exists a unique" - and the discussion suggests there is indeed a parallel, but I'm not seeing it.

Let me try:

• If I want to prove there exists a solution to $x-2=3$, not necsssarily unique, then I need to prove $x=5 \implies x-2=3$. There may be other solutions, but proving this implication doesn't confirm that, because it only confirms one solutions works.

• If I want to prove there is a unique solution to $x-2=3$, then I need to prove $x-2=3 \implies x=5$ and only $x=5$.

Imho the sequence of logical steps $x-2=3 \implies x-2+2 = 3+3 \implies x=5$ achieves that second bullet point. Note, these need not be reversible steps.

I keep looking at that last bullet and I keep interpreting it as also fulfilling the "there exists" requirement, because it finds $x=5$ which is a solution.

---

Let me try a different task:

Task: Show there exists only two solutions to $(x-1)(x-2)=0$.

Here I've generalised "unique solution" to "only n solutions".

To show there exists a solution, I can take $x=1$ without justifying where i got it, and show $x=1 \implies (x-1)(x-2) =0$.

To show there exist only two solutions I need to follow logical steps: $(x-1)(x-2)=0 \implies (x-1)=0 \lor (x-2)=0 \implies x=1 \lor x=2$. These need not be reversible steps.

Again, the last paragraph shows me there are only two solutions, and because there are two, it covers the case of showing at least one exists aka there exists.

Consider the same problem of "only two solutions", but now I apply it to "Show there exists only two solutions to $x -1 = 0$" (this is false, of course, there's only one solution).

To show there exists a solution, take $x = 1$, and show $x = 1 \implies x - 1 = 0$

To show there exist only two solutions, one can use the following logical steps: $x - 1 = 0 \implies (x - 1)(x - 2) = 0 \implies x - 1 = 0 \lor x - 2 = 0 \implies x = 1 \lor x = 2$.

Do you see why this argument is invalid? Here the proof of "there exist only two solutions" adds an extraneous solution, and something similar can happen of "exists unique", where the proof can add an extraneous solution from zero to one

[Eric Paul]

I'm just reiterating things that others have said (I think @Henrik Böving said exactly this), but here's an example.

As you said, Lean currently requires you to prove two things

1. There is a witness
2. Anything else that satisfies the condition is equal to the witness

Let's try proving that there exists a unique natural number that is equal to 2 and greater than 2.

import Mathlib

/-
  P states that there exists a unique natural number equal
  equal to 2 and greater than 2
-/
def P : Prop := ∃! (n : ℕ), n = 2 ∧ n > 2

Intuitively, this should not be possible. We can double check that this is not true in Lean:

import Mathlib

/-
  P states that there exists a unique natural number equal
  equal to 2 and greater than 2
-/
def P : Prop := ∃! (n : ℕ), n = 2 ∧ n > 2

-- Prove not `P`
example : ¬P := by
  intro p
  obtain ⟨n, satisfies, _⟩ := p
  omega

So P is false.

Now, what if we only require the second condition: "2. Anything else that satisfies the condition is equal to the witness"
That would mean that we want to prove the following:

import Mathlib

/-
  P_modified states that there exists a natural number `n` such that
  if any natural number `y` is equal to 2 and greater than 2
  it is equal to `n`
-/
def P_modified : Prop := ∃n : ℕ, ∀y : ℕ, y = 2 ∧ y > 2 → y = n

And indeed we can prove this:

import Mathlib

/-
  P_modified states that there exists a natural number `n` such that
  if any natural number `y` is equal to 2 and greater than 2
  it is equal to `n`
-/
def P_modified : Prop := ∃n : ℕ, ∀y : ℕ, y = 2 ∧ y > 2 → y = n

-- Let's prove `P_modified`
example : P_modified := by
  simp [P_modified]

Therefore, just requiring condition two cannot be equivalent to requiring both conditions because we saw we could prove just condition two but not both. Written in lean, we can prove that P and P_modified are not equivalent:

import Mathlib

/-
  P states that there exists a unique natural number equal
  equal to 2 and greater than 2
-/
def P : Prop := ∃! (n : ℕ), n = 2 ∧ n > 2

/-
  P_modified states that there exists a natural number `n` such that
  if any natural number `y` is equal to 2 and greater than 2
  it is equal to `n`
-/
def P_modified : Prop := ∃n : ℕ, ∀y : ℕ, y = 2 ∧ y > 2 → y = n

-- Prove not `P`
theorem not_P : ¬P := by
  intro p
  obtain ⟨n, satisfies, _⟩ := p
  omega

-- `P` and `P_modified` are not equivalent
example : ¬(P ↔ P_modified) := by
  simp [not_P, P_modified]

[Dan Velleman]

rzeta0 said:

• If I want to prove there exists a solution to $x-2=3$, not necsssarily unique, then I need to prove $x=5 \implies x-2=3$. There may be other solutions, but proving this implication doesn't confirm that, because it only confirms one solutions works.

Another way to look at it: This proves that there at least one solution.

• If I want to prove there is a unique solution to $x-2=3$, then I need to prove $x-2=3 \implies x=5$ and only $x=5$.

Another way to look at it: This proves that there is at most one solution. If you want to show that there is exactly one solution, you have to do both: show that there is at least one, and also at most one.

Imho the sequence of logical steps $x-2=3 \implies x-2+2 = 3+3 \implies x=5$ achieves that second bullet point. Note, these need not be reversible steps.

Right.

I keep looking at that last bullet and I keep interpreting it as also fulfilling the "there exists" requirement, because it finds $x=5$ which is a solution.

But finding $x=5$ doesn't prove that $x=5$ is a solution.

---

Let me try a different task:

Task: Show there exists only two solutions to $(x-1)(x-2)=0$.

Do you mean at most two solutions or exactly two solutions?

Here I've generalised "unique solution" to "only n solutions".

To show there exists a solution, I can take $x=1$ without justifying where i got it, and show $x=1 \implies (x-1)(x-2) =0$.

This shows that there is at least one solution.

To show there exist only two solutions I need to follow logical steps: $(x-1)(x-2)=0 \implies (x-1)=0 \lor (x-2)=0 \implies x=1 \lor x=2$. These need not be reversible steps.

This shows that there are at most two solutions. Taken together, your two steps show that there is either one solution or two solutions.

Again, the last paragraph shows me there are only two solutions, and because there are two,

But you haven't proven that there are two. You proved that 1 is a solution, but you haven't yet proven that 2 is a solution. If you add that step, then you will have shown that there are exactly two solution.

[Edward van de Meent]

assuming you take for granted that 1 = 2 is false.

[rzeta0]

@Dan Velleman - we're getting closer ..

• If I want to prove there is a unique solution to x−2=3, then I need to prove x−2=3⟹x=5 and only x=5. 

Another way to look at it: This proves that there is at most one solution.

Why does it only prove there is at most one solution?

Perhaps understanding this will crack my problem?

---

I've done wider reading and found two comments that I think are relevant:

"Note that you can show uniqueness without showing existence." (src)

I'm having trouble with this. How can a solution be unique but not exist?

"If there was a specific solution for x  in the existence part, you do not need to show that y equals that specific x" (src)

This seems to support my original thinking that for simple tasks like "show there is a unique solution to x-2=3" it is possible to find a specific solution and we "do not need to show y, a possible other solution, equals x".

---

I will continue to do wider reading on this as this has revealed a gap in my maths understanding. I can't believe I have such a gap given I've taken an amateur enthusiast interest in maths for 20+ years !!

[Daniel Weber]

Perhaps taking a look at docs#Subsingleton compared to docs#Nonempty will be helpful to you?

[Dan Velleman]

rzeta0 said:

Dan Velleman - we're getting closer ..

• If I want to prove there is a unique solution to x−2=3, then I need to prove x−2=3⟹x=5 and only x=5. 

Another way to look at it: This proves that there is at most one solution.

Why does it only prove there is at most one solution?

Here's another way to look at it. You're familiar with the fact that an implication is equivalent to its contrapositive? So that means that if you prove x - 2 = 3 → x = 5, that's equivalent to proving x ≠ 5 → x - 2 ≠ 3. This says that any number other than 5 is not a solution to the equation. But it doesn't say that 5 is a solution. That means that if 5 is a solution then it's the only solution, and if 5 isn't a solution then there are no solutions. So there is at most one solution.

I've done wider reading and found two comments that I think are relevant:

"Note that you can show uniqueness without showing existence." (src)

I'm having trouble with this. How can a solution be unique but not exist?

That's strange wording. I think what they mean is that you can prove that there is at most one solution without proving that there is at least one solution.

"If there was a specific solution for x  in the existence part, you do not need to show that y equals that specific x" (src)

This seems to support my original thinking that for simple tasks like "show there is a unique solution to x-2=3" it is possible to find a specific solution and we "do not need to show y, a possible other solution, equals x".

No, it doesn't. Suppose you're trying to prove ∃! x, P x, and your witness is a. To prove the existence part, you prove P a. The Lean strategy you've been learning is that for the uniqueness part, you prove ∀ x, P x → x = a. The web page you linked to suggests an alternative way to prove uniqueness: you can prove ∀ x, ∀ y, (P x ∧ P y) → x = y. They're not saying you can skip the uniqueness part; they're saying that in the proof of the uniqueness part, you can prove that any two solutions must be equal to each other rather than proving than any solution must be equal to your witness a. They're still saying that you must prove both parts, existence and uniqueness. (See step 3 under "Proving Uniqueness".)

Here's one more way to look at it: Another way to say that there is at most one solution is to say that there are not two different solutions, which could be written like this: ¬ ∃ x, ∃ y, P x ∧ P y ∧ x ≠ y. Now convince yourself that that's equivalent to ∀ x, ∀ y, (P x ∧ P y) → x = y.

[rzeta0]

in case it helps other readers, this reply on stack exchange was very. insightful for me :

https://math.stackexchange.com/questions/4993808/understanding-the-logic-of-unique-existence-proofs/4994592#4994592

[Michael Bucko]

@rzeta0 thank you for mentioning this book. Reading it now too!