Quick cut-elimination for strictly positive cuts

DOI10.1016/J.APAL.2011.03.002MaRDI QIDQ639680zbMATHOpenAlexFDO

Authors Toshiyasu Arai

Publication date 22 September 2011

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1010.4111

zbMATH Keywords

conservative extension of Heyting arithmeticfragments of Heyting arithmeticintuitionistic fixed point theoryquick cut elimination

Mathematics Subject Classification ID

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

Abstract: In this paper we show that the intuitionistic theory for finitely many iterations of strictly positive operators is a conservative extension of the Heyting arithmetic. The proof is inspired by the quick cut-elimination due to G. Mints. This technique is also applied to fragments of Heyting arithmetic.

Recommendations

• Intuitionistic Fixed Point Theories for Strictly Positive Operators
• Typed Lambda Calculi and Applications
• An intuitionistic fixed point theory
• Publication:3478407
• Cut elimination in the intuitionistic theory of types with axioms and rewriting cuts, constructively

Cites work

• scientific article; zbMATH DE number 2051382 (Why is no real title available?)
• An intuitionistic fixed point theory
• Fragments of HA based on \(\Sigma_ 1\)-induction
• Fragments of Heyting arithmetic
• Intuitionistic Fixed Point Theories for Strictly Positive Operators
• Intuitionistic fixed point theories over Heyting arithmetic
• Relativized realizability in intuitionistic arithmetic of all finite types
• Some results on cut-elimination, provable well-orderings, induction and reflection

Cited in

(4)

• Intuitionistic fixed point theories over set theories
• Revisiting the conservativity of fixpoints over intuitionistic arithmetic
• Proof theory of weak compactness
• Intuitionistic Fixed Point Theories for Strictly Positive Operators

This page was built for publication: Quick cut-elimination for strictly positive cuts

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