Skip to main content Accessibility help
×
Hostname: page-component-586b7cd67f-rcrh6 Total loading time: 0 Render date: 2024-11-25T16:13:25.631Z Has data issue: false hasContentIssue false

Weak theories of nonstandard arithmetic and analysis

Published online by Cambridge University Press:  31 March 2017

Stephen G. Simpson
Affiliation:
Pennsylvania State University
Get access

Summary

Abstract. A general method of interpreting weak higher-type theories of nonstandard arithmetic in their standard counterparts is presented. In particular, this provides natural nonstandard conservative extensions of primitive recursive arithmetic, elementary recursive arithmetic, and polynomial-time computable arithmetic. A means of formalizing basic real analysis in such theories is sketched.

Introduction. Nonstandard analysis, as developed by Abraham Robinson, provides an elegant paradigm for the application of metamathematical ideas in mathematics. The idea is simple: use model-theoretic methods to build rich extensions of a mathematical structure, like second-order arithmetic or a universe of sets; reason about what is true in these enriched structures; and then transfer the results back to the ordinary mathematical universe. Robinson showed that this allows one, for example, to provide a coherent and consistent development of calculus based on the use of infinitesimals.

From a foundational point of view, it is natural to try to axiomatize such nonstandard structures. By formalizing the model-theoretic arguments, one can, in general, embed standard mathematical theories is conservative, nonstandard extensions. This was done e.g. by Kreisel, for second-order arithmetic [31]; Friedman, for first-order Peano arithmetic (unpublished); Nelson, for set theory [33]; and Moerdijk and Palmgren for intuitionistic first-order Heyting arithmetic [32] (see also [7]).

In recent years there has also been an interest in formalizing parts of mathematics in weak theories, at the level of primitive recursive arithmetic (PRA), or below. The underlying motivations vary. One may be drawn by the general philosophical goal of minimizing ontological commitments, or, less ethereally, by the sport of seeing how little one can get away with. Alternatively, one may be interested in extracting additional mathematical information from standard mathematical developments (e.g. [26, 27, 29, 30]), or narrowing the theoretical gap between abstract mathematics and concrete computation. In any event, a number of appropriate formal frameworks have been developed, including subsystems of first- and second-order arithmetic (e.g. [10, 37, 17, 19, 18, 49]), theories of finite types (e.g. [28, 30]), and versions of Feferman's theories of explicit mathematics (e.g. [41]), to name just a few.

Type
Chapter
Information
Publisher: Cambridge University Press
Print publication year: 2005

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

