# If $Q(c) \iff \Sigma \vdash \phi[c]$, is $\lnot Q(c) \iff \Sigma \not\vdash \phi[c]$?

$Q$ is a relation as described above, $\Sigma$ is consistent, and $\phi$ is a formula with one variable. I think the relation in above holds because if $c$ does not belong in $Q$, then by the relation $\Sigma$ cannot prove $\phi[c]$. Not being able to prove a sentence is not the same as proving the negation of the sentence, right?

Also, what if I have another formula $\psi(w)$ and I'm given $Q(c) \iff \Sigma \vdash \lnot \psi[c]$? Does $\lnot Q(c) \iff \Sigma \not\vdash \lnot\psi[c]$? I'm thinking it is so because I treat $\lnot \psi$ as $\phi$ and argue like before.

• Yes. If $Q(c) \iff \Sigma \vdash \phi[c]$, then obviously : not $\ Q(c) \iff \$ not $\ \Sigma \vdash \phi[c]$. Then, "internalizing" the negations, in the LHS we have $\lnot Q(c)$ while in the RHS we have to "negate" the relation $\vdash$, i.e. the "verb" of the assertion : $\phi$ is provable from $\Sigma$". – Mauro ALLEGRANZA Apr 27 '15 at 12:11
• Thank you for confirming my reasoning. Can I also ask, what if I have $Q(c) \iff \Sigma \vdash \lnot\psi[c]$? When I negate LHS, I will negate $\vdash$ on RHS but do I need to negate $\lnot\psi[c]$? (I'll be adding this into my question) – jh4 Apr 27 '15 at 12:14

## 1 Answer

You are right.

If $Q(c) \iff \Sigma \vdash \phi[c]$, then obviously :

not $\ Q(c) \iff \$ not $\Sigma \vdash \phi[c]$.

Then, "internalizing" the negations, in the LHS we have $¬Q(c)$ while in the RHS we have to "negate" the relation $\vdash$.

The same for the second example.

We have an equivalence between two statements : one is the LHS, i.e. the formula $¬Q(c)$, the other one is the "meta-statement" :

"$¬ \psi[c]$ is provable from $\Sigma$".

When we negate a statement we add the negation to the "verb" : in the example, the negation of $\vdash \phi$ ("$\phi$ is provable") is $\nvdash \phi$ ("$\phi$ is not provable") and not : $\vdash \lnot \phi$ ("$\lnot \phi$ is provable").

The denial of "I will eat the cake" is "I will not eat the cake" (and not : "I will eat the not-cake" ...)