Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-sb | Structured version Visualization version GIF version |
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 2128.
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 2089, sbcom2 2166 and sbid2v 2531). Note that our definition is valid even when 𝑥 and 𝑡 are replaced with the same variable, as sbid 2256 shows. We achieve this by applying twice Tarski's definition sb6 2091 which is valid for disjoint variables, and introducing a dummy variable 𝑦 which isolates 𝑥 from 𝑡, as in dfsb7 2283 with respect to sb5 2275. We can also achieve this by having 𝑥 free in the first conjunct and bound in the second, as the alternate definition dfsb1 2502 shows. Another version that mixes free and bound variables is dfsb3 2515. When 𝑥 and 𝑡 are distinct, we can express proper substitution with the simpler expressions of sb5 2275 and sb6 2091. 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 2502. (Revised by BJ, 22-Dec-2020.) |
Ref | Expression |
---|---|
df-sb | ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vt | . . 3 setvar 𝑡 | |
4 | 1, 2, 3 | wsb 2069 | . 2 wff [𝑡 / 𝑥]𝜑 |
5 | vy | . . . . 5 setvar 𝑦 | |
6 | 5, 3 | weq 1964 | . . . 4 wff 𝑦 = 𝑡 |
7 | 2, 5 | weq 1964 | . . . . . 6 wff 𝑥 = 𝑦 |
8 | 7, 1 | wi 4 | . . . . 5 wff (𝑥 = 𝑦 → 𝜑) |
9 | 8, 2 | wal 1536 | . . . 4 wff ∀𝑥(𝑥 = 𝑦 → 𝜑) |
10 | 6, 9 | wi 4 | . . 3 wff (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
11 | 10, 5 | wal 1536 | . 2 wff ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
12 | 4, 11 | wb 209 | 1 wff ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
Colors of variables: wff setvar class |
This definition is referenced by: sbt 2071 stdpc4 2073 sbi1 2076 spsbe 2087 spsbeOLD 2088 sbequ 2089 sb6 2091 sbal 2164 hbsbw 2174 sbequ1 2248 sbequ2 2249 sbequ2OLD 2250 dfsb7 2283 dfsb7OLD 2284 sbn 2285 nfsbv 2341 sb4b 2491 sb4bOLD 2492 cbvabw 2870 bj-ssbeq 34094 bj-ssbid2ALT 34104 bj-ssbid1ALT 34106 |
Copyright terms: Public domain | W3C validator |