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