THEOREM

*******

ALL(u):[Set(u)

=> [ALL(a):[a e u => P(a)]

<=> ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]]]]

This proof makes use of a proof by contrapositive. It also makes use the Subset Axiom of set theory to construct singleton, a subset of set u.

Dan Christensen

2023-07-12

http://www.dcproof.com

PROOF

*****

Let u be an arbitrary set (the implicit so-called "domain of discourse" in standard FOL)

1 Set(u)

Premise

'=>'

Prove: ALL(a):[a e u => P(a)]

=> ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]]

Suppose...

2 ALL(a):[a e u => P(a)]

Premise

Prove: ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]]

Suppose...

3 Set(y) & ALL(b):[b e y => b e u]

Premise

4 Set(y)

Split, 3

5 ALL(b):[b e y => b e u]

Split, 3

Prove: ALL(b):[b e y => P(b)]

Suppose...

6 x e y

Premise

7 x e y => x e u

U Spec, 5

8 x e u

Detach, 7, 6

9 x e u => P(x)

U Spec, 2

10 P(x)

Detach, 9, 8

As Required:

11 ALL(b):[b e y => P(b)]

4 Conclusion, 6

As Required:

12 ALL(a):[Set(a) & ALL(b):[b e a => b e u]

=> ALL(b):[b e a => P(b)]]

4 Conclusion, 3

'=>'

As Required:

13 ALL(a):[a e u => P(a)]

=> ALL(a):[Set(a) & ALL(b):[b e a => b e u]

=> ALL(b):[b e a => P(b)]]

4 Conclusion, 2

Prove: EXIST(a):[a e u & ~P(a)]

=> EXIST(a):[Set(a) & ALL(b):[b e a => b e u] & EXIST(b):[b e a & ~P(b)]]

Using proof by contrapositive to prove the converse:

ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]]

=> ALL(a):[a e u => P(a)]

Suppose...

14 EXIST(a):[a e u & ~P(a)]

Premise

15 x e u & ~P(x)

E Spec, 14

16 x e u

Split, 15

17 ~P(x)

Split, 15

Apply the Subset Axiom to construct the singleton {x} as a subset of u

18 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e u & a=x]]

Subset, 1

Define: y y = {x}

19 Set(y) & ALL(a):[a e y <=> a e u & a=x]

E Spec, 18

20 Set(y)

Split, 19

21 ALL(a):[a e y <=> a e u & a=x]

Split, 19

Prove: ALL(b):[b e y => b e u]

Suppose...

22 z e y

Premise

Apply the definition of y

23 z e y <=> z e u & z=x

U Spec, 21

24 [z e y => z e u & z=x] & [z e u & z=x => z e y]

Iff-And, 23

25 z e y => z e u & z=x

Split, 24

26 z e u & z=x

Detach, 25, 22

27 z e u

Split, 26

As Required:

28 ALL(b):[b e y => b e u]

4 Conclusion, 22

Apply the definition of y

29 x e y <=> x e u & x=x

U Spec, 21

30 [x e y => x e u & x=x] & [x e u & x=x => x e y]

Iff-And, 29

31 x e u & x=x => x e y

Split, 30

32 x=x

Reflex

33 x e u & x=x

Join, 16, 32

34 x e y

Detach, 31, 33

35 x e y & ~P(x)

Join, 34, 17

36 EXIST(b):[b e y & ~P(b)]

E Gen, 35

37 Set(y) & ALL(b):[b e y => b e u]

Join, 20, 28

38 Set(y) & ALL(b):[b e y => b e u]

& EXIST(b):[b e y & ~P(b)]

Join, 37, 36

39 EXIST(a):[Set(a) & ALL(b):[b e a => b e u]

& EXIST(b):[b e a & ~P(b)]]

E Gen, 38

As Required:

40 EXIST(a):[a e u & ~P(a)]

=> EXIST(a):[Set(a) & ALL(b):[b e a => b e u]

& EXIST(b):[b e a & ~P(b)]]

4 Conclusion, 14

Apply the Contrapostive Rule of inference

41 ~EXIST(a):[Set(a) & ALL(b):[b e a => b e u]

& EXIST(b):[b e a & ~P(b)]] => ~EXIST(a):[a e u & ~P(a)]

Contra, 40

Switch quantifiers, etc. as required to obtain the converse:

ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]] => ALL(a):[a e u => P(a)]

42 ~EXIST(a):~[Set(a) & ALL(b):[b e a => b e u] => ~EXIST(b):[b e a & ~P(b)]] => ~EXIST(a):[a e u & ~P(a)]

Imply-And, 41

43 ~~ALL(a):~~[Set(a) & ALL(b):[b e a => b e u] => ~EXIST(b):[b e a & ~P(b)]] => ~EXIST(a):[a e u & ~P(a)]

Quant, 42

44 ALL(a):~~[Set(a) & ALL(b):[b e a => b e u] => ~EXIST(b):[b e a & ~P(b)]] => ~EXIST(a):[a e u & ~P(a)]

Rem DNeg, 43

45 ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ~EXIST(b):[b e a & ~P(b)]] => ~EXIST(a):[a e u & ~P(a)]

Rem DNeg, 44

46 ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ~~ALL(b):~[b e a & ~P(b)]] => ~EXIST(a):[a e u & ~P(a)]

Quant, 45

47 ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):~[b e a & ~P(b)]] => ~EXIST(a):[a e u & ~P(a)]

Rem DNeg, 46

48 ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):~~[b e a => ~~P(b)]] => ~EXIST(a):[a e u & ~P(a)]

Imply-And, 47

49 ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => ~~P(b)]] => ~EXIST(a):[a e u & ~P(a)]

Rem DNeg, 48

50 ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]] => ~EXIST(a):[a e u & ~P(a)]

Rem DNeg, 49

51 ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]] => ~~ALL(a):~[a e u & ~P(a)]

Quant, 50

52 ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]] => ALL(a):~[a e u & ~P(a)]

Rem DNeg, 51

53 ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]] => ALL(a):~~[a e u => ~~P(a)]

Imply-And, 52

54 ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]] => ALL(a):[a e u => ~~P(a)]

Rem DNeg, 53

'<='

As Required:

55 ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]] => ALL(a):[a e u => P(a)]

Rem DNeg, 54

Joining results...

56 [ALL(a):[a e u => P(a)]

=> ALL(a):[Set(a) & ALL(b):[b e a => b e u]

=> ALL(b):[b e a => P(b)]]]

& [ALL(a):[Set(a) & ALL(b):[b e a => b e u] => ALL(b):[b e a => P(b)]] => ALL(a):[a e u => P(a)]]

Join, 13, 55

Apply the Iff-And Rule

57 ALL(a):[a e u => P(a)]

<=> ALL(a):[Set(a) & ALL(b):[b e a => b e u]

=> ALL(b):[b e a => P(b)]]

Iff-And, 56

As Required:

58 ALL(u):[Set(u)

=> [ALL(a):[a e u => P(a)]

<=> ALL(a):[Set(a) & ALL(b):[b e a => b e u]

=> ALL(b):[b e a => P(b)]]]]

4 Conclusion, 1