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.
DOI : 10.1007/978-3-662-07964-5

URL : https://hal.archives-ouvertes.fr/hal-00344237

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.
URL : https://hal.archives-ouvertes.fr/inria-00258384

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.