zbMATH — the first resource for mathematics

Strong normalization theorem for a constructive arithmetic with definition by transfinite recursion and bar induction. (English) Zbl 0937.03067
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.
03F30 First-order arithmetic and fragments
03F05 Cut-elimination and normal-form theorems
03F50 Metamathematics of constructive systems
Full Text: DOI
[1] Girard, J. Y., Proof Theory and Logical Complexity , Bibliopolis, Napoli, 1982. · Zbl 0635.03052
[2] Troelstra, A. S., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis , Lecture Notes in Mathematics , vol. 344, Springer-Verlag, New York, 1973. · Zbl 0275.02025
[3] Yasugi, M., “Hyper-principle and the functional structure of ordinal diagrams,” Comment. Math. Univ. st. Pauli, vol. 34 (1985), pp. 227–63; vol. 35 (1986), pp. 1–37. · Zbl 0633.03052
[4] Yasugi, M., “The machinery of consistency proofs,” Annals of Pure and Applied Logic , vol. 44 (1989), pp. 139–52. · Zbl 0679.03023
[5] Yasugi, M., and S. Hayashi, “A functional system with transfinitely defined types,” pp. 31–60 in Lecture Notes in Computer Science , vol. 792, Springer-Verlag, New York, 1994.
[6] Yasugi, M., and S. Hayashi, “Interpretations of transfinite recursion and parametric abstraction in types,” pp. 452–64 in Words, Languages and Combinatorics 2 , World Scientific, Kyoto, 1994. · Zbl 0874.03069
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.