 Gödel famously named the latter formula \(\sc{BEW}(x)\) (for beweisbar) as it can be understood to express that there exists a proof from the axioms of \(\mathsf{P}\) of the formula with Gödel number \(y\). But unlike the other formulas representing primitive recursive relations which figure in its definition, \(\textrm{Prov}_{\mathsf{P}}(x)\) contains an unbounded existential quantifier. And thus as Gödel is careful to observe, there is no reason to expect that it defines a primitive recursive relation.