**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 | ⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |

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

0 | vt | ⊢ 𝑡 | |

1 | vx | ⊢ 𝑥 | |

2 | wph | ⊢ 𝜑 | |

3 | 2 1 0 | wsb | ⊢ [ 𝑡 / 𝑥 ] 𝜑 |

4 | vy | ⊢ 𝑦 | |

5 | 4 | cv | ⊢ 𝑦 |

6 | 0 | cv | ⊢ 𝑡 |

7 | 5 6 | wceq | ⊢ 𝑦 = 𝑡 |

8 | 1 | cv | ⊢ 𝑥 |

9 | 8 5 | wceq | ⊢ 𝑥 = 𝑦 |

10 | 9 2 | wi | ⊢ ( 𝑥 = 𝑦 → 𝜑 ) |

11 | 10 1 | wal | ⊢ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) |

12 | 7 11 | wi | ⊢ ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) |

13 | 12 4 | wal | ⊢ ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) |

14 | 3 13 | wb | ⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |