Hostname: page-component-cd9895bd7-jkksz Total loading time: 0 Render date: 2025-01-03T10:38:14.737Z Has data issue: false hasContentIssue false
  • English
  • Français

Bounded modified realizability

Published online by Cambridge University Press:  12 March 2014

Fernando Ferreira  and
Ana Nunes
Fernando Ferreira
Affiliation:
Departamento de Matemática, Universidade de Lisboa, P-1749-016 Lisboa, Portugal. E-mail: [email protected]
Ana Nunes
Affiliation:
Departamento de Matemática, Universidade do Algarve, P-8000 FARO, Portugal CMAF -Universidade de Lisboa, P-1649-003 Lisboa, Portugal. E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We define a notion of realizability, based on a new assignment of formulas, which does not care for precise witnesses of existential statements, but only for bounds for them. The novel form of realizability supports a very general form of the FAN theorem, refutes Markov's principle but meshes well with some classical principles, including the lesser limited principle of omniscience and weak König's lemma. We discuss some applications, as well as some previous results in the literature.

Keywords

Realizabilityboundssemi-intuitionismconservativeness
Type
Research Article
Information
The Journal of Symbolic Logic , Volume 71 , Issue 1 , March 2006 , pp. 329 - 346
Copyright
Copyright © Association for Symbolic Logic 2006

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]Akama, Y., Berardi, S., Hayashi, S., and Kohlenbach, U., An arithmetical hierarchy of the law of excluded middle and related principles, Proceedings of the 19th annual IEEE symposium on logic and computer science, vol. 117, IEEE Press, 2004, pp. 192–201.CrossRefGoogle Scholar
[2]Avigad, J. and Feferman, S., Gödel's functional (“Dialectica”) interpretation, Handbook of proof theory (Buss, S. R., editor), Studies in Logic and the Foundations of Mathematics, vol. 137, North Holland, Amsterdam, 1998, pp. 337–405.CrossRefGoogle Scholar
[3]Bezem, M., Strongly majorizable functional of finite type: a model for bar recursion containing discontinuous Junctionals. this Journal, vol. 50 (1985), pp. 652–660.Google Scholar
[4]Bridges, D. S. and Richman, F., Varieties of constructive mathematics, London Mathematical Society Lecture Notes Series, vol. 97. Cambridge University Press, 1987.CrossRefGoogle Scholar
[5]Ferreira, F. and Oliva, P., Bounded functional interpretation, Annals of Pure and Applied Logic, vol. 135 (2005), pp. 73–112.CrossRefGoogle Scholar
[6]Gödel, K., Über eine bisher noch nicht benützte Erweiterung desfiniten Standpunktes, Dialectica, vol. 12 (1958), pp. 280–287.CrossRefGoogle Scholar
[7]Howard, W. A., Hereditarily majorizable functional of finite type, Metamathematical investigation of intuitionistic Arithmetic and Analysis (Troelstra, A. S., editor), Lecture Notes in Mathematics, vol. 344, Springer, Berlin, 1973, pp. 454–461.Google Scholar
[8]Kleene, S. C., On the interpretation of intuitionistic number theory, this Journal, vol. 10 (1945), pp. 109–124.Google Scholar
[9]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.CrossRefGoogle Scholar
[10]Kohlenbach, U., Relative constructivity, this Journal, vol. 63 (1998), pp. 1218–1238.Google Scholar
[11]Kohlenbach, U., On uniform weak König's lemma, Annals of Pure Applied Logic, vol. 114 (2002), pp. 103–116.CrossRefGoogle Scholar
[12]Kohlenbach, U. and Oliva, P., Proof mining: a systematic way of analysing proofs in mathematics, Proceedings of the Steklov Institute of Mathematics, vol. 242, 2003, pp. 136–164.Google Scholar
[13]Kreisel, G., On weak completeness of intuitionistic predicate logic, this Journal, vol. 27 (1962), pp. 139–158.Google Scholar
[14]Troelstra, A. S. (editor), Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer, Berlin, 1973.CrossRefGoogle Scholar
[15]Troelstra, A. S., Introductory note to 1958 and 1972, Kurt Gödel collected works (Feferman, Solomonet al., editors), vol. II, Oxford University Press, New York, 1990, pp. 217–241.Google Scholar
[16]Troelstra, A. S., Realizability, Handbook of proof theory (Buss, S. R., editor), vol. 137, North Holland, Amsterdam, 1998, pp. 408–473.CrossRefGoogle Scholar