Hostname: page-component-586b7cd67f-t8hqh Total loading time: 0 Render date: 2024-11-24T23:38:09.062Z Has data issue: false hasContentIssue false
  • English
  • Français

Some weak fragments of HA and certain closure properties

Published online by Cambridge University Press:  12 March 2014

Morteza Moniri  and
Mojtaba Moniri
Morteza Moniri
Affiliation:
School of Mathematics, IPM, P.O.Box 19395-5746, Tehran, Iran, E-mail: [email protected]
Mojtaba Moniri
Affiliation:
Mathematics Department, Tarbiat Modarres University, P.O. BOX 14115-175, Tehran, Iran, E-mail: [email protected], [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We show that Intuitionistic Open Induction iop is not closed under the rule DNS(Ǝ1). This is established by constructing a Kripke model of iop + ¬Ly(2y > x), where Ly(2y > x) is universally quantified on x. On the other hand, we prove that iop is equivalent with the intuitionistic theory axiomatized by PA− plus the scheme of weak ¬¬ LNP for open formulas, where universal quantification on the parameters precedes double negation. We also show that for any open formula φ(y) having only y free. (PA−)i ⊢ Lyφ(y). We observe that the theories iop, i∀1 and iΠ1 are closed under Friedman's translation by negated formulas and so under VR and IP. We include some remarks on the classical worlds in Kripke models of iop.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 67 , Issue 1 , March 2002 , pp. 91 - 103
Copyright
Copyright © Association for Symbolic Logic 2002

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Ardeshir, M. and Moniri, Mojtaba, Intuitionistic open induction and least number principle and the Buss operator, Notre Dame Journal of Formal Logic, vol. 39 (1998), pp. 212–220.CrossRefGoogle Scholar
[2]Dragalin, A. G., Mathematical intuitionism, introduction to proof theory, American Mathematical Society, 1988.CrossRefGoogle Scholar
[3]Hodges, W., Model theory, Cambridge University Press, 1993.CrossRefGoogle Scholar
[4]Macintyre, A. and Marker, D., Primes and their residue rings in models of open induction, Annals of Pure and Applied Logic, vol. 43 (1989), pp. 57–77.CrossRefGoogle Scholar
[5]Markovic, Z., On the structure of Kripke models of Heyting arithmetic, Mathematical Logic Quarterly, vol. 39 (1993), pp. 531–538.CrossRefGoogle Scholar
[6]Shepherdson, J. C., A nonstandard model for a free variable fragment of number theory, Bulletin of the Polish Academy of Sciences, vol. 12 (1964), pp. 79–86.Google Scholar
[7]Smith, S. T., Fermat's last theorem and Bezout's theorem in GCD domains, Journal of Pure and Applied Algebra, vol. 79 (1992), pp. 63–85.CrossRefGoogle Scholar
[8]Smorynski, C., Applications of Kripke models, Metamathematical investigations of intuitionistic arithmetic and analysis (Troelstra, A. S., editor), Lecture Notes in Mathematics, no. 344, Springer-Verlag, 1973.Google Scholar
[9]Troelstra, A. S. and Schwichtenberg, H., Basic proof theory, Cambridge University Press, 1996.Google Scholar
[10]Troelstra, A. S. and van Dalen, D., Constructivism in mathematics, an introduction, v.1, North-Holland, 1988.Google Scholar
[11]van Dalen, D., Logic and structure, Springer-Verlag, 1997.Google Scholar
[12]Dalen, D. van, Mulder, H., Krabbe, E. C., and Visser, A., Finite Kripke models of HA are locally PA, Notre Dame Journal of Formal Logic, vol. 27 (1986), pp. 528–532.Google Scholar
[13]Wehmeier, K. F., Classical and intuitionistic models of arithmetic, Notre Dame Journal of Formal Logic, vol. 37 (1996), pp. 452–461.CrossRefGoogle Scholar
[14]Wehmeier, K. F., Fragments of HA based on Σ1-induction, Archive of Mathematical Logic, vol. 37 (1997), pp. 37–49.CrossRefGoogle Scholar
[15]Wilkie, A. J., Some results and problems on weak systems of arithmetic, Logic colloquium '77, North-Holland, 1978, pp. 285–296.CrossRefGoogle Scholar