For two theories $T,T'$, what does $T\vdash Con(T')$ really tell us about the models of $T$?

Inspired by this question, which I realized I couldn't answer (because model theory and me don't get along).

I've made a few edits to (hopefully constructively) tighten the question a bit.

If for theories $T,T'$ it happens that $T\vdash Con(T')$, what does this really tell me about models of $T$ with respect to $T'$? Does it tell us that every model of $T$ has a definable substructure that's a model of $T'$, or is it more subtle? Or is it even interesting from a model theoretic standpoint (i.e. is the proof theoretic relationship between $T$ and $T'$ generally the only interesting one)?

I would like to assume $T$ and $T'$ can both yield PA by default, but I would be interested if anything general can be said about weaker theories.

-

It is not literally true that if $T \vdash \operatorname{Con}(T')$ then every model of $T$ has a definable substructure that satisfies $T'$. For example, $T'$ might not even be in the same language as $T$, in which case no substructure of a model of $T$ can possibly satisfy $T'$.

For example, PA proves the consistency of a theory of second-order arithmetic known as $\mathsf{RCA}_0$. Now the language for $\mathsf{RCA}_0$ includes a relation symbol $\in$ that is not in the language of PA, so no substructure of PA can satisfy $\mathsf{RCA}_0$.

Similarly, PA + Con(ZFC) proves Con(ZFC), but no model of PA has a substructure that satisfies ZFC.

It is true, however, that every model of PA intereprts a model of $\mathsf{RCA}_0$. But every model of PA interprets a stronger theory of second-order arithmetic, $\mathsf{ACA}_0$, which is equiconsistent with PA. So it is also not true that $T \vdash \operatorname{Con}(T')$ is equivalent to saying that $T$ interprets $T'$.

If every model of $T$ has a definable substructure satisfying $T'$ (or, in fact, any substructure satisfying $T'$), that only shows that Con($T$) implies Con($T'$).

-
Excellent! You've given an example where $PA$ interprets $ACA_0$ and can't yield $Con(ACA_0)$; are there examples of the converse? E.g. is it also the case that $PA+Con(ZFC)$ can't interpret $ZFC$? This sounds plausible, but I distrust plausible-sounding things... – Malice Vidrine Nov 16 '13 at 16:02
@Carl: The parenthetical remark in your last paragraph looks suspicious. For example, every model of $\mathrm{PA}$ has an initial segment isomorphic to $\mathbb N$. However, this doesn't mean that $\mathrm{Con(PA)}$ implies $\mathrm{Con}(T)$ (say, over $\mathrm{PA}$) for every true recursive theory $T$. – Lawrence Wong Nov 16 '13 at 17:13
@Lawrence Wong: it does imply that; the key issue is to remember the metatheory where the result is proved. I mean that if $M$ is a sufficiently strong metatheory (e.g. ZFC) and $M$ proves that every model of $T$ has a substructure satisfying $T'$, then $M$ also proves that Con($T$) implies Con($T'$). Of course this can happen even if $M$ does not already prove Con($T$); for example ZFC proves that the consistency of ZFC plus a measurable cardinal implies the consistency of ZFC plus an inaccessible cardinal, but it does not prove either consistency statement on its own. – Carl Mummert Nov 16 '13 at 18:43
@Malice Vidrine: the closest thing I see to that is the comment by Lawrence Wong below his answer. You could ask the question in your comment as a separate question, I think it is quite interesting. – Carl Mummert Nov 16 '13 at 18:46
@Carl Mummert: You were right. Now, I see why I was confused. Of course "$\mathrm{PA}\vdash\mathrm{Con(PA)}\rightarrow\mathrm{Con}(T)$ for every recursive theory $T$ true in $\mathbb N$" is wrong. My argument only showed that if we replace the base theory $\mathrm{PA}$ by a theory $S$ good enough to talk about natural number arithmetic, and suppose $S$ thinks its natural numbers satisfy $T$, then $S\vdash\mathrm{Con(PA)}\rightarrow\mathrm{Con}(T)$. This has (almost) nothing to do with the real $\mathbb N$ (and actually tells us nothing). It is much clearer to me now. Thank you very much! – Lawrence Wong Nov 17 '13 at 9:51

Suppose $T$ and $T'$ are both theories in the language of first-order arithmetic $\mathscr L_{\mathrm{A}}$, and $T\vdash\mathrm{Con}(T')$. (This presumes the fact that $T'$ is definable in $\mathscr L_{\mathrm{A}}$.) If $T$ is strong enough to prove an appropriate version of Gödel's Completeness Theorem (in the sense described in my comment below), then, as you wrote, for every model $M\models T$, there is $K\models T'$ that is definable in $M$ (and so we may regards $K\subseteq M$).

For me, it is actually more interesting to consider this $K$ as an end-extension of $M$ (provided $T'$ extends, say, $\mathrm{PA}^-$). One can do this because in the $M$-version of $\mathscr L_{\mathrm A}$, there is a closed term $$0+\underbrace{1+1+\cdots+1}_{\text{m 1's}}$$ for every $m\in M$. As $K\models\mathrm{PA}^-$, the realizations of these terms form an initial segment of $K$, which we can identify with $M$. This is interesting because many important problems in the area are related to end-extensions.

-
Could you clarify the form of the completeness theorem that is provable in PA? – Carl Mummert Nov 16 '13 at 14:13
@Carl Mummert: This is the same as what you have in $\mathrm{WKL_0}$; so strictly speaking, it is not expressible in the language of first-order arithmetic. To put it model-theoretically: if $M\models\mathrm{PA}$ and $T'$ is a theory definable in $M$ such that $M\models\mathrm{Con}(T')$, then there is a model of $T'$ definable in $M$. – Lawrence Wong Nov 16 '13 at 16:51
!Lawrence Wong: thank you, that is completely clear. – Carl Mummert Nov 16 '13 at 18:47