5.12: Variable Assignments

Last updated
Save as PDF

Page ID: 52853

$ \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } $

$ \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} $

$ \newcommand{\id}{\mathrm{id}}$ $ \newcommand{\Span}{\mathrm{span}}$

( \newcommand{\kernel}{\mathrm{null}\,}\) $ \newcommand{\range}{\mathrm{range}\,}$

$ \newcommand{\RealPart}{\mathrm{Re}}$ $ \newcommand{\ImaginaryPart}{\mathrm{Im}}$

$ \newcommand{\Argument}{\mathrm{Arg}}$ $ \newcommand{\norm}[1]{\| #1 \|}$

$ \newcommand{\inner}[2]{\langle #1, #2 \rangle}$

$ \newcommand{\Span}{\mathrm{span}}$

$ \newcommand{\id}{\mathrm{id}}$

$ \newcommand{\Span}{\mathrm{span}}$

$ \newcommand{\kernel}{\mathrm{null}\,}$

$ \newcommand{\range}{\mathrm{range}\,}$

$ \newcommand{\RealPart}{\mathrm{Re}}$

$ \newcommand{\ImaginaryPart}{\mathrm{Im}}$

$ \newcommand{\Argument}{\mathrm{Arg}}$

$ \newcommand{\norm}[1]{\| #1 \|}$

$ \newcommand{\inner}[2]{\langle #1, #2 \rangle}$

$ \newcommand{\Span}{\mathrm{span}}$ $ \newcommand{\AA}{\unicode[.8,0]{x212B}}$

$ \newcommand{\vectorA}[1]{\vec{#1}} % arrow$

$ \newcommand{\vectorAt}[1]{\vec{\text{#1}}} % arrow$

$ \newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } $

$ \newcommand{\vectorC}[1]{\textbf{#1}} $

$ \newcommand{\vectorD}[1]{\overrightarrow{#1}} $

$ \newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}} $

$ \newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}} $

$ \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } $

$ \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} $

$\newcommand{\avec}{\mathbf a}$ $\newcommand{\bvec}{\mathbf b}$ $\newcommand{\cvec}{\mathbf c}$ $\newcommand{\dvec}{\mathbf d}$ $\newcommand{\dtil}{\widetilde{\mathbf d}}$ $\newcommand{\evec}{\mathbf e}$ $\newcommand{\fvec}{\mathbf f}$ $\newcommand{\nvec}{\mathbf n}$ $\newcommand{\pvec}{\mathbf p}$ $\newcommand{\qvec}{\mathbf q}$ $\newcommand{\svec}{\mathbf s}$ $\newcommand{\tvec}{\mathbf t}$ $\newcommand{\uvec}{\mathbf u}$ $\newcommand{\vvec}{\mathbf v}$ $\newcommand{\wvec}{\mathbf w}$ $\newcommand{\xvec}{\mathbf x}$ $\newcommand{\yvec}{\mathbf y}$ $\newcommand{\zvec}{\mathbf z}$ $\newcommand{\rvec}{\mathbf r}$ $\newcommand{\mvec}{\mathbf m}$ $\newcommand{\zerovec}{\mathbf 0}$ $\newcommand{\onevec}{\mathbf 1}$ $\newcommand{\real}{\mathbb R}$ $\newcommand{\twovec}[2]{\left[\begin{array}{r}#1 \\ #2 \end{array}\right]}$ $\newcommand{\ctwovec}[2]{\left[\begin{array}{c}#1 \\ #2 \end{array}\right]}$ $\newcommand{\threevec}[3]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \end{array}\right]}$ $\newcommand{\cthreevec}[3]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \end{array}\right]}$ $\newcommand{\fourvec}[4]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}$ $\newcommand{\cfourvec}[4]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}$ $\newcommand{\fivevec}[5]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}$ $\newcommand{\cfivevec}[5]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}$ $\newcommand{\mattwo}[4]{\left[\begin{array}{rr}#1 \amp #2 \\ #3 \amp #4 \\ \end{array}\right]}$ $\newcommand{\laspan}[1]{\text{Span}\{#1\}}$ $\newcommand{\bcal}{\cal B}$ $\newcommand{\ccal}{\cal C}$ $\newcommand{\scal}{\cal S}$ $\newcommand{\wcal}{\cal W}$ $\newcommand{\ecal}{\cal E}$ $\newcommand{\coords}[2]{\left\{#1\right\}_{#2}}$ $\newcommand{\gray}[1]{\color{gray}{#1}}$ $\newcommand{\lgray}[1]{\color{lightgray}{#1}}$ $\newcommand{\rank}{\operatorname{rank}}$ $\newcommand{\row}{\text{Row}}$ $\newcommand{\col}{\text{Col}}$ $\renewcommand{\row}{\text{Row}}$ $\newcommand{\nul}{\text{Nul}}$ $\newcommand{\var}{\text{Var}}$ $\newcommand{\corr}{\text{corr}}$ $\newcommand{\len}[1]{\left|#1\right|}$ $\newcommand{\bbar}{\overline{\bvec}}$ $\newcommand{\bhat}{\widehat{\bvec}}$ $\newcommand{\bperp}{\bvec^\perp}$ $\newcommand{\xhat}{\widehat{\xvec}}$ $\newcommand{\vhat}{\widehat{\vvec}}$ $\newcommand{\uhat}{\widehat{\uvec}}$ $\newcommand{\what}{\widehat{\wvec}}$ $\newcommand{\Sighat}{\widehat{\Sigma}}$ $\newcommand{\lt}{<}$ $\newcommand{\gt}{>}$ $\newcommand{\amp}{&}$ $\definecolor{fillinmathshade}{gray}{0.9}$

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

A variable assignment $s$ provides a value for every variable—and there are infinitely many of them. This is of course not necessary. We require variable assignments to assign values to all variables simply because it makes things a lot easier. The value of a term $t$, and whether or not a formula $A$ is satisfied in a structure with respect to $s$, only depend on the assignments $s$ makes to the variables in $t$ and the free variables of $A$. This is the content of the next two propositions. To make the idea of “depends on” precise, we show that any two variable assignments that agree on all the variables in $t$ give the same value, and that $A$ is satisfied relative to one iff it is satisfied relative to the other if two variable assignments agree on all free variables of $A$.

Proposition $\PageIndex{1}$

If the variables in a term $t$ are among $x_1$, …, $x_n$, and $s_1(x_i) = s_2(x_i)$ for $i = 1$, …, $n$, then $\Value[s_1]{t}{M} = \Value[s_2]{t}{M}$.

Proof. By induction on the complexity of $t$. For the base case, $t$ can be a constant symbol or one of the variables $x_1$, …, $x_n$. If $t = c$, then $\Value[s_1]{t}{M} = \Assign{c}{M} = \Value[s_2]{t}{M}$. If $t = x_i$, $s_1(x_i) = s_2(x_i)$ by the hypothesis of the proposition, and so $\Value[s_1]{t}{M} = s_1(x_i) = s_2(x_i) = \Value[s_2]{t}{M}$.

For the inductive step, assume that $t = \Atom{f}{t_1, \dots, t_k}$ and that the claim holds for $t_1$, …, $t_k$. Then

\[\begin{aligned}
\Value[s_1]{t}{M}
& = \Value[s_1]{\Atom{f}{t_1, \dots, t_k}}{M} =\\
& = \Assign{f}{M}(\Value[s_1]{t_1}{M}, \dots, \Value[s_1]{t_k}{M})
\end{aligned}\]

For $j = 1, \dots, k$, the variables of $t_j$ are among $x_1, \dots,x_n$. So by induction hypothesis, $\Value[s_1]{t_j}{M} = \Value[s_2]{t_j}{M}$. So,

\[\begin{aligned}
\Value[s_1]{t}{M} & = \Value[s_2]{\Atom{f}{t_1, \dots, t_k}}{M} =\\ & = \Assign{f}{M}(\Value[s_1]{t_1}{M}, \dots, \Value[s_1]{t_k}{M}) =\\ & = \Assign{f}{M}(\Value[s_2]{t_1}{M}, \dots, \Value[s_2]{t_k}{M}) =\\ & = \Value[s_2]{\Atom{f}{t_1, \dots, t_k}}{M} = \Value[s_2]{t}{M}.\end{aligned}\] ◻

Proposition $\PageIndex{2}$

If the free variables in $A$ are among $x_1$, …, $x_n$, and $s_1(x_i) = s_2(x_i)$ for $i = 1$, …, $n$, then $\Sat[,s_1]{M}{A}$ iff $\Sat[,s_2]{M}{A}$.

Proof. We use induction on the complexity of $A$. For the base case, where $A$ is atomic, $A$ can be: $\lfalse$, $\Atom{R}{t_1, \dots, t_k}$ for a $k$-place predicate $R$ and terms $t_1$, …, $t_k$, or $\eq[t_1][t_2]$ for terms $t_1$ and $t_2$.

$\indcase{A}{\lfalse}$ both $\SatN[,s_1]{M}{A}$ and $\SatN[,s_2]{M}{A}$.
$\indcase{A}{\Atom{R}{t_1, \ldots, t_k}}$ let $\Sat[,s_1]{M}{\indfrm}$. Then \[\langle \Value[s_1]{t_1}{M}, \ldots, \Value[s_1]{t_k}{M} \rangle \in \Assign{R}{M}.\nonumber\] For $i = 1$, …, $k$, $\Value[s_1]{t_i}{M} = \Value[s_2]{t_i}{M}$ by Proposition $\PageIndex{1}$. So we also have $\langle \Value[s_2]{t_i}{M}, \ldots, \Value[s_2]{t_k}{M} \rangle \in \Assign{R}{M}$.
$\indcase{A}{\eq[t_1][t_2]}$ suppose $\Sat[,s_1]{M}{\indfrm}$. Then $\Value[s_1]{t_1}{M} = \Value[s_1]{t_2}{M}$. So, \[\begin{aligned} \Value[s_2]{t_1}{M} & = \Value[s_1]{t_1}{M} & \text{(by Proposition $\PageIndex{1}$)} \\ & = \Value[s_1]{t_2}{M} & \text{(since $\Sat[,s_1]{M}{\eq[t_1][t_2]}$)}\\ &= \Value[s_2]{t_2}{M} & \text{(by Proposition $\PageIndex{1}$),} \end{aligned}\] so $\Sat[,s_2]{M}{\eq[t_1][t_2]}$.

Now assume $\Sat[,s_1]{M}{B}$ iff $\Sat[,s_2]{M}{B}$ for all formulas $B$ less complex than $A$. The induction step proceeds by cases determined by the main operator of $A$. In each case, we only demonstrate the forward direction of the biconditional; the proof of the reverse direction is symmetrical. In all cases except those for the quantifiers, we apply the induction hypothesis to sub-formulas $B$ of $A$. The free variables of $B$ are among those of $A$. Thus, if $s_1$ and $s_2$ agree on the free variables of $A$, they also agree on those of $B$, and the induction hypothesis applies to $B$.

$\indcase{A}{\lnot B}$ if $\Sat[,s_1]{M}{\indfrm}$, then $\SatN[,s_1]{M}{B}$, so by the induction hypothesis, $\SatN[,s_2]{M}{B}$, hence $\Sat[,s_2]{M}{\indfrm}$.
$\indcase{A}{B \land C}$ exercise.
$\indcase{A}{B \lor C}$ if $\Sat[,s_1]{M}{\indfrm}$, then $\Sat[,s_1]{M}{B}$ or $\Sat[,s_1]{M}{C}$. By induction hypothesis, $\Sat[,s_2]{M}{B}$ or $\Sat[,s_2]{M}{C}$, so $\Sat[,s_2]{M}{\indfrm}$.
$\indcase{A}{B \lif C}$ exercise.
$\indcase{A}{\lexists{x}{B}}$ if $\Sat[,s_1]{M}{\indfrm}$, there is an $x$-variant $s_1'$ of $s_1$ so that $\Sat[,s_1']{M}{B}$. Let $s_2'$ be the $x$-variant of $s_2$ that assigns the same thing to $x$ as does $s_1'$. The free variables of $B$ are among $x_1$, …, $x_n$, and $x$. $s_1'(x_i) = s_2'(x_i)$, since $s_1'$ and $s_2'$ are $x$-variants of $s_1$ and $s_2$, respectively, and by hypothesis $s_1(x_i) = s_2(x_i)$. $s_1'(x) = s_2'(x)$ by the way we have defined $s_2'$. Then the induction hypothesis applies to $B$ and $s_1'$, $s_2'$, so $\Sat[,s_2']{M}{B}$. Hence, there is an $x$-variant of $s_2$ that satisfies $B$, and so $\Sat[,s_2]{M}{\indfrm}$.
$\indcase{A}{\lforall{x}{B}}$ exercise.

By induction, we get that $\Sat[,s_1]{M}{A}$ iff $\Sat[,s_2]{M}{A}$ whenever the free variables in $A$ are among $x_1$, …, $x_n$ and $s_1(x_i)=s_2(x_i)$ for $i = 1$, …, $n$. ◻

Problem $\PageIndex{1}$

Complete the proof of Proposition $\PageIndex{2}$.

Sentences have no free variables, so any two variable assignments assign the same things to all the (zero) free variables of any sentence. The proposition just proved then means that whether or not a sentence is satisfied in a structure relative to a variable assignment is completely independent of the assignment. We’ll record this fact. It justifies the definition of satisfaction of a sentence in a structure (without mentioning a variable assignment) that follows.

Corollary $\PageIndex{1}$

If $A$ is a sentence and $s$ a variable assignment, then $\Sat[,s]{M}{A}$ iff $\Sat[,s']{M}{A}$ for every variable assignment $s'$.

Proof. Let $s'$ be any variable assignment. Since $A$ is a sentence, it has no free variables, and so every variable assignment $s'$ trivially assigns the same things to all free variables of $A$ as does $s$. So the condition of Proposition $\PageIndex{2}$ is satisfied, and we have $\Sat[,s]{M}{A}$ iff $\Sat[,s']{M}{A}$. ◻

Definition $\PageIndex{1}$

If $A$ is a sentence, we say that a structure $\Struct M$ satisfies $A$, $\Sat{M}{A}$, iff $\Sat[,s]{M}{A}$ for all variable assignments $s$.

If $\Sat{M}{A}$, we also simply say that $A$ is true in $\Struct{M}$.

Proposition $\PageIndex{3}$

Let $\Struct{M}$ be a structure, $A$ be a sentence, and $s$ a variable assignment. $\Sat{M}{A}$ iff $\Sat[,s]{M}{A}$.

Proof. Exercise. ◻

Problem $\PageIndex{2}$

Prove Proposition $\PageIndex{3}$.

Proposition $\PageIndex{4}$

Suppose $A(x)$ only contains $x$ free, and $\Struct M$ is a structure. Then:

$\Sat{M}{\lexists{x}{A(x)}}$ iff $\Sat[,s]{M}{A(x)}$ for at least one variable assignment $s$.
$\Sat{M}{\lforall{x}{A(x)}}$ iff $\Sat[,s]{M}{A(x)}$ for all variable assignments $s$.

Proof. Exercise. ◻

Problem $\PageIndex{3}$

Prove Proposition $\PageIndex{4}$.

Problem $\PageIndex{4}$

Suppose $\Lang L$ is a language without function symbols. Given a structure $\Struct M$, $c$ a constant symbol and $a \in \Domain M$, define $\Struct M[a/c]$ to be the structure that is just like $\Struct M$, except that $\Assign{c}{M[a/c]} = a$. Define $\Struct M \mathrel{||}\joinrel\Relbar A$ for sentences $A$ by:

$\indcase{A}{\lfalse}$ not $\Struct{M} \mathrel{||}\joinrel\Relbar\indfrm$.
$\indcase{A}{\Atom{R}{d_1, \dots, d_n}}$ $\Struct M \mathrel{||}\joinrel\Relbar\indfrm$ iff $\langle \Assign{d_1}{M}, \dots, \Assign{d_n}{M} \rangle \in \Assign{R}{M}$.
$\indcase{A}{\eq[d_1][d_2]}$ $\Struct M \mathrel{||}\joinrel\Relbar\indfrm$ iff $\Assign{d_1}{M} = \Assign{d_2}{M}$.
$\indcase{A}{\lnot B}$ $\Struct{M} \mathrel{||}\joinrel\Relbar\indfrm$ iff not $\Struct{M} \mathrel{||}\joinrel\Relbar{B}$.
$\indcase{A}{(B \land C)}$ $\Struct{M} \mathrel{||}\joinrel\Relbar \indfrm$ iff $\Struct{M} \mathrel{||}\joinrel\Relbar B$ and $\Struct{M} \mathrel{||}\joinrel\Relbar C$.
$\indcase{A}{(B \lor C)}$ $\Struct{M} \mathrel{||}\joinrel\Relbar\indfrm$ iff $\Struct{M} \mathrel{||}\joinrel\Relbar B$ or $\Struct{M} \mathrel{||}\joinrel\Relbar C$ (or both).
$\indcase{A}{(B \lif C)}$ $\Struct{M} \mathrel{||}\joinrel\Relbar\indfrm$ iff not $\Struct {M} \mathrel{||}\joinrel\Relbar B$ or $\Struct M \mathrel{||}\joinrel\Relbar C$ (or both).
$\indcase{A}{\lforall{x}{B}}$ $\Struct{M} \mathrel{||}\joinrel\Relbar{\indfrm}$ iff for all $a \in \Domain{M}$, $\Struct{M[a/c]} \mathrel{||}\joinrel\Relbar\Subst{B}{c}{x}$, if $c$ does not occur in $B$.
$\indcase{A}{\lexists{x}{B}}$ $\Struct{M} \mathrel{||}\joinrel\Relbar {\indfrm}$ iff there is an $a \in \Domain M$ such that $\Struct{M[a/c]} \mathrel{||}\joinrel\Relbar\Subst{B}{c}{x}$, if $c$ does not occur in $B$.

Let $x_1$, …, $x_n$ be all free variables in $A$, $c_1$, …, $c_n$ constant symbols not in $A$, $a_1$, …, $a_n \in \Domain M$, and $s(x_i) = a_i$.

Show that $\Sat[,s]{M}{A}$ iff $\Struct M[a_1/c_1,\dots,a_n/c_n] \mathrel{||}\joinrel\Relbar\Subst{\Subst{A}{c_1}{x_1}\dots}{c_n}{x_n}$.

(This problem shows that it is possible to give a semantics for first-order logic that makes do without variable assignments.)

Problem $\PageIndex{5}$

Suppose that $f$ is a function symbol not in $A(x,y)$. Show that there is a structure $\Struct{M}$ such that $\Sat{M}{\lforall{x}{\lexists{y}{A(x,y)}}}$ iff there is an $\Struct M'$ such that $\Sat{M'}{\lforall{x}{A(x,f(x))}}$.

(This problem is a special case of what’s known as Skolem’s Theorem; $\lforall{x}{A(x,f(x))}$ is called a Skolem normal form of $\lforall{x}{\lexists{y}{A(x,y)}}$.)

Search

Text Color

Text Size

Margin Size

Font Type