Can the "real" Peano Arithmetic be inconsistent? Assuming $\text{PA}$ is consistent. Then $\text{PA} + \neg\text{Con}(\text{PA})$ is consistent and have a model, say $M$. We know $M$ must be nonstandard, in which case, there is a nonstandard proof of $0=1$ from ($M$'s version of) $\text{PA}$ in $M$. The fact that $M$'s version of $\text{PA}$ is different from the "real" $\text{PA}$ make the assertion
$$
M\vDash\text{PA} + \neg\text{Con}(\text{PA})
$$
kind of less stunning than we might expect it to be.
My question is if we can compose some other expressions of $\text{PA}$ so that if $M\vDash\neg\text{Con}(\text{PA})$ then there is a (nonstandard) proof of absurdity making use of only the standard part of $\text{PA}$ and logic axioms. If it is impossible, how to prove it?
 A: It seems that the Feferman-style description of PA will exhibit your requirements. 
Specifically, consider the theory $P$ defined as follows. Begin to enumerate the usual PA axioms, but include the next axiom in $P$ only if doing so keeps $P$ consistent. Never add an axiom to $P$ that would make it inconsistent. 
Since PA proves of every finite subset of PA that it is consistent, it follows that PA proves of any particular axiom of PA, that it is in $P$. In this sense, this theory $P$ is the same as PA, just described in a different way. 
But because of how it is described, it follows that PA proves $\text{Con}(P)$. We never include an axiom in $P$ that would enable it to prove a contradiction. 
Therefore, there is no model $M\models PA+\neg\text{Con}(P)$, and so the theory vacuously has your desired property.
Of course, notice that all instances of your requested property must be vacuous like this, because if the proof of a contradiction inside $M$ were somehow forced to be standard, then it would be actual proof of a contradiction, and so $M$ couldn't exist in the first place, if it is a model of this theory. So it seems to me that the only way to get your situation is in the vacuous way that the Feferman theory achieves it.
