## Stream: new members

### Topic: unique existential quantifier

#### Claus-Peter Becke (Sep 18 2020 at 06:08):

Is this type of quantifier defined in Lean? If yes, which is its symbol and which keys can be used to print it in VSCode? (I didn't find it in the file lean prover/vscode-lean/translations.json) If not, is there a conventional combination of symbols which van be used to replace it? I would like to prove the following assertion: \exists uniquely a set A such that \forall B holds ( A \un B = B). Which way could I print it in VSCode as provable example?

#### Johan Commelin (Sep 18 2020 at 06:14):

\exists!

#### Johan Commelin (Sep 18 2020 at 06:16):

lemma i_am_empty (X : Type) : \exists! (A : set X), \forall (B : set X), A \union B = B :=
sorry


#### Claus-Peter Becke (Sep 18 2020 at 06:21):

@Johan Commelin: Thank you for your support.

#### Bryan Gin-ge Chen (Sep 18 2020 at 06:36):

Be careful if you try to use \exists! with multiple variables: it unfolds to a bunch of nested \exists! which usually isn't what you want. See this old thread https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/undead/near/132662688

#### Claus-Peter Becke (Sep 18 2020 at 07:59):

@Bryan Gin-ge Chen:
Thank for that warning. With respect to sets I experienced something different. Maybe you like to take a look at that. Unfortunately the proof isn't complete. I stick to a problem which I actually can't solve:

import data.set
import tactic.basic
open set

variable {U : Type}
variables A B C : set U
variable x : U

example : ∃! (A : set U), ∀ (B : set U), A ∪ B = B :=
begin
use ∅,
split,
intro B,
rw empty_union,
intro y,
intro h1,
have h2 := h1 y,
rw union_self at h2,
...
end


This is the point I arrived at. But I don't find a solution the goal y = \empty.

#### Kenny Lau (Sep 18 2020 at 08:01):

@Claus-Peter Becke that's a maths question, not a Lean one

#### Kenny Lau (Sep 18 2020 at 08:01):

solve it in maths first

#### Kyle Miller (Sep 18 2020 at 08:04):

(I've never seen the spoiler tag be used here before)

#### Johan Commelin (Sep 18 2020 at 08:04):

It's relatively new (I think)

#### Claus-Peter Becke (Sep 18 2020 at 08:13):

@Kyle Miller:
Thank you for that hint, albeit spoiled. Sometimes I don't see the forest for the trees.

#### Claus-Peter Becke (Sep 18 2020 at 08:18):

@ Kenny Lau:
I'm not sure whether you intended to advise me to look at what y \union B = B means. If yes, that wasn't necessary.

#### Kenny Lau (Sep 18 2020 at 08:19):

I intended you to prove, with paper and pen, that there is a unique set A such that A U B = B for all B

#### Kenny Lau (Sep 18 2020 at 08:19):

before formalizing the proof into Lean

#### Claus-Peter Becke (Sep 18 2020 at 08:25):

But that hadn't been my problem, because I'm aware of the fact that if y \union B = B is presupposed it follows that y is the empty set. The problem for me was to find a way to implement it. And because I'm not very experienced in writing mathematical proofs it would not have been easier to sit in front of a sheet of paper with a pencil between my fingers. I missed the idea to choose the empty set as a substitute for B. That was the problem. Admittedly that's a very elementary problem. But: Sometimes I don't see the forest for the trees.

#### Kenny Lau (Sep 18 2020 at 08:27):

then why do you know that (y U B = B for all B) implies y is the empty set?

#### Claus-Peter Becke (Sep 18 2020 at 08:36):

Because I like to be examined: We. have an equality relation between two sets what means that we have a subset-relation in two directions. This can be rewritten as an implication in two directions and that again means that every x which is an element of the antecedent must also be a member of the consequence. x \in B \r x \in B \union y. So we don't have any further elements in y.

#### Johan Commelin (Sep 18 2020 at 08:39):

@Claus-Peter Becke I think you mean to conclude that y \subset B, right? But you want to prove y = \empty. So you aren't done yet. Can you formalise this approach in Lean?

#### Kenny Lau (Sep 18 2020 at 08:40):

I think you're treating B as a fixed set, when it's bound by a universal quantifier

#### Claus-Peter Becke (Sep 18 2020 at 08:46):

In h1 B is bound by the universal quantifier, but I didn't introduce it as an arbitrary object. So I'm allowed to instantiate with a fixed set, I suppose. In this case as the empty set.

#### Kenny Lau (Sep 18 2020 at 08:47):

I'm claiming that the reason you're stuck in the formal proof is that you don't (or didn't) know the informal proof

#### Kenny Lau (Sep 18 2020 at 08:48):

hence why I said "solve it in maths first"

#### Claus-Peter Becke (Sep 18 2020 at 08:55):

At my present stage of experience with mathematical proofs I don't see an essential difference between proofs in Lean and in maths. It's only a different way to express it. I started using automated proving a few months ago with Daniel Vellemans Proof Designer. With that tool I experienced that you can express every automated step also as a corresponding "informal" one.

yes, I agree

#### Claus-Peter Becke (Sep 18 2020 at 09:21):

@Johan Comerin:
Because y is the empty set it is also a subset of B. But with those steps I described above it should be done to prove that y = \empty? Or am I wrong? I have formalized the proof without the unique existential quantifier which Is very easy to solve:

example : ∃ (A : set U), ∀ (B: set U), A ∪ B = B :=
begin
use ∅,
intro B,
rw empty_union,
end


#### Claus-Peter Becke (Sep 18 2020 at 09:23):

@ Johan Commelin:
I'm sorry. The automated correction changed the name I meant

#### Johan Commelin (Sep 18 2020 at 09:25):

Sure. Now it would be a nice exercise to also formalise the !-part along the lines of the argument that you sketched upstairs.

#### Claus-Peter Becke (Sep 18 2020 at 09:26):

Ok, I will try that.

#### Claus-Peter Becke (Sep 19 2020 at 08:26):

As far as I see there will be especially two possibilities. The first one I posted above. The second is the following:

example : (x ∈ A ∨ x ∈ B → x ∈ B) ∧ (x ∈ B → x ∈ A ∨ x ∈ B) :=
begin
end


I don't consider the second as a rational one. My guesses advise that it should be the empty set which fulfills all conditions. If I have an existential quantifier in my goal, I'm asked to look for an object which fits in. Under the given circumstances that can only be the empty set. Thus it isn't rational to presuppose something like x \in A if I expect A to be the empty set.
Maybe I understood you wrongly. If so, I would appreciate if you explained in detail what you expected and what is wrong with respect to my belefs.

#### Kevin Buzzard (Sep 19 2020 at 08:27):

You can presuppose a false thing -- that happens all the time in proofs by contradiction

#### Claus-Peter Becke (Sep 19 2020 at 08:28):

Yes, of course, but the development will show whether I was wrong or not.

#### Claus-Peter Becke (Sep 19 2020 at 08:28):

I wanted to say the development of the prooof.

#### Johan Commelin (Sep 19 2020 at 08:30):

@Claus-Peter Becke You wrote how you would finish the proof in a post above. I simply meant that you try to turn that into Lean code. It might be a fun exercise.

import data.set
import tactic.basic
open set

variable {U : Type}
variables A B C : set U
variable x : U

example : ∃! (A : set U), ∀ (B : set U), A ∪ B = B :=
begin
use ∅,
split,
intro B,
rw empty_union,
intro y,
intro h1,
-- continue your proof idea here
end


#### Johan Commelin (Sep 19 2020 at 08:30):

(I know you already know how to finish this proof in one way. I'm suggesting that you try to follow your own sketch as well.)

#### Claus-Peter Becke (Sep 19 2020 at 08:34):

In my opinion this is already done. The first time using the unique existential quantifier with the spoiled hint of Kyle Miller. And the second time with the very simple solution that uses the existential quantifier. I'm sorry, but I don't see any further solutions.

Last updated: May 14 2021 at 13:24 UTC