src/ZF/AC/AC_Equiv.thy
 author clasohm Tue Feb 06 12:27:17 1996 +0100 (1996-02-06) changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 2469 b50b8c0eec01 permissions -rw-r--r--
expanded tabs
```     1 (*  Title:      ZF/AC/AC_Equiv.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Krzysztof Grabczewski
```
```     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 the Rubins.  The others are based on the Rubins' proofs,
```
```    12 but slightly changed.
```
```    13 *)
```
```    14
```
```    15 AC_Equiv = CardinalArith + Univ + OrdQuant +
```
```    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, AC19 :: o
```
```    26   AC10, AC13              :: i => o
```
```    27   AC16                    :: [i, i] => o
```
```    28   AC18                    :: prop       ("AC18")
```
```    29
```
```    30 (* Auxiliary definitions used in definitions *)
```
```    31   pairwise_disjoint       :: i => o
```
```    32   sets_of_size_between    :: [i, i, i] => o
```
```    33
```
```    34 defs
```
```    35
```
```    36 (* Well Ordering Theorems *)
```
```    37
```
```    38   WO1_def "WO1 == ALL A. EX R. well_ord(A,R)"
```
```    39
```
```    40   WO2_def "WO2 == ALL A. EX a. Ord(a) & A eqpoll a"
```
```    41
```
```    42   WO3_def "WO3 == ALL A. EX a. Ord(a) & (EX b. b <= a & A eqpoll b)"
```
```    43
```
```    44   WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &
```
```    45                      (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
```
```    46
```
```    47   WO5_def "WO5 == EX m:nat. 1 le m & WO4(m)"
```
```    48
```
```    49   WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a
```
```    50                     & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
```
```    51
```
```    52   WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->
```
```    53                     well_ord(A,converse(R)))"
```
```    54
```
```    55   WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) -->
```
```    56                     (EX R. well_ord(A,R))"
```
```    57
```
```    58 (* Axioms of Choice *)
```
```    59
```
```    60   AC0_def "AC0 == ALL A. EX f. f:(PROD X:Pow(A)-{0}. X)"
```
```    61
```
```    62   AC1_def "AC1 == ALL A. 0~:A --> (EX f. f:(PROD X:A. X))"
```
```    63
```
```    64   AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)
```
```    65                     --> (EX C. ALL B:A. EX y. B Int C = {y})"
```
```    66
```
```    67   AC3_def "AC3 == ALL A B. ALL f:A->B. EX g. g:(PROD x:{a:A. f`a~=0}. f`x)"
```
```    68
```
```    69   AC4_def "AC4 == ALL R A B. (R<=A*B --> (EX f. f:(PROD x:domain(R). R``{x})))"
```
```    70
```
```    71   AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A.
```
```    72                     ALL x:domain(g). f`(g`x) = x"
```
```    73
```
```    74   AC6_def "AC6 == ALL A. 0~:A --> (PROD B:A. B)~=0"
```
```    75
```
```    76   AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)
```
```    77                     --> (PROD B:A. B)~=0"
```
```    78
```
```    79   AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2)
```
```    80                     --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
```
```    81
```
```    82   AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->
```
```    83                     (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
```
```    84
```
```    85   AC10_def "AC10(n) ==  ALL A. (ALL B:A. ~Finite(B)) -->
```
```    86                     (EX f. ALL B:A. (pairwise_disjoint(f`B) &
```
```    87                     sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
```
```    88
```
```    89   AC11_def "AC11 == EX n:nat. 1 le n & AC10(n)"
```
```    90
```
```    91   AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->
```
```    92             (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &
```
```    93             sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
```
```    94
```
```    95   AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &
```
```    96                                           f`B <= B & f`B lepoll m)"
```
```    97
```
```    98   AC14_def "AC14 == EX m:nat. 1 le m & AC13(m)"
```
```    99
```
```   100   AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.
```
```   101                                       f`B~=0 & f`B <= B & f`B lepoll m))"
```
```   102
```
```   103   AC16_def "AC16(n, k)  == ALL A. ~Finite(A) -->
```
```   104             (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &
```
```   105             (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
```
```   106
```
```   107   AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}.
```
```   108                     EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
```
```   109
```
```   110   AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) -->
```
```   111                  ((INT a:A. UN b:B(a). X(a,b)) =
```
```   112                  (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
```
```   113
```
```   114   AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =
```
```   115                     (UN f:(PROD B:A. B). INT a:A. f`a))"
```
```   116
```
```   117 (* Auxiliary definitions used in the above definitions *)
```
```   118
```
```   119   pairwise_disjoint_def    "pairwise_disjoint(A)
```
```   120                             == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
```
```   121
```
```   122   sets_of_size_between_def "sets_of_size_between(A,m,n)
```
```   123                             == ALL B:A. m lepoll B & B lepoll n"
```
```   124
```
```   125 end
```