The analytical completeness of Dzhaparidze's polymodal logics (Q685073)

The bimodal propositional system GLP introduced by G. Dzhaparidze in 1985 has \(\square (A\to B)\to (\square A\to \square B)\), \(\boxdot (A\to B)\to (\boxdot A\to \boxdot B)\), \(\square(\square A\to A)\to \square A\), \(\boxdot(\boxdot A\to A)\to \boxdot A\), \(\square A\to \boxdot A\), \(\neg\square A\to \boxdot\neg\square A\), and all classical tautologies as its axioms. Inference rules are modus ponens and \(\square\)-necessitation \(A/\square A\). Dzhaparidze proved arithmetical completeness of GLP with respect to reading \(\square\) and \(\boxdot\) as `is provable' and `has an \(\omega\)-inconsistent negation'. The author proves completeness of GLP with respect to reading \(\square\) and \(\boxdot\) as `is provable in second-order arithmetic' and `is provable in second-order arithmetic with \(\omega\)-rule'.