Intuitionistic fixed point theories over Heyting arithmetic
classification
🧮 math.LO
keywords
arithmeticfixedheytingintuitionisticcertainclassconservativecut-elimination
read the original abstract
In this paper we show that an intuitionistic theory for fixed points is conservative over the Heyting arithmetic with respect to a certain class of formulas. This extends partly the result of mine. The proof is inspired by the quick cut-elimination due to G. Mints.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.