You are here
Homesubstitutability
Primary tabs
substitutability
In any logical system, the way to obtain (wellformed) formulas from existing ones is by attaching logical connectives to existing ones. For example, in classical propositional logic, if $\varphi$ and $\psi$ are formulas, the following
$\varphi\vee\psi,\quad\neg\varphi,\quad\psi\wedge\varphi$ 
are formed by attaching logical connectives $\vee,\neg$, and $\wedge$ appropriately to $\varphi$ and $\psi$.
Another convenient device is substitution:
replace all occurrences of some symbol $x$ in a formula $\varphi$ by an expression $\psi$.
We denote the resulting expression by
$\varphi[\psi/x].$ 
For example, in classical propositional logic, if $\varphi$ is $p\wedge(\neg r\vee p)$, then $\varphi[(p\vee q)/p]$ is
$(p\vee q)\wedge(\neg r\vee(p\vee q))$ 
On the other hand, the expressions

$\varphi[\neg/p]$, which is $\neg\wedge(\neg r\vee\neg)$, and

$\varphi[q/\wedge]$, which is $p\;q(\neg r\vee q)$,
are not formulas. Thus, one must be careful when performing substitutions on formulas lest the resulting expressions are illformed. In other words, conditions must be placed on $x$ and $\psi$ in $\varphi[\psi/x]$ in order that $\varphi[\psi/x]$ is a (wellformed) formula. These conditions are called the substitutability conditions. In this entry, we will concentrate on substitutability conditions on predicate logic. Details on substitions in propositional logic can be found in here.
Substitution in FirstOrder Logic
Substitution works pretty much the same way for firstorder logic as in propositional logic. However, the substitutability conditions are more subtle. Take a look at the following example:
$\exists x\;(x=1)$ 
If we replace $x$ by $0$, we end up with
$\exists 0\;(0=1),$ 
which is nonsensical (not a wff). This is because $x$ occurs in the formula as a bound variable. (one reason why we distinguish the variables occurring in first order formulas into two types: free and bound).
We now formalize the notion of substitution in firstorder logic. There are two parts: substitution for terms, and substitution for formulas.
Definition. For any term $t$, any symbol $x$, and any expression $s$, define $t[s/x]$ inductively, as follows:
1. if $t$ is an individual variable or a constant symbol, then $t[s/x]$ is $s$ if $t$ is $x$, and $t[s/x]$ is $t$ otherwise;
2. if $t$ is $f(t_{1},\ldots,t_{n})$, where $f$ is an $n$ary function symbol, and each $t_{i}$ is a term, then $t[s/x]$ is $f(t_{1}[s/x],\ldots,t_{n}[s/x])$.
For example, if $t$ is $x+y$, then $t[(xy)/x]$ is $(xy)+y$.
It is easy to see that $s$ is a term and $x$ an individual variable, then $t[s/x]$ is a term. In addition, by induction, one can easily show that if the formula $s_{1}=s_{2}$ is true, so is the formula $t[s_{1}/x]=t[s_{2}/x]$.
Next, we define substitution for formulas. In light of the last example at the beginning of this section, we need to be a little careful.
Definition. Let $\varphi$ be a formula, $x$ a symbol, and $s$ an expression. The expression $\varphi[s/x]$ is again define inductively:
1. if $\varphi$ is $t_{1}=t_{2}$, then $\varphi[s/x]$ is $t_{1}[s/x]=t_{2}[s/x]$;
2. if $\varphi$ is $R(t_{1},\ldots,t_{n})$, then $\varphi[s/x]$ is $R(t_{1}[s/x],\ldots,t_{n}[s/x])$;
3. if $\varphi$ is $\neg\psi$, then $\varphi[s/x]$ is $\neg(\psi[s/x])$;
4. if $\varphi$ is $\psi\vee\sigma$, then $\varphi[s/x]$ is $\psi[s/x]\vee\sigma[s/x]$;
5. if $\varphi$ is $\exists y\psi$, then $\varphi[s/x]$ is $\exists y(\psi[s/x])$ if $x\neq y$, and $\varphi[s/x]$ is $\varphi$ otherwise.
Again, substitutions involving logical connectives $\to$, $\wedge$, and the universal quantifier $\forall$ can be derived from the rules given above.
For example, if $\varphi$ is $\exists x(x=y\vee y=z)$, then $\varphi[t/y]$ is $\exists x(x=t\vee t=z)$, whereas $\varphi[t/x]$ is just $\varphi$.
Given that $\varphi$ is a formula, it is easy to see that if $x$ is an individual variable, and $s$ is a term, then $\varphi[s/x]$ is a formula.
In addition, it is easy to see that sentences are not affected by substitutions: if $\varphi$ is a sentence, then $\varphi[s/x]$ is just $\varphi$. In other words, sentences can not be changed into formulas with free variables.
Conversely, can a formula with free variables be changed into a sentence by substitution? Certainly. For example, if $\varphi$ is
$\exists x(y<x),$ 
then $\varphi[x/y]$ is
$\exists x(x<x).$ 
Although syntactically correct, this is undesirable in many situations, particularly when we are interested in the interpretations of these formulas. In the example above, we have changed $\exists x(y<x)$, which many very well be true in many interpretations, into $\exists x(x<x)$, something with a fixed meaning (and always false if $<$ is interpreted as the usual less than relation).
The problem with the situation described in the last paragraph arises because a free variable in $t$ becomes bound in $\varphi[t/x]$. To eliminate this undesirable situation, we define the notion of “free for”:
Definition. Let $x$ be an individual variable, $t$ a term, and $\varphi$ a formula. We define the relation $t$ is free for, or substitutable for $x$ in $\varphi$, inductively, as follows:
1. $\varphi$ is an atomic formula;
2. $\varphi$ is $\neg\psi$, and $t$ is free for $x$ in $\psi$;
3. $\varphi$ is $\psi\vee\sigma$, and $t$ is free for $x$ in $\psi$ and in $\sigma$;
4. $\varphi$ is $\exists y\psi$, and either

$x\notin\operatorname{FV}(\varphi)$ ($x$ does not occur free in $\varphi$), or

$y$ does not occur in $t$, and $t$ is free for $x$ in $\psi$.

In words, $t$ is free for $x$ in $\varphi$ iff whenever $z$ is a variable in $t$, no literal subformula of $\varphi$ of the form $\exists z\psi$ contains an occurrence of $x$ which is free in $\varphi$.
For example, $f(x,y)$ is free for $x$ in the following formulas:
$P(x,y),\qquad P(x)\vee\neg Q(z),\qquad\neg\exists x\;\neg R(x,y),\qquad\mbox{% and}\qquad\neg S(y)\vee\exists yT(y,z),$ 
but not in the following formulas:
$\exists yP(x,y),\qquad Q(x)\vee\exists z\exists yR(x,y),\qquad\mbox{and}\qquad S% (y)\to\forall y(T(y,y)\wedge\neg Q(x)).$ 
Given any formula $\varphi$, we again write $\varphi(x)$ to mean that variable $x$ occurs in $\varphi$. A substitution instance of $\varphi(x)$ is just $\varphi[t/x]$, or $\varphi(t)$ for short. Furthermore, if $t$ is free for $x$ in $\varphi$, then $\varphi(t)$ is called a free substitution instance of $\varphi(x)$.
It is easy, by induction, to show that if terms $t_{1}$ and $t_{2}$ are free for $x$ in $\varphi$, and that the formula $t_{1}=t_{2}$ is true, the substitution instances $\varphi(t_{1})$ and $\varphi(t_{2})$ are logically equivalent, as intended.
Mathematics Subject Classification
03B10 no label found03B05 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections