Intuitionistic fixed point theories over set theories

TL;DR

This paper demonstrates that the intuitionistic fixed point theory FiX^{i}(X) over certain set theories is a conservative extension, provided the set theory can handle finite sequences and includes the full foundation schema.

Contribution

It establishes the conservativity of FiX^{i}(X) over set theories with specific capabilities, advancing understanding of fixed point theories in intuitionistic logic.

Findings

FiX^{i}(X) is conservative over set theories with finite sequence manipulation.

Full foundation schema is essential for the conservativity result.

The result clarifies the relationship between fixed point theories and foundational set theories.

Abstract

In this paper we show that the intuitionistic fixed point theory FiX^{i}(X) over set theories T is a conservative extension of T if T can manipulate finite sequences and has the full foundation schema.