2.1.13: Extensionality

From LibreTexts, under CC BY, as the source states it; its equations are written in TeX, which the PDF shows typeset. This page at LibreTexts.

$\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$.

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}$.
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}$.
If $t \ident x$, then $\Subst{t}{t'}{x} = t'$. But $\Value[s']{x}{M} = \Value[s]{t'}{M}$ by definition of $s'$.
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}$.

This page titled 2.1.13: Extensionality was last modified on Fri, 08 Mar 2024 05:56:26 GMT and is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .

Contents

Text

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

Problem \(\PageIndex{1}\)

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

Proposition \(\PageIndex{2}\)

Proposition \(\PageIndex{3}\)

Problem \(\PageIndex{2}\)