Definition df-sb 2069

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 elsb2 2131.

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 2179 and sbid2v 2512).

Note that our definition is valid even when 𝑥 and 𝑡 are replaced with the same variable, as sbid 2261 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 2284 with respect to sb5 2281. We can also achieve this by having 𝑥 free in the first conjunct and bound in the second, as the alternate definition dfsb1 2484 shows. Another version that mixes free and bound variables is dfsb3 2497. When 𝑥 and 𝑡 are distinct, we can express proper substitution with the simpler expressions of sb5 2281 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.

The hypothesis asserts that the definition is independent of the particular choice of the dummy variable 𝑦. Without this hypothesis, sbjust 2067 would be derivable from propositional axioms alone: one could apply the definiens for [𝑡 / 𝑥]𝜑 twice, using different dummy variables 𝑦 and 𝑧, and then invoke bitr3i 277 to establish their equivalence. This would jeopardize the independence of axioms, as demonstrated in an analoguous situation involving df-ss 3917 to prove ax-8 2116 (see in-ax8 36397).

Prefer dfsb 2070 unless you can prove the hypothesis from fewer axioms in special cases, see sbt 2072. (Contributed by NM, 10-May-1993.) Revised from the original definition dfsb1 2484. (Revised by BJ, 22-Dec-2020.) Add the justification hypothesis. (Revised by Wolf Lammen, 4-Feb-2026.)

Hypothesis

Ref	Expression
sbjust.1	⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))

Assertion

Ref	Expression
df-sb	⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

Distinct variable groups:   𝑥,𝑦,𝑧   𝑦,𝑡,𝑧   𝜑,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑡)

Detailed syntax breakdown of Definition df-sb

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		vt	. . 3 setvar 𝑡
4	1, 2, 3	wsb 2068	. 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 1540	. . . 4 wff ∀𝑥(𝑥 = 𝑦 → 𝜑)
10	6, 9	wi 4	. . 3 wff (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
11	10, 5	wal 1540	. 2 wff ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
12	4, 11	wb 206	1 wff ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

This definition is referenced by:  dfsb  2070  sbt  2072