Strong normalization theorem for a constructive arithmetic with definition by transfinite recursion and bar induction (Q1130232)

An extension of HA called TRDB (the system with Definition by Transfinite Recursion and Bar induction) is considered. It is a system designed in particular to construct the accessibility proofs for ordinal diagrams and may be considered as a modification of the system ASOD suggested by Yasugi. TRDB is a natural deduction system specified w.r.t. a certain formula \(G\) and a certain primitive recursive well-ordered set \(I\). In this paper only the case when the order type of \(I\) is less than \(\varepsilon_0\) is studied. Main results are: strong normalization theorem for TRDB; consistency of TRDB; existence and disjunction properties.