Many years ago, Takeuti constructed a first order theory of ordinal numbers which we shall denote by ORD(T) and proved that ZF+(V=L) could be interpreted in ORD(T). Let F(x) designate the unique set correlated to the ordinal number x by the specific well ordering of the universe of ZF that can be defined when V=L is added to the axioms of ZF. Takeuti showed that a certain formula S(x,y) belonging to the language of ORD(T)-in which y,z are the only variables occuring free-expresses the fact that "the set F(y) is an element of the set F(z) in ZF". This was the basis for the interpretation and it was interesting because Takeuti's axioms for ORD(T) made ORD(T) an extension of Peano's arithmetic (with the finite ordinal numbers playing the role of non-negative integers). It would then be possible to regard ZF+(V=L) as a sub-theory of (a suitably extended) arithmetic, much as arithmetic has long been rgarded as a sub-theory of ZF.

Now, if we tried to "embed" a richer set theory such as "ZF+some large cardinal axioms" into an extension of arithmetic by proceeding in this way, we would run into the problem that V=L is inconsistent with many of these large cardinal axioms. However fewer of these axioms may be inconsistent with V=OD. Let G(x) designate the unique set correlated to the ordinal number x by the specific well-ordering of the universe of ZF* that can be defined when V=OD is added to the axioms of ZF* (where ZF* denotes ZF+some large cardinal axioms).

My question is this: Could there exist (or has there been constructed) a first order theory ORD(OD) such that (1) ORD(OD) is a theory of ordinal numbers that extends Peano's arithmetic (2) there is a formula of ORD(OD)-in which y,z are the only variables occuring free- that expresses the sentence " the set G(y) is an element of the set G(z) in ZF*"?

If so, we could interpret ZF*+(V=OD) in ORD(OD). The language of these first order theories of ordinal numbers should be thought of as containing terms and formulae representing recursive functions and predicates of ordinal numbers. Among these are the the recursive functions and predicates of finite ordinal numbers (non-negative integers) which belong to the language of the sub-theory-Peano's arithmetic. This is what is meant by saying that these theories of ordinal numbers are extensions of arithmetic.