README
1The theories in this directory:
2
3wellorder:
4 A basic theory of well-orders. Includes an ordering relation on
5 well-orders, which is itself shown to be a well-order. Also proves
6 that every set can be well-ordered (using Zorn's lemma from
7 set_relationTheory).
8
9cardinal:
10 A basic theory of the cardinality partial order and equivalence
11 relations (��� and ��� respectively). Thus includes a proof that ��� is
12 anti-symmetric (Schroder-Bernstein). Also, totality of ��� (from
13 well-orderability of all sets). Finally, the important result that
14 A �� A ��� A (another use of Zorn's Lemma).
15
16ordinal:
17 By quotienting the wellorders, derive a type of ordinal numbers
18 (parameterised by the underlying type over which the wellorders are
19 constructed). Show that this includes a copy of the natural numbers
20 and a supremum operation. The latter is not always well-defined (in
21 particular, you can't take a supremum of the whole type and expect
22 to get back a new ordinal). Derive the standard arithmetic
23 operations, define constants such as �� and �����, and show that all
24 ordinals have a standard "polynomial" representation.
25
26ucord:
27 Show the existence of uncountable ordinals if the underlying type is
28 big enough (itself uncountable).
29
30ordinalNotation:
31 A development of a concrete notation for ordinals up to �����. Based on
32 the paper
33
34 "Wellfounded induction on the ordinals up to e0".
35 Matt Kaufmann and Konrad Slind,
36 TPHOLs 2007,
37 LNCS 4732
38 URL: http://dx.doi.org/10.1007/978-3-540-74591-4_22
39
40 There is a proof of the same results in the examples/acl2/ml
41 directory, but based in a theory of s-expressions.
42
43 Some minor additions to this theory show some of the connection with
44 the other presentation of ordinals.
45