Hostname: page-component-cd9895bd7-mkpzs Total loading time: 0 Render date: 2024-12-28T16:36:14.972Z Has data issue: false hasContentIssue false
  • English
  • Français

Relative constructivity

Published online by Cambridge University Press:  12 March 2014

Ulrich Kohlenbach
Ulrich Kohlenbach*
Affiliation:
Brics, Department of Computer Science, University of Århus, NYMunkegade, DK-8000 Århus C, Denmark. E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Extract

In a previous paper [13] we introduced a hierarchy (GnAω)n∈ℕ of subsystems of classical arithmetic in all finite types where the growth of definable functions of GnAω corresponds to the well-known Grzegorczyk hierarchy. Let AC-qf denote the schema of quantifier-free choice.

[11], [13], [8] and [7] study various analytical principles Γ in the context of the theories GnAω + AC-qf (mainly for n = 2) and use proof-theoretic tools like, e.g., monotone functional interpretation (which was introduced in [12]) to determine their impact on the growth of uniform bounds Φ such that

which are extractable from given proofs (based on these principles Γ) of sentences

Here A0(u, k, v, w) is quantifier-free and contains only u, k, v, w as free variables; t is a closed term and ≤p is defined pointwise. The term ‘uniform bound’ refers to the fact that Φ does not depend on v ≤ptuk (see [12] for the relevance of such uniform bounds in numerical analysis and for concrete applications to approximation theory).

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 63 , Issue 4 , December 1998 , pp. 1218 - 1238
Copyright
Copyright © Association for Symbolic Logic 1998

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., Principles of continuous choice and continuity of functions in formal systems for constructive mathematics, Annals of Mathematical Logic, vol. 12 (1977), pp. 249–322.CrossRefGoogle Scholar
[2] Bezem, M. A., Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals, this Journal, vol. 50 (1985), pp. 652–660.Google Scholar
[3] Bridges, D. and Richman, F., Varieties of constructive mathematics, London Mathematical Society Lecture Note Series, no. 97, Cambridge University Press, Cambridge, 1987.Google Scholar
[4] Gödel, K., Über eine noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica, vol. 12 (1958), pp. 280–287.Google Scholar
[5] Howard, W. A., Hereditarily majorizable functionals of finite type, in [15].Google Scholar
[6] Kohlenbach, U., Arithmetizing proofs in analysis, Lecture Notes in Logic, Springer-Verlag, Berlin, to appear in Proceedings of Logic Colloquium 96 (San Sebastian).Google Scholar
[7] Kohlenbach, U., Proof theory and computational analysis, to appear in Electronic Notes in Theoretical Computer Science, vol. 13.Google Scholar
[8] Kohlenbach, U., The use of uniform boundedness in analysis, to appear in Proceedings of Logic in Florence 1995, Synthese Library, Kluwer.Google Scholar
[9] Kohlenbach, U., Pointwise hereditary majorization and some applications, Archive for Mathematical Logic, vol. 31 (1992), pp. 227–241.Google Scholar
[10] Kohlenbach, U., Exploiting partial constructivity relatively to non-constructive lemmas in given proofs (abstract of a contributed talk presented at the Logic Colloquium 94, Clermont-Ferrand), Bulletin of Symbolic Logic, vol. 1 (1995), pp. 243–244.Google Scholar
[11] Kohlenbach, U., Real growth in standard parts of analysis, Habilitationsschrift, Frankfurt, 1995, xv + 166 p.Google Scholar
[12] Kohlenbach, U., Analysing proofs in analysis, Logic: from foundations to applications (Hodges, W., Hyland, M., Steinhorn, C., and Truss, J., editors), Oxford University Press, Oxford, 1996, European Logic Colloquium, Keele 1993, pp. 225–260.Google Scholar
[13] Kohlenbach, U., Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals, Archive for Mathematical Logic, vol. 36 (1996), pp. 31–71.Google Scholar
[14] Kreisel, G., On weak completeness of intuitionistic predicate logic, this Journal, vol. 27 (1962), pp. 139–158.Google Scholar
[15] Troelstra, A. S. (editor), Metamathematical investigation of intuitionistic arithmetic and analysis, Springer Lecture Notes in Mathematics, no. 344, Springer-Verlag, Berlin, 1973.Google Scholar
[16] Troelstra, A. S. (editor), Note on the fan theorem, this Journal, vol. 39 (1974), pp. 584–596.Google Scholar
[17] Troelstra, A. S. (editor), Realizability, ILLC Prepublication Series for Mathematical Logic and Foundations ML-92-09, Amsterdam, 1992, to appear in Buss, S. (ed.), Handbook of proof theory.Google Scholar
[18] Troelstra, A. S. and van Dalen, D., Constructivism in mathematics: An introduction, vol. I, II, North-Holland, Amsterdam, 1988.Google Scholar