First order axioms for primitive recursion in Takeuti's theory of ordinal numbers

In this article, Takeuti has introduced a theory of ordinal numbers, which in his own words, is intended to be a first order theory:

The theory of ordinal numbers we are to develop is based on the first order predicate calculus with equality, that is, it does not contain, in principle, function variables.

Regarding this, I have some difficulties in understanding the way to express the axioms related to primitive recursion. As it's been explained in the paper, an ordinal function $$f$$ is defined by primitive recursion using a function combination $$T ( { \bf h } , a _ 1 , \dots , a _ n )$$, by the equation $$f ( a _ 1 , \dots , a _ n ) = T \big( \{ x \} f ^ { a _ 1 } ( x , a _ 2 , \dots , a _ n ) , a _ 1 , \dots , a _ n \big)$$. Here:

We call $$T ( { \bf h } , a _ 1 , \dots , a _ n )$$ a function combination containing $$\bf h$$, if it is constructed from $$0$$, $$\omega$$, $$a _ 1$$, $$\dots$$, $$a _ n$$ by successive applications of $$'$$ (successor), $$<$$ (characteristic function of order), $$\max$$, $$j$$ (pairing), $$g ^ 1$$ (left projection), $$g ^ 2$$ (right projection), $$\bf h$$, the bounded minimum and function constants [of the primitive recursive functions defined before].

We shall use $$\{ x \} f ( x , a _ 1 , \dots , a _ n )$$ for emphasis in situation where $$f ( a , a _ 1 , \dots , a _ n )$$ is considered as a value of the unary function of $$a$$.

$$f ^ a$$ is given by $$f ^ a ( b , a _ 1 , \dots , a _ n ) = \begin{cases} f ( b , a _ 1 , \dots , a _ n ) & \text {if } b < a \\ 0 & \text {otherwise} \end{cases}$$.

As far as I understand, for the theory to be first order, in addition to avoiding function variables, we have to avoid the bounded minimization operator in the object language. So I read the axioms of bounded minimization,

$$f ( a _ 1 , \dots , a _ n , b ) = 0 \land b < a \to f \big( a _ 1 , \dots , a _ n , \mu x _ { x < a } f ( a _ 1 , \dots , a _ n , x ) \big) = 0 \land \mu x _ { x < a } f ( a _ 1 , \dots , a _ n , x ) \le b$$

$$\mu x _ { x < a } f ( a _ 1 , \dots , a _ n , x ) = 0 \lor \Big( f \big( a _ 1 , \dots , a _ n , \mu x _ { x < a } f ( a _ 1 , \dots , a _ n , x ) \big) = 0 \land \mu x _ { x < a } f ( a _ 1 , \dots , a _ n , x ) < a \Big)$$

this way:

$$f ( a _ 1 , \dots , a _ n , b ) = 0 \land b < a \to f \big( a _ 1 , \dots , a _ n , g ( a _ 1 , \dots , a _ n , a ) \big) = 0 \land g ( a _ 1 , \dots , a _ n , a ) \le b$$

$$g ( a _ 1 , \dots , a _ n , a ) = 0 \lor \Big( f \big( a _ 1 , \dots , a _ n , g ( a _ 1 , \dots , a _ n , a ) \big) = 0 \land g ( a _ 1 , \dots , a _ n , a ) < a \Big)$$

where $$f$$ and $$g$$ are function constants corresponding the functions $$f$$ and $$\mu x _ { x < a } f$$, respectively. (I suppose that the way Takeuti is going to formalize the theory is in fact similar to the standard way of formalizing primitive recursive arithmetic and thus we have function constants for each (definition of a) primitive recursive ordinal function. Otherwise I can't understand how the formalization is done.)

Now, I have a problem determining how the axioms for primitive recursion are supposed to be expressed. For example, if $$g$$, $$h$$ and $$l$$ are primitive recursive ordinal functions and $$f$$ is defined by primitive recursion using the equation $$f ( a ) = g \bigg( \mu x _ { x < l ( a ) } f ^ x \Big( f ^ a \big( h ( a ) \big) \Big) \bigg)$$, how should I express a first order axiom for it?

I’m not familiar with this paper, but what is wrong with just writing out the first-order definitions of the inner functions? That is, $$f(a)=g(\mu x_{x becomes $$\exists x\,(f(a)=g(x)\land\phi(a,x)),$$ where \begin{align*} \phi(a,x)&\iff(x Here, $$\chi(a,y)$$ expresses $$f^a(h(a))=y$$, $$\psi(a,x,u)$$ expresses $$f^x(f^a(h(a)))=u$$, and $$\phi(a,x)$$ expresses $$\mu x_{x.
• You're right. I think I was biased by the way that $\mathrm { PRA }$ is axiomatized, in which only atomic formulas appear and quantifiers are not used in primitive recursion axioms (other than by taking universal closure of the atomic formula perhaps). Now it seems to be such a stupid mistake to neglect the simple fact that quantifiers can be used! Thanks. Jul 12 '20 at 8:09