Least Upper Bound Theorem for N Introduction ------------ Required to prove: ALL(a):[Set(a) & ALL(b):[b ε a => b ε n] & EXIST(b):b ε a & EXIST(b):[b ε n & ALL(c):[c ε a => c<=b]] => EXIST(b):[b ε a & ALL(c):[c ε a => c<=b]]] Outline ------- Let s be a non-empty subset of n. Let ub be an upper bound of s. Suppose to the contrary that there is no least upper bound of s. Use proof by induction to show that you would then have to have, for all natural numbers, a larger number that is in s. This cannot be true for ub. Axioms and Defintions for n, 1, +, < ------------------------------------ 1 Set(n) Axiom 2 1 ε n Axiom Define: + on n 3 ALL(a):ALL(b):[a ε n & b ε n => a+b ε n] Axiom 4 ALL(a):[a ε n => ~a+1=1] Axiom 5 ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b] Axiom 6 ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1] Axiom 7 ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a] => ALL(b):[b ε n => b ε a]] Axiom Define: < on n 8 ALL(a):ALL(b):[a ε n & b ε n => [a<b <=> EXIST(c):[c ε n & a+c=b]]] Definition Previous Results ---------------- Lemma 1: 1<=x in n 9 ALL(a):[a ε n => 1<=a] Axiom Lemma 2: < to <= 10 ALL(a):ALL(b):[a ε n & b ε n & a<b => a+1<=b] Axiom Lemma 3: <= and < 11 ALL(a):ALL(b):ALL(c):[a ε n & b ε n & c ε n & a<=b & b<c => a<c] Axiom Lemma 4: <= to < 12 ALL(a):ALL(b):[a ε n & b ε n => [b<=a <=> ~a<b]] Axiom Proof ----- Let s be a non-empty subset on n with an upper bound. 13 Set(s) & ALL(b):[b ε s => b ε n] & EXIST(b):b ε s & EXIST(b):[b ε n & ALL(c):[c ε s => c<=b]] Premise 14 Set(s) Split, 13 15 ALL(b):[b ε s => b ε n] Split, 13 16 EXIST(b):b ε s Split, 13 17 EXIST(b):[b ε n & ALL(c):[c ε s => c<=b]] Split, 13 Define: x (an element of s) 18 x ε s E Spec, 16 19 x ε s => x ε n U Spec, 15 20 x ε n Detach, 19, 18 21 ub ε n & ALL(c):[c ε s => c<=ub] E Spec, 17 Define: ub (an upper bound of s) 22 ub ε n Split, 21 23 ALL(c):[c ε s => c<=ub] Split, 21 Prove: EXIST(b):[b ε s & ALL(c):[c ε s => c<=b]] Suppose to the contrary that there is no least upper bound of s. 24 ~EXIST(b):[b ε s & ALL(c):[c ε s => c<=b]] Premise 25 ~~ALL(b):~[b ε s & ALL(c):[c ε s => c<=b]] Quant, 24 26 ALL(b):~[b ε s & ALL(c):[c ε s => c<=b]] Rem DNeg, 25 27 ALL(b):~~[b ε s => ~ALL(c):[c ε s => c<=b]] Imply-And, 26 28 ALL(b):[b ε s => ~ALL(c):[c ε s => c<=b]] Rem DNeg, 27 29 ALL(b):[b ε s => ~~EXIST(c):~[c ε s => c<=b]] Quant, 28 30 ALL(b):[b ε s => EXIST(c):~[c ε s => c<=b]] Rem DNeg, 29 31 ALL(b):[b ε s => EXIST(c):~~[c ε s & ~c<=b]] Imply-And, 30 We assume that for every element of s, there exists a greater element of s. 32 ALL(b):[b ε s => EXIST(c):[c ε s & ~c<=b]] Rem DNeg, 31 Sufficient: ALL(a):[a ε n => EXIST(b):[b ε s & a<b]] 33 EXIST(b):[b ε s & 1<b] & ALL(a):[a ε n & EXIST(b):[b ε s & a<b] => EXIST(b):[b ε s & a+1<b]] => ALL(a):[a ε n => EXIST(b):[b ε s & a<b]] Induction 34 x ε s => EXIST(c):[c ε s & ~c<=x] U Spec, 32 35 EXIST(c):[c ε s & ~c<=x] Detach, 34, 18 36 x' ε s & ~x'<=x E Spec, 35 Define: x' 37 x' ε s Split, 36 38 ~x'<=x Split, 36 39 x' ε s => x' ε n U Spec, 15 40 x' ε n Detach, 39, 37 Apply Lemma 4 41 ALL(b):[x ε n & b ε n => [b<=x <=> ~x<b]] U Spec, 12 42 x ε n & x' ε n => [x'<=x <=> ~x<x'] U Spec, 41 43 x ε n & x' ε n Join, 20, 40 44 x'<=x <=> ~x<x' Detach, 42, 43 45 [x'<=x => ~x<x'] & [~x<x' => x'<=x] Iff-And, 44 46 x'<=x => ~x<x' Split, 45 47 ~x<x' => x'<=x Split, 45 48 ~x'<=x => ~~x<x' Contra, 47 49 ~x'<=x => x<x' Rem DNeg, 48 50 x<x' Detach, 49, 38 Apply Lemma 1 51 x ε n => 1<=x U Spec, 9 52 1<=x Detach, 51, 20 Apply Lemma 3 53 ALL(b):ALL(c):[1 ε n & b ε n & c ε n & 1<=b & b<c => 1<c] U Spec, 11 54 ALL(c):[1 ε n & x ε n & c ε n & 1<=x & x<c => 1<c] U Spec, 53 55 1 ε n & x ε n & x' ε n & 1<=x & x<x' => 1<x' U Spec, 54 56 1 ε n & x ε n Join, 2, 20 57 1 ε n & x ε n & x' ε n Join, 56, 40 58 1 ε n & x ε n & x' ε n & 1<=x Join, 57, 52 59 1 ε n & x ε n & x' ε n & 1<=x & x<x' Join, 58, 50 60 1<x' Detach, 55, 59 61 x' ε s & 1<x' Join, 37, 60 Base Step --------- As Required: 62 EXIST(b):[b ε s & 1<b] E Gen, 61 Inductive Step -------------- Prove: ALL(a):[a ε n & EXIST(b):[b ε s & a<b] => EXIST(b):[b ε s & a+1<b]] Suppose... 63 k ε n & EXIST(b):[b ε s & k<b] Premise 64 k ε n Split, 63 65 EXIST(b):[b ε s & k<b] Split, 63 66 k' ε s & k<k' E Spec, 65 Define: k' 67 k' ε s Split, 66 68 k<k' Split, 66 69 k' ε s => k' ε n U Spec, 15 70 k' ε n Detach, 69, 67 Apply Lemma 2 71 ALL(b):[k ε n & b ε n & k<b => k+1<=b] U Spec, 10 72 k ε n & k' ε n & k<k' => k+1<=k' U Spec, 71 73 k ε n & k' ε n Join, 64, 70 74 k ε n & k' ε n & k<k' Join, 73, 68 75 k+1<=k' Detach, 72, 74 Apply assumption 76 k' ε s => EXIST(c):[c ε s & ~c<=k'] U Spec, 32 77 EXIST(c):[c ε s & ~c<=k'] Detach, 76, 67 78 k'' ε s & ~k''<=k' E Spec, 77 Define: k'' 79 k'' ε s Split, 78 80 ~k''<=k' Split, 78 Apply definition of s 81 k'' ε s => k'' ε n U Spec, 15 82 k'' ε n Detach, 81, 79 Apply Lemma 4 83 ALL(b):[k' ε n & b ε n => [b<=k' <=> ~k'<b]] U Spec, 12 84 k' ε n & k'' ε n => [k''<=k' <=> ~k'<k''] U Spec, 83 85 k' ε n & k'' ε n Join, 70, 82 86 k''<=k' <=> ~k'<k'' Detach, 84, 85 87 [k''<=k' => ~k'<k''] & [~k'<k'' => k''<=k'] Iff-And, 86 88 k''<=k' => ~k'<k'' Split, 87 89 ~k'<k'' => k''<=k' Split, 87 90 ~k''<=k' => ~~k'<k'' Contra, 89 91 ~k''<=k' => k'<k'' Rem DNeg, 90 92 k'<k'' Detach, 91, 80 Apply Lemma 3 93 ALL(b):ALL(c):[k+1 ε n & b ε n & c ε n & k+1<=b & b<c => k+1<c] U Spec, 11 94 ALL(c):[k+1 ε n & k' ε n & c ε n & k+1<=k' & k'<c => k+1<c] U Spec, 93 95 k+1 ε n & k' ε n & k'' ε n & k+1<=k' & k'<k'' => k+1<k'' U Spec, 94 96 ALL(b):[k ε n & b ε n => k+b ε n] U Spec, 3 97 k ε n & 1 ε n => k+1 ε n U Spec, 96 98 k ε n & 1 ε n Join, 64, 2 99 k+1 ε n Detach, 97, 98 100 k+1 ε n & k' ε n Join, 99, 70 101 k+1 ε n & k' ε n & k'' ε n Join, 100, 82 102 k+1 ε n & k' ε n & k'' ε n & k+1<=k' Join, 101, 75 103 k+1 ε n & k' ε n & k'' ε n & k+1<=k' & k'<k'' Join, 102, 92 104 k+1<k'' Detach, 95, 103 105 k'' ε s & k+1<k'' Join, 79, 104 Generalizing... 106 EXIST(b):[b ε s & k+1<b] E Gen, 105 Inductive Step -------------- As Required: 107 ALL(a):[a ε n & EXIST(b):[b ε s & a<b] => EXIST(b):[b ε s & a+1<b]] Conclusion, 63 108 EXIST(b):[b ε s & 1<b] & ALL(a):[a ε n & EXIST(b):[b ε s & a<b] => EXIST(b):[b ε s & a+1<b]] Join, 62, 107 By induction... 109 ALL(a):[a ε n => EXIST(b):[b ε s & a<b]] Detach, 33, 108 Apply result for a=ub 110 ub ε n => EXIST(b):[b ε s & ub<b] U Spec, 109 111 EXIST(b):[b ε s & ub<b] Detach, 110, 22 112 ub' ε s & ub<ub' E Spec, 111 Define: ub' 113 ub' ε s Split, 112 114 ub<ub' Split, 112 Apply definition of s 115 ub' ε s => ub' ε n U Spec, 15 116 ub' ε n Detach, 115, 113 Apply definition of ub 117 ub' ε s => ub'<=ub U Spec, 23 118 ub'<=ub Detach, 117, 113 Apply Lemma 4 119 ALL(b):[ub ε n & b ε n => [b<=ub <=> ~ub<b]] U Spec, 12 120 ub ε n & ub' ε n => [ub'<=ub <=> ~ub<ub'] U Spec, 119 121 ub ε n & ub' ε n Join, 22, 116 122 ub'<=ub <=> ~ub<ub' Detach, 120, 121 123 [ub'<=ub => ~ub<ub'] & [~ub<ub' => ub'<=ub] Iff-And, 122 124 ub'<=ub => ~ub<ub' Split, 123 125 ~ub<ub' => ub'<=ub Split, 123 126 ~~ub<ub' => ~ub'<=ub Contra, 124 127 ub<ub' => ~ub'<=ub Rem DNeg, 126 128 ~ub'<=ub Detach, 127, 114 Obtain contradiction... 129 ub'<=ub & ~ub'<=ub Join, 118, 128 By contradiction... As Required: 130 ~~EXIST(b):[b ε s & ALL(c):[c ε s => c<=b]] Conclusion, 24 131 EXIST(b):[b ε s & ALL(c):[c ε s => c<=b]] Rem DNeg, 130 As Required: 132 ALL(a):[Set(a) & ALL(b):[b ε a => b ε n] & EXIST(b):b ε a & EXIST(b):[b ε n & ALL(c):[c ε a => c<=b]] => EXIST(b):[b ε a & ALL(c):[c ε a => c<=b]]] Conclusion, 13