Revisiting the conservativity of fixpoints over intuitionistic arithmetic

DOI10.1007/S00153-023-00878-2MaRDI QIDQ6178470zbMATH OpenOpenAlexFDO

Authors Mattias Granberg Olsson, Graham E. Leigh

Publication date 18 January 2024

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

conservativity fixpoint theories realizability satisfaction predicates

Mathematics Subject Classification ID

Relative consistency and interpretations (03F25) First-order arithmetic and fragments (03F30) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)

Abstract: This paper presents a novel proof of the conservativity of the intuitionistic theory of strictly positive fixpoints,

w i d e h a t m a t h r m I D_{1}^{m a t h r m i}

, over Heyting arithmetic (HA), originally proved in full generality by Arai (2011). The proof embeds

w i d e h a t m a t h r m I D_{1}^{m a t h r m 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.

Recommendations

Cites work

This page was built for publication: Revisiting the conservativity of fixpoints over intuitionistic arithmetic

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