We prove the strong normalization theorem for the natural deduction system for the constructive arithmetic TRDB (the system with Definition by Transfinite Recursion and Bar induction), which was introduced by Yasugi and Hayashi. We also establish the consistency of this system, applying the strong normalization theorem.

In this paper, we develop primitive recursive analogues of regular cardinals by using ordinal representation systems for KPi and KPM. We also define primitive recursive analogues of inaccessible and hyperinaccessible cardinals. Moreover, we characterize the primitive recursive analogue of the least (uncountable) regular cardinal.