Hostname: page-component-cd9895bd7-jkksz Total loading time: 0 Render date: 2024-12-27T01:46:01.188Z Has data issue: false hasContentIssue false
  • English
  • Français

Some theories with positive induction of ordinal strength φω0

Published online by Cambridge University Press:  12 March 2014

Gerhard Jäger  and
Thomas Strahm
Gerhard Jäger
Affiliation:
Institut für Informatik und Angewandte Mathematik, Universität Bern, Neubrückstrasse 10, CH-3012 Bern, Switzerland, E-mail: [email protected]
Thomas Strahm
Affiliation:
Institut für Informatik und Angewandte Mathematik, Universität Bern, Neubrückstrasse 10, CH-3012 Bern, Switzerland, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper deals with: (i) the theory which results from by restricting induction on the natural numbers to formulas which are positive in the fixed point constants, (ii) the theory BON(μ) plus various forms of positive induction, and (iii) a subtheory of Peano arithmetic with ordinals in which induction on the natural numbers is restricted to formulas which are Σ in the ordinals. We show that these systems have proof-theoretic strength φω0.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 61 , Issue 3 , September 1996 , pp. 818 - 842
Copyright
Copyright © Association for Symbolic Logic 1996

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]Beeson, M. J., Foundations of constructive mathematics: Metamathematical studies, Springer-Verlag, Berlin, 1984.Google Scholar
[2]Buchholz, W., Feferman, S., Pohlers, W., and Sieg, W., Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies, Lecture notes in mathematics, vol. 897, Springer-Verlag, Berlin, 1981.Google Scholar
[3]Cantini, A., Logical frameworks for truth and abstraction: an investigation of non-extensional classifications, to appear.Google Scholar
[4]Cantini, A., On the relationship between choice and comprehension principles in second order arithmetic, this Journal, vol. 51 (1986), no. 2, pp. 360–373.Google Scholar
[5]Cantini, A., Notes on formal theories of truth, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 35 (1989), no. 2, pp. 97–130.CrossRefGoogle Scholar
[6]Dershowitz, N. and Jouannaud, J.-P., Rewrite systems, Handbook of theoretical computer science (van Leeuwen, J., editor), Elsevier, 1990, pp. 243–320.Google Scholar
[7]Feferman, S., A language and axioms for explicit mathematics, Algebra and logic (Crossley, J., editor), Lecture Notes in Mathematics, vol. 450, Springer-Verlag, Berlin, 1975, pp. 87–139.CrossRefGoogle Scholar
[8]Feferman, S., A theory of variable types, Revista Colombiana de Matemáticas (1975), pp. 95–105.Google Scholar
[9]Feferman, S., Constructive theories of functions and classes, Logic colloquium '78 (Boffa, M., van Dalen, D., and McAloon, K., editors), North-Holland, Amsterdam, 1979, pp. 159–224.Google Scholar
[10]Feferman, S., Iterated inductive fixed-point theories: applications to Hancock's conjecture, The Patras symposium (Metakides, G., editor), North-Holland, Amsterdam, 1982, pp. 171–196.CrossRefGoogle Scholar
[11]Feferman, S., Reflecting on incompleteness., this Journal, vol. 56 (1991), no. 1, pp. 1–49.Google Scholar
[12]Feferman, S. and Jäger, G., Systems of explicit mathematics with non-constructive μ-operator. part I, Annals of Pure and Applied Logic, vol. 65, no. 3, pp. 243–263, 1993.CrossRefGoogle Scholar
[13]Feferman, S., Systems of explicit mathematics with non-constructive μ-operator. part II, to appear.Google Scholar
[14]Girard, J.-Y., Proof theory and logical complexitiy, Bibliopolis, Napoli, 1987.Google Scholar
[15]Glaß, T. and Strahm, T., Systems of explicit mathematics with non-constructive μ-operator and join, to appear.Google Scholar
[16]Jäger, G., Beweistheorie von KPN, Archiv für mathematische Logik und Grundlagenforschung, vol. 20 (1980), no. 3, pp. 53–64.CrossRefGoogle Scholar
[17]Jäger, G., Fixed points in Peano arithmetic with ordinals, Annals of Pure and Applied Logic, vol. 60 (1993), no. 2, pp. 119–132.CrossRefGoogle Scholar
[18]Jäger, G. and Strahm, T., Second order theories with ordinals and elementary comprehension, Archive for Mathematical Logic, vol. 34 (1995), no. 6, pp. 345–375.CrossRefGoogle Scholar
[19]Jäger, G., Totality in applicative theories, Annals of Pure and Applied Logic, vol. 74 (1995), no. 2, pp. 105–120.CrossRefGoogle Scholar
[20]Kahle, R., Natural numbers and forms of weak induction in applicative theories. Tech. Rep. 1AM 95-001, Institut für Informatik und angewandte Mathematik, Universität Bern, 1995.Google Scholar
[21]Pohlers, W, Proof theory: An introduction, Lecture notes in mathematics, vol. 1407, Springer-Verlag, Berlin, 1988.Google Scholar
[22]Schütte, K., Proof theory, Springer-Verlag, Berlin, 1977.CrossRefGoogle Scholar
[23]Sieg, W., Fragments of arithmetic, Annals of Pure and Applied Logic, vol. 28 (1985), pp. 33–71.CrossRefGoogle Scholar
[24]Takeuti, G., Proof theory, North-Holland, Amsterdam, 1987.Google Scholar
[25]Troelstra, A. and van Dalen, D., Constructivism in mathematics, vol. I., North-Holland, Amsterdam, New York, 1988.Google Scholar