Quick cut-elimination for strictly positive cuts

DOI10.1016/J.APAL.2011.03.002zbMATH Open1273.03158arXiv1010.4111OpenAlexW1963953353MaRDI QIDQ639680FDOQ639680

Authors: Toshiyasu Arai 

Publication date: 22 September 2011

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

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.

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

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

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)

Cites Work

• Intuitionistic Fixed Point Theories for Strictly Positive Operators
• Some results on cut-elimination, provable well-orderings, induction and reflection
• An intuitionistic fixed point theory
• Intuitionistic fixed point theories over Heyting arithmetic
• Title not available (Why is that?)
• Fragments of HA based on \(\Sigma_ 1\)-induction
• Relativized realizability in intuitionistic arithmetic of all finite types
• Fragments of Heyting arithmetic

Cited In (4)

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

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)