991
|
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 |
GG :: "[i, i, i] => i"
|
|
36 |
GG2 :: "[i, i, i] => i"
|
|
37 |
HH :: "[i, i, i] => i"
|
|
38 |
|
|
39 |
recfunAC16 :: "[i, i, i, i] => i"
|
|
40 |
|
|
41 |
defs
|
|
42 |
|
|
43 |
(* Well Ordering Theorems *)
|
|
44 |
|
|
45 |
WO1_def "WO1 == ALL A. EX R. well_ord(A,R)"
|
|
46 |
|
|
47 |
WO2_def "WO2 == ALL A. EX a. Ord(a) & A eqpoll a"
|
|
48 |
|
|
49 |
WO3_def "WO3 == ALL A. EX a. Ord(a) & (EX b. b <= a & A eqpoll b)"
|
|
50 |
|
|
51 |
WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a & \
|
|
52 |
\ (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
|
|
53 |
|
|
54 |
WO5_def "WO5 == EX m:nat. 1 le m & WO4(m)"
|
|
55 |
|
|
56 |
WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a \
|
|
57 |
\ & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
|
|
58 |
|
|
59 |
WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) --> \
|
|
60 |
\ well_ord(A,converse(R)))"
|
|
61 |
|
|
62 |
WO8_def "WO8 == ALL A. (0~:A --> (EX f. f : (PROD X:A. X))) --> \
|
|
63 |
\ (EX R. well_ord(A,R))"
|
|
64 |
|
|
65 |
(* Axioms of Choice *)
|
|
66 |
|
|
67 |
AC0_def "AC0 == ALL A. EX f. f:(PROD X:Pow(A)-{0}. X)"
|
|
68 |
|
|
69 |
AC1_def "AC1 == ALL A. 0~:A --> (EX f. f:(PROD X:A. X))"
|
|
70 |
|
|
71 |
AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A) \
|
|
72 |
\ --> (EX C. ALL B:A. EX y. B Int C = {y})"
|
|
73 |
|
|
74 |
AC3_def "AC3 == ALL A B. ALL f:A->B. EX g. g:(PROD x:{a:A. f`a~=0}. f`x)"
|
|
75 |
|
|
76 |
AC4_def "AC4 == ALL R A B. (R<=A*B --> (EX f. f:(PROD x:domain(R). R``{x})))"
|
|
77 |
|
|
78 |
AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A. \
|
|
79 |
\ ALL x:domain(g). f`(g`x) = x"
|
|
80 |
|
|
81 |
AC6_def "AC6 == ALL A. 0~:A --> (PROD B:A. B)~=0"
|
|
82 |
|
|
83 |
AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2) \
|
|
84 |
\ --> (PROD B:A. B)~=0"
|
|
85 |
|
|
86 |
AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2) \
|
|
87 |
\ --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
|
|
88 |
|
|
89 |
AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) --> \
|
|
90 |
\ (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
|
|
91 |
|
|
92 |
AC10_def "AC10(n) == ALL A. (ALL B:A. ~Finite(B)) --> \
|
|
93 |
\ (EX f. ALL B:A. (pairwise_disjoint(f`B) & \
|
|
94 |
\ sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
|
|
95 |
|
|
96 |
AC11_def "AC11 == EX n:nat. 1 le n & AC10(n)"
|
|
97 |
|
|
98 |
AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) --> \
|
|
99 |
\ (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) & \
|
|
100 |
\ sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
|
|
101 |
|
|
102 |
AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 & \
|
|
103 |
\ f`B <= B & f`B lepoll m)"
|
|
104 |
|
|
105 |
AC14_def "AC14 == EX m:nat. 1 le m & AC13(m)"
|
|
106 |
|
|
107 |
AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A. \
|
|
108 |
\ f`B~=0 & f`B <= B & f`B lepoll m))"
|
|
109 |
|
|
110 |
AC16_def "AC16(n, k) == ALL A. ~Finite(A) --> \
|
|
111 |
\ (EX T. T <= {X:Pow(A). X eqpoll succ(n)} & \
|
|
112 |
\ (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
|
|
113 |
|
|
114 |
AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}. \
|
|
115 |
\ EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
|
|
116 |
|
|
117 |
(***problems! X is free, and is higher-order!
|
|
118 |
AC18_def "AC18 == ALL A. A~=0 --> (ALL F. (domain(F) = A & \
|
|
119 |
\ (ALL a:A. F`a ~= 0)) --> \
|
|
120 |
\ ((INT a:A. UN b:F`a. X(a,b)) = \
|
|
121 |
\ (UN f: PROD a:A. F`a. INT a:A. X(a, f`a))))"
|
|
122 |
***)
|
|
123 |
|
|
124 |
AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) = \
|
|
125 |
\ (UN f:{f: A->Union(A). ALL B:A. f`B:B}. INT a:A. f`a))"
|
|
126 |
|
|
127 |
(* Auxiliary definitions used in theorems *)
|
|
128 |
|
|
129 |
first_def "first(u, X, R) \
|
|
130 |
\ == u:X & (ALL v:X. v~=u --> <u,v> : R)"
|
|
131 |
|
|
132 |
exists_first_def "exists_first(X,R) \
|
|
133 |
\ == EX u:X. first(u, X, R)"
|
|
134 |
|
|
135 |
pairwise_disjoint_def "pairwise_disjoint(A) \
|
|
136 |
\ == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
|
|
137 |
|
|
138 |
sets_of_size_between_def "sets_of_size_between(A,m,n) \
|
|
139 |
\ == ALL B:A. m lepoll B & B lepoll n"
|
|
140 |
|
|
141 |
(* Auxiliary definitions used in proofs *)
|
|
142 |
|
|
143 |
GG_def "GG(f,x,a) == transrec(a, %b r. (lam z:Pow(x). \
|
|
144 |
\ if(z=0, x, f`z))`(x - {r`c. c:b}))"
|
|
145 |
|
|
146 |
GG2_def "GG2(f,x,a) == transrec(a, %b r. (lam z:Pow(x). \
|
|
147 |
\ if(z=0, {x}, f`z))`(x - Union({r`c. c:b})))"
|
|
148 |
|
|
149 |
HH_def "HH(f,x,a) == transrec(a, %b r. (lam z:Pow(x). \
|
|
150 |
\ if(z=0|f`z~:z, x, f`z))`(x - {r`c. c:b}))"
|
|
151 |
|
|
152 |
recfunAC16_def
|
|
153 |
"recfunAC16(f,fa,i,a) == \
|
|
154 |
\ transrec2(i, 0, \
|
|
155 |
\ %g r. if(EX y:r. fa`g <= y, r, \
|
|
156 |
\ r Un {f`(LEAST i. fa`g <= f`i & \
|
|
157 |
\ (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
|
|
158 |
|
|
159 |
end
|