unique existential quantifier

Stream: new members

[Claus-Peter Becke]

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]

\exists!

[Johan Commelin]

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

[Claus-Peter Becke]

@Johan Commelin: Thank you for your support.

[Bryan Gin-ge Chen]

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]

@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]

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

[Kenny Lau]

solve it in maths first

[Kyle Miller]

    ...
    have h2 := h1 ∅,
    rw union_empty at h2,

[Kyle Miller]

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

[Johan Commelin]

It's relatively new (I think)

[Claus-Peter Becke]

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

[Claus-Peter Becke]

@ 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]

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]

before formalizing the proof into Lean

[Claus-Peter Becke]

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]

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

[Claus-Peter Becke]

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]

@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]

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

[Claus-Peter Becke]

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]

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]

hence why I said "solve it in maths first"

[Claus-Peter Becke]

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.

[Kenny Lau]

yes, I agree

[Claus-Peter Becke]

@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]

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

[Johan Commelin]

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]

Ok, I will try that.

[Claus-Peter Becke]

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]

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

[Claus-Peter Becke]

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

[Claus-Peter Becke]

I wanted to say the development of the prooof.

[Johan Commelin]

@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]

(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]

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.