 In Theorem V of his paper, Gödel proves that any number theoretic predicate which is primitive recursive is numeralwise expressible in P. Thus since Prf(x, y) and substitution are primitive recursive, these are decided by P when closed terms are substituted for the free variables x and y. This is the heart of the matter as we will see. Another key point about numeralwise expressibility is that although we informally interpret, for example, Prov(Sb(ru1…unZ(x1)…Z(xn))), by: ‘the formula with Gödel number r is provable if the Gödel number for the xi th numeral is substituted in place of the i th variable,’ neither the formal statement within the theory P nor anything we prove about it appeals to such meanings. On the contrary Prov(Sb(ru1…unZ(x1)…Z(xn))), is a meaningless string of logical and arithmetical symbols. As Gödel puts it in his introduction to his theorem V, ‘The fact that can be formulated vaguely by saying that every recursive relation is definable in the system P (if the usual meaning is given to the formulas of this system) is expressed in precise language, without reference to any interpretation of the formulas of P, by the following Theorem (V) (Gödel 1986, p. 171, italics Gödel’s).