2.6.7: Identity

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

The construction of the term model given in the preceding section is enough to establish completeness for first-order logic for sets \(\Gamma\) that do not contain \(\eq[][]\). The term model satisfies every \(A \in \Gamma^*\) which does not contain \(\eq[][]\) (and hence all \(A \in \Gamma\)). It does not work, however, if \(\eq[][]\) is present. The reason is that \(\Gamma^*\) then may contain a sentence \(\eq[t][t']\), but in the term model the value of any term is that term itself. Hence, if \(t\) and \(t'\) are different terms, their values in the term model—i.e., \(t\) and \(t'\), respectively—are different, and so \(\eq[t][t']\) is false. We can fix this, however, using a construction known as “factoring.”

Definition \(\PageIndex{1}\)

Let \(\Gamma^*\) be a consistent and complete set of sentences in \(\Lang L\). We define the relation \(\approx\) on the set of closed terms of \(\Lang L\) by \[t \approx t' \quad\text{ iff }\quad \eq[t][t'] \in \Gamma^*\nonumber\]

Proposition \(\PageIndex{1}\)

The relation \(\approx\) has the following properties:

1. \(\approx\) is reflexive.
2. \(\approx\) is symmetric.
3. \(\approx\) is transitive.
4. If \(t \approx t'\), \(f\) is a function symbol, and \(t_1\), …, \(t_{i-1}\), \(t_{i+1}\), …, \(t_n\) are terms, then \[\Atom{f}{t_1,\dots, t_{i-1}, t, t_{i+1}, \dots, t_n} \approx \Atom{f}{t_1,\dots, t_{i-1}, t', t_{i+1}, \dots, t_n}.\nonumber\]
5. If \(t \approx t'\), \(R\) is a predicate symbol, and \(t_1\), …, \(t_{i-1}\), \(t_{i+1}\), …, \(t_n\) are terms, then \[\begin{gathered} \Atom{R}{t_1,\dots, t_{i-1}, t, t_{i+1}, \dots, t_n} \in \Gamma^* \text{ iff } \\ \Atom{R}{t_1,\dots, t_{i-1}, t', t_{i+1}, \dots, t_n} \in \Gamma^*.\end{gathered}\]

Proof. Since \(\Gamma^*\) is consistent and complete, \(\eq[t][t'] \in \Gamma^*\) iff \(\Gamma^* \Proves \eq[t][t']\). Thus it is enough to show the following:

1. \(\Gamma^* \Proves \eq[t][t]\) for all terms \(t\).
2. If \(\Gamma^* \Proves \eq[t][t']\) then \(\Gamma^* \Proves \eq[t'][t]\).
3. If \(\Gamma^* \Proves \eq[t][t']\) and \(\Gamma^* \Proves \eq[t'][t'']\), then \(\Gamma^* \Proves \eq[t][t'']\).
4. If \(\Gamma^* \Proves \eq[t][t']\), then \[\Gamma^* \Proves \eq[\Atom{f}{t_1,\dots,t_{i-1},t,t_{i+1},,\dots,t_n}][\Atom{f}{t_1,\dots,t_{i-1},t',t_{i+1},\dots,t_n}]\nonumber\] for every \(n\)-place function symbol \(f\) and terms \(t_1\), …, \(t_{i-1}\), \(t_{i+1}\), …, \(t_n\).
5. If \(\Gamma^* \Proves \eq[t][t']\) and \(\Gamma^* \Proves \Atom{R}{t_1,\dots,t_{i-1},t,t_{i+1},\dots,t_n}\), then \(\Gamma^* \Proves \Atom{R}{t_1,\dots,t_{i-1},t',t_{i+1},\dots,t_n}\) for every \(n\)-place predicate symbol \(R\) and terms \(t_1\), …, \(t_{i-1}\), \(t_{i+1}\), …, \(t_n\).

◻

Problem \(\PageIndex{1}\)

Complete the proof of Proposition \(\PageIndex{1}\).

Definition \(\PageIndex{2}\)

