Eliminating cuts from non-nested reflection calculi

This paper introduces three cut-free sequent calculi for RC₁, the strictly positive fragment of Gödel-Löb's provability logic. We establish cut admissibility for all three systems—G1RC1, G1K4⁺, and G1K4⁺—which differ in their treatment of modal rules for necessitation and diamond transitivity. The calculi operate on single formulas rather than multisets, answering an open question about non-nested proof systems for reflection calculi. We demonstrate that our systems are equivalent to standard RC₁, yielding syntactic proofs of known results on conservativity and computational complexity, whilst also establishing new findings on uniform interpolation. We sketch a generalisation to RCΛ, which proves sound but incomplete.