THEOREM

*******

Given:

x = {0, 1} (line 3)

x2 = {(a,b): a e x & b e x}

ALL(f):[f e fs <=> ALL(a1):ALL(a2):[(a1,a2) e x2 => f(a1,a2) e x]] (Function space, line 39)

f(0,0)=0 & f(0,1)=1 & f(1,0)=1 & f(1,1)=0 (line 40)

Prove:

f e fs

By Dan Christensen

2022-01-16

This machine-verified, formal proof was written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com

PROOF

*****

Function Space Axiom (functions with 2 variables)

1 ALL(dom):ALL(cod):[Set'(dom) & EXIST(a1):EXIST(a2):(a1,a2) e dom & Set(cod)

=> EXIST(fs):[Set(fs) & ALL(f):[f e fs <=> ALL(a1):ALL(a2):[(a1,a2) e dom => f(a1,a2) e cod]]]]

Axiom

2 Set(x)

Axiom

3 ALL(a):[a e x <=> a=0 | a=1]

Axiom

4 0 e x <=> 0=0 | 0=1

U Spec, 3

5 [0 e x => 0=0 | 0=1] & [0=0 | 0=1 => 0 e x]

Iff-And, 4

6 0=0 | 0=1 => 0 e x

Split, 5

7 0=0

Reflex

8 0=0 | 0=1

Arb Or, 7

9 0 e x

Detach, 6, 8

10 1 e x <=> 1=0 | 1=1

U Spec, 3

11 [1 e x => 1=0 | 1=1] & [1=0 | 1=1 => 1 e x]

Iff-And, 10

12 1=0 | 1=1 => 1 e x

Split, 11

13 1=1

Reflex

14 1=0 | 1=1

Arb Or, 13

15 1 e x

Detach, 12, 14

16 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]

Cart Prod

17 ALL(a2):[Set(x) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e a2]]]

U Spec, 16

18 Set(x) & Set(x) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e x]]

U Spec, 17

19 Set(x) & Set(x)

Join, 2, 2

20 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e x]]

Detach, 18, 19

21 Set'(x2) & ALL(c1):ALL(c2):[(c1,c2) e x2 <=> c1 e x & c2 e x]

E Spec, 20

Define: x2

22 Set'(x2)

Split, 21

23 ALL(c1):ALL(c2):[(c1,c2) e x2 <=> c1 e x & c2 e x]

Split, 21

24 ALL(cod):[Set'(x2) & EXIST(a1):EXIST(a2):(a1,a2) e x2 & Set(cod)

=> EXIST(fs):[Set(fs) & ALL(f):[f e fs <=> ALL(a1):ALL(a2):[(a1,a2) e x2 => f(a1,a2) e cod]]]]

U Spec, 1

25 Set'(x2) & EXIST(a1):EXIST(a2):(a1,a2) e x2 & Set(x)

=> EXIST(fs):[Set(fs) & ALL(f):[f e fs <=> ALL(a1):ALL(a2):[(a1,a2) e x2 => f(a1,a2) e x]]]

U Spec, 24

26 ALL(c2):[(0,c2) e x2 <=> 0 e x & c2 e x]

U Spec, 23

27 (0,0) e x2 <=> 0 e x & 0 e x

U Spec, 26

28 [(0,0) e x2 => 0 e x & 0 e x]

& [0 e x & 0 e x => (0,0) e x2]

Iff-And, 27

29 0 e x & 0 e x => (0,0) e x2

Split, 28

30 0 e x & 0 e x

Join, 9, 9

31 (0,0) e x2

Detach, 29, 30

32 EXIST(a2):(0,a2) e x2

E Gen, 31

33 EXIST(a1):EXIST(a2):(a1,a2) e x2

E Gen, 32

34 Set'(x2) & EXIST(a1):EXIST(a2):(a1,a2) e x2

Join, 22, 33

35 Set'(x2) & EXIST(a1):EXIST(a2):(a1,a2) e x2

& Set(x)

Join, 34, 2

36 EXIST(fs):[Set(fs) & ALL(f):[f e fs <=> ALL(a1):ALL(a2):[(a1,a2) e x2 => f(a1,a2) e x]]]

Detach, 25, 35

37 Set(fs) & ALL(f):[f e fs <=> ALL(a1):ALL(a2):[(a1,a2) e x2 => f(a1,a2) e x]]

E Spec, 36

Define: fs

38 Set(fs)

Split, 37

39 ALL(f):[f e fs <=> ALL(a1):ALL(a2):[(a1,a2) e x2 => f(a1,a2) e x]]

Split, 37

Prove: ALL(f):[f(0,0)=0 & f(0,1)=1 & f(1,0)=1 & f(1,1)=0 => f e fs]

