Quick cut-elimination for strictly positive cuts

TL;DR

This paper demonstrates that the intuitionistic theory with finitely many strictly positive operators is conservative over Heyting arithmetic, using a quick cut-elimination technique inspired by G. Mints, applicable to certain arithmetic fragments.

Contribution

It introduces a novel application of quick cut-elimination to show conservativity of theories with positive operators over Heyting arithmetic.

Findings

The theory with finitely many strictly positive operators is conservative over Heyting arithmetic.

The quick cut-elimination method can be applied to fragments of Heyting arithmetic.

The approach simplifies proofs and enhances understanding of the theory's structure.

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.