Revisiting the conservativity of fixpoints over intuitionistic arithmetic

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 e...

Full description

Saved in:
Bibliographic Details
Published in:Archive for mathematical logic 2024-02, Vol.63 (1-2), p.61-87
Main Authors: Granberg Olsson, Mattias, Leigh, Graham E.
Format: Article
Language:English
Subjects:
Algebra
Algebra and Logic
Algebra och logik
Arithmetic
Conservativity
Filosofi
Fixpoint theories
Mathematical Logic and Foundations
Mathematics
Mathematics and Statistics
Philosophy
Realizability
Satisfaction predicates
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 .
ISSN:0933-5846
1432-0665
1432-0665
DOI:10.1007/s00153-023-00878-2