On bimodal logics of provability (Q1332858)

The author investigates the bimodal logics sound and complete under the interpretation of modal operators as the provability predicates in certain natural pairs of arithmetical theories \(({\mathcal T},{\mathcal U})\). He studies those pairs of theories \(({\mathcal T},{\mathcal U})\) for which \({\mathcal U}\) is axiomatized over \({\mathcal T}\) by \(\Pi_ 1\)-sentences only, and for each \(n\geq 1\), \({\mathcal U}\) proves the \(n\)-times iterated consistency of \({\mathcal T}\). 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 and reflexive extensions of this sort.