|
1 (* Title: ZF/AC/AC_Equiv.thy |
|
2 ID: $Id$ |
|
3 Author: Krzysztof Gr`abczewski |
|
4 |
|
5 Axioms AC1 -- AC19 come from "Equivalents of the Axiom of Choice, II" |
|
6 by H. Rubin and J.E. Rubin, 1985. |
|
7 |
|
8 Axiom AC0 comes from "Axiomatic Set Theory" by P. Suppes, 1972. |
|
9 |
|
10 Some Isabelle proofs of equivalences of these axioms are formalizations of |
|
11 proofs presented by Rubin. The others are based on Rubin's proofs, but |
|
12 slightly changed. |
|
13 *) |
|
14 |
|
15 AC_Equiv = CardinalArith + Univ + Transrec2 + |
|
16 |
|
17 consts |
|
18 |
|
19 (* Well Ordering Theorems *) |
|
20 WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: "o" |
|
21 WO4 :: "i => o" |
|
22 |
|
23 (* Axioms of Choice *) |
|
24 AC0, AC1, AC2, AC3, AC4, AC5, AC6, AC7, AC8, AC9, |
|
25 AC11, AC12, AC14, AC15, AC17, AC18, AC19 :: "o" |
|
26 AC10, AC13 :: "i => o" |
|
27 AC16 :: "[i, i] => o" |
|
28 |
|
29 (* Auxiliary definitions used in theorems *) |
|
30 first :: "[i, i, i] => o" |
|
31 exists_first :: "[i, i] => o" |
|
32 pairwise_disjoint :: "i => o" |
|
33 sets_of_size_between :: "[i, i, i] => o" |
|
34 |
|
35 (* Auxiliary definitions used in proofs *) |
|
36 NN :: "i => i" |
|
37 uu :: "[i, i, i, i] => i" |
|
38 |
|
39 (* Other useful definitions *) |
|
40 vv1 :: "[i, i, i] => i" |
|
41 ww1 :: "[i, i, i] => i" |
|
42 vv2 :: "[i, i, i, i] => i" |
|
43 ww2 :: "[i, i, i, i] => i" |
|
44 |
|
45 GG :: "[i, i, i] => i" |
|
46 GG2 :: "[i, i, i] => i" |
|
47 HH :: "[i, i, i] => i" |
|
48 |
|
49 recfunAC16 :: "[i, i, i, i] => i" |
|
50 |
|
51 defs |
|
52 |
|
53 (* Well Ordering Theorems *) |
|
54 |
|
55 WO1_def "WO1 == ALL A. EX R. well_ord(A,R)" |
|
56 |
|
57 WO2_def "WO2 == ALL A. EX a. Ord(a) & A eqpoll a" |
|
58 |
|
59 WO3_def "WO3 == ALL A. EX a. Ord(a) & (EX b. b <= a & A eqpoll b)" |
|
60 |
|
61 WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a & \ |
|
62 \ (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)" |
|
63 |
|
64 WO5_def "WO5 == EX m:nat. 1 le m & WO4(m)" |
|
65 |
|
66 WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a \ |
|
67 \ & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))" |
|
68 |
|
69 WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) --> \ |
|
70 \ well_ord(A,converse(R)))" |
|
71 |
|
72 WO8_def "WO8 == ALL A. (0~:A --> (EX f. f : (PROD X:A. X))) --> \ |
|
73 \ (EX R. well_ord(A,R))" |
|
74 |
|
75 (* Axioms of Choice *) |
|
76 |
|
77 AC0_def "AC0 == ALL A. EX f. f:(PROD X:Pow(A)-{0}. X)" |
|
78 |
|
79 AC1_def "AC1 == ALL A. 0~:A --> (EX f. f:(PROD X:A. X))" |
|
80 |
|
81 AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A) \ |
|
82 \ --> (EX C. ALL B:A. EX y. B Int C = {y})" |
|
83 |
|
84 AC3_def "AC3 == ALL A B. ALL f:A->B. EX g. g:(PROD x:{a:A. f`a~=0}. f`x)" |
|
85 |
|
86 AC4_def "AC4 == ALL R A B. (R<=A*B --> (EX f. f:(PROD x:domain(R). R``{x})))" |
|
87 |
|
88 AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A. \ |
|
89 \ ALL x:domain(g). f`(g`x) = x" |
|
90 |
|
91 AC6_def "AC6 == ALL A. 0~:A --> (PROD B:A. B)~=0" |
|
92 |
|
93 AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2) \ |
|
94 \ --> (PROD B:A. B)~=0" |
|
95 |
|
96 AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2) \ |
|
97 \ --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))" |
|
98 |
|
99 AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) --> \ |
|
100 \ (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))" |
|
101 |
|
102 AC10_def "AC10(n) == ALL A. (ALL B:A. ~Finite(B)) --> \ |
|
103 \ (EX f. ALL B:A. (pairwise_disjoint(f`B) & \ |
|
104 \ sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))" |
|
105 |
|
106 AC11_def "AC11 == EX n:nat. 1 le n & AC10(n)" |
|
107 |
|
108 AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) --> \ |
|
109 \ (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) & \ |
|
110 \ sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))" |
|
111 |
|
112 AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 & \ |
|
113 \ f`B <= B & f`B lepoll m)" |
|
114 |
|
115 AC14_def "AC14 == EX m:nat. 1 le m & AC13(m)" |
|
116 |
|
117 AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A. \ |
|
118 \ f`B~=0 & f`B <= B & f`B lepoll m))" |
|
119 |
|
120 AC16_def "AC16(n, k) == ALL A. ~Finite(A) --> \ |
|
121 \ (EX T. T <= {X:Pow(A). X eqpoll succ(n)} & \ |
|
122 \ (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))" |
|
123 |
|
124 AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}. \ |
|
125 \ EX f: Pow(A)-{0} -> A. f`(g`f) : g`f" |
|
126 |
|
127 (***problems! X is free, and is higher-order! |
|
128 AC18_def "AC18 == ALL A. A~=0 --> (ALL F. (domain(F) = A & \ |
|
129 \ (ALL a:A. F`a ~= 0)) --> \ |
|
130 \ ((INT a:A. UN b:F`a. X(a,b)) = \ |
|
131 \ (UN f: PROD a:A. F`a. INT a:A. X(a, f`a))))" |
|
132 ***) |
|
133 |
|
134 AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) = \ |
|
135 \ (UN f:{f: A->Union(A). ALL B:A. f`B:B}. INT a:A. f`a))" |
|
136 |
|
137 (* Auxiliary definitions used in theorems *) |
|
138 |
|
139 first_def "first(u, X, R) \ |
|
140 \ == u:X & (ALL v:X. v~=u --> <u,v> : R)" |
|
141 |
|
142 exists_first_def "exists_first(X,R) \ |
|
143 \ == EX u:X. first(u, X, R)" |
|
144 |
|
145 pairwise_disjoint_def "pairwise_disjoint(A) \ |
|
146 \ == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2" |
|
147 |
|
148 sets_of_size_between_def "sets_of_size_between(A,m,n) \ |
|
149 \ == ALL B:A. m lepoll B & B lepoll n" |
|
150 |
|
151 (* Auxiliary definitions used in proofs *) |
|
152 |
|
153 NN_def "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a \ |
|
154 \ & (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}" |
|
155 |
|
156 uu_def "uu(f, beta, gamma, delta) \ |
|
157 \ == (f`beta * f`gamma) Int f`delta" |
|
158 |
|
159 (* Other useful definitions *) |
|
160 |
|
161 vv1_def "vv1(f,b,m) == if(f`b ~= 0, \ |
|
162 \ domain(uu(f,b, \ |
|
163 \ LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 & \ |
|
164 \ domain(uu(f,b,g,d)) lesspoll m)), \ |
|
165 \ LEAST d. domain(uu(f,b, \ |
|
166 \ LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 & \ |
|
167 \ domain(uu(f,b,g,d)) lesspoll m)), d)) ~= 0 & \ |
|
168 \ domain(uu(f,b, \ |
|
169 \ LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 & \ |
|
170 \ domain(uu(f,b,g,d)) lesspoll m)), d)) lesspoll m)), 0)" |
|
171 |
|
172 ww1_def "ww1(f,b,m) == f`b - vv1(f,b,m)" |
|
173 |
|
174 vv2_def "vv2(f,b,g,s) == \ |
|
175 \ if(f`g ~= 0, {uu(f,b,g,LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)" |
|
176 |
|
177 ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)" |
|
178 |
|
179 GG_def "GG(f,x,a) == transrec(a, %b r. (lam z:Pow(x). \ |
|
180 \ if(z=0, x, f`z))`(x - {r`c. c:b}))" |
|
181 |
|
182 GG2_def "GG2(f,x,a) == transrec(a, %b r. (lam z:Pow(x). \ |
|
183 \ if(z=0, {x}, f`z))`(x - Union({r`c. c:b})))" |
|
184 |
|
185 HH_def "HH(f,x,a) == transrec(a, %b r. (lam z:Pow(x). \ |
|
186 \ if(z=0|f`z~:z, x, f`z))`(x - {r`c. c:b}))" |
|
187 |
|
188 recfunAC16_def |
|
189 "recfunAC16(f,fa,i,a) == \ |
|
190 \ transrec2(i, 0, \ |
|
191 \ %g r. if(EX y:r. fa`g <= y, r, \ |
|
192 \ r Un {f`(LEAST i. fa`g <= f`i & \ |
|
193 \ (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))" |
|
194 |
|
195 end |