I have a basic question about the use of judgment-level negation $\nvdash$. Though I meet it in some of my courses on proof theory, I usually treat it as a metalevel expression and I don't know how to handle it if it appears in the object language. The concrete question that I meet is as follows:
Here are two “statements”:
- (a) $\Gamma\nvdash\neg\exists xA(x)$.
- (b) for some $x$, $\Gamma\nvdash\neg A(x)$.
Assuming that we are working with classical logic, are (a) and (b) logically equivalent? Thanks in advance!
I assume that $x$ does not occur free in $\Gamma$.
Yes, it is equivalent to say
Both of them mean that there is a model of $\Gamma$ and $\exists x A(x)$. Roughly, it means that it is possible to make $\Gamma$ and $\exists x A(x)$ true simultaneously.
Indeed, $\Gamma \not\vdash \lnot \exists x A(x)$ means that $\lnot \exists x A(x)$ is not provable from the hypothesis $\Gamma$, which amounts to say that there is a model of $\Gamma$ and $\exists x A(x)$.
Under the assumption that $x$ is not free in $\Gamma$, $\Gamma \vdash \lnot A(x)$ means that $\lnot A(x)$ is provable from the hypothesis $\Gamma$, for any $x$. It amounts to say that $\Gamma \vdash \forall x \lnot A(x)$.
Therefore, saying that $\Gamma \not\vdash \lnot A(x)$ for some $x$ (i.e. negating that $\Gamma \vdash \lnot A(x)$ for any $x$) means that $\Gamma \not\vdash \forall x \lnot A(x)$, which amounts to say that there is a model of $\Gamma$ and $\lnot \forall x \lnot A(x)$, i.e. there is a model of $\Gamma$ and $\exists x A(x)$.