15 AC_Equiv = CardinalArith + Univ + OrdQuant + |
15 AC_Equiv = CardinalArith + Univ + OrdQuant + |
16 |
16 |
17 consts |
17 consts |
18 |
18 |
19 (* Well Ordering Theorems *) |
19 (* Well Ordering Theorems *) |
20 WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: "o" |
20 WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: o |
21 WO4 :: "i => o" |
21 WO4 :: i => o |
22 |
22 |
23 (* Axioms of Choice *) |
23 (* Axioms of Choice *) |
24 AC0, AC1, AC2, AC3, AC4, AC5, AC6, AC7, AC8, AC9, |
24 AC0, AC1, AC2, AC3, AC4, AC5, AC6, AC7, AC8, AC9, |
25 AC11, AC12, AC14, AC15, AC17, AC19 :: "o" |
25 AC11, AC12, AC14, AC15, AC17, AC19 :: o |
26 AC10, AC13 :: "i => o" |
26 AC10, AC13 :: i => o |
27 AC16 :: "[i, i] => o" |
27 AC16 :: [i, i] => o |
28 AC18 :: "prop" ("AC18") |
28 AC18 :: prop ("AC18") |
29 |
29 |
30 (* Auxiliary definitions used in definitions *) |
30 (* Auxiliary definitions used in definitions *) |
31 pairwise_disjoint :: "i => o" |
31 pairwise_disjoint :: i => o |
32 sets_of_size_between :: "[i, i, i] => o" |
32 sets_of_size_between :: [i, i, i] => o |
33 |
33 |
34 defs |
34 defs |
35 |
35 |
36 (* Well Ordering Theorems *) |
36 (* Well Ordering Theorems *) |
37 |
37 |