L. T3lt_psi, = [|| [&& a==a', b==b' & c < c'], [&& a==a', b < b' & c <

V. Claims, V. Are, and . To, We first show that if x ? b or x ? c, then x < [a, b, c], by induction on the size of x. Consider the case x ? b. Assume x = [a ? , b ? , c ? , n ? , d ? ]. It suffices to show By induction b ? < y and c ? < y. By assumption y < b, so that b ? < b and c ? < b. By induction, b ? and c ? are less than [a, b, c]. The result follows The case x ? c is similar (if a = a ? , we have to compare b and b ? ) Assume now x ? a. The same argument as above gives a ? < a, The result follows from G6e

. Lemma-succ_inj-x-y, T3nf x -> T3nf y -> (T3succ x == T3succ y) = (x==y)

. Lemma-lt_succ_succe-x-y, T3nf x -> T3nf y -> (T3succ x < T3succ y) = (x < y)

. Lemma-le_succ_succe-x-y, T3nf x -> T3nf y -> (T3succ x <= T3succ y) = (x <= y)

. Lemma, T3succ a <= b -> a < b. Lemma lt_succ_le_2 a b: T3nf a -> a < T3succ b -> a <= b. Lemma lt_succ_le_3 a b, p.3

J. Grimm-lemma-t3sub0n, Lemma T3subnn x: x -x = zero. Lemma minus_lt a b: a < b -> a -b = zero. Lemma minus_le a b: a <= b -> a -b = zero

. Lemma, T3succ a = a + one Lemma add1Nfin a: ~~ T3finite a -> one + a = a. Lemma sub1Nfin a: ~~ T3finite a -> a -one = a. Lemma sub1a x: x != zero ->

. Lemma-sub_1ace, T3bad) : one + (a -one) != a. Lemma sub_1bCE (a:= T3bad) : (one + a -one) != a

. Lemma-split_add-x, let: (y,n) :=T3split x in T3nf x -> (x == y + \F n) && ((y==zero) || T3limit y )

. Lemma-add_inj-a-b-c, T3nf b -> T3nf c -> a + b = a + c -> b = c. Lemma sub_pr1 a b: T3nf b -> a <= b -> b = a + (b -a)

L. Assume and ?. , Then L( f , [x, 0, y + 1]). Same method as above

L. Assume and ?. , Then L( f , [x, y, z + 1])

J. Grimm, If x < ? 0 , the quantities x 1 , x 2 and R(x) defined by (5.2) are all < ? 0 . One can generalize the Veblen construction: from f (x) we get f (x, y), then f (x, y, z), etc. [This is not yet implemented in COQ] Veblen considers a function f (x 1 , x 2 , . . .) with an arbitrary number of arguments; this means that the argument of f is a function x, such that for every ordinal i , x i is an ordinal; the value of x i is zero except for a finite number of ordinals i . The equivalent of ? 0 is called the small Veblen ordinal (if the number of arguments is finite ), or the large Veblen ordinal (if the number of arguments is infinite, sometimes denoted ? ? ? (0) or ? ? ? (0); here ? = ? 1 is the set of all countable ordinals, and an element of ? ? (resp. ? ? ) is a finite (resp infinite countable) sequence of countable ordinals

T. Let, Consider T ? as a set E in the Bourbaki sense. The comparison on T ? induces a comparison on E that makes it a well-ordered set; there is a unique function f : E ? O(?) such that ? is an ordinal, O(?) is the set of ordinals less than ?, and f is an order-isomorphism This means: there is a unique ordinal ? and function f , such that f maps NF elements of type T to an ordinal < ?, and f is an order isomorphism we study the function f . This is not so easy We first postulate that f satisfies the following property Every x of T can be written as x = x 0 · (n + 1) + r , where n is an integer, r < x 0 and x is AP (Recall that an element x of T has the form [a, n, r ], [a, b, n, r ] or [a, b, c, n, r ]; here x 0 is obtained from x by replacing n and r by zero) We assume f (x)+ f (y) = f (x + y) and that f maps an AP element to an AP ordinal [we believe that this postulate can be proved]. Write relation (5.1) for y = f (x) as y = C(y) · (n + 1) + R(y), so that f (x 0 ) = C(y), f (r ) = R(y) This says that f is uniquely defined by the values f (x 0 ) We shall also postulate that f (x 0 ) has the form g ( f (a)), G( f (a), f (b)) or ?( f (a), f (b), f (c)) in the cases T 1 , T 2 , T 3 . [This is not completely obvious]. This means that we introduce a function g , G or ?, and study the properties. The assumptions are: the value of the function is an AP, and g (x) < g (y) or ?(a, bc) < ?(a ? , b ? , c ? ) is equivalent to the ordering of T 1 or T 3 ; this relation is simple in the first case, this chapter

L. Ex2, Ro a = Ro b -> a = b. Proof. by move => a b ; apply:R_inj, p.1

. Lemma-set_to_t1_pr-x, Hx: inc x T1) : set_to_T1 x = Bo Hx. Lemma set_to_T1_inj x y: inc x T1 -> inc y T1 -> set_to_T1 x =

E. Let and . Be-the, We consider the order induced by G on E ? . The associated relation x < E y is: x ? E, and y ? E ? and x ? 1 y. We prove here that it is an order on E ? , a total order, a well-order. Note that ? E is total since ? is total. Now we use Corollary 1 of Proposition 6 of Bourbaki: A totally ordered set is well-ordered if and only if every decreasing sequence is stationary. If E were not well-ordered, we could construct a non-stationary decreasing sequence, extract a strictly decreasing sequence

=. Set-a-k, We have a k+1 < N a k , where < N is the relation proved to be well-founded on page 18

F. T1tob, Set := if x is cons a n b then omega0 ^o (T1toB a) *o (nat_to_B n.+1) +o

. Lemma-t1tob_injective-x-y, T1nf x -> T1nf y -> T1toB x = T1toB y -> x = y. Consider now the type T 2 and O 2 (0) = 0, O 2 (b)) · (n + 1) + O 2 (c)

<. We-show-x and =. O. , (y) whenever x and y are NF, by induction on the size of the arguments Assume x =, We have O 2 (x) = O 2 (x ? ) · (n + 1) + O 2 (c)

W. Ackermann, Konstruktiver Aufbau eines Abschnitts der zweiten Cantorschen Zahlenklasse, Mathematische Zeitschrift, vol.53, issue.5, pp.403-413, 1951.
DOI : 10.1007/BF01175640

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, 2004.

G. Cantor, Contributions to the Founding of the Theory of Transfinite Numbers, Trans. P. Jourdain, 1897.

G. Gonthier and A. Mahboubi, A Small Scale Reflection Extension for the Coq system, 2008.

J. Grimm, Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets, 2009.

J. Grimm, Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers, 2009.

K. Schütte, Proof theory, 1977.

O. Veblen and C. , Continous increasing functions of finite and transfinite ordinals, Transactions of ther AMS, vol.9, issue.3 6, 1908.