[FOM] Can extended ordinal arithmetic serve as a foundational theory of mathematics?

[Zuhair Abdul Ghafoor Al-Johar]

Dear Sirs, 
The following theory is a kind of extended ordinal arithmetic, it involves
four kinds of primitive concepts, those of equality "=", strict ordinal smaller
than "<", set membership"E", and ordered pairing "<>". It is a bi-sorted first
order theory, with first sort objects represented by lower cases ranging
over all ordinal numbers and the second sort objects represented by upper
cases ranging over all sets of ordinal numbers. The sorts are disjoint. The
theory speaks nothing about the internal structure of ordinals. Syntactical
restrictions includes limiting appearance of the symbol < between lower
cases only; limiting E only between lower cases on the left and upper
cases on the right, and "<>" can only be used with two lower cases inside
it, and it is meant to be a total binary function symbol from first sort objects
to first sort objects. There is no syntactical restriction on equality symbol.

So we have the following axioms about sorts:
forall x forall Y (x=/=Y) 
forall a forall b exists x (x = <a,b>) 

The idea is to form limits (with respect to <) on sets of ordinals, that are
themselves of course ordinals, such that there is an ordinal number strictly
greater than all natural ordinals; every set of ordinals that is equal in size
to a set of ordinals that has a limit, then it has a limit, and for every ordinal
d the set of all ordinals whose anterior sets (the set of all ordinals strictly
smaller than them) are equal in size to the anterior set of d, has a limit. 

So we have a theory of flat sets of ordinals, having all the ordinals that
ZFC can define. 

Here I'll present two questions: 

1. Can Gödel's constructible universe "L" be encoded inside this theory?
     thereby interpreting ZFC+(V=L)

2. If the answer to 1 is to the positive, then what significance would that
bear on the foundational level of mathematics? 

As regards 2, I mean we'll have a theory of ordinals that is not less natural
than ZFC, any conundrum about any of its axioms would be a conundrum
about axioms of ZFC, and moreover the structure of this theory would be
much simpler, since there is no hierarchical set structure, only one set
level is involved. In some sense this would be a kind of a structure
reduction, where the huge cumulative set hierarchical structure of ZFC is
collapsed into a simple flat set structure on ordinals.  

Axioms: those of equality theory +   

 1. Extensionality:  forall z (z E X <-> z E Y) -> X=Y 

 2. Comprehension: if phi is a formula in which X is not free, then      
exists X forall y (y E X <-> phi(y)); is an axiom. 

Define: X={y: phi(y)} <->  forall y (y E X <-> phi(y))  
 
Define: X=V <-> forall y (y E X) 

 3. Well ordering: < well orders V.   

4. Ordered pairs: <m,n> = <o,p>  -> m=o /\ n=p  

 Define: y=0 <-> ~ exists x (x < y) 

 Define: Nat(x) <->  forall y =< x (forall z < y exists k (z < k< y) -> y=0) 

 5. Infinity: exists l forall x (Nat(x) -> x < l) 

 Define: |X| = |Y| <-> exists F (F:X -> Y /\ F is a bijection) 

 6. Size:  forall x,S(|{y: y < x}| = |S| -> exists l forall s E S (s < l)) 

 7. Successor cardinals:  forall x exists y forall z (|{r: r < z}| = |{k: k < x}| -> z < y)

A related issue to this theory is that if one replace 7 by a power set axiom,
that is:

Power set: forall a exists l exists B forall X [X subseteq {m: m<a} -> 
exists b<I forall x (<x,b> E B <-> x E X)],

then it appears that this can interpret L inside it, thereby interpreting ZFC+
(V=L). But this looks like hierarchical set theory in disguise. While the first
axiomatization has no clear imports from hierarchical set theory, it is rather
straightforwardly motivated by ordinal formation by posing limits on flat 
sets of ordinals.

I'm aware that attempts along the same general lines had been made
before, by Takeuti (https://urldefense.proofpoint.com/v2/url?u=https-3A__projecteuclid.org_euclid.jmsj_1261154153&d=DwIFaQ&c=slrrB7dE8n7gBJbeO0g-IQ&r=xXZM6ZrkjVxXknjzIxhAvQ&m=9NqoPn9ORvHDdgB0q1rTQ5cTD5b-ZyYbvarARRPjTXY&s=4KGghomFotvc_8cxNNG03vEyp_Bq7V-nns9Z5_YTpLo&e= ),
and Peter Koepke, Martin Koerwien (https://urldefense.proofpoint.com/v2/url?u=https-3A__arxiv.org_abs_math_0502265&d=DwIFaQ&c=slrrB7dE8n7gBJbeO0g-IQ&r=xXZM6ZrkjVxXknjzIxhAvQ&m=9NqoPn9ORvHDdgB0q1rTQ5cTD5b-ZyYbvarARRPjTXY&s=NsJz7aNk-p1OXbLVS4hYiHn-8Qq1GbXJUBQRdV2P-7Q&e= ).
But I didn't see this particular approach tackled. 

Best Regards
Zuhair