Implement substitution/substitutability

[ed963]

• Definition 1.8.1. Suppose that $u$ is a term, $x$ is a varable, and $t$ is a term. We define the term $u_t^x$ (" $u$ with $x$ replaced by $t$") as follows:

  1. If $u$ is a variable not equal to $x$, then $u_t^x$ is $u$.
  2. If $u$ is $x$, then $u_t^x$ is $t$.
  3. If $u$ is a constant symbol, then $u_t^x$ is $u$.
  4. If $u:\equiv fu_1u_2\dots u_n$, where $f$ is an $n$-ary function symbol and the $u_i$ are terms, then $u_t^x$ is $f(u_1)^x_t(u_2)^x_t\dots(u_n)^x_t$.

• Definition 1.8.2. Suppose that $\phi$ is an $\cal L$-formula, $t$ is a term, and $x$ is a variable. We define the formula $\phi_t^x$ as follows:

  1. If $\phi:\equiv=u_1u_2$, then $\phi_t^x$ is $=(u_1)^x_t(u_2)^x_t$.
  2. If $\phi:\equiv Ru_1u_2\dots u_n$, then $\phi^x_t$ is $R(u_1)^x_t(u_2)^x_t\dots(u_n)^x_t$.
  3. If $\phi:\equiv(\neg\alpha)$, then $\phi_t^x$ is $(\neg\alpha_t^x)$.
  4. If $\phi:\equiv(\alpha\vee\beta)$, then $\phi_t^x$ is $(\alpha^x_t\vee\beta^x_t)$.
  5. If $\phi:\equiv(\forall y)(\alpha)$, then

     \phi^x_t = \begin{cases} \phi &\text{if $x$ is $y$}\\ (\forall y)(\alpha_t^x) &\text{otherwise} \end{cases}

• Definition 1.8.3. Suppose that $\phi$ is an $\cal L$-formula, $t$ is a term, and $x$ is a variable. We say that $t$ is substitutable for $x$ in $\phi$ if:

  1. $\phi$ is atomic, or
  2. $\phi:\equiv(\neg\alpha)$ and $t$ is substitutable for $x$ in $\alpha$, or
  3. $\phi:\equiv(\alpha\vee\beta)$ and $t$ is substitutable for $x$ in both $\alpha$ and $\beta$, or
  4. $\phi:\equiv(\forall y)(\alpha)$ and either a. $x$ is not free in $\phi$, or b. $y$ does not occur in $t$ and $t$ is substitutable for $x$ in $\alpha$

[ed963]

b1e2dcc728c60f8ec0a356952f1a0105ee410d06 096d91766298a8ab7a53e2e707b372b0d937299b