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

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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/0168-0072(94)90071-x
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 51,480
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Systems of Logic Based on Ordinals.Alan Mathison Turing - 1939 - London: Printed by C.F. Hodgson & Son.
Transfinite Recursive Progressions of Axiomatic Theories.Solomon Feferman - 1962 - Journal of Symbolic Logic 27 (3):259-316.
Arithmetization of Metamathematics in a General Setting.S. Feferman - 1966 - Journal of Symbolic Logic 31 (2):269-270.
The Formalization of Interpretability.Albert Visser - 1991 - Studia Logica 50 (1):81 - 105.

View all 10 references / Add more references

Citations of this work BETA

Iterated Local Reflection Versus Iterated Consistency.Lev Beklemishev - 1995 - Annals of Pure and Applied Logic 75 (1-2):25-48.
Undecidability in Diagonalizable Algebras.V. Yu Shavrukov - 1997 - Journal of Symbolic Logic 62 (1):79-116.
Bimodal Logics for Extensions of Arithmetical Theories.Lev D. Beklemishev - 1996 - Journal of Symbolic Logic 61 (1):91-124.

View all 6 citations / Add more citations

Similar books and articles

Bimodal Logics for Extensions of Arithmetical Theories.Lev D. Beklemishev - 1996 - Journal of Symbolic Logic 61 (1):91-124.
On Sequent Systems for Bimodal Provability Logics MOS and Prl1.Katsumi Sasaki - 2002 - Bulletin of the Section of Logic 31 (2):91-101.


Added to PP index

Total views
15 ( #615,743 of 2,330,852 )

Recent downloads (6 months)
1 ( #587,623 of 2,330,852 )

How can I increase my downloads?


My notes