Suppose \(\Gamma^*\) is a consistent and complete set in a language \(\Lang L\), \(t\) is a term, and \(\approx\) as in the previous definition. Then: \[\equivrep{t}{\approx} = \Setabs{t'}{t'\in \Trm[L], t \approx t'}\nonumber\] and \(\equivclass{\Trm[L]}{\approx} = \Setabs{\equivrep{t}{\approx}}{t \in \Trm[L]}\).

Definition \(\PageIndex{3}\)

Let \(\Struct M = \Struct M(\Gamma^*)\) be the term model for \(\Gamma^*\). Then \(\Struct{\equivclass{M}{\approx}}\) is the following structure:

1. \(\Domain{\equivclass{M}{\approx}} = \equivclass{\Trm[L]}{\approx}\).
2. \(\Assign{c}{\equivclass{M}{\approx}} = \equivrep{c}{\approx}\)
3. \(\Assign{f}{\equivclass{M}{\approx}}(\equivrep{t_1}{\approx}, \dots, \equivrep{t_n}{\approx}) = \equivrep{\Atom{f}{t_1,\dots, t_n}}{\approx}\)
4. \(\tuple{\equivrep{t_1}{\approx}, \dots, \equivrep{t_n}{\approx}} \in \Assign{R}{\equivclass{M}{\approx}}\) iff \(\Sat{M}{\Atom{R}{t_1,\dots, t_n}}\).

Note that we have defined \(\Assign{f}{\equivclass{M}{\approx}}\) and \(\Assign{R}{\equivclass{M}{\approx}}\) for elements of \(\equivclass{\Trm[L]}{\approx}\) by referring to them as \(\equivrep{t}{\approx}\), i.e., via representatives \(t \in \equivrep{t}{\approx}\). We have to make sure that these definitions do not depend on the choice of these representatives, i.e., that for some other choices \(t'\) which determine the same equivalence classes (\(\equivrep{t}{\approx} = \equivrep{t'}{\approx}\)), the definitions yield the same result. For instance, if \(R\) is a one-place predicate symbol, the last clause of the definition says that \(\equivrep{t}{\approx} \in \Assign{R}{\equivclass{M}{\approx}}\) iff \(\Sat{M}{\Atom{R}{t}}\). If for some other term \(t'\) with \(t \approx t'\), \(\SatN{M}{\Atom{R}{t}}\), then the definition would require \(\equivrep{t'}{\approx} \notin \Assign{R}{\equivclass{M}{\approx}}\). If \(t \approx t'\), then \(\equivrep{t}{\approx} = \equivrep{t'}{\approx}\), but we can’t have both \(\equivrep{t}{\approx} \in \Assign{R}{\equivclass{M}{\approx}}\) and \(\equivrep{t}{\approx} \notin \Assign{R}{\equivclass{M}{\approx}}\). However, Proposition \(\PageIndex{1}\) guarantees that this cannot happen.

Proposition \(\PageIndex{2}\)

\(\Struct{\equivclass{M}{\approx}}\) is well defined, i.e., if \(t_1\), …, \(t_n\), \(t_1'\), …, \(t_n'\) are terms, and \(t_i \approx t_i'\) then

1. \(\equivrep{\Atom{f}{t_1,\dots, t_n}}{\approx} = \equivrep{\Atom{f}{t_1',\dots, t_n'}}{\approx}\), i.e., \[\Atom{f}{t_1,\dots, t_n} \approx \Atom{f}{t_1',\dots, t_n'}\nonumber\] and
2. \(\Sat{M}{\Atom{R}{t_1,\dots, t_n}}\) iff \(\Sat{M}{\Atom{R}{t_1',\dots, t_n'}}\), i.e., \[\Atom{R}{t_1,\dots, t_n} \in \Gamma^* \text{ iff } \Atom{R}{t_1',\dots, t_n'} \in \Gamma^*.\nonumber\]

Proof. Follows from Proposition \(\PageIndex{1}\) by induction on \(n\). ◻

Lemma \(\PageIndex{1}\)

\(\Sat{\equivclass{M}{\approx}}{A}\) iff \(A \in \Gamma^*\) for all sentences \(A\).

Proof. By induction on \(A\), just as in the proof of Lemma \(\PageIndex{1}\). The only case that needs additional attention is when \(A \ident \eq[t][t']\). \[\begin{aligned} \Sat{\equivclass{M}{\approx}}{\eq[t][t']} & \text{ iff } \equivrep{t}{\approx} = \equivrep{t'}{\approx} \text{ (by definition of $\Struct{\equivclass{M}{\approx}}$)}\\ & \text{ iff } t \approx t' \text{ (by definition of $\equivrep{t}{\approx}$)}\\ & \text{ iff } \eq[t][t'] \in \Gamma^* \text{ (by definition of $\approx$).}\end{aligned}\] ◻

Note that while \(\Struct{M(\Gamma^*)}\) is always enumerable and infinite, \(\Struct{\equivclass{M}{\approx}}\) may be finite, since it may turn out that there are only finitely many classes \(\equivrep{t}{\approx}\). This is to be expected, since \(\Gamma\) may contain sentences which require any structure in which they are true to be finite. For instance, \(\lforall{x}{\lforall{y}{x = y}}\) is a consistent sentence, but is satisfied only in structures with a domain that contains exactly one element.