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

DOI10.1305/ndjfl/1039700743zbMath0937.03067OpenAlexW1970906905MaRDI QIDQ1130232

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

natural deduction systemrecursive definitionsstrong normalizationconservativityconstructive arithmetic

Mathematics Subject Classification ID

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

Cites Work

• The machinery of consistency proofs
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Unnamed Item
• Unnamed Item
• Unnamed Item

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