Suppose...

40 f(0,0)=0 & f(0,1)=1 & f(1,0)=1 & f(1,1)=0

Premise

41 f(0,0)=0

Split, 40

42 f(0,1)=1

Split, 40

43 f(1,0)=1

Split, 40

44 f(1,1)=0

Split, 40

45 f e fs <=> ALL(a1):ALL(a2):[(a1,a2) e x2 => f(a1,a2) e x]

U Spec, 39

46 [f e fs => ALL(a1):ALL(a2):[(a1,a2) e x2 => f(a1,a2) e x]]

& [ALL(a1):ALL(a2):[(a1,a2) e x2 => f(a1,a2) e x] => f e fs]

Iff-And, 45

Sufficient: For f e fs

47 ALL(a1):ALL(a2):[(a1,a2) e x2 => f(a1,a2) e x] => f e fs

Split, 46

Prove: ALL(a1):ALL(a2):[(a1,a2) e x2 => f(a1,a2) e x]

Suppose...

48 (t,u) e x2

Premise

49 ALL(c2):[(t,c2) e x2 <=> t e x & c2 e x]

U Spec, 23

50 (t,u) e x2 <=> t e x & u e x

U Spec, 49

51 [(t,u) e x2 => t e x & u e x]

& [t e x & u e x => (t,u) e x2]

Iff-And, 50

52 (t,u) e x2 => t e x & u e x

Split, 51

53 t e x & u e x

Detach, 52, 48

54 t e x

Split, 53

55 u e x

Split, 53

56 t e x <=> t=0 | t=1

U Spec, 3

57 [t e x => t=0 | t=1] & [t=0 | t=1 => t e x]

Iff-And, 56

58 t e x => t=0 | t=1

Split, 57

Two cases to consider:

59 t=0 | t=1

Detach, 58, 54

60 u e x <=> u=0 | u=1

U Spec, 3

61 [u e x => u=0 | u=1] & [u=0 | u=1 => u e x]

Iff-And, 60

62 u e x => u=0 | u=1

Split, 61

Two sub-cases to consider:

63 u=0 | u=1

Detach, 62, 55

Case 1

Prove: t=0 => f(t,u) e x

Suppose...

64 t=0

Premise

Sub-case 1

Prove: u=0 => f(t,u) e x

Suppose...

65 u=0

Premise

66 f(t,0)=0

Substitute, 64, 41

67 f(t,u)=0

Substitute, 65, 66

68 f(t,u) e x

Substitute, 67, 9

As Required:

69 u=0 => f(t,u) e x

4 Conclusion, 65

Sub-case 2

Prove: u=1 => f(t,u) e x

Suppose...

70 u=1

Premise

71 f(t,1)=1

Substitute, 64, 42

72 f(t,u)=1

Substitute, 70, 71

73 f(t,u) e x

Substitute, 72, 15

As Required:

74 u=1 => f(t,u) e x

4 Conclusion, 70

75 [u=0 => f(t,u) e x] & [u=1 => f(t,u) e x]

Join, 69, 74

76 f(t,u) e x

Cases, 63, 75

As Required:

77 t=0 => f(t,u) e x

4 Conclusion, 64

Case 2

Prove: t=1 => f(t,u) e x

Suppose...

78 t=1

Premise

Sub-case 1

Prove: u=0 => f(t,u) e x

Suppose...

79 u=0

Premise

80 f(t,0)=1

Substitute, 78, 43

81 f(t,u)=1

Substitute, 79, 80

82 f(t,u) e x

Substitute, 81, 15

As Required:

83 u=0 => f(t,u) e x

4 Conclusion, 79

Sub-case 2

Prove: u=1 => f(t,u) e x

Suppose...

84 u=1

Premise

85 f(t,1)=0

Substitute, 78, 44

86 f(t,u)=0

Substitute, 84, 85

87 f(t,u) e x

Substitute, 86, 9

As Required:

88 u=1 => f(t,u) e x

4 Conclusion, 84

89 [u=0 => f(t,u) e x] & [u=1 => f(t,u) e x]

Join, 83, 88

90 f(t,u) e x

Cases, 63, 89

As Required:

91 t=1 => f(t,u) e x

4 Conclusion, 78

92 [t=0 => f(t,u) e x] & [t=1 => f(t,u) e x]

Join, 77, 91

93 f(t,u) e x

Cases, 59, 92

As Required:

94 ALL(a1):ALL(a2):[(a1,a2) e x2 => f(a1,a2) e x]

4 Conclusion, 48

95 f e fs

Detach, 47, 94

As Required:

96 ALL(f):[f(0,0)=0 & f(0,1)=1 & f(1,0)=1 & f(1,1)=0 => f e fs]

4 Conclusion, 40