11. Some Theories in First-Order Logic

In this lecture, we continue our exploration of first-order logic. First, we see how to establish or refute logical consequences. Then, we examine two important theories: group theory, and a theory of arithmetic.

Proofs and Refutations

Some logical consequences can be established directly. Others are more easily established using a proof by contradiction.

Proposition. For any first-order language whose signature includes the unary predicate \(P\),

\[\{ \forall x_1 \neg P(x_1)\} \vDash \neg \exists x_1 P(x_1).\]

Proof. Assume on the contrary that \(\{ \forall x_1 \neg P(x_1)\} \not\vDash \neg \exists x_1 P(x_1)\). This means that there exists a structure \(\mathcal{M}\) over some domain \(D\) for which

\[\mathrm{val}_{\mathcal{M}}\big( \forall x_1 \neg P(x_1) \big) = \mathrm{True}\]

and

\[\mathrm{val}_{\mathcal{M}}\big( \neg \exists x_1 P(x_1) \big) = \mathrm{False}.\]

By the definition of valuation, the last identity implies that \(\mathrm{val}_{\mathcal{M}}\big( \exists x_1 P(x_1) \big) = \mathrm{True}.\) In turn, this means that there is some element \(d \in D\) for which \(\mathrm{val}_{\mathcal{M}}\big( P(d) \big) = \mathrm{True}.\) But the first identity of the proof implies that

\[\mathrm{val}_{\mathcal{M}}\big( \neg P(d) \big) = \mathrm{True},\]

implying in turn that \(\mathrm{val}_{\mathcal{M}}\big( P(d) \big) = \mathrm{False}.\) This contradicts our earlier assertion since the value of \(P(d)\) cannot be both True and False.

In the case of logical consequences that do not hold, as in \(\Gamma \not\vDash \phi\), we refute the consequence by providing an example of a structure that satisfies the formulas in \(\Gamma\) but does not satisfy \(\phi.\)

Proposition. Let \(P\) and \(Q\) be unary predicates in a first-order language. Then

\[\{ (\forall x_1 P(x_1) \to \forall x_1 Q(x_1)) \} \not\vDash \forall x_1 (P(x_1) \to Q(x_1)).\]

Proof. Consider the structure \(\mathcal{M}\) on the domain \(D = \{0,1\}\) where we define \(P = \{ 0 \}\) and \(Q = \{ 1 \}\).

Since \(\mathrm{val}_{\mathcal{M}}(P(1)) = \mathrm{False}\), we also have that \(\mathrm{val}_{\mathcal{M}}(\forall x_1 P(x_1)) = \mathrm{False}\). Therefore, the structure \(\mathcal{M}\) satisfies \((\forall x_1 P(x_1) \to \forall x_1 Q(x_1)).\)

However, the element \(0 \in D\) satisfies \(\mathrm{val}_{\mathcal{M}}(P(0)) = \mathrm{True}\) and \(\mathrm{val}_{\mathcal{M}}(Q(0)) = \mathrm{False}\) so that \(\mathcal{M}\) does not satisfy \(\forall x_1 (P(x_1) \to Q(x_1)).\)

Group Theory

Let us now examine concrete examples of first-order theories. The study of group theory emerged from the study of numbers, polynomials, and geometry. Despite many differences between the study of these objects, many fundamental results in all of these fields (and many others) have a common justification which is based on some of the structure that binary operators on those objects satisfy. The formalization of what ensures this structure and the study of this structure in more abstract terms led to the development of group theory.

More precisely, we can define a first-order theory of groups with the following set of axioms.

Definition. For a first-order language that includes the binary function \(\cdot\) and the constant \(\mathbf{e}\), the set \(\Gamma_G\) of group theory axioms includes the following three axioms:

\[\begin{align*} & \forall x \forall y \forall z (x \cdot (y \cdot z)) = ((x \cdot y) \cdot z) & \mbox{(Associativity)}\\ & \forall x \, ((x\cdot \mathbf{e}) = x \wedge (\mathbf{e} \cdot x) = x) & \mbox{(Identity)} \\ & \forall x \exists y \, ((x \cdot y) = \mathbf{e} \wedge (y \cdot x) = \mathbf{e}) & \mbox{(Inverse)} \end{align*}\]

A model \(\mathcal{G} = (G, \cdot^{\mathcal{G}}, \mathbf{e}^{\mathcal{G}})\) of \(\Gamma_G\) is called a group.

The theory of groups is extensive. Let us begin exploring this theory by establishing a few easy theorems.

Theorem. \(\Gamma_G \vDash (\mathbf{e} \cdot \mathbf{e}) = \mathbf{e}.\)

Proof. This is an immediate consequence of the identity axiom with \(x = \mathbf{e}\).

The following theorem is slightly more interesting. Its proof uses all three of the group theory axioms as well as the property that whenever \(a = b\), then for any element \(c\) we must have \(a \cdot c = b \cdot c.\) (This is by definition of equality, since \(a=b\) can hold only when they both represent the same element of the domain.)

Theorem. \(\Gamma_G \vDash \forall x \, ((x \cdot x) = x \to x = \mathbf{e}).\)

Proof. For every \(g \in G\) where \((g \cdot g) \neq g\), the implication \(((g \cdot g) = g \to g = \mathbf{e})\) is true.

Fix now any \(g \in G\) that satisfies \((g \cdot g) = g.\) By the inverse axiom, there exists an element \(h \in G\) that satisfies \(g \cdot h = \mathbf{e}.\) Fix such an \(h\). Then

