Sentence S (similar to a Godel sentence) where S iff the negation of S is provable?

Question

The diagonal lemma can be used to generate the Godel sentence, where G is true iff G is not provable in theory T. Can we use the lemma to construct a sentence (call it S) where S is true iff the negation of S is indeed provable in some theory T?

Answer 1

Yes, but in fact we don't need to invoke the diagonal lemma again - just take $S$ to be the negation of $G$. Then - reasoning in $T$ - we have:

• If $S$ is true, then $G$ is false, which by hypothesis on $G$ means that $T$ proves $G$, which is to say $T$ proves $\neg S$.

• If $T$ proves $\neg S$, then $T$ proves $G$, in which case $G$ is false and hence $S$ is true.

That is, $T$ proves "$S$ iff $T$ proves $\neg S$."

(Note that that's a little stronger than what you've asked for - we don't just have that $S$ is true iff $T$ proves $\neg S$, but rather that that equivalence itself is provable in $T$. This type of stronger result is no harder to prove - we just observe that the obvious reasoning goes through in $T$ - and is often something we care about down the road.)

---

EDIT: That said, if you want to use the diagonal lemma, here's how:

DL says that for any formula $\varphi$ there is some sentence $\theta$ such that $$T\vdash\theta\leftrightarrow\varphi(\underline{\ulcorner\theta\urcorner})$$ where $T$ is an "appropriate" theory, $\vdash$ is the (metatheoretic) provability relation, $\ulcorner\cdot\urcorner$ is an "appropriate" Godel numbering system, and $\underline{k}$ is the numeral correpsonding to $k$.

At this point there's an important caveat to make: $\theta$ and $\varphi(\underline{\ulcorner\theta\urcorner})$ need not be (and probably will not be) literally the same sentence, they're just $T$-provably equivalent. That said, see here.

In our case, $\varphi(x)$ should intuitively be the formula "$x$ is disprovable;" the DL then directly says that there is some sentence asserting its own disprovability, that is, some $\theta$ with the property that $T$ proves "$\theta$ is true iff $\neg\theta$ is $T$-provable."

A bit more precisely, we'll use the formula $$\Phi(x):\quad\forall y(Neg(x,y)\implies Prov_T(y)),$$ where

• $Prov_T$ is the already-set-up formula expressing provability (in some texts you might see this denoted "$Bew$" - that was the original notation), and

• $Neg(\cdot,\cdot)$ is some formula representing negation; that is, some formula with the property that for all $a,b\in\mathbb{N}$ we have $T\vdash Neg(\underline{a},\underline{b})$ iff there is some sentence $\psi$ such that $a$ is the Godel number of $\psi$ and $b$ is the Godel number of $\neg\psi$.

You can (somewhat sloppily) read $\Phi(x)$ as saying "Everything which is the negation of $x$ is $T$-provable." We could also have gone with $\exists y(Neg (x,y)\wedge Prov_T(y))$ ("There is something which is the negation of $x$ and which is $T$-provable"); the fact that we're dealing with a unique object (for each $m$ there is exactly one $n$ such that $T\vdash Neg(\underline{m},\underline{n})$) gives us some freedom here.