 which without being primitive recursive, is however obtained from Prf(x, y) by existentially quantifying x. (Prov(y) satisfies only the ‘positive’ part of numeralwise expressibility, and not the negative part; but the negative part is not needed.)