Abstract
In this paper we show that the intuitionistic fixed point theory FiXi(T) over set theories T is a conservative extension of T if T can manipulate finite sequences and has the full foundation schema.
Similar content being viewed by others
References
Arai T.: Consistency proof via pointwise induction. Arch. Math. Logic 37, 149–165 (1998)
Arai T.: Some results on cut-elimination, provable well-orderings, induction and reflection. Ann. Pure Appl. Logic 95, 93–184 (1998)
Arai T.: Non-elementary speed-ups in logic calculi. Math. Logic Q. 6, 629–640 (2008)
Arai T.: Intuitionistic fixed point theories over Heyting arithmetic. In: Feferman, S., Sieg, W. (eds.) Proofs Categories and Computations. Essays in honor of Grigori Mints, pp. 1–14. College Publications, King’s College London, London (2010)
Arai T.: Quick cut-elimination for strictly positive cuts. Ann. Pure Appl. Logic 162, 807–815 (2011)
Arai T.: Proof theory of weak compactness. J. Math. Logic 13, 1350003 (2013)
Arai, T.: Conservations of first-order reflections. J. Symb. Logic 79, 814–825 (2014)
Arai, T.: Lifting proof theory to the countable ordinals : Zermelo–Fraenkel’s set theory. J. Symb. Logic 79, 25–354 (2014)
Arai, T.: Proof theory of second order indescribability (in preparation)
Avigad J.: On the relationship between ATR0 and \({\widehat{\rm ID}_{ < \omega}}\). J. Symb. Logic 61, 768–779 (1996)
Barwise J.: Admissible Sets and Structures. Springer, Berlin (1975)
Beeson M.: Goodman’s theorem and beyond. Pac. J. Math. 84, 1–16 (1979)
Buchholz W.: \({{\it\Omega}_{\mu+1}}\)-rule. In: Buchholz, W., Feferman, S., Pohlers, W., Sieg, W. (eds.) Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies. Lecture Notes in Mathematics, vol. 897, pp. 188–233. Springer, Berlin (1981)
Buchholz W.: Notation system for infinitary derivations. Arch. Math. Logic 30, 277–296 (1991)
Buchholz W.: An intuitionistic fixed point theory. Arch. Math. Logic 37, 21–27 (1997)
Feferman S.: Iterated inductive fixed-point theories: applications to Hancock’s conjecture. In: Metakides, G. (ed.) Patras Logic Symposion, pp. 171–196. North-Holland, Amsterdam (1982)
Mints, G.E.: Quick cut-elimination for monotone cuts. In: Games, Logic, and Constructive Sets (Stanford, CA, 2000), CSLI Lecture Notes, vol. 161, pp. 75–83. CSLI Publications, Stanford (2003)
Rüede C., Strahm T.: Intuitionistic fixed point theories for strictly positive operators. Math. Logic Q. 48, 195–202 (2002)
Schindler R., Zeman M.: Fine structure. In: Foreman, M., Kanamori, A. (eds.) Handbook of Set Theory, vol. 1, pp. 605–656. Springer, Berlin (2010)
Takeuti, G.: Proof Theory, 2nd edn. North-Holland, Amsterdam (1987). Reprinted from Dover Publications (2013)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Arai, T. Intuitionistic fixed point theories over set theories. Arch. Math. Logic 54, 531–553 (2015). https://doi.org/10.1007/s00153-015-0426-y
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00153-015-0426-y