0
$\begingroup$

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?

Improve this question
$\endgroup$
1
  • 5
    $\begingroup$ I'm going to guess that your difficulty is merely a matter of misplaced parentheses. Diagonalization applied to NProv gives us a sentence $\psi$ such that $T\vdash(\psi\leftrightarrow\text{NProv}(\ulcorner\psi\urcorner))$. We do not have $(T\vdash\psi)\leftrightarrow(\text{NProv}(\ulcorner\psi\urcorner))$. $\endgroup$
    – Andreas Blass
    Jun 19, 2019 at 23:03

1 Answer 1

Reset to default
2
$\begingroup$

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$.

Improve this answer
$\endgroup$
2
  • $\begingroup$ When you say "which is unprovable in $T$"", does "which" refer to $\psi$, or does it refer to $\psi \leftrightarrow \lnot\mathrm{Prov}(\overline{\ulcorner \psi \urcorner})$? $\endgroup$
    – Andrej Bauer
    Jun 20, 2019 at 5:53
  • $\begingroup$ $\psi$, although on re-reading I see that the sentence was less clearly phrased than it could have been. $\endgroup$
    – Benedict Eastaugh
    Jun 20, 2019 at 14:32

Your Answer

By clicking β€œPost Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.