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.
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".
For instance, each theory Tn can be understood as T augmented with all true Πn sentences as additional axioms.
[4] Among the most notable applications of GLP has been its use in proof-theoretically analyzing Peano arithmetic, elaborating a canonical way for recovering ordinal notation up to ɛ0 from the corresponding algebra, and constructing simple combinatorial independent statements (Beklemishev [9]).