2.1.9: Structures for First-order Languages

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

First-order languages are, by themselves, uninterpreted: the constant symbols, function symbols, and predicate symbols have no specific meaning attached to them. Meanings are given by specifying structure. It specifies the domain, i.e., the objects which the constant symbols pick out, the function symbols operate on, and the quantifiers range over. In addition, it specifies which constant symbols pick out which objects, how a function symbol maps objects to objects, and which objects the predicate symbols apply to. Structures are the basis for semantic notions in logic, e.g., the notion of consequence, validity, satisfiablity. They are variously called “structures,” “interpretations,” or “models” in the literature.

Definition \(\PageIndex{1}\): Structures

A structure \(\Struct M\), for a language \(\Lang{L}\) of first-order logic consists of the following elements:

1. Domain: a non-empty set, \(\Domain M\)
2. Interpretation of constant symbols: for each constant symbol \(c\) of \(\Lang{L}\), an element \(\Assign{c}{M} \in \Domain M\)
3. Interpretation of predicate symbols: for each \(n\)-place predicate symbol \(R\) of \(\Lang{L}\) (other than \(\eq[][]\)), an \(n\)-place relation \(\Assign{R}{M} \subseteq \Domain{M}^n\)
4. Interpretation of function symbols: for each \(n\)-place function symbol \(f\) of \(\Lang{L}\), an \(n\)-place function \(\Assign{f}{M} \colon \Domain{M}^n \to \Domain{M}\)

Example \(\PageIndex{1}\)

A structure \(\Struct M\) for the language of arithmetic consists of a set, an element of \(\Domain M\), \(\Assign{\Obj 0}{M}\), as interpretation of the constant symbol \(\Obj 0\), a one-place function \(\Assign{\Obj \prime}{M} \colon \Domain{M} \to \Domain M\), two two-place functions \(\Assign{\Obj +}{M}\) and \(\Assign{\Obj \times}{M}\), both \(\Domain M^2 \to \Domain M\), and a two-place relation \(\Assign{\Obj <}{M} \subseteq \Domain{M}^2\).

An obvious example of such a structure is the following:

1. \(\Domain N = \Nat\)
2. \(\Assign{\Obj 0}{N} = 0\)
3. \(\Assign{\Obj \prime}{N}(n) = n + 1\) for all \(n \in \Nat\)
4. \(\Assign{\Obj +}{N}(n, m) = n + m\) for all \(n, m \in \Nat\)
5. \(\Assign{\Obj \times}{N}(n, m) = n\cdot m\) for all \(n, m \in \Nat\)
6. \(\Assign{\Obj <}{N} = \Setabs{\tuple{n, m}}{n \in \Nat, m \in \Nat, n < m}\)

The structure \(\Struct N\) for \(\Lang L_A\) so defined is called the standard model of arithmetic, because it interprets the non-logical constants of \(\Lang L_A\) exactly how you would expect.

However, there are many other possible structures for \(\Lang L_A\). For instance, we might take as the domain the set \(\Int\) of integers instead of \(\Nat\), and define the interpretations of \(\Obj 0\), \(\Obj \prime\), \(\Obj +\), \(\Obj \times\), \(\Obj <\) accordingly. But we can also define structures for \(\Lang L_A\) which have nothing even remotely to do with numbers.

Example \(\PageIndex{2}\)

A structure \(\Struct M\) for the language \(\Lang L_Z\) of set theory requires just a set and a single-two place relation. So technically, e.g., the set of people plus the relation “\(x\) is older than \(y\)” could be used as a structure for \(\Lang L_Z\), as well as \(\Nat\) together with \(n \ge m\) for \(n, m \in \Nat\).

A particularly interesting structure for \(\Lang L_Z\) in which the elements of the domain are actually sets, and the interpretation of \(\Obj \in\) actually is the relation “\(x\) is an element of \(y\)” is the structure \(\Struct{ {HF} }\) of hereditarily finite sets:

1. \(\Domain{ { {HF} } } = \emptyset \cup \Pow{\emptyset} \cup \Pow{\Pow{\emptyset}} \cup \Pow{\Pow{\Pow{\emptyset}}} \cup \dots\);
2. \(\Assign{\Obj \in}{ { {HF} } } = \Setabs{\tuple{x, y}}{x, y \in \Domain{ { {HF} } }, x \in y}\).

The stipulations we make as to what counts as a structure impact our logic. For example, the choice to prevent empty domains ensures, given the usual account of satisfaction (or truth) for quantified sentences, that \(\lexists{x}{(A(x) \lor \lnot A(x))}\) is valid—that is, a logical truth. And the stipulation that all constant symbols must refer to an object in the domain ensures that the existential generalization is a sound pattern of inference: \(A(a)\), therefore \(\lexists{x}{A(x)}\). If we allowed names to refer outside the domain, or to not refer, then we would be on our way to a free logic, in which existential generalization requires an additional premise: \(A(a)\) and \(\lexists{x}{\eq[x][a]}\), therefore \(\lexists{x}{A(x)}\).