Interpreting $\textbf{PA} + \neg\text{Con}(\textbf{PA})$ in $\textbf{PA}$ How does one interpret $\textbf{PA} + \neg\text{Con}(\textbf{PA})$ in $\textbf{PA}$, and what is the significance of such an aberrant interpretation?
I'm interested in the following: $\textbf{ZF} - \textbf{Inf}$ can be interpreted in $\textbf{PA}$, so I thought that any $\textbf{ZF}$-theorem in the language of $\textbf{PA}$ (under the translation) that is independent of $\textbf{PA}$ (such as Goodstein's) must necessarily involve some application of an infinite totality, that is $\textbf{Inf}$ must be used. Since otherwise it would be provable in $\textbf{ZF} - \textbf{Inf}$, and hence there would be a $\textbf{PA}$-proof of a sentence which "says" the same as Goodstein's sentence, at least in the sense that the original formulation is $\textbf{PA}$-equivalent to the there-and-back translated version. This is at least what my intuition tells me when I consider the Ackermann interpretation.
But I'm not completely sure what "says" really is here. My teacher said that interpretations do not have to preserve meaning and gave $\textbf{PA} + \neg\text{Con}(\textbf{PA})$ in $\textbf{PA}$ as an example. He also said that "[my] reasoning assumes that any proof going beyond $\textbf{ZF} - \textbf{Inf}$ would involve infinity, but that's not obvious (for instance, there might be statements $\textbf{ZF} - \textbf{Inf}$ can't prove not because they involve Infinity but because involve instances of Separation that are not first-order definable)"
I'm unsure about the meaning of both his points.
 A: This is not exactly an answer to your question, since it's more about the particular result that $\mathsf{PA} + \neg\mathsf{Con}(\mathsf{PA})$ is interpretable in $\mathsf{PA}$. Still, I hope it is of some help.
This result was proved by Feferman in his important paper "Arithmetization of Metamathematics in a General Setting" (it's theorem 6.5 in the paper). The notation in the paper is a bit heavy and old-fashioned, though, so it may take some time to get used to it. I'm not going to prove his result here, since the proof is rather laborious, but I do want to make some quick remarks about it.
(1) The first thing to note is that the result relies on the following fundamental point made in Feferman's paper, namely that some care must be taken when handling consistency statements (for an introductory treatment of the same point, cf. chapter 36 of Peter Smith's Gödels book). In particular, in that paper, Feferman constructs consistency statements relative to a particular formula coding the theory, and this may be relevant.
That is, if $T$ is a theory, then he roughly says that a formula $\alpha(x)$ of the language of arithmetic numerates the theory if for every sentence $\phi$ of the language of the theory, $\phi \in T$ iff $\mathsf{Q} \vdash \alpha(\ulcorner \phi \urcorner)$, where $\mathsf{Q}$ is Robinson's arithmetic. If, moreover, $\alpha$ is such that if $\phi \not \in T$ iff $\mathsf{Q} \vdash \neg \alpha(\ulcorner \phi \urcorner)$, then $\alpha$ is said to bi-numerate the theory. (These notions correspond to what is generally called weakly represent and strongly represent, respectively.)
Anyway, the point is that consistency statements are relative to such bi-numerations, so that they are better expressed by Feferman's notation $\mathsf{Con}_\alpha(T)$. Indeed, by exploiting some coding tricks, Feferman shows (Theorem 5.9) roughly that if $T$ is a recursive consistent extension of $\mathsf{PA}$, then there is a rather strange bi-numeration $\alpha^*$ of $T$ such that $T \vdash \mathsf{Con}_{\alpha^*}(T)$. In particular (Corollary 5.10), there is a bi-numeration $\pi^*$ of $\mathsf{PA}$ such that $\mathsf{PA} \vdash \mathsf{Con}_{\pi^*}(\mathsf{PA})$.
As Feferman notes, this does not contradicts Gödel's theorem because these bi-numerations do not "properly express membership" in the given theory: "Indeed, inspection of the proof of 5.9 reveals that it expresses membership in a certain subsystem of [$T$] which, independent of the consistency of [$T$], is always consistent" (p. 69).
In fact, using a similar technique, Feferman also shows that, letting $\alpha$ be a bi-numeration of $\mathsf{PA}$ and setting $T=\mathsf{PA} + \neg \mathsf{Con}_\alpha(\mathsf{PA})$, there is a bi-numeration $\beta^*$ of $T$ such that $\mathsf{PA} \vdash \mathsf{Con}_{\beta^*}(T)$! (This is theorem 5.11.)
Using these results, Feferman then shows, first, that if $T$ is a theory and $\alpha$ is a numeration of $T$, then $T$ is interpretable in $\mathsf{PA} + \mathsf{Con}_\alpha(T)$ (theorem 6.2), which he then uses to prove (a result that implies) that there is a numeration $\alpha$ of $\mathsf{PA}$ such that $\mathsf{PA} + \neg \mathsf{Con}_\alpha(\mathsf{PA})$ is interpretable in $\mathsf{PA}$. The idea is roughly this, again using $T = \mathsf{PA} + \neg\mathsf{Con}_\alpha(\mathsf{PA})$:
By 5.11 there is a bi-numeration $\beta^*$ such that $\mathsf{PA} \vdash \mathsf{Con}_{\beta^*}(T)$. By 6.2, $T$ is interpretable in $\mathsf{PA} + \mathsf{Con}_{\beta^*}(T)$. But we have just seen that $\mathsf{PA} + \mathsf{Con}_{\beta^*}(T)$ just is $\mathsf{PA}$. Hence, the result follows.
(2) As Feferman notes, this roughly means that "we can construct a 'non-standard model' of [$\mathsf{PA}$] within [$\mathsf{PA}$] which, moreover, we can verify, axiom by axiom, to be a model of [$\mathsf{PA} + \neg\mathsf{Con}_{\beta^*}(\mathsf{PA})$]" (p. 77). Moreover, as he also observes in a footnote appended to this text, this is not all that surprising, given Gödel's theorems. The second incompleteness theorems basically states that, if $\mathsf{PA}$ is consistent, then so is $\mathsf{PA}$ extended with the negation of its consistency statement. Given that we generally use interpretations to prove relative consistency, this is basically a translation of that idea to relative consistency proofs.

EDIT: Well, I'm far from an expert on these questions, but here are my two cents (take these with lots of salt!):
First, it seems to me that there are two separate issues in the background of your question: (i) whether interpretation preserves meaning and (ii) whether the incompleteness of $\mathsf{ZF} + \neg \mathsf{Inf}$ is due to the negation of the axiom of infinity or some other limitation (the issue about arbitrary sets). Let's tackle these in order.
(i) It is true that just having an interpretation between theories is generally not sufficient to preserve "meaning", whatever that is. Indeed, one can have two theories being mutually interpretable without these interpretations preserving nice properties such as decidability, etc. Still, when two theories are mutually interpretable, perhaps the interpretations are of such a nature that we might as well identify the two theories. Here is a reasonable test. Suppose two theories, $T$ and $T'$, are mutually interpretable with interpretations $i: T \rightarrow T'$ and $j: T' \rightarrow T$. Suppose moreover that $i \circ j$ is the identity on $T'$ and $j \circ i$ is the identity on $T$, i.e. when I translate a formula using $i$, and then translate back using $j$, I always end up with the formula which I originally started (and vice-versa). When this situation takes place, say that the theories are bi-interpretable. Now, bi-interpretation can be reasonably taken to imply sameness of "meaning", since it preserves most of the interesting properties of the theories (technically, this is usually called synonymy, but the difference here is not relevant---cf. this article by Friedman and Visser for more on the difference).
So, given this, what is the situation with $\mathsf{PA}$ and $\mathsf{ZF} + \neg\mathsf{Inf}$ (which I'll call in the sequel $\mathsf{ZF}_{\mathsf{Fin}}$)? These theories are mutually interpretable, but, disappoitingly, they are not bi-interpretable. In fact, they don't satisfy a weaker requirement of "sentential equivalence", as shown by Enayat, Schmerl, and Visser in "$\omega$-models of Finite Set Theory", theorem 5.1; the proof is not difficult, but it does use some facts about the model theory of $\mathsf{PA}$ (and of $\mathsf{ZF}_{\mathsf{Fin}}$).
On the other hand, there is a theory in the vicinity which is bi-interpretable with $\mathsf{PA}$, namely $\mathsf{ZF}_{\mathsf{Fin}} + \mathsf{TC}$, where $\mathsf{TC}$ is the axiom which states that every set is contained in a transitive set (cf. this article by Kaye and Wong). The issue is related to $\varepsilon$-induction: adding this axiom is essentially equivalent to adding $\varepsilon$-induction (see again the article by Kaye and Wong). So there is a very strong sense in which these two theories are the same.
(ii) On the other hand, there is the issue about whether the fact that $\mathsf{ZF}_{\mathsf{Fin}} + \mathsf{TC}$ cannot prove Goodstein's theorem is due to the absence of an axiom of infinity or something else. From what I understand, he's probably referring to the fact that first-order $\mathsf{ZFC}$ does not fully capture the idea of an arbitrary set (cf. this article by Ferreirós for an analysis of the notion). Now, I'm really out of my depth here, but I thought the issue arose only for infinite sets. Is there an hereditarily finite set that is not first-order definable? If not, then his complaint is mute. If, however, there are such sets, then he may be on to something.
