**Description:** Define proper substitution. For our notation, we use [ t / x ] ph
to mean "the wff that results from the proper substitution of t for
x in the wff ph ". That is, t properly replaces x .
For example, [ t / x ] z e. x is the same as z e. t (when x
and z are distinct), as shown in elsb4 .

Our notation was introduced in Haskell B. Curry's*Foundations of
Mathematical Logic* (1977), p. 316 and is frequently used in textbooks
of lambda calculus and combinatory logic. This notation improves the
common but ambiguous notation, " ph ( t ) is the wff that results
when t is properly substituted for x in ph ( x ) ". For
example, if the original ph ( x ) is x = t , then ph ( t )
is t = t , from which we obtain that ph ( x ) is x = x . So
what exactly does ph ( x ) mean? Curry's notation solves this
problem.

A very similar notation, namely ( y | x ) ph , was introduced in Bourbaki's Set Theory (Chapter 1, Description of Formal Mathematic, 1953).

In most books, proper substitution has a somewhat complicated recursive definition with multiple cases based on the occurrences of free and bound variables in the wff. Instead, we use a single formula that is exactly equivalent and gives us a direct definition. We later prove that our definition has the properties we expect of proper substitution (see Theorems sbequ , sbcom2 and sbid2v ).

Note that our definition is valid even when x and t are replaced with the same variable, as sbid shows. We achieve this by applying twice Tarski's definition sb6 which is valid for disjoint variables, and introducing a dummy variable y which isolates x from t , as in dfsb7 with respect to sb5 . We can also achieve this by having x free in the first conjunct and bound in the second, as the alternate definition dfsb1 shows. Another version that mixes free and bound variables is dfsb3 . When x and t are distinct, we can express proper substitution with the simpler expressions of sb5 and sb6 .

Note that the occurrences of a given variable in the definiens are either all bound ( x , y ) or all free ( t ). Also note that the definiens uses only primitive symbols.

This double level definition will make several proofs using it appear as doubled. Alternately, one could often first prove as a lemma the same theorem with a disjoint variable condition on the substitute and the substituted variables, and then prove the original theorem by applying this lemma twice in a row. (Contributed by NM, 10-May-1993) Revised from the original definition dfsb1 . (Revised by BJ, 22-Dec-2020)

Ref | Expression | ||
---|---|---|---|

Assertion | df-sb | $${\u22a2}\left[{t}/{x}\right]{\phi}\leftrightarrow \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi}\right)\right)$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

0 | vt | $${setvar}{t}$$ | |

1 | vx | $${setvar}{x}$$ | |

2 | wph | $${wff}{\phi}$$ | |

3 | 2 1 0 | wsb | $${wff}\left[{t}/{x}\right]{\phi}$$ |

4 | vy | $${setvar}{y}$$ | |

5 | 4 | cv | $${setvar}{y}$$ |

6 | 0 | cv | $${setvar}{t}$$ |

7 | 5 6 | wceq | $${wff}{y}={t}$$ |

8 | 1 | cv | $${setvar}{x}$$ |

9 | 8 5 | wceq | $${wff}{x}={y}$$ |

10 | 9 2 | wi | $${wff}\left({x}={y}\to {\phi}\right)$$ |

11 | 10 1 | wal | $${wff}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi}\right)$$ |

12 | 7 11 | wi | $${wff}\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi}\right)\right)$$ |

13 | 12 4 | wal | $${wff}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi}\right)\right)$$ |

14 | 3 13 | wb | $${wff}\left(\left[{t}/{x}\right]{\phi}\leftrightarrow \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi}\right)\right)\right)$$ |