2

I'm referring to the proof to Lemma $25\text{B} \ $,pg$\ 133$ of Enderton's Mathematical Introduction to Logic($2^\text{nd}$ edition): $\overline s(u^{x}_{t})=\overline {s(x|\overline s(t))}(u).$

The author gives a brief induction proof on the term $u.$ But I'm unsure of how the induction step goes. So if $u=ft_1...t_n,$ where $t_1=x,$ then $u^{x}_{t}=ft...t_n$ and $\overline s(u^{x}_{t})= f^{\frak{A}}(\overline s(x),...,\overline s(t_n)).$ Could anyone advise me on how to proceed further? Thank you.

Alexy Vincenzo
  • 5,400

1 Answers1

1

You must think on the "corresponding commutative diagram" of page 133.

The basis case is easy : see page 133 where $u$ is a constant $c$, or $u$ is $x$, or $u$ is $y \ne x$.

For the induction step, we have that :

if $u=ft_1...t_n$,

then

$u^{x}_{t}=f(t_1[x \leftarrow t],...t_n[x \leftarrow t])$

i.e. we must subst $t$ in place of $x$ in each term $t_i$ iside the "complex" term $u$.

Now : $\overline s(u^{x}_{t})= f^{\frak{A}}(\overline s(t_1[x \leftarrow t]),...,\overline s(t_n[x \leftarrow t]))$

by def of $\overline s$ [see page 83].

But $t_1, ... t_n$ are "shorter" than $u$; thus, by induction hypotheses :

$\overline s(t_i[x \leftarrow t])=\overline {s(x|\overline s(t))}(t_i)$.

Putting all together :

$\overline s(u^{x}_{t}) = f^{\frak{A}}(\overline {s(x|\overline s(t))}(t_1), .... \overline {s(x|\overline s(t))}(t_n))$.

But the var $x$ is not "contained" into the symbol $f$, so that :

$\overline s(u^{x}_{t}) = \overline {s(x|\overline s(t))}(u)$.

Mauro ALLEGRANZA
  • 94,169