\[\begin{align*} (g \cdot g) &= g \\ \Rightarrow ((g \cdot g) \cdot h) &= (g \cdot h) \\ \Rightarrow (g \cdot (g \cdot h)) &= (g \cdot h) & \mbox{(by associativity)} \\ \Rightarrow (g \cdot \mathbf{e}) &= \mathbf{e} & \mbox{(by choice of } h) \\ \Rightarrow g &= \mathbf{e} & \mbox{(by identity)} \end{align*}\]

Combining the two cases above, we conclude that every \(g \in G\) causes the sentence \(((g \cdot g) = g \to g = \mathbf{e})\) to evaluate to True.

Similarly, we can prove the useful left cancellation property of groups.

Theorem. \(\Gamma_G \vDash \forall x \forall y \forall z \, ((x \cdot y) = (x \cdot z) \to y = z).\)

Proof. By the inverse axiom, we know that for any \(g \in G\), there exists an element \(g^{-1} \in G\) such that \(g^{-1} \cdot g = \mathbf{e}\). Then for any \(g,h,i \in G,\)

\[\begin{align*} (g \cdot h) &= (g \cdot i) \\ \Rightarrow (g^{-1} \cdot (g \cdot h) &= (g^{-1} \cdot (g \cdot i)) \\ \Rightarrow ((g^{-1} \cdot g) \cdot h) &= ((g^{-1} \cdot g) \cdot i) & \mbox{(by associativity)} \\ \Rightarrow (\mathbf{e} \cdot h) &= (\mathbf{e} \cdot i) & \mbox{(by inverse)} \\ \Rightarrow h &= i & \mbox{(by identity)} \end{align*}\]

We can continue to build on these results to obtain more complex theorems. But it’s worth pointing out that there are also many quite reasonable sentences that do not follow from the group theory axioms. For example,

\[\Gamma_G \not\vDash \forall x \forall y \, (x \cdot y) = (y \cdot x).\]

(Can you find a group with a finite domain \(G\) that refutes this consequence?)

The property encoded by the above sentence is known as commutativity. It can be added to \(\Gamma_G\) to form a set of axioms for the class of Abelian groups. Similarly, we can add other axioms to \(\Gamma_G\) to obtain theories of other classes of graphs. Or we can add different axioms (as well as additional functions, constants and/or predicates to the signature) to obtain theories of rings, fields, and many other types of algebraic structures.

Peano Axioms of Arithmetic

The Peano Axioms provide a way to study arithmetic in first-order logic.

Definition. A set of Peano Axioms over a first-order language with the unary function \(S\), the binary functions \(+\) and \(\times\) and the constant \(\mathbf{0}\) is the set \(\Gamma_{\mathrm{PA}}\) that includes the sentences

\[\begin{align*} &\forall x \, \neg S(x) = \mathbf{0} \\ &\forall x \forall y \, ( S(x) = S(y) \to x = y) \\ &\forall x \, (x+\mathbf{0}) = x \\ &\forall x \forall y \, (x+S(y)) = S(x+y) \\ &\forall x \, x \times \mathbf{0} = \mathbf{0} \\ &\forall x \forall y \, x \times S(y) = (x \times y) + x \end{align*}\]

as well as the infinite collection of all sentences of the form

\[\forall x_1 \cdots \forall x_n (( \phi(\mathbf{0}) \wedge \forall y (\phi(y) \to \phi(S(y)))) \to \forall y \phi(y))\]

for any formula \(\phi\) that contains the free variables \(y\) and \(x_1,\ldots,x_n\), where here we write \(\phi(\mathbf{0}) = \phi_{[y/\mathbf{0}]}\) to represent the formula obtained by replacing \(y\) with the element \(\mathbf{0}\).

Note that there are other alternative formulations of the Peano axioms for first-order logic that are equivalent to \(\Gamma_{\mathrm{PA}}\).

We can prove many interesting results in number theory from the Peano axioms. But, as in the case of group theory, the better starting point for working with the theory of \(\Gamma_{\mathrm{PA}}\) is a collection of very simple theorems.

Exercise. Can you prove the following theorems of Peano arithmetic? You should prove the theorems in order, and you may use the theorems you establish in the proofs of the following ones. (But you may not use later theorems to prove earlier ones to make sure you avoid circular arguments!)

  1. \(\Gamma_{\mathrm{PA}} \vDash \forall x (\mathbf{0} + x) = x\).
  2. \(\Gamma_{\mathrm{PA}} \vDash \forall x \forall y \, (S(x) + y) = S(x+y)\).
  3. \(\Gamma_{\mathrm{PA}} \vDash \forall x \forall y \, x+y = y+x\).
  4. \(\Gamma_{\mathrm{PA}} \vDash \forall x \, (\mathbf{0} \times x) = 0\).
  5. \(\Gamma_{\mathrm{PA}} \vDash \forall x \forall y \, (S(x) \times y) = x \times y + y\).
  6. \(\Gamma_{\mathrm{PA}} \vDash \forall x \forall y \, x \times y = y \times x\).
  7. \(\Gamma_{\mathrm{PA}} \vDash \forall x \forall y \forall z \, (x \times (y + z)) = ((x \times y) + (x \times z))\).
  8. \(\Gamma_{\mathrm{PA}} \vDash \forall x \forall y \forall z \, (x + z = y + z \to x = y)\).

Relatedly, you can also prove these and many other similar theorems in Lean. See the Natural Number Game for a great introduction to these challenges.