Revisiting the Conservativity of Fixpoints over Intuitionistic Arithmetic
Archive for Mathematical Logic(2021)
Abstract
This paper presents a novel proof of the conservativity of the intuitionistic theory of strictly positive fixpoints, ID_1^i , over Heyting arithmetic ( HA ), originally proved in full generality by Arai (Ann Pure Appl Log 162:807–815, 2011. https://doi.org/10.1016/j.apal.2011.03.002 ). The proof embeds ID_1^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 (Indag Math 29:260–275, 2018. https://doi.org/10.1016/j.indag.2017.07.009 ) that Heyting arithmetic with partial terms plus the schema of self realizability for arithmetic formulae is conservative over HA .
MoreTranslated text
Key words
Fixpoint theories,Conservativity,Realizability,Satisfaction predicates,03F50,03F25,03F30,03F55
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined