THEOREM

*******

ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => F(x) | F(y)]]]

<=> EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

where U is a non-empty domain of discourse

This formal proof was written and verified with the aid of the author's DC Proof 2.0 freeware now available at http://www.dproof.com

Dan Christensen

2020-11-23

PROOF

*****

U is a non-empty domain of discourse

1 EXIST(x):U(x)

Axiom

'=>'

Prove: ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => F(x) | F(y)]]]

=> EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

Suppose...

2 ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => F(x) | F(y)]]]

Premise

Two cases to consider:

3 ALL(x):[U(x) => F(x)] | ~ALL(x):[U(x) => F(x)]

Or Not

Case 1

Prove: ALL(x):[U(x) => F(x)]

=> EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

Suppose...

4 ALL(x):[U(x) => F(x)]

Premise

5 U(a)

E Spec, 1

Prove: ALL(y):[U(y) => [~a=y => F(y)]]

Suppose...

6 U(b)

Premise

7 U(b) => F(b)

U Spec, 4

8 F(b)

Detach, 7, 6

9 ~a=b => F(b)

Arb Ante, 8

As Required:

10 ALL(y):[U(y) => [~a=y => F(y)]]

4 Conclusion, 6

11 U(a) & ALL(y):[U(y) => [~a=y => F(y)]]

Join, 5, 10

12 EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

E Gen, 11

Case 1

As Required:

13 ALL(x):[U(x) => F(x)]

=> EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

4 Conclusion, 4

Case 2

Prove: ~ALL(x):[U(x) => F(x)]

=> EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

Suppose...

14 ~ALL(x):[U(x) => F(x)]

Premise

15 ~~EXIST(x):~[U(x) => F(x)]

Quant, 14

16 EXIST(x):~[U(x) => F(x)]

Rem DNeg, 15

17 EXIST(x):~~[U(x) & ~F(x)]

Imply-And, 16

18 EXIST(x):[U(x) & ~F(x)]

Rem DNeg, 17

19 U(a) & ~F(a)

E Spec, 18

20 U(a)

Split, 19

21 ~F(a)

Split, 19

22 U(a) => ALL(y):[U(y) => [~a=y => F(a) | F(y)]]

U Spec, 2

23 ALL(y):[U(y) => [~a=y => F(a) | F(y)]]

Detach, 22, 20

Prove: ALL(y):[U(y) => [~a=y => F(y)]

Suppose...

24 U(b)

Premise

25 U(b) => [~a=b => F(a) | F(b)]

U Spec, 23

26 ~a=b => F(a) | F(b)

Detach, 25, 24

Prove: ~a=b => F(b)

Suppose...

27 ~a=b

Premise

28 F(a) | F(b)

Detach, 26, 27

29 ~F(a) => F(b)

Imply-Or, 28

30 F(b)

Detach, 29, 21

As Required:

31 ~a=b => F(b)

4 Conclusion, 27

As Required:

32 ALL(y):[U(y) => [~a=y => F(y)]]

4 Conclusion, 24

33 U(a) & ALL(y):[U(y) => [~a=y => F(y)]]

Join, 20, 32

34 EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

E Gen, 33

Case 2

As Required:

35 ~ALL(x):[U(x) => F(x)]

=> EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

4 Conclusion, 14

Join results

36 [ALL(x):[U(x) => F(x)]

=> EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]]

& [~ALL(x):[U(x) => F(x)]

=> EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]]

Join, 13, 35

Apply Cases Rule

37 EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

Cases, 3, 36

As Required:

38 ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => F(x) | F(y)]]]

=> EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

4 Conclusion, 2

'<='

Prove: EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

=> ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => F(x) | F(y)]]]

Suppose...

39 EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

Premise

40 U(a) & ALL(y):[U(y) => [~a=y => F(y)]]

E Spec, 39

41 U(a)

Split, 40

42 ALL(y):[U(y) => [~a=y => F(y)]]

Split, 40

43 ALL(y):[U(y) => [~F(y) => ~~a=y]]

Contra, 42

