# Gödel's theorems and nonstandard model of $PA$

According to the Second incompleteness theorem $Con(PA)$ is independent of $PA$. So if $PA$ is consistent $PA + \neg Con(PA)$ is also consistent which means that there exist a number $t$ which codes a proof of $1=0$. But $t$ isn't a "regular" natural number because $PA + \neg Con(PA)$ is a nonstandard model of $PA$.

My question is, how do we know that the Gödel's sentence of $PA + \neg Con(PA)$ exists (its code is a "regular" natural number)?

• We don't know if $Con(PA)$ is independent of $PA$. Second incompleteness theorem only guarantees that $Con(PA)$ is not provable from $PA$ ($\neg Con(PA)$ might still be provable), which isn't quite what "independent" means. – Wojowu Oct 30 '15 at 16:38
• Because one has been explicitly constructed, or at least a precise recipe for constructing it has been given. {Except that the word "it" hides some complications.) – André Nicolas Oct 30 '15 at 16:39
• (Sorry, the downvote was mine - I misclicked.) – Noah Schweber Oct 30 '15 at 16:40
• @Wojowu How could PA prove $\neg$ Con(PA)? In the standard model, Con(PA) is true so PA cannot prove its negation. Sorry if I misunderstood your remark. – hot_queen Oct 30 '15 at 20:07
• @hot_queen It might be the case that only nonstandard models of arithmetic exist. – Wojowu Oct 30 '15 at 20:09

First, "$PA+\neg Con(PA)$ is a nonstandard model of $PA$" is false. "$PA+\neg Con(PA)$" is a set of sentences. It can be true, or false, in nonstandard models, but it is not a model itself.
As to how we know the sentence "$\neg Con(PA)$" (which is the only weird sentence in $PA+\neg Con(PA)$) exists: we can actually explicitly write it down! Godel's original paper gives a recipe for how to do this. Actually carrying the recipe out all the way is lengthy, but has been done - see e.g. What does a Godel sentence actually look like?. And there are much more efficient ways to do it, too.
This holds in particular for $\mathrm{PA}+\neg\mathit{Con}(\mathrm{PA})$.