Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-20T11:42:00.170Z Has data issue: false hasContentIssue false
  • English
  • Français

Fragments of Heyting arithmetic

Published online by Cambridge University Press:  12 March 2014

Wolfgang Burr
Wolfgang Burr*
Affiliation:
Institut für Mathematische Logik und Grundlagenforschung, der Westfälischen Wilhelms-Universität Münster, Einsteinstr. 62, D-48149 Münster, Germany E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We define classes Φn of formulae of first-order arithmetic with the following properties:

(i) Every φ ϵ Φn is classically equivalent to a Πn-formula (n ≠ 1, Φ1 := Σ1).

(ii)

(iii) IΠn and iΦn (i.e., Heyting arithmetic with induction schema restricted to Φn-formulae) prove the same Π2-formulae.

We further generalize a result by Visser and Wehmeier. namely that prenex induction within intuitionistic arithmetic is rather weak: After closing Φn both under existential and universal quantification (we call these classes Θn) the corresponding theories iΘn still prove the same Π2-formulae. In a second part we consider iΔ0 plus collection-principles. We show that both the provably recursive functions and the provably total functions of are polynomially bounded. Furthermore we show that the contrapositive of the collection-schema gives rise to instances of the law of excluded middle and hence .

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 65 , Issue 3 , September 2000 , pp. 1223 - 1240
Copyright
Copyright © Association for Symbolic Logic 2000

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]Avigad, Jeremy, Interpreting classical theories in constructive ones, preprint, 1998.Google Scholar
[2]Avigad, Jeremy and Sommer, Rick, A model-theoretic approach to ordinal analysis, The Bulletin of Symbolic Logic, vol. 3 (1997), pp. 17–52.CrossRefGoogle Scholar
[3]Beklemishev, Lev D., A proof-theoretic analysis of collection, Archive for Mathematical Logic, vol. 37 (1998), pp. 275–296.CrossRefGoogle Scholar
[4]Buss, Samuel, Bounded arithmetic, Bibliopolis, Naples, 1986, revision of 1985 Princeton University Ph. D. thesis.Google Scholar
[5]Coquand, Thierry and Hofmann, Martin, A new method for establishing conservativity of classical systems over their intuitionistic version, Lambda calculus and logic, Mathematical Structures in Computer Science, vol. 9 (1999), no. 4, pp. 323–333.CrossRefGoogle Scholar
[6]Diller, Justus and Nahm, Werner, Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen, Archiv für mathematische Logik und Grundlagenforschung, vol. 16 (1974), pp. 49–66.CrossRefGoogle Scholar
[7]Diller, Justus and Schütte, Kurt, Simultane Rekursionen in der Theorie der Funktionale endlicher Typen, Archiv für mathematische Logik und Grundlagenforschung, vol. 14 (1970), pp. 69–74.Google Scholar
[8]Gödel, Kurt, Über eine bisher noch nicht benützte Erweiterung desfiniten Standpunktes, Dialectica, vol. 12 (1958), pp. 280–287.CrossRefGoogle Scholar
[9]Hájek, Petr and Pudlák, Pavel, Metamathematics of first-order arithmetic, Berlin, 1993.CrossRefGoogle Scholar
[10]Kaye, Richard, Models of Peano arithmetic, Oxford, 1991.CrossRefGoogle Scholar
[11]Kohlenbach, Ulrich, Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals, Archive for Mathematical Logic, vol. 36 (1996), pp. 31–71.CrossRefGoogle Scholar
[12]Leivant, Daniel, Implicational complexity in intuitionistic arithmetic, this Journal, vol. 46 (1981), pp. 240–248.Google Scholar
[13]Parsons, Charles, On n-quantifier induction, this Journal, vol. 37 (1972), pp. 466–482.Google Scholar
[14]Pohlers, Wolfram, Proof theory, Berlin, 1989.CrossRefGoogle Scholar
[15]Schütte, Kurt, Proof theory, Heidelberg, 1977.CrossRefGoogle Scholar
[16]Shoenfield, J. R., Mathematical logic, 2nd ed., Addison-Wesley, Reading, Massachusetts, 1973.Google Scholar
[17]Sieg, Wilfred, Fragments of arithmetic, Annals of Pure and Applied Logic, vol. 28 (1985), pp. 33–71.CrossRefGoogle Scholar
[18]Troelstra, A. S. (editor), Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin, 1973.CrossRefGoogle Scholar
[19]Troelstra, A. S., Aspects of constructive mathematics, Handbook of mathematical logic (Barwise, Jon, editor), North-Holland, 1977, pp. 973–1052.Google Scholar
[20]Troelstra, A. S. and van Dalen, D., Constructivism in mathematics, vol. I, North-Holland, Amsterdam, 1988.Google Scholar
[21]Wehmeier, Kai F., Semantical investigations in intuitionistic first-order arithmetic, Ph.D. thesis, Münster, 1996.Google Scholar
[22]Wehmeier, Kai F., Fragments of HA based on Σ1-induction, Archive for Mathematical Logic, vol. 37 (1997), pp. 445–460.CrossRefGoogle Scholar
[23]Weiermann, Andreas, How is it, that infinitary methods can be applied to finitary mathematics? Gödel's T; a case study, this Journal, vol. 63 (1998), pp. 1348–1370.Google Scholar