  Vardanyan's Theorem states that quantified provability logic is
$\Pi^0_2$-complete, and in particular impossible to recursively axiomatize for
consistent theories containing a minimum of arithmetic. However, the proof of
this fact cannot be performed in a strictly positive signature. The logic
QRC$_1$ was previously introduced as a candidate first-order provability logic.
Here we show that QRC$_1$ is indeed complete with respect to arithmetical
semantics. This is achieved via a Solovay-type construction applied to constant
domain Kripke models. As a corollary we conclude that QRC$_1$ is also the
quantified provability logic of HA.
