1
$\begingroup$

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'$.

  1. If $\mathcal {M} \models T'$, then $\mathcal M$ is a definitional expansion of $M\upharpoonright L$.

  2. If $T$ is complete, then $T'$ is complete.

  3. 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$.

  1. 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?

  2. 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?

  3. 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.

$\endgroup$
  • 1
    $\begingroup$ I think "let $T'$ be a definitional extension of $T$" only applies to statements 1 and 2. The statements are true not "merely by the definitions", you need to use the soundness and completeness of first-order logic, but given that the proofs are quite simple. $\endgroup$ – Rob Arthan Apr 19 '15 at 9:34
  • $\begingroup$ Actually, for 3 $T$ is a complete Theory and $T'$ a complete extension, you are right, I missed that. I'm a bit confused at how to use soundness and completeness here, could you please help give me some advice about it? I do understand that what I'm trying to prove is the link between semantics and syntax and that is exactly what completeness do, but I don't know how to start the proof. Thank you for your help. $\endgroup$ – Sara Apr 19 '15 at 9:48
1
$\begingroup$

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:

  • Not necessary: we can do everything in $T$ if we insist;
  • Permissible: nothing goes wrong by using the new symbols of $T'$!

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:

  • $x = \varnothing$ instead of $\forall y: y \notin x$;
  • $x = 2^y$ instead of $\forall v: v \in x \iff (\forall w: w \in v \implies w \in y)$.
$\endgroup$
  • $\begingroup$ Thank you for your input, I will work on this and come back in case I hit some other wall, but I definitely see things clearer now. $\endgroup$ – Sara Apr 19 '15 at 10:32
  • $\begingroup$ Hi, I'm a bit stuck in the second one, I'm having issues with the part about proving that every T model can be extended to a T' model. I get the idea in general, it is: T is complete, every T model can extended into a T' model, so I extend it, once its extended I substitute the things on the definitions, so it's still complete. But I don't really know how to go about it, or to say it in a clearer way, I would really appreciate your advice. $\endgroup$ – Sara Apr 19 '15 at 17:41
  • $\begingroup$ Thank you very much for your help, the formal aspect of this is way more clear to me now, not only the intuitive part. This has been really helpful! $\endgroup$ – Sara Apr 20 '15 at 10:53
  • $\begingroup$ @Sara You're welcome. It was also helpful to me to go through these things once more. Cheers :). $\endgroup$ – Lord_Farin Apr 20 '15 at 12:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.