44 ALL(y):[U(y) => [~F(y) => a=y]]

Rem DNeg, 43

Prove: ~EXIST(x):[U(x) & EXIST(y):[U(y) & [~x=y & [~F(x) & ~F(y)]]]]

Suppose to the contrary...

45 EXIST(x):[U(x) & EXIST(y):[U(y) & [~x=y & [~F(x) & ~F(y)]]]]

Premise

46 U(b) & EXIST(y):[U(y) & [~b=y & [~F(b) & ~F(y)]]]

E Spec, 45

47 U(b)

Split, 46

48 EXIST(y):[U(y) & [~b=y & [~F(b) & ~F(y)]]]

Split, 46

49 U(c) & [~b=c & [~F(b) & ~F(c)]]

E Spec, 48

50 U(c)

Split, 49

51 ~b=c & [~F(b) & ~F(c)]

Split, 49

52 ~b=c

Split, 51

53 ~F(b) & ~F(c)

Split, 51

54 ~F(b)

Split, 53

55 ~F(c)

Split, 53

56 U(b) => [~F(b) => a=b]

U Spec, 44

57 ~F(b) => a=b

Detach, 56, 47

58 a=b

Detach, 57, 54

59 U(c) => [~F(c) => a=c]

U Spec, 44

60 ~F(c) => a=c

Detach, 59, 50

61 a=c

Detach, 60, 55

62 b=c

Substitute, 58, 61

63 ~b=c & b=c

Join, 52, 62

As Required:

64 ~EXIST(x):[U(x) & EXIST(y):[U(y) & [~x=y & [~F(x) & ~F(y)]]]]

4 Conclusion, 45

65 ~~ALL(x):~[U(x) & EXIST(y):[U(y) & [~x=y & [~F(x) & ~F(y)]]]]

Quant, 64

66 ALL(x):~[U(x) & EXIST(y):[U(y) & [~x=y & [~F(x) & ~F(y)]]]]

Rem DNeg, 65

67 ALL(x):~~[U(x) => ~EXIST(y):[U(y) & [~x=y & [~F(x) & ~F(y)]]]]

Imply-And, 66

68 ALL(x):[U(x) => ~EXIST(y):[U(y) & [~x=y & [~F(x) & ~F(y)]]]]

Rem DNeg, 67

69 ALL(x):[U(x) => ~~ALL(y):~[U(y) & [~x=y & [~F(x) & ~F(y)]]]]

Quant, 68

70 ALL(x):[U(x) => ALL(y):~[U(y) & [~x=y & [~F(x) & ~F(y)]]]]

Rem DNeg, 69

71 ALL(x):[U(x) => ALL(y):~~[U(y) => ~[~x=y & [~F(x) & ~F(y)]]]]

Imply-And, 70

72 ALL(x):[U(x) => ALL(y):[U(y) => ~[~x=y & [~F(x) & ~F(y)]]]]

Rem DNeg, 71

73 ALL(x):[U(x) => ALL(y):[U(y) => ~~[~x=y => ~[~F(x) & ~F(y)]]]]

Imply-And, 72

74 ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => ~[~F(x) & ~F(y)]]]]

Rem DNeg, 73

75 ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => ~~[~~F(x) | ~~F(y)]]]]

DeMorgan, 74

76 ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => ~~F(x) | ~~F(y)]]]

Rem DNeg, 75

77 ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => F(x) | ~~F(y)]]]

Rem DNeg, 76

78 ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => F(x) | F(y)]]]

Rem DNeg, 77

As Required:

79 EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

=> ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => F(x) | F(y)]]]

4 Conclusion, 39

Joining results...

80 [ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => F(x) | F(y)]]]

=> EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]]

& [EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

=> ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => F(x) | F(y)]]]]

Join, 38, 79

As Required:

81 ALL(x):[U(x) => ALL(y):[U(y) => [~x=y => F(x) | F(y)]]]

<=> EXIST(x):[U(x) & ALL(y):[U(y) => [~x=y => F(y)]]]

Iff-And, 80