Intuitionistic Fixed Point Theories for Strictly Positive Operators

In this paper it is shown that the intuitionistic fixed point theory ID i (strict) for times iterated fixed points of strictly positive operator forms is conservative for negative arithmetic and 0 2 sentences over the theory ACA-i for times iterated arithmetic comprehension without set parameters. This generalizes results previously due to Buchholz [5] and Arai [2].

• Type: Journal
• Year: 2002
• Where: MLQ
• Authors: Christian Rüede, Thomas Strahm
• Keywords: Intuitionistic Fixed Point, MLQ 2002, Negative Arithmetic, Positive Operator Forms