2.2.3: Examples of First-Order Theories

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

Example \(\PageIndex{1}\)

The theory of strict linear orders in the language \(\Lang L_<\) is axiomatized by the set \[\begin{aligned} & \lforall{x}{\lnot x < x}, \\ & \lforall{x}{\lforall{y}{((x < y \lor y < x) \lor x = y)}}, \\ & \lforall{x}{\lforall{y}{\lforall{z}{((x < y \land y < z) \lif x < z)}}}\end{aligned}\] It completely captures the intended structures: every strict linear order is a model of this axiom system, and vice versa, if \(R\) is a linear order on a set \(X\), then the structure \(\Struct M\) with \(\Domain M = X\) and \(\Assign{<}{M} = R\) is a model of this theory.

Example \(\PageIndex{2}\)

The theory of groups in the language \(\Obj 1\) (constant symbol), \(\cdot\) (two-place function symbol) is axiomatized by \[\begin{aligned} & \lforall{x}{\eq[(x \cdot \Obj 1)][x]}\\ & \lforall{x}{\lforall{y}{\lforall{z}{\eq[(x \cdot (y \cdot z))][((x \cdot y) \cdot z)]}}}\\ & \lforall{x}{\lexists{y}{\eq[(x \cdot y)][\Obj 1]}}\end{aligned}\]

Example \(\PageIndex{3}\)

The theory of Peano arithmetic is axiomatized by the following sentences in the language of arithmetic \(\Lang L_A\).

\[\begin{aligned}
& \lforall{x}{\lforall{y}{(\eq[x'][y'] \lif \eq[x][y])}}\\
& \lforall{x}{\eqN[\Obj 0][x']}\\
& \lforall{x}{\eq[(x + \Obj 0)][x]}\\
& \lforall{x}{\lforall{y}{\eq[(x + y')][(x + y)']}}\\
& \lforall{x}{\eq[(x \times \Obj 0)][\Obj 0]}\\
& \lforall{x}{\lforall{y}{\eq[(x \times y')][((x \times y) + x)]}}\\
& \lforall{x}{\lforall{y}{(x < y \liff \lexists{z}{\eq[(z' + x)][y])})}}
\end{aligned}\]

plus all sentences of the form

\[(A(\Obj 0) \land \lforall{x}{(A(x) \lif A(x'))}) \lif \lforall{x}{A(x)}\nonumber\]

Since there are infinitely many sentences of the latter form, this axiom system is infinite. The latter form is called the induction schema. (Actually, the induction schema is a bit more complicated than we let on here.)

The last axiom is an explicit definition of \(<\).

Example \(\PageIndex{4}\)

The theory of pure sets plays an important role in the foundations (and in the philosophy) of mathematics. A set is pure if all its elements are also pure sets. The empty set counts therefore as pure, but a set that has something as an element that is not a set would not be pure. So the pure sets are those that are formed just from the empty set and no “urelements,” i.e., objects that are not themselves sets.

The following might be considered as an axiom system for a theory of pure sets:

\[\begin{aligned}
& \lexists{x}{\lnot \lexists{y}{y \in x}}\\
& \lforall{x}{\lforall{y}{(\lforall{z}{}(z \in x \liff z \in y) \lif \eq[x][y])}}\\
& \lforall{x}{\lforall{y}{\lexists{z}{\lforall{u}{(u \in z \liff (\eq[u][x] \lor \eq[u][y]))}}}}\\
& \lforall{x}{\lexists{y}{\lforall{z}{(z \in y \liff \lexists{u}{(z \in u \land u \in x)})}}}\end{aligned}\]

plus all sentences of the form

\[\lexists{x}{\lforall{y}{(y \in x \liff A(y))}}\nonumber\]

The first axiom says that there is a set with no elements (i.e., \(\emptyset\) exists); the second says that sets are extensional; the third that for any sets \(X\) and \(Y\), the set \(\{X, Y\}\) exists; the fourth that for any set \(X\), the set \(\cup X\) exists, where \(\cup X\) is the union of all the elements of \(X\).

The sentences mentioned last are collectively called the naive comprehension scheme. It essentially says that for every \(A(x)\), the set \(\Setabs{x}{A(x)}\) exists—so at first glance a true, useful, and perhaps even necessary axiom. It is called “naive” because, as it turns out, it makes this theory unsatisfiable: if you take \(A(y)\) to be \(\lnot y \in y\), you get the sentence \[\lexists{x}{\lforall{y}{(y \in x \liff \lnot y \in y)}}\nonumber\] and this sentence is not satisfied in any structure.

Example \(\PageIndex{5}\)

In the area of mereology, the relation of parthood is a fundamental relation. Just like theories of sets, there are theories of parthood that axiomatize various conceptions (sometimes conflicting) of this relation.

The language of mereology contains a single two-place predicate symbol \(\Obj P\), and \(\Atom{\Obj P}{x, y}\) “means” that \(x\) is a part of \(y\). When we have this interpretation in mind, a structure for this language is called a parthood structure. Of course, not every structure for a single two-place predicate will really deserve this name. To have a chance of capturing “parthood,” \(\Assign{\Obj P}{M}\) must satisfy some conditions, which we can lay down as axioms for a theory of parthood. For instance, parthood is a partial order on objects: every object is a part (albeit an improper part) of itself; no two different objects can be parts of each other; a part of a part of an object is itself part of that object. Note that in this sense “is a part of” resembles “is a subset of,” but does not resemble “is an element of” which is neither reflexive nor transitive.

\[\begin{aligned} & \lforall{x}{\Atom{\Obj P}{x,x}}, \\ & \lforall{x}{\lforall{y}{((\Part{x}{y} \land \Part{y}{x}) \lif \eq[x][y])}}, \\ & \lforall{x}{\lforall{y}{\lforall{z}{((\Part{x}{y} \land \Part{y}{z}) \lif \Part{x}{z})}}},\end{aligned}\]

Moreover, any two objects have a mereological sum (an object that has these two objects as parts, and is minimal in this respect).

\[\lforall{x}{\lforall{y}{\lexists{z}{\lforall{u}{(\Part{z}{u} \liff (\Part{x}{u} \land \Part{y}{u}))}}}}\nonumber\]

These are only some of the basic principles of parthood considered by metaphysicians. Further principles, however, quickly become hard to formulate or write down without first introducting some defined relations. For instance, most metaphysicians interested in mereology also view the following as a valid principle: whenever an object \(x\) has a proper part \(y\), it also has a part \(z\) that has no parts in common with \(y\), and so that the fusion of \(y\) and \(z\) is \(x\).