2.1.13: Extensionality

\(\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} } }\)

Extensionality, sometimes called relevance, can be expressed informally as follows: the only factors that bears upon the satisfaction of formula \(A\) in a structure \(\Struct M\) relative to a variable assignment \(s\), are the size of the domain and the assignments made by \(\Struct M\) and \(s\) to the elements of the language that actually appear in \(A\).

One immediate consequence of extensionality is that where two structures \(\Struct M\) and \(\Struct M'\) agree on all the elements of the language appearing in a sentence \(A\) and have the same domain, \(\Struct M\) and \(\Struct M'\) must also agree on whether or not \(A\) itself is true.

Proposition \(\PageIndex{1}\): Extensionality

Let \(A\) be a formula, and \(\Struct M_1\) and \(\Struct M_2\) be structures with \(\Domain{M_1} = \Domain{M_2}\), and \(s\) a variable assignment on \(\Domain{M_1} = \Domain{M_2}\). If \(\Assign{c}{M_1} = \Assign{c}{M_2}\), \(\Assign{R}{M_1}=\Assign{R}{M_2}\), and \(\Assign{f}{M_1} = \Assign{f}{M_2}\) for every constant symbol \(c\), relation symbol \(R\), and function symbol \(f\) occurring in \(A\), then \(\Sat[,s]{M_1}{A}\) iff \(\Sat[,s]{M_2}{A}\).

Proof. First prove (by induction on \(t\)) that for every term, \(\Value[s]{t}{M_1} = \Value[s]{t}{M_2}\). Then prove the proposition by induction on \(A\), making use of the claim just proved for the induction basis (where \(A\) is atomic). ◻

Problem \(\PageIndex{1}\)

Carry out the proof of Proposition \(\PageIndex{1}\) in detail.

Corollary \(\PageIndex{1}\): Extensionality for Sentences

Let \(A\) be a sentence and \(\Struct{M_1}\), \(\Struct{M_2}\) as in Proposition \(\PageIndex{1}\). Then \(\Sat{M_1}{A}\) iff \(\Sat{M_2}{A}\).

Proof. Follows from Proposition \(\PageIndex{1}\) by Corollary 5.12.1. ◻

Moreover, the value of a term, and whether or not a structure satisfies a formula, only depends on the values of its subterms.

Proposition \(\PageIndex{2}\)

Let \(\Struct M\) be a structure, \(t\) and \(t'\) terms, and \(s\) a variable assignment. Let \(\varAssign{s'}{s}{x}\) be the \(x\)-variant of \(s\) given by \(s'(x) = \Value[s]{t'}{M}\). Then \(\Value[s]{\Subst{t}{t'}{x}}{M} = \Value[s']{t}{M}\).

Proof. By induction on \(t\).

1. If \(t\) is a constant, say, \(t\ident c\), then \(\Subst{t}{t'}{x} = c\), and \(\Value[s]{c}{M} = \Assign{c}{M} = \Value[s']{c}{M}\).
2. If \(t\) is a variable other than \(x\), say, \(t \ident y\), then \(\Subst{t}{t'}{x} = y\), and \(\Value[s]{y}{M} = \Value[s']{y}{M}\) since \(\varAssign{s'}{s}{x}\).
3. If \(t \ident x\), then \(\Subst{t}{t'}{x} = t'\). But \(\Value[s']{x}{M} = \Value[s]{t'}{M}\) by definition of \(s'\).
4. If \(t \ident \Atom{f}{t_1,\dots,t_n}\) then we have: \[\begin{gathered} \begin{aligned}[b] \Value[s]{\Subst{t}{t'}{x}}{M} & = \Value[s]{\Atom{f}{\Subst{t_1}{t'}{x}, \dots, \Subst{t_n}{t'}{x}}}{M}\\ & \qquad \text{ by definition of $\Subst{t}{t'}{x}$}\\ & = \Assign{f}{M}(\Value[s]{\Subst{t_1}{t'}{x}}{M}, \dots, \Value[s]{\Subst{t_n}{t'}{x}}{M})\\ & \qquad \text{ by definition of $\Value[s]{\Atom{f}{\dots}}{M}$}\\ & = \Assign{f}{M}(\Value[s']{t_1}{M}, \dots, \Value[s']{t_n}{M})\\ & \qquad \text{ by induction hypothesis}\\ & = \Value[s']{t}{M} \text{ by definition of $\Value[s']{\Atom{f}{\dots}}{M}$} \end{aligned}\end{gathered}\]

◻

Proposition \(\PageIndex{3}\)

Let \(\Struct M\) be a structure, \(A\) a formula, \(t\) a term, and \(s\) a variable assignment. Let \(\varAssign{s'}{s}{x}\) be the \(x\)-variant of \(s\) given by \(s'(x) = \Value[s]{t}{M}\). Then \(\Sat[,s]{M}{\Subst{A}{t}{x}}\) iff \(\Sat[,s']{M}{A}\).

Proof. Exercise. ◻

Problem \(\PageIndex{2}\)

Prove Proposition \(\PageIndex{3}\).