On bimodal logics of provability (Q1332858): Difference between revisions

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.