Does the fixed point lemma / diagonalization require capturing or not?

Question

Peter Smith's formulation of the diagonalization lemma is essentially as follows, from Theorem 47 of his (fantastic) online book:

If theory T extends Robinson Arithmetic, and P is an one-place open sentence of T's language (i.e., a well-formed formula in T), then there is a sentence 𝝍 s.t.:

T ⊢ 𝝍 ↔ P(⌜𝝍⌝)

Where the quine corner brackets represent the function that converts a well-formed sentence into a Gödel numeral. He then defines Prf(x,y) as the T-sentence which is true when x is the Gödel number of a well-formed T-proof which proves the well-formed T-formula which y is the Gödel number of. And as he says on page 83, a well-formed formula in T corresponding to Prf(x,y) does in fact exist.

Then he defines Prov(y) as the provability predicate for T:

Prov(y) ≡ ∃x Prf(x,y).

But then here's where I'm confused: If Prf(x,y) is a well-formed formula, then ∃x Prf(x,y) should be one as well. And so should its negation: ¬∃x Prf(x,y). And if ¬∃x Prf(x,y) is a well-formed formula, then why wouldn't the diagonalization lemma apply to it?

Let's use NProv(y) as shorthand for ¬∃x Prf(x,y). If the diagonalization lemma applies to NProv, then we get:

T ⊢ 𝝍 ↔ NProv(⌜𝝍⌝)

And this trivially leads to inconsistency: We can show that if T ⊢ 𝝍 then T ⊢ ⊥, and likewise if T ⊢ ¬𝝍 then T ⊢ ⊥.

It seems to me that the fix is to edit Smith's Theorem 47 so that it says:

If theory T extends Robinson Arithmetic, and the numerical property P is captured by a one-place open sentence of T's language (i.e., a well-formed formula in T), then there is a sentence 𝝍 s.t.:

T ⊢ 𝝍 ↔ P(⌜𝝍⌝)

Because then although T can express NProv by the wff ¬∃x Prf(x,y), it cannot capture it (meaning that (1) if 𝝍 is true then T ⊢ NProv(⌜𝝍⌝), and (2) if 𝝍 is false then T ⊢ ¬NProv(⌜𝝍⌝)), and thus diagonalization wouldn't apply.

But I see this mistake elsewhere as well. So what's the deal? Can the fixed point lemma / diagonalization lemma be applied to any well-formed formula? And if so, why isn't NProv a well-formed formula? Or does the numerical property diagonalization is applied to need to be capturable in T? And if so, why doesn't Peter Smith's version state this?

Answer 1

this trivially leads to inconsistency: We can show that if T ⊢ 𝝍 then T ⊢ ⊥, and likewise if T ⊢ ¬𝝍 then T ⊢ ⊥.

In the case of $\neg\mathrm{Prov}(n)$, applying the diagonal lemma gives one (where $T$ extends Robinson's Q) a sentence $\psi$ such that $T \vdash \psi \leftrightarrow \neg\mathrm{Prov}(\overline{\ulcorner \psi \urcorner})$. This sentence $\psi$ is unprovable in $T$, as its negation $\neg\psi$. In other words, $\psi$ is a Gödel sentence. Indeed, your argument is the standard way of showing (under the assumption that $T$ is consistent) that $T$ does not prove $\psi$.