Hostname: page-component-8448b6f56d-c4f8m Total loading time: 0 Render date: 2024-04-19T22:03:55.578Z Has data issue: false hasContentIssue false
  • English
  • Français

Groundwork for weak analysis

Published online by Cambridge University Press:  12 March 2014

António M. Fernandes  and
Fernando Ferreira
António M. Fernandes
Affiliation:
Departamento de Matemática, Instituto Superior Técnico, Av. Rovisco Pais. 1096 Lisboa Codex., Portugal, E-mail: amfernandes@netcabo.pt
Fernando Ferreira
Affiliation:
Departamento de Matemática, Universidade de Lisboa, Rua Ernesto de Vasconcelos, Bloco C1-3. P-1749-016 Lisboa, Portugal, E-mail: ferferr@cii.fc.ul.pt
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper develops the very basic notions of analysis in a weak second-order theory of arithmetic BTFA whose provably total functions are the polynomial time computable functions. We formalize within BTFA the real number system and the notion of a continuous real function of a real variable. The theory BTFA is able to prove the intermediate value theorem, wherefore it follows that the system of real numbers is a real closed ordered field. In the last section of the paper, we show how to interpret the theory BTFA in Robinson's theory of arithmetic Q. This fact entails that the elementary theory of the real closed ordered fields is interpretable in Q.

Keywords

Weak analysispolytime computabilityinterpretability
Type
Research Article
Information
The Journal of Symbolic Logic , Volume 67 , Issue 2 , June 2002 , pp. 557 - 578
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]Boolos, George and Jeffrey, Richard, Computability and logic, 2nd ed., Cambridge University Press, 1990.Google Scholar
[2]Buchholz, Wilfried and Sieg, Wilfried, A note on polynomial time arithmetic, Logic and computation (Sieg, Wilfried, editor). American Mathematical Society, 1990, pp. 51–55.CrossRefGoogle Scholar
[3]Buss, Samuel, Bounded arithmetic, Ph.D. thesis, Princeton University, 06 1985, a revision of this thesis was published by Bibliopolis in 1986.Google Scholar
[4]Cantini, Andrea, Asymmetric interpretations for bounded theories, Mathematical Logic Quarterly, vol. 42 (1996), no. 1, pp. 270–288.CrossRefGoogle Scholar
[5]Ferreira, Fernando, Polynomial time computable arithmetic and conservative extensions, Ph.D. thesis, Pennsylvania State University, 12 1988, pp. vii+168.Google Scholar
[6]Ferreira, Fernando, Polynomial time computable arithmetic, Logic and computation (Sieg, Wilfried, editor), American Mathematical Society, 1990, pp. 137–156.CrossRefGoogle Scholar
[7]Ferreira, Fernando, Stockmeyer induction, Feasible mathematics (Buss, Samuel and Scott, Philip, editors), Birkhäuser, 1990, pp. 161–180.CrossRefGoogle Scholar
[8]Ferreira, Fernando, A feasible theory for analysis, this Journal, vol. 59 (1994), pp. 1001–1011.Google Scholar
[9]Ferreira, Fernando, On end-extensions of models of ¬exp, Mathematical Logic Quarterly, vol. 42 (1996), pp. 1–18.CrossRefGoogle Scholar
[10]Friedman, Harvey, FOM:73:Hilbert's program wide open?, FOM e-mail list: http://www.math.psu.edu/simpson/fom, 12 20 1999.Google Scholar
[11]Hájek, Petr and Pudlák, Pavel, Metamathematics of first-order arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, 1993.CrossRefGoogle Scholar
[12]Hatzikiriakou, Kostas, Algebraic disguises of Σ10 induction, Archive for Mathematical Logic, vol. 29 (1989), pp. 47–51.CrossRefGoogle Scholar
[13]Hilbert, David and Bernays, Paul, Grundlagen der Mathematik, second ed., Grundlehren der mathematischen Wißenschaften, Springer-Verlag, 1968–1970, two volumes.CrossRefGoogle Scholar
[14]Kaye, Richard, Models of Peano arithmetic, Oxford Logic Guides, vol. 15, Clarendon Press, 1991.CrossRefGoogle Scholar
[15]Knuth, Donald, The art of computer programming, Seminumerical algorithms, 2nd ed., vol. 2, Addison-Wesley, 1981.Google Scholar
[16]Ker-Iko, , Complexity theory of real functions, Birkhauser, 1991.Google Scholar
[17]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
[18]Kohlenbach, Ulrich, Arithmetizing proofs in analysis, Proceedings of the logic colloquium (1996) (Larrazabal, J., Lascar, J., and Mints, G., editors). Springer Lecture Notes in Logic, vol. 12, 1998, pp. 115–158.CrossRefGoogle Scholar
[19]Kohlenbach, Ulrich, Proof theory and computational analysis, Electronic Notes in Theoretical Computer Science, vol. 13 (1998), 34 pages, http://www.elsevier.nl.locate/entcs/volumel3.html.CrossRefGoogle Scholar
[20]Nelson, Edward, Predicative arithmetic, Mathematical Notes, Princeton University Press, 1986.CrossRefGoogle Scholar
[21]Razborov, Alexander, An equivalence between second order bounded domain bounded arithmetic and first order bounded arithmetic, Arithmetic, proof theory and computational complexity (Clote, Peter and Krajíček, Jan, editors), Clarendon Press, 1993, pp. 247–277.CrossRefGoogle Scholar
[22]Shoenfield, Joseph, Mathematical logic, Addison-Wesley, 1967. reprinted by the Association for Symbolic Logic, 2001.Google Scholar
[23]Simpson, Stephen, Subsystems of second-order arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, 1999.CrossRefGoogle Scholar
[24]Simpson, Stephen and Rao, Ju, Reverse algebra, Handbook of recursive mathematics, Volume 2: Recursive algebra, analysis and combinatorics, Studies in Logic and the Foundations of Mathematics, vol. 139, Elsevier, 1998, pp. 1355–1372.CrossRefGoogle Scholar
[25]Simpson, Stephen and Smith, Rick, Factorization of polynomials and Σ10 induction, Annals of Pure and Applied Logic, vol. 31 (1986), pp. 289–306.CrossRefGoogle Scholar
[26]Takeuti, Gaisi, RSUV isomorphisms, Arithmetic, proof theory and computational complexity (Clote, Peter and Krajíček, Jan, editors), Clarendon Press, 1993, pp. 364–386.CrossRefGoogle Scholar
[27]Tarski, Alfred, A decision method for elementary algebra and geometry, Technical report, Rand Corporation, 1958.Google Scholar
[28]Yamazaki, Takeshi, Reverse mathematics and basic feasible systems of 0-1 strings, manuscript. 8 pages, to appear in “Reverse Mathematics 2001” (Simpson, Stephen, editor). 2000.Google Scholar
[29]Yamazaki, Takeshi, Some more conservation results on the Baire category theorem, Mathematical Logic Quarterly, vol. 46 (2000), pp. 105–110.3.0.CO;2-2>CrossRefGoogle Scholar