NameDateSize

..09-Nov-202024

.gitignoreH A D25-Jul-201912

cardinalScript.smlH A D07-Jul-2020142.3 KiB

emitOrdinalScript.smlH A D10-Jul-20201,019

finite_setScript.smlH A D11-Aug-202025.8 KiB

HolmakefileH A D25-Jul-201985

ordinalNotationScript.smlH A D10-Jul-202031.7 KiB

ordinalScript.smlH A D06-Aug-202080.7 KiB

ordNotationSemanticsScript.smlH A D07-Jul-202027.2 KiB

READMEH A D25-Jul-20191.7 KiB

simpleSetCatScript.smlH A D11-Aug-202016.6 KiB

ucordScript.smlH A D07-Jul-20203.8 KiB

veblenScript.smlH A D07-Jul-20205.3 KiB

wellorderScript.smlH A D11-Jun-202066.6 KiB

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