2.2.4: Expressing Relations in a Structure

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

One main use formulas can be put to is to express properties and relations in a structure \(\Struct M\) in terms of the primitives of the language \(\Lang L\) of \(\Struct M\). By this we mean the following: the domain of \(\Struct M\) is a set of objects. The constant symbols, function symbols, and predicate symbols are interpreted in \(\Struct M\) by some objects in \(\Domain M\), functions on \(\Domain M\), and relations on \(\Domain M\). For instance, if \(\Obj A^2_0\) is in \(\Lang L\), then \(\Struct M\) assigns to it a relation \(R = \Assign{ {\Obj A^2_0} }{M}\). Then the formula \(\Atom{\Obj A^2_0}{\Obj v_1, \Obj v_2}\) expresses that very relation, in the following sense: if a variable assignment \(s\) maps \(\Obj v_1\) to \(a \in \Domain{M}\) and \(\Obj v_2\) to \(b \in \Domain M\), then \[Rab \quad\text{ iff}\quad \Sat[,s]{M}{\Atom{\Obj A^2_0}{\Obj v_1, \Obj v_2}}.\nonumber\] Note that we have to involve variable assignments here: we can’t just say “\(Rab\) iff \(\Sat{M}{\Atom{\Obj A^2_0}{a, b}}\)” because \(a\) and \(b\) are not symbols of our language: they are elements of \(\Domain{M}\).

Since we don’t just have atomic formulas, but can combine them using the logical connectives and the quantifiers, more complex formulas can define other relations which aren’t directly built into \(\Struct M\). We’re interested in how to do that, and specifically, which relations we can define in a structure.

Definition \(\PageIndex{1}\)

Let \(A(\Obj v_1,\dots, \Obj v_n)\) be a formula of \(\Lang L\) in which only \(\Obj v_1\),…, \(\Obj v_n\) occur free, and let \(\Struct M\) be a structure for \(\Lang L\). \(A(\Obj v_1,\dots, \Obj v_n)\) expresses the relation \(R \subseteq \Domain M^n\) iff \[Ra_1\dots a_n \quad\text{ iff}\quad \Sat[,s]{M}{\Atom{A}{\Obj v_1,\dots, \Obj v_n}}\nonumber\] for any variable assignment \(s\) with \(s(\Obj v_i) = a_i\) (\(i = 1, \dots, n\)).

Example \(\PageIndex{1}\)

In the standard model of arithmetic \(\Struct N\), the formula \(\Obj v_1 < \Obj v_2 \lor \eq[\Obj v_1][\Obj v_2]\) expresses the \(\le\) relation on \(\Nat\). The formula \(\eq[\Obj v_2][\Obj v_1']\) expresses the successor relation, i.e., the relation \(R \subseteq \Nat^2\) where \(Rnm\) holds if \(m\) is the successor of \(n\). The formula \(\eq[\Obj v_1][\Obj v_2']\) expresses the predecessor relation. The formulas \(\lexists{\Obj v_3}{(\eqN[\Obj v_3][\Obj 0] \land \eq[\Obj v_2][(\Obj v_1 + \Obj v_3)])}\) and \(\lexists{\Obj v_3}{\eq[(\Obj v_1 + {\Obj v_3}')][v_2]}\) both express the \(\Obj <\) relation. This means that the predicate symbol \(<\) is actually superfluous in the language of arithmetic; it can be defined.

This idea is not just interesting in specific structures, but generally whenever we use a language to describe an intended model or models, i.e., when we consider theories. These theories often only contain a few predicate symbols as basic symbols, but in the domain they are used to describe often many other relations play an important role. If these other relations can be systematically expressed by the relations that interpret the basic predicate symbols of the language, we say we can define them in the language.

Problem \(\PageIndex{1}\)

Find formulas in \(\Lang L_A\) which define the following relations:

1. \(n\) is between \(i\) and \(j\);
2. \(n\) evenly divides \(m\) (i.e., \(m\) is a multiple of \(n\));
3. \(n\) is a prime number (i.e., no number other than \(1\) and \(n\) evenly divides \(n\)).

Problem \(\PageIndex{2}\)

Suppose the formula \(A(\Obj v_1, \Obj v_2)\) expresses the relation \(R \subseteq \Domain M^2\) in a structure \(\Struct M\). Find formulas that express the following relations:

1. the inverse \(R^{-1}\) of \(R\);
2. the relative product \(R \mid R\);

Can you find a way to express \(R^+\), the transitive closure of \(R\)?

Problem \(\PageIndex{3}\)

Let \(\Lang{L}\) be the language containing a 2-place predicate symbol \(<\) only (no other constant symbols, function symbols or predicate symbols— except of course \(\eq[][]\)). Let \(\Struct{N}\) be the structure such that \(\Domain{N} = \Nat\), and \(\Assign{<}{N} = \Setabs{\tuple{n,m}}{n < m}\). Prove the following:

1. \(\{ 0 \}\) is definable in \(\Struct{N}\);
2. \(\{ 1 \}\) is definable in \(\Struct{N}\);
3. \(\{ 2 \}\) is definable in \(\Struct{N}\);
4. for each \(n \in \Nat\), the set \(\{ n \}\) is definable in \(\Struct{N}\);
5. every finite subset of \(\Domain{N}\) is definable in \(\Struct{N}\);
6. every co-finite subset of \(\Domain{N}\) is definable in \(\Struct{N}\) (where \(X \subseteq \Nat\) is co-finite iff \(\Nat \setminus X\) is finite).