Strong normalization theorem for a constructive arithmetic with definition by transfinite recursion and bar induction.

*(English)*Zbl 0937.03067An 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.

Reviewer: S.V.Solov’ev (Durham)

##### MSC:

03F30 | First-order arithmetic and fragments |

03F05 | Cut-elimination and normal-form theorems |

03F50 | Metamathematics of constructive systems |

##### Keywords:

constructive arithmetic; recursive definitions; strong normalization; conservativity; natural deduction system
PDF
BibTeX
XML
Cite

\textit{O. Takaki}, Notre Dame J. Formal Logic 38, No. 3, 350--373 (1997; Zbl 0937.03067)

Full Text:
DOI

**OpenURL**

##### References:

[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.