MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sb Structured version   Visualization version   GIF version

Definition df-sb 2061
Description: Define proper substitution. For our notation, we use [𝑡 / 𝑥]𝜑 to mean "the wff that results from the proper substitution of 𝑡 for 𝑥 in the wff 𝜑". That is, 𝑡 properly replaces 𝑥. For example, [𝑡 / 𝑥]𝑧𝑥 is the same as 𝑧𝑡 (when 𝑥 and 𝑧 are distinct), as shown in elsb4 2121.

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, "𝜑(𝑡) is the wff that results when 𝑡 is properly substituted for 𝑥 in 𝜑(𝑥)". For example, if the original 𝜑(𝑥) is 𝑥 = 𝑡, then 𝜑(𝑡) is 𝑡 = 𝑡, from which we obtain that 𝜑(𝑥) is 𝑥 = 𝑥. So what exactly does 𝜑(𝑥) mean? Curry's notation solves this problem.

A very similar notation, namely (𝑦𝑥)𝜑, 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 2081, sbcom2 2158 and sbid2v 2547).

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

Note that the occurrences of a given variable in the definiens are either all bound (𝑥, 𝑦) or all free (𝑡). 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 2506. (Revised by BJ, 22-Dec-2020.)

Assertion
Ref Expression
df-sb ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)))
Distinct variable groups:   𝑥,𝑦   𝑦,𝑡   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑡)

Detailed syntax breakdown of Definition df-sb
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 vt . . 3 setvar 𝑡
41, 2, 3wsb 2060 . 2 wff [𝑡 / 𝑥]𝜑
5 vy . . . . 5 setvar 𝑦
65, 3weq 1955 . . . 4 wff 𝑦 = 𝑡
72, 5weq 1955 . . . . . 6 wff 𝑥 = 𝑦
87, 1wi 4 . . . . 5 wff (𝑥 = 𝑦𝜑)
98, 2wal 1526 . . . 4 wff 𝑥(𝑥 = 𝑦𝜑)
106, 9wi 4 . . 3 wff (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑))
1110, 5wal 1526 . 2 wff 𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑))
124, 11wb 207 1 wff ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)))
Colors of variables: wff setvar class
This definition is referenced by:  sbt  2062  stdpc4  2064  sbi1  2067  spsbe  2079  spsbeOLD  2080  sbequ  2081  sb6  2084  sbal  2156  sbequ1  2240  sbequ2  2241  sbequ2OLD  2242  dfsb7  2277  dfsb7OLD  2278  sbn  2279  nfsbv  2341  sb4b  2495  sb4bOLD  2496  bj-ssbeq  33884  bj-ssbid2ALT  33894  bj-ssbid1ALT  33896
  Copyright terms: Public domain W3C validator