6 Orders in Zermelo-Fraenkel Set Theory |
6 Orders in Zermelo-Fraenkel Set Theory |
7 *) |
7 *) |
8 |
8 |
9 Order = WF + Perm + |
9 Order = WF + Perm + |
10 consts |
10 consts |
11 part_ord :: "[i,i]=>o" (*Strict partial ordering*) |
11 part_ord :: [i,i]=>o (*Strict partial ordering*) |
12 linear, tot_ord :: "[i,i]=>o" (*Strict total ordering*) |
12 linear, tot_ord :: [i,i]=>o (*Strict total ordering*) |
13 well_ord :: "[i,i]=>o" (*Well-ordering*) |
13 well_ord :: [i,i]=>o (*Well-ordering*) |
14 mono_map :: "[i,i,i,i]=>i" (*Order-preserving maps*) |
14 mono_map :: [i,i,i,i]=>i (*Order-preserving maps*) |
15 ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*) |
15 ord_iso :: [i,i,i,i]=>i (*Order isomorphisms*) |
16 pred :: "[i,i,i]=>i" (*Set of predecessors*) |
16 pred :: [i,i,i]=>i (*Set of predecessors*) |
17 ord_iso_map :: "[i,i,i,i]=>i" (*Construction for linearity theorem*) |
17 ord_iso_map :: [i,i,i,i]=>i (*Construction for linearity theorem*) |
18 |
18 |
19 defs |
19 defs |
20 part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)" |
20 part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)" |
21 |
21 |
22 linear_def "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)" |
22 linear_def "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)" |