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