2.6.6: Construction of a Model

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

Right now we are not concerned about \(\eq[][]\), i.e., we only want to show that a consistent set \(\Gamma\) of sentences not containing \(\eq[][]\) is satisfiable. We first extend \(\Gamma\) to a consistent, complete, and saturated set \(\Gamma^*\). In this case, the definition of a model \(\Struct{M(\Gamma^*)}\) is simple: We take the set of closed terms of \(\Lang{L'}\) as the domain. We assign every constant symbol to itself, and make sure that more generally, for every closed term \(t\), \(\Value{t}{M(\Gamma^*)} = t\). The predicate symbols are assigned extensions in such a way that an atomic sentence is true in \(\Struct{M(\Gamma^*)}\) iff it is in \(\Gamma^*\). This will obviously make all the atomic sentences in \(\Gamma^*\) true in \(\Struct{M(\Gamma^*)}\). The rest are true provided the \(\Gamma^*\) we start with is consistent, complete, and saturated.

Definition \(\PageIndex{1}\): Term model

Let \(\Gamma^*\) be a complete and consistent, saturated set of sentences in a language \(\Lang L\). The term model \(\Struct M(\Gamma^*)\) of \(\Gamma^*\) is the structure defined as follows:

1. The domain \(\Domain{M(\Gamma^*)}\) is the set of all closed terms of \(\Lang L\).
2. The interpretation of a constant symbol \(c\) is \(c\) itself: \(\Assign{c}{M(\Gamma^*)} = c\).
3. The function symbol \(f\) is assigned the function which, given as arguments the closed terms \(t_1\), …, \(t_n\), has as value the closed term \(f(t_1, \dots, t_n)\): \[\Assign{f}{M(\Gamma^*)}(t_1, \dots, t_n) = f(t_1,\dots, t_n)\nonumber\]
4. If \(R\) is an \(n\)-place predicate symbol, then \[\tuple{t_1, \dots, t_n} \in \Assign{R}{M(\Gamma^*)} \text{ iff } \Atom{R}{t_1, \dots, t_n} \in \Gamma^*.\nonumber\]

A structure \(\Struct{M}\) may make an existentially quantified sentence \(\lexists{x}{A(x)}\) true without there being an instance \(A(t)\) that it makes true. A structure \(\Struct{M}\) may make all instances \(A(t)\) of a universally quantified sentence \(\lforall{x}{A(x)}\) true, without making \(\lforall{x}{A(x)}\) true. This is because in general not every element of \(\Domain{M}\) is the value of a closed term (\(\Struct{M}\) may not be covered). This is the reason the satisfaction relation is defined via variable assignments. However, for our term model \(\Struct{M(\Gamma^*)}\) this wouldn’t be necessary—because it is covered. This is the content of the next result.

Proposition \(\PageIndex{1}\)

Let \(\Struct M(\Gamma^*)\) be the term model of Definition \(\PageIndex{1}\).

1. \(\Sat{M(\Gamma^*)}{\lexists{x}{A(x)}}\) iff \(\Sat{M}{A(t)}\) for at least one term \(t\).
2. \(\Sat{M(\Gamma^*)}{\lforall{x}{A(x)}}\) iff \(\Sat{M}{A(t)}\) for all terms \(t\).

Proof.

1. By Proposition 5.12.4, \(\Sat{M(\Gamma^*)}{\lexists{x}{A(x)}}\) iff for at least one variable assignment \(s\), \(\Sat[,s]{M(\Gamma^*)}{A(x)}\). As \(\Domain{M(\Gamma^*)}\) consists of the closed terms of \(\Lang{L}\), this is the case iff there is at least one closed term \(t\) such that \(s(x) = t\) and \(\Sat[,s]{M(\Gamma^*)}{A(x)}\). By Proposition 5.13.3, \(\Sat[,s]{M(\Gamma^*)}{A(x)}\) iff \(\Sat[,s]{M(\Gamma^*)}{A(t)}\), where \(s(x) = t\). By Proposition 5.12.3, \(\Sat[,s]{M(\Gamma^*)}{A(t)}\) iff \(\Sat{M(\Gamma^*)}{A(t)}\), since \(A(t)\) is a sentence.
2. Exercise.

◻

Problem \(\PageIndex{1}\)

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

Lemma \(\PageIndex{1}\): Truth Lemma

Suppose \(A\) does not contain \(\eq[][]\). Then \(\Sat{M(\Gamma^*)}{A}\) iff \(A \in \Gamma^*\).

Proof. We prove both directions simultaneously, and by induction on \(A\).

1. \(\indcase{A}{\lfalse}\) \({\SatN{M(\Gamma^*)}{\lfalse}}\) by definition of satisfaction. On the other hand, \(\lfalse \notin \Gamma^*\) since \(\Gamma^*\) is consistent.
2. \(\indcase{A}{R(t_1, \dots, t_n)}\) \(\Sat{M(\Gamma^*)}{\Atom{R}{t_1, \dots, t_n}}\) iff \(\tuple{t_1, \dots, t_n} \in \Assign{R}{M(\Gamma^*)}\) (by the definition of satisfaction) iff \(R(t_1, \dots, t_n) \in \Gamma^*\) (by the construction of \(\Struct M(\Gamma^*)\)).
3. \(\indcase{A}{\lnot B}\) \(\Sat{M(\Gamma^*)}{\indfrm}\) iff \({\SatN{M(\Gamma^*)}{B}}\) (by definition of satisfaction). By induction hypothesis, \({\SatN{M(\Gamma^*)}{B}}\) iff \(B \notin \Gamma^*\). Since \(\Gamma^*\) is consistent and complete, \(B \notin \Gamma^*\) iff \(\lnot B \in \Gamma^*\).
4. \(\indcase{A}{B \land C}\) exercise.
5. \(\indcase{A}{B \lor C}\) \(\Sat{M(\Gamma^*)}{\indfrm}\) iff \(\Sat{M(\Gamma^*)}{B}\) or \(\Sat{M(\Gamma^*)}{C}\) (by definition of satisfaction) iff \(B \in \Gamma^*\) or \(C \in \Gamma^*\) (by induction hypothesis). This is the case iff \((B \lor C) \in \Gamma^*\) (by Proposition 10.3.1(3)).
6. \(\indcase{A}{B \lif C}\) exercise.
7. \(\indcase{A}{\lforall{x}{B(x)}}\) exercise.
8. \(\indcase{A}{\lexists{x}{B(x)}}\) \(\Sat{M(\Gamma^*)}{\indfrm}\) iff \(\Sat{M(\Gamma^*)}{B(t)}\) for at least one term \(t\) (Proposition \(\PageIndex{1}\)). By induction hypothesis, this is the case iff \(B(t) \in \Gamma^*\) for at least one term \(t\). By Proposition 10.4.2, this in turn is the case iff \(\lexists{x}{B(x)} \in \Gamma^*\).

◻

Problem \(\PageIndex{2}\)

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