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

DOI10.1305/NDJFL/1039700743zbMATH Open0937.03067OpenAlexW1970906905MaRDI QIDQ1130232FDOQ1130232

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

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

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)

Cites Work

• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Title not available (Why is that?)
• Title not available (Why is that?)
• The machinery of consistency proofs
• Title not available (Why is that?)

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)