The uniqueness of the empty set: A simple application of vacuous truth

[Dan Christensen]

THEOREM

The empty set is unique.

ALL(e1):ALL(e2):[Set(e1) & Set(e2) => [ALL(a):~a in e1 & ALL(a):~a in e2 => e1=e2]]

This proof makes use of the Axiom of Set Equality (line 5) and the principle of vacuous truth (lines 17 and 24).

PROOF

Let e1 and e2 be sets

1. Set(e1) & Set(e2)
Premise

Let e1 and e2 b3 empty

2. ALL(a):~a in e1 & ALL(a):~a in e2
Premise

3. ALL(a):~a in e1
Split, 2

4. ALL(a):~a in e2
Split, 2

Apply Axiom of Set Equality

5. ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c in a <=> c in b]]]
Set Equality

6. ALL(b):[Set(e1) & Set(b) => [e1=b <=> ALL(c):[c in e1 <=> c in b]]]
U Spec, 5

7. Set(e1) & Set(e2) => [e1=e2 <=> ALL(c):[c in e1 <=> c in e2]]
U Spec, 6

8. e1=e2 <=> ALL(c):[c in e1 <=> c in e2]
Detach, 7, 1

9. [e1=e2 => ALL(c):[c in e1 <=> c in e2]]
& [ALL(c):[c in e1 <=> c in e2] => e1=e2]
Iff-And, 8

Sufficient: For e1=e2

10. ALL(c):[c in e1 <=> c in e2] => e1=e2
Split, 9

11. x in e1
Premise

12. ~x in e1
U Spec, 3

13. ~x in e2
Premise

14. x in e1 & ~x in e1
Join, 11, 12

15. ~~x in e2
Conclusion, 13

16. x in e2
Rem DNeg, 15

Vacuously true:

17. ALL(c):[c in e1 => c in e2]
Conclusion, 11

18. y in e2
Premise

19. ~y in e2
U Spec, 4

20. ~y in e1
Premise

21. y in e2 & ~y in e2
Join, 18, 19

22. ~~y in e1
Conclusion, 20

23. y in e1
Rem DNeg, 22

Vacuously true:

24. ALL(c):[c in e2 => c in e1]
Conclusion, 18

25. ALL(c):[[c in e1 => c in e2] & [c in e2 => c in e1]]
Join, 17, 24

26. ALL(c):[c in e1 <=> c in e2]
Iff-And, 25

27. e1=e2
Detach, 10, 26

28. ALL(a):~a in e1 & ALL(a):~a in e2 => e1=e2
Conclusion, 2

29. ALL(e1):ALL(e2):[Set(e1) & Set(e2)
=> [ALL(a):~a in e1 & ALL(a):~a in e2 => e1=e2]]
Conclusion, 1


Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[Mostowski Collapse]

Looks like you don't understand your own proof.
You critize my proof based on:

> From your premise on line 2, we can derive EXIST(x):[~Odd(x) & ~Even(x)],
which is inconsistent with your axiom.

But watch out: Its not an axiom. Its a premise that gets
discharged. Just like in your proof here:

11. x in e1
Premise

The uniqueness of the empty set: A simple application of vacuous truth
https://groups.google.com/g/sci.logic/c/68uls4gBFqM

You also make premises, which are in conflict later:

14. x in e1 & ~x in e1
Join, 11, 12

The uniqueness of the empty set: A simple application of vacuous truth
https://groups.google.com/g/sci.logic/c/68uls4gBFqM

Whats the prolololoblem Bozo the Clown?

[Mostowski Collapse]

Do you have the slightest clue what your
DC Proof does, or is supposed to do?

LoL

[Dan Christensen]

On Sunday, February 12, 2023 at 5:38:47 PM UTC-5, Mostowski Collapse wrote:
> Looks like you don't understand your own proof.

I start with empty sets e1 and e2. Using the Axiom of Set Equality and the principle of vacuous truth, I prove that e1 = e2. Deal with it Mr. Collapse.

> You critize my proof based on:
>
> > From your premise on line 2, we can derive EXIST(x):[~Odd(x) & ~Even(x)],
> which is inconsistent with your axiom.
>

That wasn't a criticism, but a summary.

> But watch out: Its not an axiom.

Did you even read your own proof, Mr. Collapse? Did someone else (maybe AP) write it for you?

But change it to a premise and repost it, if you want. The result will be essentially the same.

[Mostowski Collapse]

I am not talking about your axiom, you moron.

You wrote "From your premise on line 2"
I said its not an axiom, its a premise.

Whats wrong with you?

[Mostowski Collapse]

You wrote:
> Your bizarre choice of predicates Even and Odd
> made it even more confusing to readers (e.g. Ross).

I didn't chose the predicates. They are from your post here:

1 ALL(x):[Odd(x) <=> ~Even(x)]
Axiom
https://dcproof.com/EvenNextOdd.htm

There is also a long thread where you fight that "Odd"
is the "Opposite" of "Even", the way you wanted it to
model in the axiom above. Namely without a domain restriction.

I only showed you now that the axiom implies trivially:

21 ALL(x):[Unicorn(x) => Even(x) | Odd(x)]
Rem DNeg, 20

Now you deny that your axiom implies the above theorem?
Whats your point Dan-O-Matik?

[Dan Christensen]

See my reply just now to your identical posting in another thread here.

Dan

On Monday, February 13, 2023 at 2:32:46 AM UTC-5, Mostowski Collapse wrote:
> You wrote:
> > Your bizarre choice of predicates Even and Odd
> > made it even more confusing to readers (e.g. Ross).
>
> I didn't chose the predicates. They are from your post here:
>

[snip]