**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?