Some Results on Intuitionistic Π_{1}-Induction

Morteza Moniri

This is joint work with Mojtaba Moniri.

Consider the fragment iΠ_{1} of HA which is the intuitionistic counterpart of the fragment IΠ_{1} of P A. Wehmeier has proved that IΠ_{1} is not Π_{2}-conservative over iΠ_{1}, see [W]. On the other hand it is easy to see that iΠ_{1} is closed under the negative translation. Hence iΠ_{1} is not closed under Friedman’s translation by arbitrary formulas.

However we prove that iΠ_{1} is closed under Friedman’s translation by negated formulas. Using this, we show that the proof given in [TD] for the closure of HA under the rule Independence of Premises IP works for iΠ_{1} too.

We also present equivalence of iΠ_{1} with intuitionistic transfinite Π_{1}-induction. Furthermore we show that iΠ_{1} proves ¬¬LNP on Π_{1}-formulas with one free variable.

[MM] Morteza Moniri and Mojtaba Moniri, Some Weak Fragments of HA and Certain Closure Properties, submitted.

[TD] A.S. Troelstra and D. van Dalen, Constructivism in Mathematics, v.I, North-Holland, 1988.

[W] K.F. Wehmeier, Fragments of HA Based on Σ_{1}-Induction, Arch. Math. Logic, 37 (1997) 37-49.

Address: Logic Group, Institute for Studies in Theoretical Physics and Mathematics, P.O. Box 19395-5746, Niavaran, Tehran, Iran

E-mail: ezmoniri@karun.ipm.ac.ir