Japaridze's polymodal logic
Japaridze's polymodal logic (GLP), is a system of provability logic with infinitely many modal (provability) operators. This system has played an important role in some applications of provability algebras in proof theory, and has been extensively studied since the late 1980s. It is named after Giorgi Japaridze.
The language of GLP extends that of the language of classical propositional logic by including the infinite series [0],[1],[2],... of “necessity” operators. Their dual “possibility” operators <0>,<1>,<2>,... are defined by <n>p = ¬[n]¬p.
The axioms of GLP are all classical tautologies and all formulas of one of the following forms:
And the rules of inference are:
Consider a “sufficiently strong” first-order theory T such as Peano Arithmetic PA. Define the series T0,T1,T2,... of theories as follows:
For each n, let Prn(x) be a natural arithmetization of the predicate “x is the Gödel number of a sentence provable in Tn.
A realization is a function * which sends each nonlogical atom a of the language of GLP to a sentence a * of the language of T. It extends to all formulas of the language of GLP by stipulating that * commutes with the Boolean connectives, and that ([n]F) * is Pr_n(‘F *’), where ‘F *’ stands for the (numeral for) the Gödel number of F *.
An arithmetical completeness theorem for GLP states that a formula F is provable in GLP if and only if, for every interpretation *, the sentence F * is provable in T.
The above understanding of the series T0,T1,T2,... of theories is not the only natural understanding yielding the soundness and completeness of GLP. For instance, each theory Tn can be understood as T augmented with all true ∏1 sentences as additional axioms. George Boolos showed that GLP remains sound and complete with analysis (second-order arithmetic) in the role of the base theory T.
GLP has been shown to be incomplete with respect to any class of Kripke frames.
A natural topological semantics of GLP interprets modalities as derivative operators of a polytopological space. Such spaces are called GLP-spaces whenever they satisfy all the axioms of GLP. GLP is complete w.r.t. the class of all GLP-spaces.
...
Wikipedia