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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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.
E. Antonakos, Justified knowledge is sufficient, Technical Report TR-2006004, CUNY Ph.D. Program in Computer Science (2006).
S. Artemov, Extensions of Arithmetic and Modal Logics (in Russian), Ph.D. Thesis, Moscow State University-Steklov Mathematical Insitute (1979).
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.
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.
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.
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.
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.
S. Artemov, Logic of proofs, Ann. Pure Appl. Logic 67 (1994), 29–59.
S. Artemov, Operational modal logic, Technical Report MSI 95-29, Cornell University (1995).
S. Artemov, Logic of proofs: a unified semantics for modality and λ-terms, Technical Report CFIS 98-06, Cornell University (1998).
S. Artemov, Explicit provability and constructive semantics, Bull. Symb. Log. 7 (2001), 1–36.
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.
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.
S. Artemov, Embedding of modal lambda-calculus into the logic of proofs, Proc. Steklov Math. Inst. 242 (2003), 36–49.
S. Artemov, Evidence-based common knowledge, Technical Report TR-2004018, CUNY Ph.D. Program in Computer Science (2004), revised version of 2005.
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.
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.
S. Artemov, Justified common knowledge, Theor. Comput. Sci. 357 (2006), 4–22.
S. Artemov and L. Beklemishev, On propositional quantifiers in provability logic, Notre Dame J. Formal Logic 34 (1993), 401–419.
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.
S. Artemov and R. Iemhoff, The basic intuitionistic logic of proofs, Technical Report TR-2005002, CUNY Ph.D. Program in Computer Science (2005).
S. Artemov and R. Iemhoff, The basic intuitionistic logic of proofs, J. Symb. Log. (2006). [To appear]
S. Artemov, E. Kazakov, and D. Shapiro, Epistemic logic with justi-fications, Technical Report CFIS 99-12, Cornell University (1999).
S. Artemov and R. Kuznets, Logical omniscience via proof complexity, accepted to Computer Science Logic’ 06.
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).
S. Artemov and E. Nogina, Introducing justification into epistemic logic, J. Log. Comput. 15 (2005), 1059–1073.
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.
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.
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).
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.
S. Artemov and T. Yavorskaya (Sidon), On the first order logic of proofs, Moscow Math. J. 1 (2001), 475–490.
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.
L. Beklemishev, On bimodal logics of provability, Ann. Pure Appl. Logic 68 (1994), 115–160.
L. Beklemishev, Bimodal logics for extensions of arithmetical theories, J. Symb. Log. 61 (1996), 91–124.
L. Beklemishev, Parameter free induction and provably total computable functions, Theor. Comput. Sci. 224 (1999), 13–33.
L. Beklemishev, Proof-theoretic analysis by iterated reflection, Arch. Math. Logic 42 (2003), 515–552.
L. Beklemishev, The Worm principle, Logic Group Preprint Series 219, University of Utrecht (2003).
L. Beklemishev, On the idea of formalisation in logic and law (2004), Logic and Law, 6th Augustus De MorganWorkshop, King’s College London.
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.
L. Beklemishev, M. Pentus, and N. Vereshchagin, Provability, complexity, grammars, Am. Math. Soc., Translations (2), 192 (1999).
A. Berarducci, The interpretability logic of Peano Arithmetic, J. Symb. Log. 55 (1990), 1059–1089.
A. Berarducci and R. Verbrugge, On the provability logic of bounded arithmetic, Ann. Pure Appl. Logic 61 (1993), 75–93.
C. Bernardi, The uniqueness of the fixed point in every diagonalizable algebra, Stud. Log. 35 (1976), 335–343.
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.]
G. Boolos, On deciding the truth of certain statements involving the notion of consistency, J. Symb. Log. 41 (1976), 779–781.
G. Boolos, Reflection principles and iterated consistency assertions, J. Symb. Log. 44 (1979), 33–35.
G. Boolos, The Unprovability of Consistency: An Essay in Modal Logic, Cambridge Univ. Press, 1979.
G. Boolos, Extremely undecidable sentences, J. Symb. Log. 47 (1982), 191–196.
G. Boolos, The logic of provability, Am. Math. Mon. 91 (1984), 470–480.
G. Boolos, The Logic of Provability, Cambridge Univ. Press, 1993.
G. Boolos and G. Sambin, Provability: the emergence of a mathematical modality, Stud. Log. 50 (1991), 1–23.
V. Brezhnev, On explicit counterparts of modal logics, Technical Report CFIS 2000-05, Cornell University (2000).
V. Brezhnev, On the logic of proofs, In: Proceedings of the Sixth ESSLLI Student Session, Helsinki, 2001, pp. 35–46.
V. Brezhnev and R. Kuznets, Making knowledge explicit: How hard it is, Theor. Comput. Sci. 357 (2006), 23–34.
S. Buss, The modal logic of pure provability, Notre Dame J. Formal Logic 31 (1990), 225–231.
A. Carbone and F. Montagna, Rosser orderings in bimodal logics, Z. Math. Logik Grundlagen Math. 35 (1989), 343–358.
A. Carbone and F. Montagna, Much shorter proofs: A bimodal investigation, Z. Math. Logik Grundlagen Math. 36 (1990), 47–66.
T. Carlson, Modal logics with several operators and provability interpretations, Isr. J. Math. 54 (1986), 14–24.
A. Chagrov and M. Zakharyaschev, Modal companions of intermediate propositional logics, Stud. Log. 51 (1992), 49–82.
A. Chagrov and M. Zakharyaschev, Modal Logic, Oxford Science Publications, 1997.
R. Constable, Types in logic, mathematics and programming, In: Handbook of Proof Theory, S. Buss (Ed.), Elsevier, 1998, pp. 683–786.
D. de Jongh and G. Japaridze, Logic of provability, In: Handbook of Proof Theory, S. Buss (Ed.), Elsevier, 1998, pp. 475–546.
D. de Jongh and F. Montagna, Much shorter proofs, Z. Math. Logik Grundlagen Math. 35 (1989), 247–260.
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.
G. Dzhaparidze (Japaridze), The logic of linear tolerance, Stud. Log. 51 (1992), 249–277.
G. Dzhaparidze (Japaridze), A generalized notion of weak interpretability and the corresponding modal logic, Ann. Pure Appl. Logic 61 (1993), 113–160.
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.)]
R. Fagin, J. Halpern, Y. Moses, and M. Vardi, Reasoning About Knowledge, The MIT Press, 1995.
S. Feferman, Arithmetization of metamathematics in a general setting, Fundam. Math. 49 (1960), 35–92.
M. Fitting, Semantics and tableaus for LPS4, Technical Report TR-2004016, CUNY Ph.D. Program in Computer Science (2004).
M. Fitting, A logic of explicit knowledge, In: The Logica Yearbook 2004, L. Behounek and M. Bilkova (Eds.), Filosofia, 2005, pp. 11–22.
M. Fitting, The logic of proofs, semantically, Ann. Pure Appl. Logic 132 (2005), 1–25.
H. Friedman, 102 problems in mathematical logic, J. Symb. Log. 40 (1975), 113–129.
D. Gabbay, Labelled Deductive Systems, Oxford Univ. Press, 1994.
D. Gabelaia, Modal Definability in Topology (2001), ILLC Publications, Master of Logic Thesis (MoL) Series MoL-2001-11.
E. Gettier, Is Justified True Belief Knowledge?, Analysis 23 (1963), 121–123.
J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, Cambridge Univ. Press, 1989.
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.
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.
R. Goldblatt, Arithmetical necessity, provability and intuitionistic logic, Theoria 44 (1978), 38–46.
A. Goldman, A causal theory of knowing, J. Philos. 64 (1967), 335–372.
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.
E. Goris and J. Joosten, Modal matters in interpretability logics, Technical report, Utrecht University. Institute of Philosophy (2004), Logic Group preprint series; 226.
A. Grzegorczyk, Some relational systems and the associated topological spaces, Fundam. Math. 60 (1967), 223–231.
D. Guaspari and R. Solovay, Rosser sentences, Ann. Pure Appl. Logic 16 (1979), 81–99.
P. Hájek and F. Montagna, The logic of Π1-conservativity, Arch. Math. Logic 30 (1990), 113–123.
P. Hájek and F. Montagna, The logic of Π1-conservativity continued, Arch. Math. Logic 32 (1992), 57–63.
P. Hájek and P. Pudlák, Metamathematics of First Order Arithmetic, Springer-Verlag, Berlin, Heidelberg, New York, 1993.
V. Hendricks, Active agents, J. Logic Lang. Inf. 12 (2003), no. 4, 469–495.
A. Heyting, Die intuitionistische grundlegung der mathematik, Erkenntnis 2 (1931), 106–115.
A. Heyting, Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie, Springer, 1934.
A. Heyting, Intuitionism: An Introduction, North-Holland, 1956.
D. Hilbert and P. Bernays, Grundlagen der Mathematik, Vols. I and II, 2d ed. Springer, 1968.
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.
R. Iemhoff, On the admissible rules of intuitionistic propositional logic, J. Symb. Log. 66 (2001), 281–294.
R. Iemhoff, Provability Logic and Admissible Rules, Ph.D. Thesis, University of Amsterdam (2001).
K. Ignatiev, Partial conservativity and modal logics, ITLI Prepublication Series X-91-04, University of Amsterdam (1991).
K. Ignatiev, On strong provability predicates and the associated modal logics, J. Symb. Log. 58 (1993), 249–290.
K. Ignatiev, The provability logic for Σ1-interpolability, Ann. Pure Appl. Logic 64 (1993), 1–25.
G. Japaridze, The Modal Logical Means of Investigation of Provability (in Russian), Ph.D. Thesis, Moscow State University (1986).
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.
G. Japaridze, Introduction to computability logic, Ann. Pure Appl. Logic 123 (2003), 1–99.
G. Japaridze, From truth to computability I, Theor. Comput. Sci. 357 (2006), 100–135.
J. Joosten, Interpretability Formalized, Ph.D. Thesis, University of Utrecht (2004).
S. Kleene, Introduction to Metamathematics, Van Norstrand, 1952.
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.
S. Kripke, Semantical considerations on modal logic, Acta Philos. Fenn. 16 (1963), 83–94.
N. Krupski, Some Algorithmic Questions in Formal Systems with Internalization (in Russian), Ph.D. Thesis, Moscow State University (2006).
N. Krupski, On the complexity of the reflected logic of proofs, Theor. Comput. Sci. 357 (2006), 136–142.
N. Krupski, Typing in reflective combinatory logic, Ann. Pure Appl. Logic 141 (2006), 243–256.
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.
V. Krupski, The single-conclusion proof logic and inference rules specification, Ann. Pure Appl. Log. 113 (2001), 181–206.
V. Krupski, Referential logic of proofs, Theor. Comput. Sci. 357 (2006), 143–166.
R. Kuznets, On the complexity of explicit modal logics, In: Computer Science Logic 2000, Lect. Notes Comput. Sci. 1862, Springer, 2000, pp. 371–383.
R. Kuznets, Complexity of Evidence-Based Knowledge, In: Proceedings of the Rationality and Knowledge Workshop, ESSLLI, 2006.
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.
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.
A. Kuznetsov and A. Muravitsky, On superintuitionistic logics as fragments of proof logic, Stud. Log. 45 (1986), 77–99.
K. Lehrer and T. Paxson, Knowledge: undefeated justified true belief, J. Philos. 66 (1969), 1–22.
E. Lemmon, New foundations for Lewis’s modal systems, J. Symb. Log. 22 (1957), 176–186.
W. Lenzen, Knowledge, belief and subjective probability, In: Knowledge Contributors, K. J. V. Hendricks and S. Pedersen, (Eds.), Kluwer, 2003.
D. Lewis, Elusive knowledge, Australian J. Philos. 7 (1996), 549–567.
P. Lindstrm, Provability logic — a short introduction, Theoria 62 (1996), 19–61.
M. Löb, Solution of a problem of Leon Henkin, J. Symb. Log. 20 (1955), 115–118.
D. Luchi and F. Montagna, An operational logic of proofs with positive and negative information, Stud. Log. 63 (1999), no.1, 7–25.
A. Macintyre and H. Simmons, Gödel’s diagonalization technique and related properties of theories, Colloquium Mathematicum 28 (1973).
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.
R. Magari, Representation and duality theory for diagonalizable algebras (the algebraization of theories which express Theor.:IV), Stud. Log. 34 (1975), 305–313.
J. McKinsey and A. Tarski, Some theorems about the sentential calculi of Lewis and Heyting, J. Symb. Log. 13 (1948), 1–15.
Meyer, J.-J. Ch. and W. van der Hoek, Epistemic Logic for AI and Computer Science, Cambridge Univ. Press, 1995.
R. Milnikel, Derivability in certain subsystems of the logic of proofs is П p2 -complete, Ann. Pure Appl. Logic (2006). [To appear]
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.
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.
F. Montagna, On the diagonalizable algebra of Peano arithmetic, Boll. Unione Mat. Ital. B (5) 16 (1979), 795–812.
F. Montagna, Undecidability of the first-order theory of diagonalizable algebras, Stud. Log. 39 (1980), 347–354.
F. Montagna, The predicate modal logic of provability, Notre Dame J. Formal Logic 25 (1987), 179–189.
R. Montague, Syntactical treatments of modality with corollaries on reflection principles and finite axiomatizability, Acta Philos. Fenn. 16 (1963), 153–168.
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.
J. Myhill, Some remarks on the notion of proof, J. Philos. 57 (1960), 461–471.
J. Myhill, Intensional set theory, In: Intensional Mathematics, S. Shapiro (Ed.), North-Holland, 1985, pp. 47–61.
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).
E. Nogina, Grzegorczyk logic with arithmetical proof operators (in Russian), Fundam. Prikl. Mat. 2 (1996), no. 2, 483–499.
E. Nogina, On logic of proofs and provability, Bull. Symb. Log. 12 (2006), no. 2, 356.
P. Novikov, Constructive Mathematical Logic from the Viewpoint of the Classical One (in Russian), Nauka, 1977.
Nozick, R., Philosophical Explanations, Harvard Univ. Press, 1981.
I. Orlov, The calculus of compatibility of propositions (in Russian), Mat. Sb. 35 (1928), 263–286.
E. Pacuit, A note on some explicit modal logics (2005), 5th Panhellenic Logic Symposium, Athens.
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.
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.
B. Renne, Bisimulation and public announcements in logics of explicit knowledge, In: Proceedings of the Rationality and Knowledge Workshop, 2006.
B. Renne, Semantic cut-elimination for an explicit modal logic, In: Proceedings of the ESSLLI 2006 Student Session, Malaga, 2006.
J. Rosser, Extensions of some theorems of Gödel and Church, J. Symb. Log. 1 (1936), 87–91.
N. Rubtsova, Semantics for Logic of Explicit Knowledge Corresponding to S5, In: Proceedings of the Rationality and Knowledge Workshop, ESSLLI, 2006.
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.
N. Rubtsova. and T. Yavorskaya-Sidon, Operations on proofs and labels, J. Appl. Non-Classical Logics. [To appear]
S. Shapiro, Epistemic and intuitionistic arithmetic, In: Intensional Mathematics, S. Shapiro (Ed.), North-Holland, 1985, pp. 11–46.
S. Shapiro, Intensional mathematics and constructive mathematics, In: Intensional Mathematics, S. Shapiro (Ed.), North-Holland, 1985, pp. 1–10.
V. Shavrukov, The logic of relative interpretability over Peano arithmetic, Preprint, Steklov Mathematical Institute, Moscow (1988), in Russian.
V. Shavrukov, On Rosser’s provability predicate, Z. Math. Logik Grundlagen Math. 37 (1991), 317–330.
V. Shavrukov, A smart child of Peano’s, N Notre Dame J. Formal Logic 35 (1994), 161–185.
V. Shavrukov, Isomorphisms of diagonalizable algebras, Theoria 63 (1997), 210–221.
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.
T. Smiley, The logical basis of ethics, Acta Philos. Fenn. 16 (1963), 237–246.
C. Smorynski, The incompleteness theorems, In: Handbook of Mathematical Logic, J. Barwise (Ed.), North Holland, 1977, pp. 821–865.
C. Smorynski, Self-Reference and Modal Logic, Springer, 1985.
R. Solovay, Provability interpretations of modal logic, Isr. J. Math. 25 (1976), 287–304.
V. Švejdar, Modal analysis of generalized Rosser sentences, J. Symb. Log. 48 (1983), 986–999.
G. Takeuti, Proof Theory, Elsevier, 1987.
A. Tarski, A. Mostovski, and R. Robinson, Undecidable Theories, North-Holland, 1953.
A. Troelstra and D. van Dalen, Constructivism in Mathematics, Vols 1, 2, North-Holland, 1988.
J. van Benthem, Reflections on epistemic logic, Logique Anal. Nouv. Ser. 133–134 (1993), 5–14.
J. van Benthem, Modal frame correspondence generalized, Technical Report PP-2005-08, Institute for Logic, Language, and Computation, Amsterdam (2005).
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.
A. Visser, Aspects of Diagonalization and Provability, Ph.D. Thesis, University of Utrecht (1981).
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.
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).
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.
A. Visser, Interpretability logic, In: Mathematical Logic, P. Petkov (Ed.), Plenum Press, 1990, pp. 175–208.
A. Visser, Propositional combinations of Σ1 -sentences in Heyting’s arithmetic, Logic Group Preprint Series 117, Department of Philosophy, University of Utrecht (1994).
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.
A. Visser, Rules and arithmetics, Notre Dame J. Formal Logic 40 (1999), 116–140.
A. Visser, Substitutions of Σ 01 -sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic, Ann. Pure Appl. Logic 114 (2002), 227–271.
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.
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.
T. Yavorskaya (Sidon), Logic of proofs and provability, Ann. Pure Appl. Logic 113 (2001), 345–372.
T. Yavorskaya (Sidon), Negative operations on proofs and labels, J. Log. Comput. 15 (2005), 517–537.
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.
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.
R. Yavorsky, Provability logics with quantifiers on proofs, Ann. Pure Appl. Logic 113 (2001), 373–387.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2007 Springer Science+Business Media, LLC
About this chapter
Cite this chapter
Artemov, S. (2007). On Two Models of Provability. In: Gabbay, D.M., Zakharyaschev, M., Goncharov, S.S. (eds) Mathematical Problems from Applied Logic II. International Mathematical Series, vol 5. Springer, New York, NY. https://doi.org/10.1007/978-0-387-69245-6_1
Download citation
DOI: https://doi.org/10.1007/978-0-387-69245-6_1
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-69244-9
Online ISBN: 978-0-387-69245-6
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)