It is known that if Peano arithmetic (PA) is consistent then $PA+\neg Con(PA)$ is also consistent. One way we can express $Con(PA)$ is $\forall x(\neg P(x))$ where $P(x)$ expresses that $x$ encodes a proof of $0=1$. We prove PA is consistent by proving there is one contradiction we can't prove, namely, $0=1 \land 0\neq 1$. If PA were inconsistent we could prove any contradiction.
I want to use a different contradiction. Let $Q(x)$ express that $x$ encodes a proof of $\exists x(S(x)=0)$. Given a proof of $\exists x(S(x)=0)$, I can easily derive the contradiction $\exists x(S(x)=0) \land \forall x(S(x) \neq 0)$ in the language of PA. Let $M$ be a model of $PA + \exists x(Q(x))$.
Is $\exists x(S(x)=0)$ actually true in $M$ in the sense there is an $x \in M$ whose successor is $0$? Or is the nonstandard length proof of $\exists x(S(x)=0)$ simply wrong?
I think Willemien brings up a valid concern. This concern is why I asked this question. Assume I state $\exists x(Q(x))$ the way Asaf suggests. $Q(x)$ would be an extremely complex arithmetic formula that assumes $x$ encodes a finite (in the model) sequence of finite sentences. $Q(x)$ will have a finite number of huge constants that encode theorems of the theory, etc. $Q(x)=1$ if $x$ encodes a proof of $\exists x(S(x)=0)$ otherwise $Q(x)=0$.
What if this $x$ is a standard natural number? This would mean our "model" has a finite (in the standard model) length proof of inconsistency and is actually inconsistent. The only way $PA+\exists x(Q(x))$ can have a model is if we assume $x$ is non-standard. There is no way to state this assumption in the language of PA. What if $x$ is not the shortest proof of a contradiction? Again, the axiom does not require $x$ to be the shortest proof of $\neg Con(PA)$.
I want to accept Carl Mummert's answer but I am still confused as to why $M \vDash \text{Bew}(\# \phi)$ is different from $M \vDash \phi$. It seems irrelevent that $\# \phi$ encodes the sentence $\phi$. If $\phi$ is a proof of $\exists x(S(x)=0)$, how is it different from any other proof? Is $\phi$ simply too long to be considered a valid proof?
Best Answer
Say that $\text{Bew}(x)$ means "$x$ codes a formula, and that formula is provable in PA".
Let $\phi$ be a formula and $M$ be a model of PA. There is a very significant difference between $$M \vDash \text{Bew}(\phi)$$ and $$M \vDash \phi.$$
It is a common, false intuition to think $\text{Bew}(\phi)$ implies $\phi$. The scheme that includes all statements of the form $\text{Bew}(\phi) \to \phi$ is known as a reflection scheme. Relatively few instances of that scheme are provable in PA.
In fact, by Löb's theorem, the only way for $\text{Bew}(\phi) \to \phi$ to be provable in PA is for $\phi$ itself to be provable in PA.
Moreover, say $M$ is a model of $\lnot \text{Con}(\text{PA})$ (that is, a model of $\text{Bew}(0=1)$). Because PA proves $0=1 \to \phi$ for every $\phi$, this model $M$ will satisfy $\text{Bew}(\phi)$ for every $\phi$. But $M$ cannot satisfy every formula! So $M$ already shows you that the entire reflection scheme cannot be provable in PA.
In particular, this $M$ will satisfy $\text{Bew}((\exists x)[x+1=0])$ but (since it is a model of PA) it will not satisfy $(\exists x)[x+1=0]$.
It is true, of course, that if $\phi$ is provable from PA then $\phi$ is true in every model of PA. But $\text{Bew}(\phi)$ is only an imitation of the real "provable" predicate.
Soundness
We say that a logic is sound if, when the logic proves a formula, the formula is true in every model. There is another sense of soundness for theories of arithmetic. A theory of arithmetic is sound for a given class of formulas if, whenever the theory proves a formula in that class, the formula is true (true in the standard model of arithmetic).
$\lnot \text{Con}(\text{PA})$ is a formula in the syntactic class $\Sigma^0_1$. Any theory that proves this is, therefore, not sound for $\Sigma^0_1$ formulas. This notion of soundness, and a few others, are discussed in the Wikipedia article on ω-consistent theories.