Hostname: page-component-cd9895bd7-q99xh Total loading time: 0 Render date: 2024-12-22T15:53:29.809Z Has data issue: false hasContentIssue false
  • English
  • Français

Forcing in Proof Theory

Published online by Cambridge University Press:  15 January 2014

Jeremy Avigad
Jeremy Avigad*
Affiliation:
Department of Philosophy, Carnegie Mellon University, Baker Hall 135, Pittsburgh, PA 15213, USAE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Paul Cohen's method of forcing, together with Saul Kripke's related semantics for modal and intuitionistic logic, has had profound effects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. Here, I argue that forcing also has a place in traditional Hilbert-style proof theory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or syntactic terms. I will discuss the aspects of forcing that are useful in this respect, and some sample applications. The latter include ways of obtaining conservation results for classical and intuitionistic theories, interpreting classical theories in constructive ones, and constructivizing model-theoretic arguments.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 10 , Issue 3 , September 2004 , pp. 305 - 333
Copyright
Copyright © Association for Symbolic Logic 2004

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] Ajtai, Miklos, The complexity of the pigeonhole principle, Proceedings of the IEEE 29th annual symposium on foundations of computer science, 1988, pp. 346–355.Google Scholar
[2] Avigad, Jeremy, Formalizing forcing arguments in subsystems of second-order arithmetic, Annals of Pure and Applied Logic, vol. 82 (1996), pp. 165–191.Google Scholar
[3] Avigad, Jeremy, Interpreting classical theories in constructive ones, The Journal of Symbolic Logic, vol. 65 (2000), pp. 1785–1812.Google Scholar
[4] Avigad, Jeremy, Algebraic proofs of cut elimination, The Journal of Logic and Algebraic Programming, vol. 49 (2001), pp. 15–30.Google Scholar
[5] Avigad, Jeremy, Notes on -conservativity, ω-submodels, and the collection schema, Technical Report CMU-PHIL-125, Carnegie Mellon University, 2001.Google Scholar
[6] Avigad, Jeremy, Saturated models of universal theories, Annals of Pure and Applied Logic, vol. 118 (2002), pp. 219–234.Google Scholar
[7] Avigad, Jeremy, Eliminating definitions and Skolem functions in first-order logic, ACM Transactions on Computer Logic, vol. 4 (2003), pp. 402–415, Conference version: Proceedings of the 16th annual IEEE symposium on logic in computer science , pp. 139-146, 2001.Google Scholar
[8] Avigad, Jeremy, Weak theories of nonstandard arithmetic and analysis, to appear.Google Scholar
[9] Avigad, Jeremy and Helzner, Jeffrey, Transfer principles in nonstandard intuitionistic arithmetic, Archive for Mathematical Logic, vol. 41 (2002), pp. 581–602.Google Scholar
[10] Baker, Theodore, Gill, John, and Solovay, Robert, Relativizations of the P = ? NP question, SIAM Journal of Computing, vol. 4 (1975), pp. 431–442.Google Scholar
[11] Beeson, Micfael, Principles of continuous choice and continuity offunctions in formal systems for constructive mathematics, Annals of Mathematical Logic, vol. 12 (1977), pp. 249–322.Google Scholar
[12] Beeson, Micfael, Continuity in intuitionistic set theories, Logic colloquium '78 (Mons, 1978), Studies in Logic and Foundations of Mathematics, vol. 97, North-Holland, Amsterdam, 1979, pp. 1–52.Google Scholar
[13] Beeson, Micfael, Foundations of constructive mathematics, Springer, Berlin, 1985.Google Scholar
[14] Boileau, Andre and Joyal, Andre, La logique des topos, The Journal of Symbolic Logic, vol. 46 (1981), pp. 6–16.Google Scholar
[15] Brown, Douglas and Simpson, Stepfen, The Baire category theorem in weak subsystems of second-order arithmetic, The Journal of Symbolic Logic, vol. 58 (1993), pp. 557–578.Google Scholar
[16] Bucffolz, Wilfried, Ein ausgezeichnetes Modell fur die intuitionistische Typenlogik, Archive for Mathematical Logic, vol. 17 (1975), pp. 55–60.Google Scholar
[17] Bucffolz, Wilfried, Feferman, Solomon, Poflers, Wolfram, and Sieg, Wilfried, Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies, Lecture Notes in Mathematics, vol. 897, Springer, Berlin, 1981.Google Scholar
[18] Chellas, Brian, Modal logic: an introduction, Cambridge University Press, Cambridge, 1980.CrossRefGoogle Scholar
[19] Cholak, Peter, Jockusch, Carl, and Slaman, Theodore, On the strength of Ramsey's theorem for pairs, The Journal of Symbolic Logic, vol. 66 (2001), pp. 1–55.Google Scholar
[20] Chuaqui, Rolando and Suppes, Patrick, Free-variable axiomatic foundations of infinitesimal analysis: a fragment with finitary consistency proof, The Journal of Symbolic Logic, vol. 60 (1995), pp. 122–159.Google Scholar
[21] Cooper, S. Barry, Computability theory, Chapman & Hall / CRC Mathematics, Boca Raton, 2004.Google Scholar
[22] Coquand, Thierry, Constructive topology and combinatorics, Constructivity in computer science (San Antonio, TX, 1991), Lecture Notes in Computer Science, vol. 613, Springer, Berlin, 1992, pp. 159–164.Google Scholar
[23] Coquand, Thierry, Computational content of classical logic, Semantics and logics of computation (Cambridge, 1995), Publications of the Newton Institute, vol. 14, Cambridge University Press, Cambridge, 1997, pp. 33–78.Google Scholar
[24] Coquand, Thierry, Minimal invariant spaces in formal topology, The Journal of Symbolic Logic, vol. 62 (1997), pp. 689–698.Google Scholar
[25] Coquand, Thierry, Two applications of Boolean models, Archive for Mathematical Logic, vol. 37 (1997), pp. 143–147.CrossRefGoogle Scholar
[26] Coquand, Thierry, A Boolean model of ultrafilters, Annals of Pure and Applied Logic, vol. 99 (1999), pp. 231–239.Google Scholar
[27] Coquand, Thierry and Hofmann, Martin, A new method ofestablishing conservativity ofclassical systems over their intuitionistic version, Mathematical Structures in Computer Science, vol. 9 (1999), pp. 323–333.Google Scholar
[28] Coquand, Thierry and Smith, Jan, An application of constructive completeness, Proccedings of the workshop TYPES '95 (S. Berardi and M. Copo, editors), Lecture Notes in Computer Science, vol. 1158, Springer, 1996, pp. 76–84.Google Scholar
[29] Coste, Michel, Lombardi, Henri, and Roy, Marie-Françoise, Dynamical method in algebra: effective Nullstellensätze, Annals of Pure Applied Logic, vol. 111 (2001), pp. 203–256.Google Scholar
[30] Dragalin, Albert, Mathematical intuitionism: Introduction to proof theory, Translations of mathematical monographs, American Mathematical Society, 1988.Google Scholar
[31] Fernandes, Antonio, Strict -reflection, Manuscript.Google Scholar
[32] Ferreira, Fernando, A feasible theory for analysis, The Journal of Symbolic Logic, vol. 59 (1994), pp. 1001–1011.Google Scholar
[33] Fitting, Melvin, Intuitionistic logic, model theory, and forcing, North-Holland, Amsterdam, 1969.Google Scholar
[34] Fourman, Michael, Continuous truth. I. Nonconstructive objects, Logic colloquium '82 (Florence, 1982), Studies in Logic and the Foundations of Mathematics, vol. 112, North-Holland, Amsterdam, 1984, pp. 161–180.CrossRefGoogle Scholar
[35] Fourman, Michael and Grayson, R. J., Formal spaces, The L. E. J. Brouwer centenary symposium (Noordwijkerhout, 1981), Studies in Logic and the Foundations of Mathematics, vol. 110, North-Holland, Amsterdam, 1982, pp. 107–122.Google Scholar
[36] Goldblatt, Robert, The categorial analysis of logic, Topoi, Studies in Logic and the Foundations of Mathematics, vol. 98, North-Holland, Amsterdam, 1984.Google Scholar
[37] Goldblatt, Robert, Logics of time and computation, second ed., CSLI Lecture Notes, vol. 7, Stanford University Center for the Study of Language and Information, Stanford, CA, 1992.Google Scholar
[38] Goldblatt, Robert, Mathematical modal logic: a view of its evolution, Draft available at http://www.mcs.vuw.ac.nz/~rob. Google Scholar
[39] Grayson, R. J., Forcing in intuitionistic systems without power-set, The Journal of Symbolic Logic, vol. 48 (1983), pp. 670–682.Google Scholar
[40] Hájek, Petr, Interpretability and fragments of arithmetic, Arithmetic, proof theory, and computational complexity (Peter Clote and Jan Krajíček, editors), Oxford University Press, Oxford, 1993, pp. 185–196.Google Scholar
[41] Hayashi, Susumu, A note on bar induction rule, The L. E. J. Brouwer centenary symposium (Noordwijkerhout, 1981), Studies in Logic and the Foundations of Mathematics, vol. 110, North-Holland, Amsterdam, 1982, pp. 149–163.Google Scholar
[42] Hilbert, David and Bernays, Paul, Grundlagen der Mathematik, vol. 1, Springer, Berlin, 1934, vol. 2, 1939.Google Scholar
[43] Hirst, Jeffry, Combinatorics in subsystems of second order arithmetic, Ph.D. thesis , The Pennsylvania State University, 1987.Google Scholar
[44] Hughes, G. E. and Cresswell, M. J., A new introduction to modal logic, Routledge, London, 1996.Google Scholar
[45] Jockusch, Carl, Ramsey's theorem and recursion theory, The Journal of Symbolic Logic, vol. 37 (1972), pp. 268–280.Google Scholar
[46] Jockusch, Carl and Soare, Robert, classes and degrees of theories, Transactions of the American Mathematical Society, vol. 173 (1972), pp. 33–56.Google Scholar
[47] Johnstone, Peter, The point of pointless topology, American Mathematical Society. Bulletin. New Series., vol. 8 (1983), pp. 41–53.Google Scholar
[48] Johnstone, Peter, The art of pointless thinking: a student's guide to the category of locales, Category theory at work (Bremen, 1990), Research and Exposition in Mathematics, vol. 18, Heldermann, Berlin, 1991, pp. 85–107.Google Scholar
[49] Kechris, Alexander, Classical descriptive set theory, Graduate Texts in Mathematics, vol. 156, Springer, New York, 1995.Google Scholar
[50] Krajíček, Jan, Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and its Applications, vol. 60, Cambridge University Press, Cambridge, 1995.Google Scholar
[51] Kreisel, Georg, Axiomatizations of nonstandard analysis that are conservative extensions ofclassical systems ofanalysis, Applications ofmodel theory to algebra, analysis, and probability (Luxemburg, W. A. J., editor), Holt, Rinehart, and Winston, 1967, pp. 93–106.Google Scholar
[52] Kunen, Kenneth, Set theory: an introduction to independence proofs, Studies in Logic and the Foundations of Mathematics, vol. 102, North-Holland, Amsterdam, 1980.Google Scholar
[53] Kuroda, S., Intuitionistische Untersuchungen der formalistischen Logik, Nagoya Mathematical Journal, vol. 2 (1951), pp. 35–47.Google Scholar
[54] Lerman, Manuel, Degrees of unsolvability: local and global theory, Perspectives in Mathematical Logic, Springer, Berlin, 1983.CrossRefGoogle Scholar
[55] Lubarsky, Robert S., IKP and friends, The Journal of Symbolic Logic, vol. 67 (2002), no. 4, pp. 1295–1322.Google Scholar
[56] Lane, Saunders Mac and Moerdijk, Ieke, Sheaves in geometry and logic, Springer, New York, 1992.Google Scholar
[57] Mathias, A. R. D., The strength of Mac Lane set theory, Annals of Pure and Applied Logic, vol. 110 (2001), pp. 107–234.CrossRefGoogle Scholar
[58] Moerdijk, Ieke, A modelfor intuitionistic non-standard arithmetic, Annals of Pure and Applied Logic, vol. 73 (1995), pp. 37–51.CrossRefGoogle Scholar
[59] Moerdijk, Ieke and palmgren, Erik, Minimal models of Heyting arithmetic, The Journal of Symbolic Logic, vol. 62 (1997), pp. 1448–1460.Google Scholar
[60] Moerdijk, Ieke and Reyes, Gonzalo, Models for smooth infinitesimal analysis, Springer, New York, 1991.Google Scholar
[61] Moore, Gregory, The origins of forcing, Logic colloquium '86 (Hull, 1986), Studies in Logic and the Foundations of Mathematics, vol. 124, North-Holland, Amsterdam, 1988, pp. 143–173.Google Scholar
[62] Nelson, Edward, Internal set theory: anew approach to nonstandard analysis, Bulletin of the American Mathematical Society, vol. 83 (1977), pp. 1165–1198.Google Scholar
[63] Okada, Mitsuhiro, A uniform semantic prooffor cut-elimination and completeness of various first and higher order logics, Theoretical Computer Science, vol. 281 (2002), pp. 471–498.Google Scholar
[64] Palmgren, Erik, Constructive sheaf semantics, Mathematical Logic Quarterly, vol. 43 (1997) , pp. 321–327.Google Scholar
[65] Palmgren, Erik, Developments in constructive nonstandard analysis, this Bulletin, vol. 4 (1998), pp. 233–272.Google Scholar
[66] Palmgren, Erik, An effective conservation result for nonstandard analysis, Mathematical Logic Quarterly, vol. 46 (2000), pp. 17–23.Google Scholar
[67] Riis, Søren, Making infinite structures finite in models of second order bounded arithmetic, Arithmetic, proof theory, and computational complexity (Prague, 1991), Oxford Logic Guides, vol. 23, Oxford University Press, New York, 1993, pp. 289–319.Google Scholar
[68] Sacks, Gerald, Higher recursion theory, Perspectives in Mathematical Logic, Springer, Berlin, 1990.Google Scholar
[69] Sambin, Giovanni, Some points in formal topology, Theoretical Computer Science, vol. 305 (2003), pp. 347–408.Google Scholar
[70] Seetapun, David and Slaman, Theodore A., On the strength of Ramsey's theorem, Notre Dame Journal of Formal Logic, vol. 36 (1995), pp. 570–582.Google Scholar
[71] Shoenfield, Josepf, Mathematical logic, Association for Symbolic Logic, Urbana, IL, 2001, Reprint of the 1973 second printing.Google Scholar
[72] Simpson, Stepfen, Subsystems of second-order arithmetic, Springer, Berlin, 1998.Google Scholar
[73] Simpson, Stephen and Smith, Rick, Factorization of polynomials and induction, Annals of Pure and Applied Logic, vol. 31 (1986), pp. 289–306.Google Scholar
[74] Simpson, Stephen, Tanaka, Kazuyuki, and Yamazaki, Takeshi, Some conservation results on weak König's lemma, Annals of Pure Applied Logic, vol. 118 (2002), pp. 87–114.CrossRefGoogle Scholar
[75] Sommer, Richard and Suppes, Patrick, Finite models of elementary recursive nonstandard analysis, Notas De la Sociedad de Matematica de Chile, vol. 15 (1996), pp. 73–95.Google Scholar
[76] Takeuti, Gaisi, Two applications of logic to mathematics, Publications of the Mathematical Society of Japan, vol. 13, Iwanami Shoten and Princeton University Press, 1978.Google Scholar
[77] Takeuti, Gaisi, Proof theory, second ed., North-Holland, Amsterdam, 1987.Google Scholar
[78] Takeuti, Gaisi and Yasumoto, Masahiro, Forcing on bounded arithmetic. II, The Journal of Symbolic Logic, vol. 63 (1998), pp. 860–868.Google Scholar
[79] Troelstra, A. S., Realizability, Handbook of proof theory, Studies in Logic and the Foundations of Mathematics, vol. 137, North-Holland, Amsterdam, 1998, pp. 407–473.Google Scholar
[80] Troelstra, A. S. and Van Dalen, Dirk, Constructivism in mathematics: An introduction, vol. 1, North-Holland, Amsterdam, 1988.Google Scholar
[81] Weyl, Hermann, Das Kontinuum. Kritische Untersuchungen über die Grundlagen der Analysis, Veit, Leipzig, 1918, Second edition, 1932.Google Scholar
[82] Wilkie, Alex and Paris, Jeff, On the scheme of induction for bounded arithmetic formulas, Annals of Pure and Applied Logic, vol. 35 (1987), pp. 261–302.Google Scholar