Intuitionistic fixed point theories over Heyting arithmetic

MaRDI QIDQ3001089zbMATH OpenFDO

Authors Toshiyasu Arai

Publication date 31 May 2011

Full work available at URL https://arxiv.org/abs/1005.1991

zbMATH Keywords

cut eliminationfixed pointHeyting arithmeticinfinitary derivations

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Intuitionistic mathematics (03F55)

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.

Recommendations

• An intuitionistic fixed point theory
• Fixed-Point Elimination in the Intuitionistic Propositional Calculus
• Intuitionistic Fixed Point Theories for Strictly Positive Operators
• Provably recursive functions of constructive and relatively constructive theories
• Intuitionistic fixed point theories over set theories

Cited in

(9)

• An intuitionistic fixed point theory
• An intensional fixed point theory over first order arithmetic
• A parametrised functional interpretation of Heyting arithmetic
• scientific article; zbMATH DE number 4148083 (Why is no real title available?)
• Intuitionistic Fixed Point Theories for Strictly Positive Operators
• Intuitionistic fixed point theories over set theories
• On Heckits, LATE, and Numerical Equivalence
• Quick cut-elimination for strictly positive cuts
• Elementary inductive definitions in HA: From strictly positive towards monotone

This page was built for publication: Intuitionistic fixed point theories over Heyting arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3001089)