**Edit** After Andreas Blass answer below and comments below the original post I have changed it to accommodate posters' remarks. I hope it is clear and makes more sense now.


Let $\mathrm{PA}$ be the first-order Peano Arithmetic with full induction schema. Let $\mathrm{Con(PA)}$ be the standard $\Pi\_1$ consistency statement for $\mathrm{PA}$. By the 2nd Incompleteness Theorem we know that $\mathrm{PA}\nvdash \mathrm{Con(PA)}$, if only $\mathrm{PA}$ is consistent. Therefore (assuming consistency of $\mathrm{PA}$) the theory $\mathrm{PA^+}=\mathrm{PA}+\neg\mathrm{Con(PA)}$ is consistent and has a model. This theory is $\omega$-inconsistent, since we know that no natural number codes a proof of, say, '$0=1$', therefore for every number $n$ we have that $\mathrm{PA}\vdash\neg\mathrm{Proof}(\overline{\ulcorner0=1\urcorner},\overline{n})$, where $\mathrm{Proof}(x,y)$ represents in $\mathrm{PA}$ recursive relation: $y$ *codes a proof of a formula whose number is* $x$; yet $\mathrm{PA^+}\vdash\exists y\,\mathrm{Proof}(\overline{\ulcorner0=1\urcorner},y)$. Thus in a model $\mathfrak{M}$ of $\mathrm{PA^+}$ there is a non-standard number which codes a proof of '$0=1$'.


I have the following questions:


* How can I interpret *$y$ is coding a proof of `$0=1$'* in this situation?


My questions is motivated by the following. $\mathrm{Proof}(x,y)$ represents derivability relation for Peano Arithmetic; in case $\mathrm{PA}$ is consistent there cannot be a PA-proof of `$0=1$'. So can I choose an arbitrary non-standard number $q$ to serve as interpreting the variable $y$ in $\mathrm{Proof}(\overline{\ulcorner0=1\urcorner},y)$ and satisfying the formula in question? Or is this interpretation determined in some other way?



An interpretation of not-Con(PA)
The witness coding a proof of 0=1 in a nonstandard model is likely to be very specific; depending on your encoding, most nonstandard numbers may not code proofs at all. And even if all numbers encode proofs, many nonstandard numbers will encode proofs of true formulas, or of other false formulas.


The encoding of proofs that you've chosen reduces proofs to some combinatorial structure, and that structure is still around in the nonstandard model. For instance, say you've decided that $q$ encodes a proof if $q$ has the form
$$2^{q\_1}3^{q\_2}5^{q\_3}\cdots p\_n^{q\_n}$$
where each $q\_i$ encodes a formula and $q\_{i}$ is derived from $\{q\_j\}\_{j<i}$ by some finite list of operations. If this is the encoding, a nonstandard $q$ only encodes a proof if it is of this form, but with $n$ a nonstandard number.


In this case $q$ actually describes a list of steps where each step follows from the ones above it; the problem is that this list isn't well-founded, so it doesn't correspond to a genuine proof. But you can still ask questions like "what is the 7th step" (and also, what is the $a$-th step for $a$ a nonstandard integer $\leq n$), and the 8th step really does follow from steps $1,\ldots,7$.


