Advertisement

On Two Models of Provability

  • Sergei Artemov
Part of the International Mathematical Series book series (IMAT, volume 5)

Abstract

Gödel’s modal logic approach to analyzing provability attracted a great deal of attention and eventually led to two distinct mathematical models. The first is the modal logic GL, also known as the Provability Logic, which was shown in 1979 by Solovay to be the logic of the formal provability predicate. The second is Gödel’s original modal logic of provability S4, together with its explicit counterpart, the Logic of Proofs LP, which was shown in 1995 by Artemov to provide an exact provability semantics for S4. These two models complement each other and cover a wide range of applications, from traditional proof theory to λ-calculi and formal epistemology.

Keywords

Modal Logic Intuitionistic Logic Epistemic Logic Modal Formula Peano Arithmetic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    J. Alt and S. Artemov, Reflective λ-calculus, In: Proceedings of the Dagstuhl-Seminar on Proof Theory in Computer Science, Lect. Notes Comput. Sci. 2183, Springer, 2001, pp. 22–37.Google Scholar
  2. 2.
    E. Antonakos, Justified knowledge is sufficient, Technical Report TR-2006004, CUNY Ph.D. Program in Computer Science (2006).Google Scholar
  3. 3.
    S. Artemov, Extensions of Arithmetic and Modal Logics (in Russian), Ph.D. Thesis, Moscow State University-Steklov Mathematical Insitute (1979).Google Scholar
  4. 4.
    S. Artemov, Arithmetically complete modal theories (in Russian), In: Semiotika Informatika 14, VINITI, Moscow, 1980, pp. 115–133; English transl.: S. Artemov, et al., Six Papers in Logic, Am. Math. Soc., Translations (2), 135, 1987.Google Scholar
  5. 5.
    S. Artemov, Nonarithmeticity of truth predicate logics of provability (in Russian), Dokl. Akad. Nauk SSSR 284 (1985), 270–271; English transl.: Sov. Math. Dokl. 32 (1985), 403–405.Google Scholar
  6. 6.
    S. Artemov, On modal logics axiomatizing provability (in Russian), Izv. Dokl. Akad. Nauk SSSR Ser. Mat. 49 (1985), 1123–1154; English transl.: Math. USSR Izv. 27 (1986), 401–429.MATHGoogle Scholar
  7. 7.
    S. Artemov, Numerically correct provability logics (in Russian), Dokl. Akad. Nauk SSSR 290 (1986), 1289–1292; English transl. Sov. Math. Dokl. 34 (1987), 384–387.Google Scholar
  8. 8.
    S. Artemov, Kolmogorov logic of problems and a provability interpretation of intuitionistic logic, In: Theoretical Aspects of Reasoning about Knowledge-III Proceedings (1990), pp. 257–272.Google Scholar
  9. 9.
    S. Artemov, Logic of proofs, Ann. Pure Appl. Logic 67 (1994), 29–59.MATHGoogle Scholar
  10. 10.
    S. Artemov, Operational modal logic, Technical Report MSI 95-29, Cornell University (1995).Google Scholar
  11. 11.
    S. Artemov, Logic of proofs: a unified semantics for modality and λ-terms, Technical Report CFIS 98-06, Cornell University (1998).Google Scholar
  12. 12.
    S. Artemov, Explicit provability and constructive semantics, Bull. Symb. Log. 7 (2001), 1–36.MATHGoogle Scholar
  13. 13.
    S. Artemov, Operations on proofs that can be specified by means of modal logic, In: Advances in Modal Logic, Vol. 2, CSLI Publications, Stanford University, 2001, pp. 59–72.Google Scholar
  14. 14.
    S. Artemov, Unified semantics for modality and λ-terms via proof polynomials, In: Algebras, Diagrams and Decisions in Language, Logic and Computation, K. Vermeulen and A. Copestake (Eds.), CSLI Publications, Stanford University, 2002, pp. 89–119.Google Scholar
  15. 15.
    S. Artemov, Embedding of modal lambda-calculus into the logic of proofs, Proc. Steklov Math. Inst. 242 (2003), 36–49.Google Scholar
  16. 16.
    S. Artemov, Evidence-based common knowledge, Technical Report TR-2004018, CUNY Ph.D. Program in Computer Science (2004), revised version of 2005.Google Scholar
  17. 17.
    S. Artemov, Kolmogorov and Gödel’s approach to intuitionistic logic: current developments (in Russian), Usp. Mat. Nauk 59 (2003), No.2, 9–36; English transl.: Russ. Math. Surv. 59 (2004), 203–229.Google Scholar
  18. 18.
    S. Artemov, Existential semantics for modal logic, In: We Will Show Them: Essays in Honour of Dov Gabbay, Vol. 1, H. Barringer, A. d’Avila Garcez, L. Lamb, and J. Woods (Eds.), College Publications, London, 2005, pp. 19–30.Google Scholar
  19. 19.
    S. Artemov, Justified common knowledge, Theor. Comput. Sci. 357 (2006), 4–22.MATHGoogle Scholar
  20. 20.
    S. Artemov and L. Beklemishev, On propositional quantifiers in provability logic, Notre Dame J. Formal Logic 34 (1993), 401–419.MATHGoogle Scholar
  21. 21.
    S. Artemov and L. Beklemishev, Provability logic, In: Handbook of Philosophical Logic, 2nd edition, D. Gabbay and F. Guenthner (Eds.), Kluwer, 2004, pp. 229–403.Google Scholar
  22. 22.
    S. Artemov and R. Iemhoff, The basic intuitionistic logic of proofs, Technical Report TR-2005002, CUNY Ph.D. Program in Computer Science (2005).Google Scholar
  23. 23.
    S. Artemov and R. Iemhoff, The basic intuitionistic logic of proofs, J. Symb. Log. (2006). [To appear]Google Scholar
  24. 24.
    S. Artemov, E. Kazakov, and D. Shapiro, Epistemic logic with justi-fications, Technical Report CFIS 99-12, Cornell University (1999).Google Scholar
  25. 25.
    S. Artemov and R. Kuznets, Logical omniscience via proof complexity, accepted to Computer Science Logic’ 06.Google Scholar
  26. 26.
    S. Artemov and E. Nogina, Logic of knowledge with justifications from the provability perspective, Technical Report TR-2004011, CUNY Ph.D. Program in Computer Science (2004).Google Scholar
  27. 27.
    S. Artemov and E. Nogina, Introducing justification into epistemic logic, J. Log. Comput. 15 (2005), 1059–1073.MATHGoogle Scholar
  28. 28.
    S. Artemov and E. Nogina, On epistemic logic with justification, In: Theoretical Aspects of Rationality and Knowledge. Proceedings of the Tenth Conference (TARK 2005), June 10–12, 2005, R. van der Meyden (Ed.), Singapore. 2005, pp. 279–294.Google Scholar
  29. 29.
    S. Artemov and T. Strassen, The basic logic of proofs, In: Computer Science Logic. 6th Workshop, CSL’ 92. San Miniato, Italy, September/October 1992. Selected Papers, E. Börger, G. Jäger, H. K. Büning, S. Martini, and M. Richter (Eds.), Lect. Notes Comput. Sci. 702, Springer, 1992, pp. 14–28.Google Scholar
  30. 30.
    S. Artemov and T. Strassen, Functionality in the basic logic of proofs, Technical Report IAM 93-004, Department of Computer Science, University of Bern, Switzerland (1993).Google Scholar
  31. 31.
    S. Artemov and T. Strassen, The logic of the Gödel proof predicate, In: Computational Logic and Proof Theory. Third Kurt Gödel Colloquium, KGC’ 93. Brno, Chech Republic, August 1993. Proceedings, G. Gottlob, A. Leitsch, and D. Mundici (Eds.), Lect. Notes Comput. Sci. 713, Springer, 1993, pp. 71–82.Google Scholar
  32. 32.
    S. Artemov and T. Yavorskaya (Sidon), On the first order logic of proofs, Moscow Math. J. 1 (2001), 475–490.MATHGoogle Scholar
  33. 33.
    L. Beklemishev, On the classification of propositional provability logics (in Russian), Izv. Dokl. Akad. Nauk SSSR Ser. Mat. 53 (1989), 915–943; English transl.: Math. USSR Izv. 35 (1990), 247–275.Google Scholar
  34. 34.
    L. Beklemishev, On bimodal logics of provability, Ann. Pure Appl. Logic 68 (1994), 115–160.MATHGoogle Scholar
  35. 35.
    L. Beklemishev, Bimodal logics for extensions of arithmetical theories, J. Symb. Log. 61 (1996), 91–124.MATHGoogle Scholar
  36. 36.
    L. Beklemishev, Parameter free induction and provably total computable functions, Theor. Comput. Sci. 224 (1999), 13–33.MATHGoogle Scholar
  37. 37.
    L. Beklemishev, Proof-theoretic analysis by iterated reflection, Arch. Math. Logic 42 (2003), 515–552.MATHGoogle Scholar
  38. 38.
    L. Beklemishev, The Worm principle, Logic Group Preprint Series 219, University of Utrecht (2003).Google Scholar
  39. 39.
    L. Beklemishev, On the idea of formalisation in logic and law (2004), Logic and Law, 6th Augustus De MorganWorkshop, King’s College London.Google Scholar
  40. 40.
    L. Beklemishev, Reflection principles and provability algebras in formal arithmetic (in Russian), Usp. Mat. Nauk 60 (2005), 3–78; English transl.: Russ. Math. Surv. 60 (2005), 197–268.Google Scholar
  41. 41.
    L. Beklemishev, M. Pentus, and N. Vereshchagin, Provability, complexity, grammars, Am. Math. Soc., Translations (2), 192 (1999).Google Scholar
  42. 42.
    A. Berarducci, The interpretability logic of Peano Arithmetic, J. Symb. Log. 55 (1990), 1059–1089.MATHGoogle Scholar
  43. 43.
    A. Berarducci and R. Verbrugge, On the provability logic of bounded arithmetic, Ann. Pure Appl. Logic 61 (1993), 75–93.MATHGoogle Scholar
  44. 44.
    C. Bernardi, The uniqueness of the fixed point in every diagonalizable algebra, Stud. Log. 35 (1976), 335–343.MATHGoogle Scholar
  45. 45.
    L. Bonjour, The coherence theory of empirical knowledge, Philos. Stud. 30 (1976), 281–312. [Reprinted in: Contemporary Readings in Epistemology, M. F. Goodman and R.A. Snyder (Eds), Prentice Hall, 1993, pp. 70–89.]Google Scholar
  46. 46.
    G. Boolos, On deciding the truth of certain statements involving the notion of consistency, J. Symb. Log. 41 (1976), 779–781.Google Scholar
  47. 47.
    G. Boolos, Reflection principles and iterated consistency assertions, J. Symb. Log. 44 (1979), 33–35.MATHGoogle Scholar
  48. 48.
    G. Boolos, The Unprovability of Consistency: An Essay in Modal Logic, Cambridge Univ. Press, 1979.Google Scholar
  49. 49.
    G. Boolos, Extremely undecidable sentences, J. Symb. Log. 47 (1982), 191–196.MATHGoogle Scholar
  50. 50.
    G. Boolos, The logic of provability, Am. Math. Mon. 91 (1984), 470–480.MATHGoogle Scholar
  51. 51.
    G. Boolos, The Logic of Provability, Cambridge Univ. Press, 1993.Google Scholar
  52. 52.
    G. Boolos and G. Sambin, Provability: the emergence of a mathematical modality, Stud. Log. 50 (1991), 1–23.MATHGoogle Scholar
  53. 53.
    V. Brezhnev, On explicit counterparts of modal logics, Technical Report CFIS 2000-05, Cornell University (2000).Google Scholar
  54. 54.
    V. Brezhnev, On the logic of proofs, In: Proceedings of the Sixth ESSLLI Student Session, Helsinki, 2001, pp. 35–46.Google Scholar
  55. 55.
    V. Brezhnev and R. Kuznets, Making knowledge explicit: How hard it is, Theor. Comput. Sci. 357 (2006), 23–34.MATHGoogle Scholar
  56. 56.
    S. Buss, The modal logic of pure provability, Notre Dame J. Formal Logic 31 (1990), 225–231.MATHGoogle Scholar
  57. 57.
    A. Carbone and F. Montagna, Rosser orderings in bimodal logics, Z. Math. Logik Grundlagen Math. 35 (1989), 343–358.MATHGoogle Scholar
  58. 58.
    A. Carbone and F. Montagna, Much shorter proofs: A bimodal investigation, Z. Math. Logik Grundlagen Math. 36 (1990), 47–66.MATHGoogle Scholar
  59. 59.
    T. Carlson, Modal logics with several operators and provability interpretations, Isr. J. Math. 54 (1986), 14–24.MATHGoogle Scholar
  60. 60.
    A. Chagrov and M. Zakharyaschev, Modal companions of intermediate propositional logics, Stud. Log. 51 (1992), 49–82.MATHGoogle Scholar
  61. 61.
    A. Chagrov and M. Zakharyaschev, Modal Logic, Oxford Science Publications, 1997.Google Scholar
  62. 62.
    R. Constable, Types in logic, mathematics and programming, In: Handbook of Proof Theory, S. Buss (Ed.), Elsevier, 1998, pp. 683–786.Google Scholar
  63. 63.
    D. de Jongh and G. Japaridze, Logic of provability, In: Handbook of Proof Theory, S. Buss (Ed.), Elsevier, 1998, pp. 475–546.Google Scholar
  64. 64.
    D. de Jongh and F. Montagna, Much shorter proofs, Z. Math. Logik Grundlagen Math. 35 (1989), 247–260.MATHGoogle Scholar
  65. 65.
    D. de Jongh and A. Visser, Embeddings of Heyting algebras, In: Logic: From Foundations to Applications. European Logic Colloquium, Keele, UK, July 20–29, 1993, W. Hodges, M. Hyland, C. Steinhorn, and J. Truss (Eds.), Clarendon Press, Oxford, 1996, pp. 187–213.Google Scholar
  66. 66.
    G. Dzhaparidze (Japaridze), The logic of linear tolerance, Stud. Log. 51 (1992), 249–277.MATHGoogle Scholar
  67. 67.
    G. Dzhaparidze (Japaridze), A generalized notion of weak interpretability and the corresponding modal logic, Ann. Pure Appl. Logic 61 (1993), 113–160.MATHGoogle Scholar
  68. 68.
    L. Esakia, Intuitionistic logic and modality via topology, Ann. Pure Appl. Logic 127 (2004), 155–170. [Provinces of logic determined. Essays in the memory of Alfred Tarski. Parts IV, V and VI, Z. Adamowicz, S. Artemov, D. Niwinski, E. Orlowska, A. Romanowska, and J. Wolenski (Eds.)]MATHGoogle Scholar
  69. 69.
    R. Fagin, J. Halpern, Y. Moses, and M. Vardi, Reasoning About Knowledge, The MIT Press, 1995.Google Scholar
  70. 70.
    S. Feferman, Arithmetization of metamathematics in a general setting, Fundam. Math. 49 (1960), 35–92.MATHGoogle Scholar
  71. 71.
    M. Fitting, Semantics and tableaus for LPS4, Technical Report TR-2004016, CUNY Ph.D. Program in Computer Science (2004).Google Scholar
  72. 72.
    M. Fitting, A logic of explicit knowledge, In: The Logica Yearbook 2004, L. Behounek and M. Bilkova (Eds.), Filosofia, 2005, pp. 11–22.Google Scholar
  73. 73.
    M. Fitting, The logic of proofs, semantically, Ann. Pure Appl. Logic 132 (2005), 1–25.MATHGoogle Scholar
  74. 74.
    H. Friedman, 102 problems in mathematical logic, J. Symb. Log. 40 (1975), 113–129.MATHGoogle Scholar
  75. 75.
    D. Gabbay, Labelled Deductive Systems, Oxford Univ. Press, 1994.Google Scholar
  76. 76.
    D. Gabelaia, Modal Definability in Topology (2001), ILLC Publications, Master of Logic Thesis (MoL) Series MoL-2001-11.Google Scholar
  77. 77.
    E. Gettier, Is Justified True Belief Knowledge?, Analysis 23 (1963), 121–123.Google Scholar
  78. 78.
    J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, Cambridge Univ. Press, 1989.Google Scholar
  79. 79.
    K. Gödel, Eine Interpretation des intuitionistischen Aussagenkalkuls, Ergebnisse Math. Kolloq. 4 (1933), 39–40; English transl. in: Kurt Gödel Collected Works, Vol. 1,, S. Feferman et al. (Eds.), Oxford Univ. Press, Oxford, Clarendon Press, New York, 1986, pp. 301–303.Google Scholar
  80. 80.
    K. Gödel, Vortrag bei Zilsel, 1938, In: Kurt Gödel Collected Works. Volume III, S. Feferman (Ed.), Oxford Univ. Press, 1995, pp. 86–113.Google Scholar
  81. 81.
    R. Goldblatt, Arithmetical necessity, provability and intuitionistic logic, Theoria 44 (1978), 38–46.MATHGoogle Scholar
  82. 82.
    A. Goldman, A causal theory of knowing, J. Philos. 64 (1967), 335–372.Google Scholar
  83. 83.
    E. Goris, Logic of proofs for bounded arithmetic, In: Computer Science — Theory and Application, D. Grigoriev, J. Harrison, and E. Hirsch (Eds.), Lect. Notes Comput. Sci. 3967, Springer, 2006, pp. 191–201.Google Scholar
  84. 84.
    E. Goris and J. Joosten, Modal matters in interpretability logics, Technical report, Utrecht University. Institute of Philosophy (2004), Logic Group preprint series; 226.Google Scholar
  85. 85.
    A. Grzegorczyk, Some relational systems and the associated topological spaces, Fundam. Math. 60 (1967), 223–231.MATHGoogle Scholar
  86. 86.
    D. Guaspari and R. Solovay, Rosser sentences, Ann. Pure Appl. Logic 16 (1979), 81–99.MATHGoogle Scholar
  87. 87.
    P. Hájek and F. Montagna, The logic of Π1-conservativity, Arch. Math. Logic 30 (1990), 113–123.MATHGoogle Scholar
  88. 88.
    P. Hájek and F. Montagna, The logic of Π1-conservativity continued, Arch. Math. Logic 32 (1992), 57–63.MATHGoogle Scholar
  89. 89.
    P. Hájek and P. Pudlák, Metamathematics of First Order Arithmetic, Springer-Verlag, Berlin, Heidelberg, New York, 1993.MATHGoogle Scholar
  90. 90.
    V. Hendricks, Active agents, J. Logic Lang. Inf. 12 (2003), no. 4, 469–495.MATHGoogle Scholar
  91. 91.
    A. Heyting, Die intuitionistische grundlegung der mathematik, Erkenntnis 2 (1931), 106–115.Google Scholar
  92. 92.
    A. Heyting, Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie, Springer, 1934.Google Scholar
  93. 93.
    A. Heyting, Intuitionism: An Introduction, North-Holland, 1956.Google Scholar
  94. 94.
    D. Hilbert and P. Bernays, Grundlagen der Mathematik, Vols. I and II, 2d ed. Springer, 1968.Google Scholar
  95. 95.
    R. Iemhoff, A modal analysis of some principles of the provability logic of Heyting arithmetic, In: Advances in Modal Logic, Vol. 2, CSLI, M. Zakharyaschev, K. Segerberg, M. de Rijke, and H. Wansing (Eds.), Lect. Notes 119, CSLI Publications, Stanford, 2001, pp. 301–336.Google Scholar
  96. 96.
    R. Iemhoff, On the admissible rules of intuitionistic propositional logic, J. Symb. Log. 66 (2001), 281–294.MATHGoogle Scholar
  97. 97.
    R. Iemhoff, Provability Logic and Admissible Rules, Ph.D. Thesis, University of Amsterdam (2001).Google Scholar
  98. 98.
    K. Ignatiev, Partial conservativity and modal logics, ITLI Prepublication Series X-91-04, University of Amsterdam (1991).Google Scholar
  99. 99.
    K. Ignatiev, On strong provability predicates and the associated modal logics, J. Symb. Log. 58 (1993), 249–290.MATHGoogle Scholar
  100. 100.
    K. Ignatiev, The provability logic for Σ1-interpolability, Ann. Pure Appl. Logic 64 (1993), 1–25.MATHGoogle Scholar
  101. 101.
    G. Japaridze, The Modal Logical Means of Investigation of Provability (in Russian), Ph.D. Thesis, Moscow State University (1986).Google Scholar
  102. 102.
    G. Japaridze, The polymodal logic of provability (in Russian), In: Intensional Logics and Logical Structure of Theories: Material from the fourth Soviet-Finnish Symposium on Logic, Telavi, May 20–24, 1985, Metsniereba, Tbilisi, 1988, pp. 16–48.Google Scholar
  103. 103.
    G. Japaridze, Introduction to computability logic, Ann. Pure Appl. Logic 123 (2003), 1–99.MATHGoogle Scholar
  104. 104.
    G. Japaridze, From truth to computability I, Theor. Comput. Sci. 357 (2006), 100–135.MATHGoogle Scholar
  105. 105.
    J. Joosten, Interpretability Formalized, Ph.D. Thesis, University of Utrecht (2004).Google Scholar
  106. 106.
    S. Kleene, Introduction to Metamathematics, Van Norstrand, 1952.Google Scholar
  107. 107.
    A. Kolmogoroff, Zur Deutung der intuitionistischen logik (in German), Math. Z. 35 (1932), 58–65; English transl.: Selected works of A.N. Kolmogorov. Vol. I: Mathematics and Mechanics, V. M. Tikhomirov (Ed.), Kluwer, 1991 pp. 151–158.MATHGoogle Scholar
  108. 108.
    S. Kripke, Semantical considerations on modal logic, Acta Philos. Fenn. 16 (1963), 83–94.MATHGoogle Scholar
  109. 109.
    N. Krupski, Some Algorithmic Questions in Formal Systems with Internalization (in Russian), Ph.D. Thesis, Moscow State University (2006).Google Scholar
  110. 110.
    N. Krupski, On the complexity of the reflected logic of proofs, Theor. Comput. Sci. 357 (2006), 136–142.MATHGoogle Scholar
  111. 111.
    N. Krupski, Typing in reflective combinatory logic, Ann. Pure Appl. Logic 141 (2006), 243–256.MATHGoogle Scholar
  112. 112.
    V. Krupski, Operational logic of proofs with functionality condition on proof predicate, In: Logical Foundations of Computer Science ‘97, Yaroslavl’, S. Adian and A. Nerode (Eds.), Lect. Notes Comput. Sci. 1234, Springer, 1997, pp. 167–177.Google Scholar
  113. 113.
    V. Krupski, The single-conclusion proof logic and inference rules specification, Ann. Pure Appl. Log. 113 (2001), 181–206.Google Scholar
  114. 114.
    V. Krupski, Referential logic of proofs, Theor. Comput. Sci. 357 (2006), 143–166.MATHGoogle Scholar
  115. 115.
    R. Kuznets, On the complexity of explicit modal logics, In: Computer Science Logic 2000, Lect. Notes Comput. Sci. 1862, Springer, 2000, pp. 371–383.Google Scholar
  116. 116.
    R. Kuznets, Complexity of Evidence-Based Knowledge, In: Proceedings of the Rationality and Knowledge Workshop, ESSLLI, 2006.Google Scholar
  117. 117.
    A. Kuznetsov and A. Muravitsky, The logic of provability (in Russian), In: Abstracts of the 4th All-Union Conference on Mathematical Logic, Kishinev, 1976, p. 73.Google Scholar
  118. 118.
    A. Kuznetsov and A. Muravitsky, Magari algebras (in Russian), In: Fourteenth All-Union Algebra Conference, Abstracts, Part 2: Rings, Algebraic Structures, 1977, pp. 105–106.Google Scholar
  119. 119.
    A. Kuznetsov and A. Muravitsky, On superintuitionistic logics as fragments of proof logic, Stud. Log. 45 (1986), 77–99.MATHGoogle Scholar
  120. 120.
    K. Lehrer and T. Paxson, Knowledge: undefeated justified true belief, J. Philos. 66 (1969), 1–22.Google Scholar
  121. 121.
    E. Lemmon, New foundations for Lewis’s modal systems, J. Symb. Log. 22 (1957), 176–186.MATHGoogle Scholar
  122. 122.
    W. Lenzen, Knowledge, belief and subjective probability, In: Knowledge Contributors, K. J. V. Hendricks and S. Pedersen, (Eds.), Kluwer, 2003.Google Scholar
  123. 123.
    D. Lewis, Elusive knowledge, Australian J. Philos. 7 (1996), 549–567.Google Scholar
  124. 124.
    P. Lindstrm, Provability logic — a short introduction, Theoria 62 (1996), 19–61.Google Scholar
  125. 125.
    M. Löb, Solution of a problem of Leon Henkin, J. Symb. Log. 20 (1955), 115–118.MATHGoogle Scholar
  126. 126.
    D. Luchi and F. Montagna, An operational logic of proofs with positive and negative information, Stud. Log. 63 (1999), no.1, 7–25.MATHGoogle Scholar
  127. 127.
    A. Macintyre and H. Simmons, Gödel’s diagonalization technique and related properties of theories, Colloquium Mathematicum 28 (1973).Google Scholar
  128. 128.
    R. Magari, The diagonalizable algebras (the algebraization of the theories which express Theor.:II), Bollettino della Unione Matematica Italiana, Serie 4 12 (1975), suppl. fasc. 3, 117–125.Google Scholar
  129. 129.
    R. Magari, Representation and duality theory for diagonalizable algebras (the algebraization of theories which express Theor.:IV), Stud. Log. 34 (1975), 305–313.Google Scholar
  130. 130.
    J. McKinsey and A. Tarski, Some theorems about the sentential calculi of Lewis and Heyting, J. Symb. Log. 13 (1948), 1–15.MATHGoogle Scholar
  131. 131.
    Meyer, J.-J. Ch. and W. van der Hoek, Epistemic Logic for AI and Computer Science, Cambridge Univ. Press, 1995.Google Scholar
  132. 132.
    R. Milnikel, Derivability in certain subsystems of the logic of proofs is П2p-complete, Ann. Pure Appl. Logic (2006). [To appear]Google Scholar
  133. 133.
    G. Mints, Lewis’ systems and system T (a survey 1965-1973) (in Russian), In: Modal Logic, Nauka, Moscow, 1974, pp. 422–509; English transl.: G. Mints, Selected Papers in Proof Theory, Bibliopolis, Napoli, 1992.Google Scholar
  134. 134.
    A. Mkrtychev, Models for the logic of proofs, In: Logical Foundations of Computer Science’ 97, Yaroslavl’, S. Adian and A. Nerode (Eds.), Lect. Notes Comput. Sci. 1234, Springer, 1997, pp. 266–275.Google Scholar
  135. 135.
    F. Montagna, On the diagonalizable algebra of Peano arithmetic, Boll. Unione Mat. Ital. B (5) 16 (1979), 795–812.MATHGoogle Scholar
  136. 136.
    F. Montagna, Undecidability of the first-order theory of diagonalizable algebras, Stud. Log. 39 (1980), 347–354.MATHGoogle Scholar
  137. 137.
    F. Montagna, The predicate modal logic of provability, Notre Dame J. Formal Logic 25 (1987), 179–189.Google Scholar
  138. 138.
    R. Montague, Syntactical treatments of modality with corollaries on reflection principles and finite axiomatizability, Acta Philos. Fenn. 16 (1963), 153–168.MATHGoogle Scholar
  139. 139.
    Y. Moses, Resource-bounded knowledge, In: Proceedings of the Second Conference on Theoretical Aspects of Reasoning about Knowledge, held in Pacific Grove, California, USA, March 7–9, 1988, M. Vardi (Ed.), Morgan Kaufmann, 1988, pp. 261–276.Google Scholar
  140. 140.
    J. Myhill, Some remarks on the notion of proof, J. Philos. 57 (1960), 461–471.Google Scholar
  141. 141.
    J. Myhill, Intensional set theory, In: Intensional Mathematics, S. Shapiro (Ed.), North-Holland, 1985, pp. 47–61.Google Scholar
  142. 142.
    E. Nogina, Logic of proofs with the strong provability operator, Technical Report ILLC Prepublication Series ML-94-10, Institute for Logic, Language and Computation, University of Amsterdam (1994).Google Scholar
  143. 143.
    E. Nogina, Grzegorczyk logic with arithmetical proof operators (in Russian), Fundam. Prikl. Mat. 2 (1996), no. 2, 483–499.MATHGoogle Scholar
  144. 144.
    E. Nogina, On logic of proofs and provability, Bull. Symb. Log. 12 (2006), no. 2, 356.Google Scholar
  145. 145.
    P. Novikov, Constructive Mathematical Logic from the Viewpoint of the Classical One (in Russian), Nauka, 1977.Google Scholar
  146. 146.
    Nozick, R., Philosophical Explanations, Harvard Univ. Press, 1981.Google Scholar
  147. 147.
    I. Orlov, The calculus of compatibility of propositions (in Russian), Mat. Sb. 35 (1928), 263–286.Google Scholar
  148. 148.
    E. Pacuit, A note on some explicit modal logics (2005), 5th Panhellenic Logic Symposium, Athens.Google Scholar
  149. 149.
    R. Parikh, Knowledge and the problem of logical omniscience, In: ISMIS-8 (International Symposium on Methodolody for Intellectual Systems) 1987, Z. Ras and M. Zemankova (Eds.), pp. 432–439.Google Scholar
  150. 150.
    R. Parikh, Logical omniscience, In: Logic and Computational Complexity, International Workshop LCC’ 94, Indianapolis, Indiana, USA, 13–16 October 1994, D. Leivant (Ed.), Lect. Notes Comput. Sci. 960, Springer, 1995, pp. 22–29.Google Scholar
  151. 151.
    B. Renne, Bisimulation and public announcements in logics of explicit knowledge, In: Proceedings of the Rationality and Knowledge Workshop, 2006.Google Scholar
  152. 152.
    B. Renne, Semantic cut-elimination for an explicit modal logic, In: Proceedings of the ESSLLI 2006 Student Session, Malaga, 2006.Google Scholar
  153. 153.
    J. Rosser, Extensions of some theorems of Gödel and Church, J. Symb. Log. 1 (1936), 87–91.MATHGoogle Scholar
  154. 154.
    N. Rubtsova, Semantics for Logic of Explicit Knowledge Corresponding to S5, In: Proceedings of the Rationality and Knowledge Workshop, ESSLLI, 2006.Google Scholar
  155. 155.
    N. Rubtsova, Evidence Reconstruction of Epistemic Modal Logic S5, In: Computer Science-Theory and Application, D. Grigoriev, J. Harrison, and E. Hirsch (Eds.), Lect. Notes Comput. Sci. 3967, Springer, 2006, pp. 313–321.Google Scholar
  156. 156.
    N. Rubtsova. and T. Yavorskaya-Sidon, Operations on proofs and labels, J. Appl. Non-Classical Logics. [To appear]Google Scholar
  157. 157.
    S. Shapiro, Epistemic and intuitionistic arithmetic, In: Intensional Mathematics, S. Shapiro (Ed.), North-Holland, 1985, pp. 11–46.Google Scholar
  158. 158.
    S. Shapiro, Intensional mathematics and constructive mathematics, In: Intensional Mathematics, S. Shapiro (Ed.), North-Holland, 1985, pp. 1–10.Google Scholar
  159. 159.
    V. Shavrukov, The logic of relative interpretability over Peano arithmetic, Preprint, Steklov Mathematical Institute, Moscow (1988), in Russian.Google Scholar
  160. 160.
    V. Shavrukov, On Rosser’s provability predicate, Z. Math. Logik Grundlagen Math. 37 (1991), 317–330.MATHGoogle Scholar
  161. 161.
    V. Shavrukov, A smart child of Peano’s, N Notre Dame J. Formal Logic 35 (1994), 161–185.MATHGoogle Scholar
  162. 162.
    V. Shavrukov, Isomorphisms of diagonalizable algebras, Theoria 63 (1997), 210–221.Google Scholar
  163. 163.
    T. Sidon, Provability logic with operations on proofs, In: Logical Foundations of Computer Science’ 97, Yaroslavl’, S. Adian and A. Nerode (Eds.), Lect. Notes Comput. Sci. 1234, Springer, 1997, pp. 342–353.Google Scholar
  164. 164.
    T. Smiley, The logical basis of ethics, Acta Philos. Fenn. 16 (1963), 237–246.Google Scholar
  165. 165.
    C. Smorynski, The incompleteness theorems, In: Handbook of Mathematical Logic, J. Barwise (Ed.), North Holland, 1977, pp. 821–865.Google Scholar
  166. 166.
    C. Smorynski, Self-Reference and Modal Logic, Springer, 1985.Google Scholar
  167. 167.
    R. Solovay, Provability interpretations of modal logic, Isr. J. Math. 25 (1976), 287–304.MATHGoogle Scholar
  168. 168.
    V. Švejdar, Modal analysis of generalized Rosser sentences, J. Symb. Log. 48 (1983), 986–999.Google Scholar
  169. 169.
    G. Takeuti, Proof Theory, Elsevier, 1987.Google Scholar
  170. 170.
    A. Tarski, A. Mostovski, and R. Robinson, Undecidable Theories, North-Holland, 1953.Google Scholar
  171. 171.
    A. Troelstra and D. van Dalen, Constructivism in Mathematics, Vols 1, 2, North-Holland, 1988.Google Scholar
  172. 172.
    J. van Benthem, Reflections on epistemic logic, Logique Anal. Nouv. Ser. 133–134 (1993), 5–14.Google Scholar
  173. 173.
    J. van Benthem, Modal frame correspondence generalized, Technical Report PP-2005-08, Institute for Logic, Language, and Computation, Amsterdam (2005).Google Scholar
  174. 174.
    V. Vardanyan, Arithmetic comlexity of predicate logics of provability and their fragments (in Russian), Dokl. Akad. Nauk SSSR 288 (1986), 11–14; English transl.: Sov. Math. Dokl. 33 (1986), 569–572.Google Scholar
  175. 175.
    A. Visser, Aspects of Diagonalization and Provability, Ph.D. Thesis, University of Utrecht (1981).Google Scholar
  176. 176.
    A. Visser, The provability logics of recursively enumerable theories extending Peano Arithmetic at arbitrary theories extending Peano Arithmetic, J. Philos. Logic 13 (1984), 97–113.Google Scholar
  177. 177.
    A. Visser, Evaluation, provably deductive equivalence in Heyting arithmetic of substitution instances of propositional formulas, Logic Group Preprint Series 4, Department of Philosophy, University of Utrecht (1985).Google Scholar
  178. 178.
    A. Visser, Peano’s smart children. A provability logical study of systems with built-in consistency, Notre Dame J. Formal Logic 30 (1989), 161–196.MATHGoogle Scholar
  179. 179.
    A. Visser, Interpretability logic, In: Mathematical Logic, P. Petkov (Ed.), Plenum Press, 1990, pp. 175–208.Google Scholar
  180. 180.
    A. Visser, Propositional combinations of Σ1 -sentences in Heyting’s arithmetic, Logic Group Preprint Series 117, Department of Philosophy, University of Utrecht (1994).Google Scholar
  181. 181.
    A. Visser, An overview of interpretability logic, In: Advances in Modal Logic, Vol. 1, M. Kracht, M. de Rijke, and H. Wansing (Eds.), CSLI Publications, Stanford University, 1998, pp. 307–360.Google Scholar
  182. 182.
    A. Visser, Rules and arithmetics, Notre Dame J. Formal Logic 40 (1999), 116–140.MATHGoogle Scholar
  183. 183.
    A. Visser, Substitutions of Σ10-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic, Ann. Pure Appl. Logic 114 (2002), 227–271.MATHGoogle Scholar
  184. 184.
    A. Visser, Löb’s Logic meets the μ-Calculus, In: Processes, Terms and Cycles: Steps on the Road to Infinity. Essays Dedicated to Jan Willem Klop on the Occasion of his 60th Birthday, A. Middeldorp, V. van Oostrom, F. van Raamsdonk, and R. deVrijer (Eds.), Lect. Notes Comput. Sci. 3838, Springer, 2005, pp. 14–25.Google Scholar
  185. 185.
    J. von Neumann, A letter to Gödel on January 12, 1931, In: Kurt Gödel Collected Works, Vol. V, S. Feferman, J. Dawson, W. Goldfarb, C. Parsons, and W. Sieg (Eds.), Oxford Univ. Press, 2003, pp. 341–345.Google Scholar
  186. 186.
    T. Yavorskaya (Sidon), Logic of proofs and provability, Ann. Pure Appl. Logic 113 (2001), 345–372.Google Scholar
  187. 187.
    T. Yavorskaya (Sidon), Negative operations on proofs and labels, J. Log. Comput. 15 (2005), 517–537.MATHGoogle Scholar
  188. 188.
    T. Yavorskaya (Sidon), Logic of proofs with two proof predicates, In: Computer Science-Theory and Application, D. Grigoriev, J. Harrison, and E. Hirsch (Eds.), Lect. Notes Comput. Sci. 3967, Springer, 2006, pp. 369–380.Google Scholar
  189. 189.
    R. Yavorsky, On the logic of the standard proof predicate, In: Computer Science Logic 2000, Lect. Notes Comput. Sci. 1862, Springer, 2000, pp. 527–541.Google Scholar
  190. 190.
    R. Yavorsky, Provability logics with quantifiers on proofs, Ann. Pure Appl. Logic 113 (2001), 373–387.Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2007

Authors and Affiliations

  • Sergei Artemov
    • 1
  1. 1.CUNY Graduate CenterNew YorkUSA

Personalised recommendations