Exercise 2: Prove g:{0}-->{0,1} such that g(0)=0 is NOT surjective

Define: Surjective predicate (abbreviation based on Terence Tao's definition, "Analysis I," p.54))

1 ALL(fun):ALL(dom):ALL(cod):[Surjective(fun,dom,cod) <=> ALL(a):[a e cod => EXIST(b):[b e dom & fun(b)=a]]]

Axiom

Define: x, y, 0, 1

2 ~0=1

Axiom

3 Set(x)

Axiom

4 ALL(a):[a e x <=> a=0]

Axiom

5 Set(y)

Axiom

6 ALL(a):[a e y <=> a=0 | a=1]

Axiom

Prove: ALL(g):[ALL(a):[a e x => EXIST(b):[b e y & g(a)=b]] & g(0)=0 => ~Surjective(g,x,y)]

Suppose g is a function mapping {0} to {0,1} such that g(0)=0

7 ALL(a):[a e x => EXIST(b):[b e y & g(a)=b]] & g(0)=0

Premise

8 ALL(a):[a e x => EXIST(b):[b e y & g(a)=b]]

Split, 7

9 g(0)=0

Split, 7

Apply definition of Surjective

10 ALL(dom):ALL(cod):[Surjective(g,dom,cod) <=> ALL(a):[a e cod => EXIST(b):[b e dom & g(b)=a]]]

U Spec, 1

11 ALL(cod):[Surjective(g,x,cod) <=> ALL(a):[a e cod => EXIST(b):[b e x & g(b)=a]]]

U Spec, 10

12 Surjective(g,x,y) <=> ALL(a):[a e y => EXIST(b):[b e x & g(b)=a]]

U Spec, 11

13 [Surjective(g,x,y) => ALL(a):[a e y => EXIST(b):[b e x & g(b)=a]]]

& [ALL(a):[a e y => EXIST(b):[b e x & g(b)=a]] => Surjective(g,x,y)]

Iff-And, 12

14 Surjective(g,x,y) => ALL(a):[a e y => EXIST(b):[b e x & g(b)=a]]

Split, 13

15 ~ALL(a):[a e y => EXIST(b):[b e x & g(b)=a]] => ~Surjective(g,x,y)

Contra, 14

16 ~~EXIST(a):~[a e y => EXIST(b):[b e x & g(b)=a]] => ~Surjective(g,x,y)

Quant, 15

17 EXIST(a):~[a e y => EXIST(b):[b e x & g(b)=a]] => ~Surjective(g,x,y)

Rem DNeg, 16

18 EXIST(a):~~[a e y & ~EXIST(b):[b e x & g(b)=a]] => ~Surjective(g,x,y)

Imply-And, 17

19 EXIST(a):[a e y & ~EXIST(b):[b e x & g(b)=a]] => ~Surjective(g,x,y)

Rem DNeg, 18

20 EXIST(a):[a e y & ~~ALL(b):~[b e x & g(b)=a]] => ~Surjective(g,x,y)

Quant, 19

21 EXIST(a):[a e y & ALL(b):~[b e x & g(b)=a]] => ~Surjective(g,x,y)

Rem DNeg, 20

22 EXIST(a):[a e y & ALL(b):~~[b e x => ~g(b)=a]] => ~Surjective(g,x,y)

Imply-And, 21

Sufficient: For ~Surjective(g,x,y)

23 EXIST(a):[a e y & ALL(b):[b e x => ~g(b)=a]] => ~Surjective(g,x,y)

Rem DNeg, 22

Prove: ALL(b):[b e x => ~g(b)=1]

Suppose...

24 t e x

Premise

25 t e x <=> t=0

U Spec, 4

26 [t e x => t=0] & [t=0 => t e x]

Iff-And, 25

27 t e x => t=0

Split, 26

28 t=0

Detach, 27, 24

29 g(t)=0

Substitute, 28, 9

30 ~g(t)=1

Substitute, 29, 2

As Required:

31 ALL(b):[b e x => ~g(b)=1]

4 Conclusion, 24

32 1 e y <=> 1=0 | 1=1

U Spec, 6

33 [1 e y => 1=0 | 1=1] & [1=0 | 1=1 => 1 e y]

Iff-And, 32

34 1=0 | 1=1 => 1 e y

Split, 33

35 1=1

Reflex

36 1=0 | 1=1

Arb Or, 35

37 1 e y

Detach, 34, 36

38 1 e y & ALL(b):[b e x => ~g(b)=1]

Join, 37, 31

39 EXIST(a):[a e y & ALL(b):[b e x => ~g(b)=a]]

E Gen, 38

40 ~Surjective(g,x,y)

Detach, 23, 39

As Required:

41 ALL(g):[ALL(a):[a e x => EXIST(b):[b e y & g(a)=b]] & g(0)=0

=> ~Surjective(g,x,y)]

4 Conclusion, 7