Revisiting the conservativity of fixpoints over intuitionistic arithmetic

TL;DR

This paper provides a new proof of the conservativity of the intuitionistic theory of strictly positive fixpoints over Heyting arithmetic, using embeddings and interpretations involving partial terms and satisfaction predicates.

Contribution

It introduces a novel proof technique embedding the theory into logic of partial terms and applying existing conservativity results, extending understanding of fixpoint theories over HA.

Findings

The proof confirms the conservativity of $oxed{ ext{ID}_1^{ ext{i}}}$ over HA.

It demonstrates the effectiveness of interpretations via realizability and satisfaction predicates.

The approach generalizes previous results by Arai (2011).

Abstract

This paper presents a novel proof of the conservativity of the intuitionistic theory of strictly positive fixpoints, $\widehat{\mathrm{ID}}{}_{1}^{\mathrm{i}}$, over Heyting arithmetic (HA), originally proved in full generality by Arai (2011). The proof embeds $\widehat{\mathrm{ID}}{}_{1}^{\mathrm{i}}$ into the corresponding theory over Beeson's logic of partial terms and then uses two consecutive interpretations, a realizability interpretation of this theory into the subtheory generated by almost negative fixpoints, and a direct interpretation into Heyting arithmetic with partial terms using a hierarchy of satisfaction predicates for almost negative formulae. It concludes by applying van den Berg and van Slooten's result (2018) that Heyting arithmetic with partial terms plus the schema of self realizability for arithmetic formulae is conservative over HA.