Gödel's Second Incompleteness Theorem and Arithmetically Non-Definable Theories

OK, here is Mingzhong's answer.

$\mathbf{Theorem }$: Let $T$ be a first order definable theory stronger than $PA+Con(PA)$, then there is a theory $T'\equiv T$ so that $T'\vdash Con(T')$.

$\mathbf{Proof}$: Let $T$ be such a theory. Define $T'$ so that $T'=PA$ if $\neg Con(T)$, or $T'=T$ if $Con(T)$.

We prove that $T'\vdash (Con(T)\vee \neg Con(T))\rightarrow Con(T')$ and so $T'\vdash Con(T')$. Note that $T'\equiv T\vdash Con(PA)$.

$T'\vdash Con(T)\rightarrow T=T'$ and so $T'\vdash Con(T)\rightarrow Con(T')$.

$T'\vdash\neg Con(T)\rightarrow T'=PA$. But $T'\vdash Con(PA)$, so $T'\vdash \neg Con(T)\rightarrow Con(T')$. QED

Note that $T'$ cannot "recognize" this proof. In other words, usually $T'\not\vdash Prb_{T'}(Con(T'))$. Some additional effort are needed to prove this, but not quite difficult.