Intuitionistic fixed point theories over Heyting arithmetic

TL;DR

This paper proves that an intuitionistic fixed point theory is conservative over Heyting arithmetic for specific formulas, extending previous results and using a proof technique inspired by G. Mints' quick cut-elimination.

Contribution

It introduces an intuitionistic fixed point theory over Heyting arithmetic and demonstrates its conservativity for a class of formulas, extending prior work in the area.

Findings

Fixed point theory is conservative over Heyting arithmetic for certain formulas

The proof utilizes a method inspired by G. Mints' quick cut-elimination

Extends previous results on intuitionistic fixed point theories

Abstract

In this paper we show that an intuitionistic theory for fixed points is conservative over the Heyting arithmetic with respect to a certain class of formulas. This extends partly the result of mine. The proof is inspired by the quick cut-elimination due to G. Mints.