# An “internal” condition on $T$ so that for the standard provability predicate, $T$ proves $\text{Pf}(\underline S)$ implies $T$ proves $S$?

This is probably quite basic, but I'd like to make sure I got this right. Regarding the proof of Goedel's first incompleteness theorem, say that we have $T$ containing $PA$ effectively axiomatizable and consistent. Construct a sentence $S$ such that $T$ proves $S \leftrightarrow \lnot \text{Pf}(\underline{S})$, and assume $T$ proves $S$, so that $T$ proves $\lnot \text{Pf} ( \underline S)$ by modus ponens. Since $T$ proves $S$, also $T$ proves $\text{Pf}(\underline S)$: there is some $T$-proof $P$ of $S$, with Goedel number $k$, then $T$ proves $\text{Prf} (k, \underline S)$. So $T$ is able to recognize whenever it does prove something, and $T$ does not prove $S$. So far, so good.

Now assume $T$ proves $\lnot S$, so that is proves $\text{Prf}(\underline S)$ by modus ponens. What I'd like to now say is that $T$ now proves $S$, which would be a contradiction. My question is: is the inference from $T$ proves $\text{Prf}(\underline M)$ to $T$ proves $M$ hold if $T$ is $\omega$-consistent? If not, what's a good counter-example? (Note that $T + \lnot Con(T)$ is an example of a consistent theory where the implication fails.) Assuming $T$ is sound with respect to $\Sigma_1$ statements, I see it does, since $T$ proves $\text{Pf}( \underline M)$ means $\text{Pf}( \underline M)$ is true, so that $T$ proves $M$. But I know soundness for $\Sigma_1$ statements is strictly stronger than consistency. (Also stronger than $\omega$-consistency?)

Compare this "proof" with this one using $\omega$-consistency. Again assume $T$ proves $\lnot S$, so that $T$ proves $\text{Pf}(\underline S)$ by MP. But from above, $T$ does not prove $S$, so for each $k$, $T$ proves $\lnot \text{Prf}(\underline k, \underline S)$, which contradicts $\omega$-consistency. So this proof does the job, but I'm curious under which conditions can we assume what we'd want to assume: that $T$ proves $\text{Pf}(\underline M)$ really does imply that $T$ proves $M$, and that the $\text{Pf}$ predicate is nice! Namely, I'd be very happy to find a "T-internal" property like ($\omega$-)consistency which implied this, rather than a ''T-external'' one like soundness, or a proof why this is not possible.

Many thanks!

EDIT: The answer is yes, $\omega$-consistency is enough for $T$ proves $\text{Pf}(\underline S)$ to imply $T$ proves $S$. For say it didn't, then for each $k$, $T$ proves $\lnot \text{Prf} (\underline k, \underline S)$ by the fact that $\text{Prf}$ numeral-wise represents provability. But this would contradict $\omega$-consistency since we'd have proven $\exists x \text{Prf}(x, \underline S)$, as well as the negations of each of its instances.

-