I need to prove this,
Let $T$ be a theory in language $L$, let $T'$ be a definitional extension of $T$ to language $L\subseteq L'$.
If $\mathcal {M} \models T'$, then $\mathcal M$ is a definitional expansion of $M\upharpoonright L$.
If $T$ is complete, then $T'$ is complete.
If some model of $T$ has a definitional expansion to $T'$, then $T'$ is a definitional extension of $T$.
My problem is that it feels like all that is true merely by the definitions, so I guess I'm missing something, and would like your input about it. The definitions I'm working with are:
An L'-theory $T'$ is a definitional extension of an L-theory $T$ if $T \subseteq T'$ and $T'$ is axiomatized by $T \cup \Delta$ where $\Delta = \{\delta_s | s \in L' - L\}$ and each $\delta_s$ is a definition in $T$ of the symbol $s$.
A definitional expansion of $M$ is an expansion $M'$ of $M$ to some language $L \subseteq L'$ such that for each symbol $s \in L'- L$, $s^{M'}$ is definable in $M$.
Let $\mathcal {M} \models T'$, and $T' = T \cup \Delta$ where $\Delta = \{\delta_s | s \in L' - L\}$ for each $\delta_s$ of each symbol $s$, so it looks pretty clear that that is exactly the definition of definitional expansion. Any ideas about how to argue it better?
The idea is, $T'$ and $T$ prove the same things, the extensions are conservative, clearly if $T$ is complete so will be $T'$, but I have trouble saying it formally enough, or did I miss something?
Same issue it feels like just 2 different shades of the same definition, and I don't know how to connect them, besides noting that we are talking about pretty much the same thing.
I would very much appreciate your advice, I feel slightly baffled.
As to 1., indeed, it isn't too difficult. Just choose $\delta_s$ to make $s$ definable in $M$.
As to 2., it's just: $$T' \models \phi \iff T' \models \phi^L \iff T \models \phi^L$$ These equivalences deserve some extra attention. The first is just a substitution theorem, the second requires you to prove that every $T$-model can be extended to a $T'$-model. Then we can apply completeness of $T$ to deduce completeness of $T'$.
Finally, for 3., denote the model with $M$, the expansion with $M'$. Since the new symbols are definable in $M'$, we can use the defining formulas as a hypothetical $\Delta$ (this works because $T$ is complete). To conclude that $T'$ is actually axiomatised as $T \cup \Delta$, we will need to use the other completeness hypothesis.
As requested, some more detail on the second part. We need to prove that:
$$T'\not\models \phi \implies T'\models \neg\phi$$
Suppose that $M \models T'\cup \neg\phi$. Then $M \restriction L \models T$. Then by completeness of $T$, $T \models (\neg \phi)^L$. Consequently, $T'\models (\neg\phi)^L$.
Note that we only required the "easy" direction:
$$T\models (\neg\phi)^L \implies T' \models (\neg\phi)^L$$
which amounts to the fact that every $T'$-model carries a natural $T$-model.
I guess that would've sufficed.
However, there were other things at play here which came along quite naturally -- at least to me.
Namely, the converse is of considerable conceptual importance. Suppose we forgot about $T$ being complete. Here it is once more:
$$T'\models (\neg\phi)^L \implies T \models (\neg\phi)^L$$
What does extending every $T$-model to a $T'$-model mean? It's not hard, really (define each term $s$ by means of its $\delta_s$, prove by structural induction that the result models $T'$). But why bother?
If we pass to the proof-theoretic side of things, we obtain:
$$T' \vdash \phi \iff T \vdash \phi$$
That is to say, all these fancy new symbols, relations and functions are:
Thus, if we choose to work in our favourite theory $\sf ZFC$, we can make our lives easier and stick to the mathematical practice of introducing new notation, using convenient shorthands like: