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

DOI10.1305/NDJFL/1039700743MaRDI QIDQ1130232zbMATH OpenOpenAlexFDO

Authors Osamu Takaki

Publication date 8 November 1998

Published in Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1305/ndjfl/1039700743

zbMATH Keywords

conservativityconstructive arithmeticnatural deduction systemrecursive definitionsstrong normalization

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Metamathematics of constructive systems (03F50)

Review text

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.

Recommendations

• Computer Science Logic
• scientific article; zbMATH DE number 1047956
• Strong normalization of barrecursive terms without using infinite terms
• Arithmetic transfinite induction and recursive well-orderings

Cites work

• scientific article; zbMATH DE number 4029551 (Why is no real title available?)
• scientific article; zbMATH DE number 4033738 (Why is no real title available?)
• scientific article; zbMATH DE number 1047956 (Why is no real title available?)
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• The machinery of consistency proofs

Cited in

(2)

• Strong normalization of barrecursive terms without using infinite terms
• scientific article; zbMATH DE number 1047956 (Why is no real title available?)

This page was built for publication: Strong normalization theorem for a constructive arithmetic with definition by transfinite recursion and bar induction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1130232)