Skip to content

Substitutions

If \(t\) and \(s\) are terms, we write \(t[s/x]\) for the term where \(x\) is replaced by \(s\). The following is a compositional definition of \(t[s/x]\):

  1. \(x[s/x]= s\);
  2. \(y[s/x]=y\) for \(y\ne x\);
  3. \(c[s/x]=c\), where \(c\) is a constant symbol.
  4. \(f(t_1,t_2,\ldots, t_n)[s/x]=f(t_1[s/x],t_2[s/x],\ldots, t_n[s/x])\), where \(f\) is an \(n\)-ary function symbol.

Similarly, for a first-order formula \(\varphi\), \(\varphi[s/x]\) is the formula in which all free occurrences of \(x\) are replaced with \(s\). The compositional definition for this is:

  1. \((t_1=t_2)[s/x]\) is \((t_1[s/x] = t_2[s/x])\)
  2. \(\bot[s/x]\) is \(\bot\)
  3. \(R(t_1,\ldots,t_n)[s/x]\) is \(R(t_1[s/x],\ldots,t_n[s/x])\), where \(R\) is an \(n\)-ary relation symbol.
  4. \((\neg\psi)[s/x]\) is \((\neg \psi[s/x])\)
  5. \((\psi_1\wedge\psi_2)[s/x]\) is \((\psi_1[s/x]\wedge\psi_2[s/x])\)
    (similarly for the other Boolean connectives \(\vee\), \(\rightarrow\), and \(\leftrightarrow\))
  6. \((\forall x (\psi))[s/x]\) is \((\forall x)\psi\)
  7. \((\forall y (\psi))[s/x]\) is \((\forall y (\psi[s/x]))\), where \(y\ne x\)
  8. \((\exists x (\psi))[s/x]\) is \((\forall x)\psi\)
  9. \((\exists y (\psi))[s/x]\) is \((\forall y (\psi[s/x]))\), where \(y\ne x\)

Examples

  1. \((x=y)[y/x]\) is \(y=y\)
  2. \((x=y)[x/y]\) is \(x=x\),
  3. \((\forall x (x=y))[y/x]\) is \(\forall x (x=y)\),
  4. \((\forall x (x=y))[x/y]\) is \(\forall x (x=x)\),
  5. \((\forall x (x=x))[y/x]\) is \(\forall x (x=x)\),
  6. \((\forall x (P(x))\rightarrow P(x))[s/x]\) is \((\forall x) P(x) \rightarrow P(s)\), where \(s\) is a term.

Exercises

The tutorial questions are available at https://umd.instructure.com/courses/1301043/assignments/5552980