Induction on formulas in First Order Languages

279 Views Asked by At

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?)

1

There are 1 best solutions below

6
On BEST ANSWER

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.