Example of PA model in which Prov(1=0) and 1 != 0?

Question

$PA$ cannot prove $Prov(\phi) \to \phi$; and in particular $PA$ cannot prove "$Prov( 0 = 1 ) \to 0 = 1$".

This can be viewed as a simple consequence of Lob's theorem; but we can also interpret it as "there are (non-standard) models of $PA$ in which both $Prov(0 = 1)$ and $0 \neq 1$ are true".

Is there an intuitive way to build an example of such non-standard model of $PA$ in which $Prov( 0 = 1 )$ and $0 \neq 1$ ?

Is $\neg Con(PA)$ mandatory in such non standard model?

Answer 1

Briefly:

• "$0\not=1$" holds in every model of PA. This is because, well, PA proves "$0\not=1$." There's no way to get around this: even if PA were to also prove "$0=1$," all that would tell us is that PA has no models at all (because in every model we would have to have both $0\not=1$ and $0=1$).

• Yes, "$Prov(0=1)$" and "$\neg Con($PA$)$" are equivalent, provably in PA (and indeed much less). Indeed, $Con($PA$)$ is often an abbreviation for "$\neg Prov(0=1)$," which makes the equivalence trivial.

• No concrete nonstandard models of PA are really known at all. In particular, Tennenbaum's theorem prevents us from having too snappy a description of such a model. That said, the proof of the completeness theorem is rather intuitive after a while: we pass to a complete theory $T$ in a larger language which contains PA and has the "witness property" - if it proves "$\exists x\varphi(x)$," then it proves "$\varphi(t)$" for some term $t$ (generating these extra terms is why we need to expand the language) - and then the set of terms in this larger language, modulo $T$-provable equivalence, forms a model of $T$ (and hence has a reduct which is a model of PA). The reason this doesn't describe a single construction is that we have lots of freedom in building $T$, but if you blackbox that step the construction of the term model of $T$ is (in my opinion) very intuitive.

Incidentally, by the MRDP theorem we can think of a model of PA satisfying "$Prov(0=1)$" as simply a model of PA where a certain polynomial has a root which didn't before.

You may also find this question interesting.

Answer 2

Hint: Using the axioms at First-order theory of arithmetic. If we start with Peano's Axioms for $(N,S,0)$ with $1$ not yet defined (as at link), then from FOL we have $0=0$ and $\exists x: x=0$.