[1] Miklos, Ajtai, The complexity of the pigeonhole principle,Proceedings of the IEEE 29th annual symposium on foundations of computer science, 1988, pp. 346–355.
[2] Jeremy, Avigad, Formalizing forcing arguments in subsystems of second-order arithmetic,Annals of Pure and Applied Logic, vol. 82 (1996), no. 2, pp. 165–191.
[3] Jeremy, Avigad, Interpreting classical theories in constructive ones,The Journal of Symbolic Logic, vol. 65 (2000), no. 4, pp. 1785–1812.
[4] Jeremy, Avigad Ordinal analysis without proofs,Reflections on the foundations of mathematics (Stanford, California, 1998), Lecture Notes in Logic, vol. 15, Association for Symbolic Logic, Urbana, Illinois, 2002, pp. 1–36.
[5] Jeremy, Avigad, Saturated models of universal theories,Annals of Pure and Applied Logic, vol. 118 (2002), pp. 219–234.
[6] Jeremy, Avigad and Solomon, Feferman, Gödel's functional (“Dialectica”) interpretation, In Buss [13], pp. 337–405.
[7] Jeremy, Avigad and Jeffrey, Helzner, Transfer principles in nonstandard intuitionistic arithmetic,Archive for Mathematical Logic, vol. 41 (2002), no. 6, pp. 581–602.
[8] Jon, Barwise (editor), The handbook of mathematical logic, North-Holland, Amsterdam, 1977.
[9] Michael J., Beeson, Foundations of constructive mathematics, Springer, Berlin, 1985.
[10] Samuel R., Buss, Bounded arithmetic, Bibliopolis, Naples, 1986, A reprinting of the author's 1985 Princeton University dissertation.
[11] Samuel R., Buss, A conservation result concerning bounded theories and the collection axiom,Proceedings of the American Mathematical Society, vol. 100 (1987), pp. 709–716.
[12] Samuel R., Buss, First-order proof theory of arithmetic, In Buss [13].
[13] Samuel R., Buss (editor), The handbook of proof theory, North-Holland, Amsterdam, 1998.
[14] Rolando, Chuaqui and Patrick, Suppes, Free-variable axiomatic foundations of infinitesimal analysis: a fragment with finitary consistency proof,The Journal of Symbolic Logic, vol. 60 (1995), no. 1, pp. 122–159.
[15] Stephen A., Cook and Alasdair, Urquhart, Functional interpretations of feasibly constructive arithmetic,Annals of Pure and Applied Logic, vol. 63 (1993), pp. 103–200.
[16] Solomon, Feferman, Theories of finite type related to mathematical practice, In Barwise [8], pp. 913–971.
[17] António M., Fernandes and Fernando, Ferreira, Groundwork for weak analysis,The Journal of Symbolic Logic, vol. 67 (2002), no. 2, pp. 557–578.
[18] António M., Fernandes, Basic applications ofweak König's lemma in feasible analysis, Reverse mathematics 2001 (S., Simpson, editor), LectureNotes in Logic, vol. 22, AK Peters, 2005, this volume, pp. 175– 188.
[19] Fernando, Ferreira, A feasible theory for analysis,The Journal of Symbolic Logic, vol. 59 (1994), pp. 1001–1011.
[20] Fernando, Ferreira, A note on a result of Buss concerning bounded theories and the collection scheme,Portugaliae Mathematica, vol. 52 (1995), no. 3, pp. 331–336.
[21] KurtGödel, Collectedworks, vol. II, Oxford University Press, NewYork, 1990, Solomon Feferman et al., editors.
[22] Robert, Goldblatt, Lectures on the hyperreals: an introduction to nonstandard analysis, Springer, New York, 1998.
[23] Petr, Hájek and Pavel, Pudlák, Metamathematics of first-order arithmetic, Springer, Berlin, 1993.
[24] Richard, Kaye, Models of Peano arithmetic, Clarendon, Oxford, 1991.
[25] Ker-I, Ko, Complexity theory of real functions, Birkhäuser, Boston, 1991.
[26] Ulrich W., Kohlenbach, Effective moduli from ineffective uniqueness proofs: an unwinding of de La Vallée Poussin's proof for Chebycheff approximation,Annals of Pure and Applied Logic, vol. 64 (1993), pp. 27–94.
[27] Ulrich W., Kohlenbach, Analyzing proofs in analysis,Logic: From foundations to applications: European logic colloquium '93(W., Hodges et al., editors), Clarendon Press, Oxford, 1996, pp. 225–260.
[28] Ulrich W., Kohlenbach, Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals,Archive for Mathematical Logic, vol. 36 (1996), pp. 31–71.
[29] Ulrich W., Kohlenbach, Proof theory and computational analysis,Third workshop on computation and approximation (Comprox III,Birmingham, 1997), Elsevier, Amsterdam, 1998, 34 pp. (electronic).
[30] Ulrich W., Kohlenbach, Foundational and mathematical uses of higher types,Reflections on the foundations of mathematics (Stanford, California, 1998), Lecture Notes in Logic, vol. 15, Association for Symbolic Logic, Urbana, Illinois, 2002, pp. 92–116.
[31] Georg, Kreisel, Axiomatizations of nonstandard analysis that are conservative extensions of classical systems of analysis,Applications of model theory to algebra, analysis, and probability (W. A. J., Luxemburg, editor), Holt, Rinehart, and Winston, 1967, pp. 93–106.
[32] Ieke, Moerdijk and Erik, Palmgren, Minimal models of Heyting arithmetic,The Journal of Symbolic Logic, vol. 62 (1997), pp. 1448–1460.
[33] Edward, Nelson, Internal set theory: a new approach to nonstandard analysis,Bulletin of the American Mathematical Society, vol. 83 (1977), pp. 1165–1198.
[34] Edward, Nelson, Radically elementary probability theory, Princeton University, 1987.
[35] Erik, Palmgren, Developments in constructive nonstandard analysis,The Bulletin of Symbolic Logic, vol. 4 (1998), pp. 233–272.
[36] Erik, Palmgren, An effective conservation result for nonstandard analysis,Mathematical Logic Quarterly, vol. 46 (2000), pp. 17–23.
[37] Stephen G., Simpson, Subsystems of second order arithmetic, Springer, Berlin, 1998.
[38] Stephen G., Simpson and Rick L., Smith, Factorization of polynomials and Σ0/1 induction,Annals of Pure and Applied Logic, vol. 31 (1986), pp. 289–306.
[39] Richard, Sommer and Patrick, Suppes, Finite models of elementary recursive nonstandard analysis,Notas de la Sociedad de Matematica de Chile, vol. 15 (1996), no. 1, pp. 73–95.
[40] Richard, Sommer and Patrick, Suppes, Dispensing with the continuum,Journal of Mathematical Psychology, vol. 41 (1997), no. 1, pp. 3–10.
[41] Thomas, Strahm, Theories with self-application and computational complexity,Information and Computation, vol. 185 (2003), pp. 263–297.
[42] Kazuyuki, Tanaka, Non-standard analysis in WKL0, Mathematical Logic Quarterly, vol. 43 (1997), pp. 401–412.Google Scholar
[43] A.S., Troelstra, Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes inMathematics, vol. 344, Springer, Berlin, 1973.
[44] A.S., Troelstra, Aspects of constructive mathematics, In Barwise [8], pp. 973–1052.
[45] A.S., Troelstra, Introductory note to 1958 and 1972, In Gödel [21], pp. 217–241.
[46] A.S., Troelstra, Realizability, In Buss [13], pp. 407–473.
[47] Alex, Wilkie, Modèles non standard de l'arithmétique, et complexité algorithmique,Modèles non standard en arithmétique et théorie des ensembles, Publications Mathémathiques de l'Université Paris VII, vol. 22, 1985.
[48] Alan R., Woods, Approximating the structures accepted by a constant depth circuit or satisfying a sentence—a nonstandard approach,Logic and random structures (New Brunswick, New Jersey, 1995), American Mathematical Society, Providence, Rhode Island, 1997, pp. 109–130.
[49] Takeshi, Yamazaki, Reverse mathematics and weak systems of 0-1 strings for feasible analysis,Reverse mathematics 2001 (S., Simpson, editor), Lecture Notes in Logic, vol. 22, AK, Peters, 2005, this volume, pp. 394–401.Google Scholar

Save book to Kindle

To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.

Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.

Find out more about the Kindle Personal Document Service.

Available formats
×

Save book to Dropbox

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.

Available formats
×

Save book to Google Drive

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.

Available formats
×