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

strong normalizationconservativityrecursive definitionsnatural deduction systemconstructive arithmetic

Mathematics Subject Classification ID

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

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

(1)

• Strong normalization of barrecursive terms without using infinite terms

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)