  For recent proof-theoretic investigations of provability logic based on different cut-free sequent calculi see (Negri 2005, 2014; Poggiolesi 2009). Negri presents two equivalent labelled sequent calculi for GL and a syntactic proof of cut elimination. Even if a full subformula property does not hold for these calculi because of the labelling, the usual consequences of the subformula property can be established: The labelled formalism allows a direct completeness proof, which can be used to establish decidability as well as the finite model property, which means that any formula that is not provable has a finite counter-model. 