Gentzen's consistency proof and model of $PA+\neg Con(PA)$

Question

Gentzen's consistency proof demonstrates that $PA$ is consistent. Does it also demonstrate there exists no model of $PA + \neg Con(PA)$? Naturally, this initially seems to be so, but if PA is consistent then there should be a model of $PA + \neg Con(PA)$. But some texts write that Gentzen's consistency proof demonstrates $Con(PA)$, which adds confusion. $Con(PA)$ is a sentence in a theory, so it is not clear if Gentzen's consistency proof actually demonstrates it. In other words, even if Gentzen's consistency proof demonstrates consistency of $PA$, $\neg Con(PA)$ being satisfied still seems possibility.

Answer 1

Gentzen's proof establishes Con(PA) from assumptions that are not provable in PA. In particular, Gentzen's proof uses transfinite induction up to the ordinal $\epsilon_0$ (see $\epsilon$ numbers on Wikipedia). This amount of transfinite induction is not provable in PA. The ordinal $\epsilon_0$ is the "proof theoretic ordinal" of PA - Gentzen's proof led to a general program of ordinal analysis to try to classify the strength of theories by their proof theoretic ordinals.

As you said, none of this contradicts the existence of models of PA + $\lnot \text{Con}(\text{PA})$. The incompleteness theorem shows that PA does not prove Con(PA), so any sufficiently strong metatheory (like ZF) will be able to construct models of PA + $\lnot \text{Con}(\text{PA})$.