 As to the proof theory of provability logic, Valentini (1983) proved that a standard sequent calculus formulation of GL obeys cut elimination, which means, roughly formulated, that each formula provable from GL in the sequent calculus also has a GL sequent proof “without detours” (see the entry  the development of proof theory for a precise explanation of cut elimination). In recent years, there has been renewed interest in the proof theory of GL, see for example Goré and Ramanayake (2008). Cut-elimination leads to the desirable subformula property for GL, because all formulas that appear in a cut-free proof are subformulas of the endsequent formulas. 