  In this paper, we introduce a proof system $\mathsf{NQGL}$ for a Kripke
complete predicate extension of the logic $\mathbf{GL}$, that is, the logic of
provability, which is defned by $\mathbf{K}$ and the L\"{o}b formula $\Box(\Box
p\supset p)\supset\Box p$. $\mathsf{NQGL}$ is a modal extension of Gentzen's
sequent calculus $\mathsf{LK}$. Although the propositional fragment of
$\mathsf{NQGL}$ axiomatizes $\mathbf{GL}$, it does not have the L\"{o}b formula
as its axiom. Instead, it has a non-compact rule, that is, a derivation rule
with countably many premises. We show that $\mathsf{NQGL}$ enjoys cut
admissibility and is complete with respect to the class of Kripke frames such
that for each world, the supremum of the length of the paths from the world is
finite.
