On bimodal logics of provability

Annals of Pure and Applied Logic 68 (2):115-159 (1994)
  Copy   BIBTEX

Abstract

We investigate the bimodal logics sound and complete under the interpretation of modal operators as the provability predicates in certain natural pairs of arithmetical theories . Carlson characterized the provability logic for essentially reflexive extensions of theories, i.e. for pairs similar to . Here we study pairs of theories such that the gap between and is not so wide. In view of some general results concerning the problem of classification of the bimodal provability logics we are particularly interested in such pairs that is axiomatized over by ∏1-sentences only, and, for each n 1, proves the n-times iterated consistency of . A complete axiomatization, along with the appropriate Kripke semantics and decision procedures, is found for the two principal cases: finitely axiomatizable extensions of this sort, like e.g. ), ), etc., and reflexive extensions, like ¦n 1\s}), etc. We show that the first logic, ICP, is the minimal and the second one, RP, is the maximal within the class of the provability logics for such pairs of theories. We also show that there are some provability logics lying strictly between these two. As an application of the results of this paper, in the last section the polymodal provability logics for natural recursive progressions of theories based on iteration of consistency are characterized. We construct a system of ordinal notation , which gives exactly one notation to each constructive ordinal, such that the logic corresponding to any progression along coincides with that along natural Kalmar elementary well-orderings

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 103,388

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Bimodal logics for extensions of arithmetical theories.Lev D. Beklemishev - 1996 - Journal of Symbolic Logic 61 (1):91-124.
A course on bimodal provability logic.Albert Visser - 1995 - Annals of Pure and Applied Logic 73 (1):109-142.
The polytopologies of transfinite provability logic.David Fernández-Duque - 2014 - Archive for Mathematical Logic 53 (3-4):385-431.
Provability logics with quantifiers on proofs.Rostislav E. Yavorsky - 2001 - Annals of Pure and Applied Logic 113 (1-3):373-387.
The analytical completeness of Dzhaparidze's polymodal logics.George Boolos - 1993 - Annals of Pure and Applied Logic 61 (1-2):95-111.
Rosser Provability and Normal Modal Logics.Taishi Kurahashi - 2020 - Studia Logica 108 (3):597-617.
Münchhausen provability.Joost J. Joosten - 2021 - Journal of Symbolic Logic 86 (3):1006-1034.

Analytics

Added to PP
2014-01-16

Downloads
51 (#447,550)

6 months
5 (#702,808)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Iterated local reflection versus iterated consistency.Lev Beklemishev - 1995 - Annals of Pure and Applied Logic 75 (1-2):25-48.
Bimodal logics for extensions of arithmetical theories.Lev D. Beklemishev - 1996 - Journal of Symbolic Logic 61 (1):91-124.
Undecidability in diagonalizable algebras.V. Shavrukov - 1997 - Journal of Symbolic Logic 62 (1):79-116.

View all 8 citations / Add more citations