# Induction on formulas in First Order Languages

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.

• 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. – Huy Truong Oct 3 '16 at 23:59
• @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. – Noah Schweber Oct 4 '16 at 0:03
• 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. – Huy Truong Oct 4 '16 at 1:16
• @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. – Noah Schweber Oct 4 '16 at 1:45
• 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. – Huy Truong Oct 4 '16 at 2:27