2.1.8: Substitution

\(\def\Assign#1#2{ { #1^{\Struct{#2}} } }\)
\(\def\Atom#1#2{ { \mathord{#1}(#2) } }\)
\(\def\Bin{ {\mathbb{B}} }\)
\(\def\cardeq#1#2{ { #1 \approx #2 } }\)
\(\def\cardle#1#2{ { #1 \preceq #2 } }\)
\(\def\cardless#1#2{ { #1 \prec #2 } }\)
\(\def\cardneq#1#2{ { #1 \not\approx #2 } }\)
\(\def\comp#1#2{ { #2 \circ #1 } }\)
\(\def\concat{ { \;\frown\; } }\)
\(\def\Cut{ { \text{Cut} } }\)
\(\def\Discharge#1#2{ { [#1]^#2 } }\)
\(\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }\)
\(\def\dom#1{ {\operatorname{dom}(#1)} }\)
\(\def\Domain#1{ {\left| \Struct{#1} \right|} }\)
\(\def\Elim#1{ { {#1}\mathrm{Elim} } }\)
\(\newcommand{\Entails}{\vDash}\)
\(\newcommand{\EntailsN}{\nvDash}\)
\(\def\eq[#1][#2]{ { #1 = #2 } }\)
\(\def\eqN[#1][#2]{ { #1 \neq #2 } }\)
\(\def\equivclass#1#2{ { #1/_{#2} } }\)
\(\def\equivrep#1#2{ { [#1]_{#2} } }\)
\(\def\Exchange{ { \text{X} } }\)
\(\def\False{ { \mathbb{F} } }\)
\(\def\FalseCl{ { \lfalse_C } }\)
\(\def\FalseInt{ { \lfalse_I } }\)
\(\def\fCenter{ { \,\Sequent\, } }\)
\(\def\fdefined{ { \;\downarrow } }\)
\(\def\fn#1{ { \operatorname{#1} } }\)
\(\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }\)
\(\def\fundefined{ { \;\uparrow } }\)
\(\def\funimage#1#2{ { #1[#2] } }\)
\(\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }\)
\(\newcommand{\ident}{\equiv}\)
\(\newcommand{\indcase}[2]{#1 \ident #2\text{:}}\)
\(\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}\)
\(\def\indfrm{ { A } }\)
\(\def\indfrmp{ { A } }\)
\(\def\joinrel{\mathrel{\mkern-3mu}}\)
\(\def\lambd[#1][#2]{\lambda #1 . #2}\)
\(\def\Lang#1{ { \mathcal{#1} } }\)
\(\def\LeftR#1{ { {#1}\mathrm{L} } }\)
\(\def\len#1{ {\operatorname{len}(#1)} }\)
\(\def\lexists#1#2{ { \exists #1\, #2 } }\)
\(\def\lfalse{ {\bot} }\)
\(\def\lforall#1#2{ { \forall#1\, #2 } }\)
\(\newcommand{\lif}{\rightarrow}\)
\(\newcommand{\liff}{\leftrightarrow}\)
\(\def\Log#1{ { \mathbf{#1} } }\)
\(\def\ltrue{ {\top} }\)
\(\def\Id#1{ {\operatorname{Id}_#1} }\)
\(\def\Int{ {\mathbb{Z}} }\)
\(\def\Intro#1{ { {#1}\mathrm{Intro} } }\)
\(\def\mModel#1{ { \mathfrak{#1} } }\)
\(\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}\)
\(\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}\)
\(\def\Nat{ {\mathbb{N}} }\)
\(\def\nicefrac#1#2{ {{}^#1/_#2} }\)
\(\def\num#1{ { \overline{#1} } }\)

\(\def\ran#1{ {\operatorname{ran}(#1)} }\)
\(\newcommand{\Obj}[1]{\mathsf{#1}}\)
\(\def\Rat{ {\mathbb{Q}} }\)
\(\def\Real{ {\mathbb{R}} }\)
\(\def\RightR#1{ { {#1}\mathrm{R} } }\)
\(\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }\)
\(\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }\)
\(\def\PosInt{ {\mathbb{Z}^+} }\)
\(\def\Pow#1{ {\wp(#1)} }\)
\(\newcommand{\Proves}{\vdash}\)
\(\newcommand{\ProvesN}{\nvdash}\)
\(\def\Relbar{\mathrel{=}}\)
\(\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}\)
\(\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}\)
\(\newcommand{\Sequent}{\Rightarrow}\)
\(\def\Setabs#1#2{ { \{#1:#2\} } }\)
\(\newcommand{\sFmla}[2]{#1\,#2}\)
\(\def\Struct#1{ {#1} }\)
\(\def\subst#1#2{ { #1/#2 } }\)
\(\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }\)
\(\def\TMblank{ { 0 } }\)
\(\newcommand{\TMendtape}{\triangleright}\)
\(\def\TMleft{ { L } }\)
\(\def\TMright{ { R } }\)
\(\def\TMstay{ { N } }\)
\(\def\TMstroke{ { 1 } }\)
\(\def\TMtrans#1#2#3{ { #1,#2,#3 } }\)
\(\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }\)
\(\def\True{ { \mathbb{T} } }\)
\(\newcommand{\TRule}[2]{#2#1}\)
\(\def\tuple#1{ {\langle #1 \rangle} }\)
\(\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}\)
\(\def\Var{ { \mathrm{Var} } }\)
\(\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}\)
\(\def\Weakening{ { \text{W} } }\)

Definition \(\PageIndex{1}\): Substitution in a term

We define \(\Subst{s}{t}{x}\), the result of substituting \(t\) for every occurrence of \(x\) in \(s\), recursively:

1. \(\indcase{s}{c}\) \(\Subst{s}{t}{x}\) is just \(s\).
2. \(\indcase{s}{y}\) \(\Subst{s}{t}{x}\) is also just \(s\), provided \(y\) is a variable and \(y \not\ident x\).
3. \(\indcase{s}{x}\) \(\Subst{s}{t}{x}\) is \(t\).
4. \(\indcase{s}{\Atom{f}{t_1, \dots, t_n}}\) \(\Subst{s}{t}{x}\) is \(\Atom{f}{\Subst{t_1}{t}{x}, \dots, \Subst{t_n}{t}{x}}\).

Definition \(\PageIndex{2}\)

A term \(t\) is free for \(x\) in \(A\) if none of the free occurrences of \(x\) in \(A\) occur in the scope of a quantifier that binds a variable in \(t\).

Example \(\PageIndex{1}\)

1. \(\Obj v_8\) is free for \(\Obj v_1\) in \(\lexists{\Obj v_3}{}\Atom{\Obj A^2_4}{\Obj v_3,\Obj v_1}\)
2. \(\Obj f^2_1(\Obj v_1, \Obj v_2)\) is not free for \(\Obj v_0\) in \(\lforall{\Obj v_2}{}\Atom{\Obj A^2_4}{\Obj v_0,\Obj v_2}\)

Definition \(\PageIndex{3}\): Substitution in a formula

If \(A\) is a formula, \(x\) is a variable, and \(t\) is a term free for \(x\) in \(A\), then \(\Subst{A}{t}{x}\) is the result of substituting \(t\) for all free occurrences of \(x\) in \(A\).

1. \(\indcase{A}{\lfalse}\) \(\Subst{\indfrm}{t}{x}\) is \(\lfalse\).
2. \(\indcase{A}{\Atom{P}{t_1,\dots, t_n}}\) \(\Subst{\indfrm}{t}{x}\) is \(\Atom{P}{\Subst{t_1}{t}{x}, \dots, \Subst{t_n}{t}{x}}\).
3. \(\indcase{A}{\eq[t_1][t_2]}\) \(\Subst{\indfrmp}{t}{x}\) is \(\Subst{t_1}{t}{x} = \Subst{t_2}{t}{x}\).
4. \(\indcase{A}{\lnot B}\) \(\Subst{\indfrmp}{t}{x}\) is \(\lnot \Subst{B}{t}{x}\).
5. \(\indcase{A}{(B \land C)}\) \(\Subst{\indfrmp}{t}{x}\) is \((\Subst{B}{t}{x} \land \Subst{C}{t}{x})\).
6. \(\indcase{A}{(B \lor C)}\) \(\Subst{\indfrmp}{t}{x}\) is \((\Subst{B}{t}{x} \lor \Subst{C}{t}{x})\).
7. \(\indcase{A}{(B \lif C)}\) \(\Subst{\indfrmp}{t}{x}\) is \((\Subst{B}{t}{x} \lif \Subst{C}{t}{x})\).
8. \(\indcase{A}{\lforall{y}{B}}\) \(\Subst{\indfrmp}{t}{x}\) is \(\lforall{y}{\Subst{B}{t}{x}}\), provided \(y\) is a variable other than \(x\); otherwise \(\Subst{\indfrmp}{t}{x}\) is just \(\indfrm\).
9. \(\indcase{A}{\lexists{y}{B}}\) \(\Subst{\indfrmp}{t}{x}\) is \(\lexists{y}{\Subst{B}{t}{x}}\), provided \(y\) is a variable other than \(x\); otherwise \(\Subst{\indfrmp}{t}{x}\) is just \(\indfrm\).

Note that substitution may be vacuous: If \(x\) does not occur in \(A\) at all, then \(\Subst{A}{t}{x}\) is just \(A\).

The restriction that \(t\) must be free for \(x\) in \(A\) is necessary to exclude cases like the following. If \(A \ident \lexists{y}{x < y}\) and \(t \ident y\), then \(\Subst{A}{t}{x}\) would be \(\lexists{y}{y < y}\). In this case the free variable \(y\) is “captured” by the quantifier \(\lexists{y}{}\) upon substitution, and that is undesirable. For instance, we would like it to be the case that whenever \(\lforall{x}{B}\) holds, so does \(\Subst{B}{t}{x}\). But consider \(\lforall{x}{\lexists{y}{x < y}}\) (here \(B\) is \(\lexists{y}{x < y}\)). It is sentence that is true about, e.g., the natural numbers: for every number \(x\) there is a number \(y\) greater than it. If we allowed \(y\) as a possible substitution for \(x\), we would end up with \(\Subst{B}{y}{x} \ident \lexists{y}{y < y}\), which is false. We prevent this by requiring that none of the free variables in \(t\) would end up being bound by a quantifier in \(A\).

We often use the following convention to avoid cumbersume notation: If \(A\) is a formula with a free variable \(x\), we write \(A(x)\) to indicate this. When it is clear which \(A\) and \(x\) we have in mind, and \(t\) is a term (assumed to be free for \(x\) in \(A(x)\)), then we write \(A(t)\) as short for \(\Subst{A(x)}{t}{x}\).