1) Let $L$ be a language. Let $k \in \mathbb{N}$ and let $R$ be a $k$-ary relational symbol that is not in $L$. Set $L' = L \cup \{ R \}$. Let $M$ be an $L$ structure and $F[x_1,....,x_k]$ be a formula. Let $M'$ be an expansion by definition of $M$ in the language $L'$.

Show by induction on formulas that for any $L'$-formula $G[y_1,...,y_k]$, there is an $L$-formula $\tilde{G}[y_1,...y_n]$ such that for any $(a_1,...,a_n) \in M^n$, we have

$M' \vDash G[a_1,...a_n] \iff M \vDash \tilde{G}[a_1,...,a_n]$.

Conclude that any set definable in $M'$ is definable in $M$.

2) Do the same thing for a constant symbol $c$ not appear in $L$ and define $L' = L \cup \{ c \}$.

3) The same thing for a function symbol $f$.

Attempt: I think this problem should be a very straight forward induction on the formulas, but somehow I couldn't find any direction, probably because I'm still confused with all the new terminology. I will focus on (1) as (2) and (3) I believe are very similar.

The problem is given a $G$, how should we define $\tilde{G}$. So I start with an example. Say we have $L=\{ < \}$ and let $M = (\mathbb{N},<)$. Let $L' = L \cup \{> \}=\{<,>\}$ and so $M'=(\mathbb{N},<,>)$, an expansion by definition of $M$. Now in $L$, say we have a formula $x<y$, and atomic formula. In $L'$ to write $x>y$, we just simply negate it, i.e., $\neg((x<y)\vee(x\simeq y))$. Thus, my guess is that for a $G=Rt_1...t_k$ where $R$ is not in $L$, we put $\tilde{G}=\neg Rt_1...t_k$. Then $M' \vDash G[a_1,...,a_n] \iff...$ and this is where I got stuck because I couldn't use the fact that $M'$ is an expansion by definition of $M$. Could someone give me some hints? Thanks!

UPDATE: Let $G=Rt_1...t_k$ and assume that $R$ defined by $F[x_1,...,x_k]$ (in $M$) is not part of $L$; otherwise, we are done. Put $\tilde{G} = F_{t_1/x_1}...,F_{t_k/x_k}$. Then we have $M' \vDash G[a_1,...,a_n] \iff (t^{M'}_1[a_1,...,a_n],...,t_k^{M'}[a_1,...a_n]) \in R^{M'}$ (by definition when a structure satisfies an atomic formula) $\iff M \vDash F[t^{M'}_1[a_1,...,a_n],...,t_k^{M'}[a_1,...a_n]]$ (my explanation for this step is that because $R^{M'}$ is definable in $M$ so $M$ must satisfy $F$ with this tuple plugged in; but this is where I have problem, it looks just right but is it even formal?) $\iff M' \vDash \tilde{G}[a_1,...,a_n]$ (again, it looks right, but is it even correct according to the formal approach of logic?)


Note that the $\tilde{G}$ you describe also isn't in the old language $L$, since it still uses the symbol "$R$"! You need to find a way to get rid of every instance of $R$; or rather, to replace each occurrence of "$R$" with some expression in the old language.

Remember what "expansion by definitions" means: the new symbol, $R$, can be defined in terms of the old ones. So, for instance, in the example you give the new symbol is "$>$," and it can be defined (as you observe) in terms of the old one via $$(*)\quad\neg(x<y \vee x=y).$$ Now let's try to use this in an example. Suppose I want to rewrite a complicated formula like $$\forall x\exists y(x>y\wedge \forall z(x>z\vee z>y)).$$ Ignore what it means for a moment; if you think "mechanically," you want to replace each instance of "$>$" with the formula $(*)$ above. Specifically, the following is the natural thing to do: $$\forall x\exists y([\neg(x<y \vee x=y)]\wedge \forall z([\neg(x<z \vee x=z)]\vee [\neg(z<y \vee z=y)])).$$ What have I done? Well, I know that every formula of the form $$"u>v"$$ is equivalent to $$"\neg(u<v\vee u=v),"$$ so I've just gone through and substituted the latter for the former.

Do you see how to do this in general? If $R$ is defined by a formula $F(x_1, . . . , x_k)$ in the old language, and I have a complicated formula $G$ which uses $R$, what should I replace each instance of $R(t_1, . . . , t_k)$ in $G$ by?

Proving that this works requires induction on the complexity of $G$ - even defining the transformation $G\rightarrow\tilde{G}$ is a bit messy, and in full formality uses definition by recursion - but nothing particularly interesting happens along the way: once you see what $\tilde{G}$ should be, everything else is a bit tedious but straightforward.

  • $\begingroup$ Thanks for your help Noah. I gave the proof in the case when $G$ is an atomic formula in the UPDATE part in my original post. Could you help me check if it's formally correct? I believe once I get through this step, I can get the rest of induction steps done because I understand the main idea, it just the technical writing here causes me a lot of troubles. $\endgroup$ – Huy Truong Oct 3 '16 at 23:59
  • $\begingroup$ @HuyTruong I think you mean "$F(t_1, ..., t_k)$" instead of "$F_{t_1/x_1}, . . ., F_{t_k/x_k}$", but that's the only issue I see. The part where you ask "Is this even formal?" is justified by the assumption on $R$: saying $R$ is defined by $F$ means precisely what we have there. $\endgroup$ – Noah Schweber Oct 4 '16 at 0:03
  • $\begingroup$ I did mean the second one. $F [t_1,...t_k]$ from what I learned, this means that the t's are variables or constants. That's why I had to do the substitutions t's for x's. And so I'm not sure if this is formally correct. $\endgroup$ – Huy Truong Oct 4 '16 at 1:16
  • $\begingroup$ @HuyTruong I don't think you get my correction: I'm saying that your sentence "Put $\tilde{G} = F_{t_1/x_1}...,F_{t_k/x_k}$." is grammatically incorrect (it should be $F(t_1/x_1, . . . , t_k/x_k)$ - you have unnecessary subscripts and too many $F$s). I don't see what the problem is re: formal correctness; you're saying that $\tilde{G}$ is formula gotten by replacing each $x_i$ in "$F(x_1, . . . , x_k)$" with the corresponding $t_i$. How is that not formal? Also, in "$F[t_1,. . . , t_k]$" the $t_i$s are arbitrary terms - not just variables or constants. $\endgroup$ – Noah Schweber Oct 4 '16 at 1:45
  • $\begingroup$ I see. It's just sometimes I don't feel confident when solving problems in logic since I'm too overwhelmed with all the definitions and propositions which look very clear but requires a page to write down... I'm using the textbook by Cori and the author sometimes explains the concepts or make some remarks in such a complicated way that I don't understand what's going on. But thanks for all your help so far, Noah. $\endgroup$ – Huy Truong Oct 4 '16 at 2:27

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.