THEOREM
*******
The proposed definition of finite (FiniteA) is equivalent to Dedekind finite (FiniteB)
This proof was written with the aid of and mechanically verified by the author's DC Proof 2.0 software available at http://www.dcproof.com
Define: FiniteA() (Proposed definition)
*****************
1 ALL(s):[Set(s) => [FiniteA(s)
<=> ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]]]]
Axiom
Define: FiniteB() (Dedekind-finite)
*****************
2 ALL(s):[Set(s) => [FiniteB(s)
<=> ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]]]]
Axiom
PROOF
*****
Prove: ALL(s):[Set(s) => [FiniteA(s) <=> FiniteB(s)]]
Suppose...
3 Set(s)
Premise
'=>'
Prove: FiniteA(s) => FiniteB(s)
Suppose...
4 FiniteA(s)
Premise
Apply definition of FiniteA for set s
5 Set(s) => [FiniteA(s)
<=> ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]]]
U Spec, 1
6 FiniteA(s)
<=> ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]]
Detach, 5, 3
7 [FiniteA(s) => ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]]]
& [ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]] => FiniteA(s)]
Iff-And, 6
8 FiniteA(s) => ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]]
Split, 7
9 ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]] => FiniteA(s)
Split, 7
10 ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]]
Detach, 8, 4
Apply definition of FiniteB for set s
11 Set(s) => [FiniteB(s)
<=> ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]]]
U Spec, 2
12 FiniteB(s)
<=> ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]]
Detach, 11, 3
13 [FiniteB(s) => ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]]]
& [ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]] => FiniteB(s)]
Iff-And, 12
14 FiniteB(s) => ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]]
Split, 13
Sufficient: For FiniteB(s)
15 ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]] => FiniteB(s)
Split, 13
Prove: ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]]
Suppose...
16 ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
Premise
Define: f
*********
17 ALL(a):[a e s => f(a) e s]
Split, 16
18 ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
Split, 16
Prove: ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]
Suppose...
19 x e s
Premise
Apply definition of FiniteA for element x and function f
20 ALL(f):[x e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x]]
U Spec, 10
21 x e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x]
U Spec, 20
Joining results...
22 x e s & ALL(a):[a e s => f(a) e s]
Join, 19, 17
23 x e s & ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
Join, 22, 18
24 EXIST(xn):[xn e s & f(xn)=x]
Detach, 21, 23
As Required:
25 ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]
4 Conclusion, 19
As Required:
26 ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]]
4 Conclusion, 16
27 FiniteB(s)
Detach, 15, 26
'=>'
As Required:
28 FiniteA(s) => FiniteB(s)
4 Conclusion, 4
'<='
Prove: FiniteB(s) => FiniteA(s)
Suppose...
29 FiniteB(s)
Premise
Apply definition of FiniteB for set s
30 Set(s) => [FiniteB(s)
<=> ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]]]
U Spec, 2
31 FiniteB(s)
<=> ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]]
Detach, 30, 3
32 [FiniteB(s) => ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]]]
& [ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]] => FiniteB(s)]
Iff-And, 31
33 FiniteB(s) => ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]]
Split, 32
34 ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]] => FiniteB(s)
Split, 32
35 ALL(f):[ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]]
Detach, 33, 29
Apply definition of FiniteA for set s
36 Set(s) => [FiniteA(s)
<=> ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]]]
U Spec, 1
37 FiniteA(s)
<=> ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]]
Detach, 36, 3
38 [FiniteA(s) => ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]]]
& [ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]] => FiniteA(s)]
Iff-And, 37
39 FiniteA(s) => ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]]
Split, 38
Sufficient: For FiniteA(s)
40 ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]] => FiniteA(s)
Split, 38
Prove: ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]]
Suppose...
41 x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
Premise
Define: x0
42 x0 e s
Split, 41
Define: f
43 ALL(a):[a e s => f(a) e s]
Split, 41
44 ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
Split, 41
Apply definition of FiniteB for function f
45 ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]
U Spec, 35
Joining results...
46 ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
Join, 43, 44
47 ALL(a):[a e s => EXIST(xn):[xn e s & f(xn)=a]]
Detach, 45, 46
48 x0 e s => EXIST(xn):[xn e s & f(xn)=x0]
U Spec, 47
49 EXIST(xn):[xn e s & f(xn)=x0]
Detach, 48, 42
As Required:
50 ALL(x0):ALL(f):[x0 e s
& ALL(a):[a e s => f(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f(a)=f(b) => a=b]]
=> EXIST(xn):[xn e s & f(xn)=x0]]
4 Conclusion, 41
51 FiniteA(s)
Detach, 40, 50
'<='
As Required:
52 FiniteB(s) => FiniteA(s)
4 Conclusion, 29
53 [FiniteA(s) => FiniteB(s)]
& [FiniteB(s) => FiniteA(s)]
Join, 28, 52
54 FiniteA(s) <=> FiniteB(s)
Iff-And, 53
As Required:
55 ALL(s):[Set(s) => [FiniteA(s) <=> FiniteB(s)]]
4 Conclusion, 3