2021/10/15 by Mattias Granberg Olsson, Olsson, Mattias Granberg, Graham E. Leigh +1
Arts and Humanities · Mathematics · Psychology · #03F25 #03F30 #03F50 (Primary) #03F55 (Secondary) #Advanced Topology and Set Theory #Epistemology, Ethics, and Metaphysics #FOS: Mathematics #Logic (math.LO) #Philosophy and Theoretical Science
paper · pdf · doi:10.48550/arxiv.2110.08240
openalex publication_date 2021/10/15 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
This paper presents a novel proof of the conservativity of the intuitionistic theory of strictly positive fixpoints, \widehatID1i, over Heyting arithmetic (HA), originally proved in full generality by Arai (2011). The proof embeds \widehatID1i 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.