---
title: Logic as a Mathematical Model of Deduction
module: Foundations
moduleNumber: 1
lessonNumber: 1
order: 101
summary: >
  Symbolic logic models deductive reasoning the way probability theory models
  chance: it keeps the form of a correct deduction and discards its content. A
  deduction is valid when its conclusion follows from the form of the premises
  alone, independent of what the non-logical words mean. Two models carry the
  subject — coarse sentential logic and fine first-order logic — and four
  questions organize it: logical consequence, methods of proof, the gap between
  provable and true, and the link between logic and computability. Tuples,
  relations, functions, equivalence classes, and cardinality supply the
  set-theoretic vocabulary every later chapter uses.
topics: [Foundations]
sources:
  - book: Enderton
    ref: "Introduction"
  - book: Enderton
    ref: "Ch. 0 — Useful Facts about Sets"
draft: false
---

Symbolic logic is a mathematical model of deductive thought.[^intro] It stands
to reasoning roughly as probability theory stands to chance: a precise
mathematical structure that captures some features of a messy real phenomenon
and ignores the rest. The phenomenon here is the logically correct deduction —
the kind of inference a working mathematician makes when asserting that a
sentence follows from the axioms. The subject builds a formal object that mirrors
those inferences closely enough to study them with the tools of mathematics.

The word "logic" sometimes names remedial thinking; that is not the sense in use
here. The subject does not aim to improve anyone's reasoning. It turns reasoning
into an object — a thing with a definition, subject to theorems — and proves
things about it.

## The modeling stance

A model is made by selection. Begin with a real object, an airplane, and choose
which of its properties to represent. Its shape is essential to how it flies, so
the model keeps the shape; its full size is irrelevant to a wind-tunnel test, so
the model discards the size. Whether the model serves its purpose depends
entirely on that choice of what to keep and what to throw away.

$$
% caption: Modeling is selection: a scale model keeps an airplane's shape and
% drops its size, exactly as sentential and first-order logic keep the form of a
% deduction and drop its subject matter.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  box/.style={draw, minimum width=26mm, minimum height=12mm, align=center},
  lab/.style={font=\scriptsize, text=black}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[box] (obj)  at (0,1.4)   {airplane};
  \node[box] (sel)  at (4.4,1.4) {keep shape,\\drop size};
  \node[box, draw=acc, text=acc] (mod) at (8.8,1.4) {scale model};
  \draw[->, acc, thick] (obj) -- (sel);
  \draw[->, acc, thick] (sel) -- (mod);
  \node[box] (ded)  at (0,-1.2)   {real deductions};
  \node[box] (sel2) at (4.4,-1.2) {keep form,\\drop content};
  \node[box, draw=acc, text=acc] (frm) at (8.8,-1.2) {formal system};
  \draw[->, acc, thick] (ded) -- (sel2);
  \draw[->, acc, thick] (sel2) -- (frm);
  \node[lab] at (0,0.35) {real object};
  \node[lab] at (8.8,0.35) {abstraction};
\end{tikzpicture}
$$

The real objects of logic are certain correct deductions. The property to be
kept is their _form_; the property to be discarded is their _content_. A precise
version of that criterion — "correct by form, independent of content" — is the
first thing the model must deliver, and pinning it down is what motivates the
turn to mathematics.

## Validity is a property of form

Consider the standard example.

$$
% caption: The inference is valid by its shape alone; replacing the words with
% nonsense preserves the validity, so the correctness cannot depend on what the
% words mean.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  prem/.style={draw, minimum width=52mm, minimum height=9mm, align=left, inner xsep=3mm},
  conc/.style={draw, minimum width=52mm, minimum height=9mm, align=left, inner xsep=3mm, draw=acc, text=acc}]
  \definecolor{acc}{HTML}{4A6FA5}
  % left: meaningful
  \node[prem] (p1) at (0,2)   {All men are mortal.};
  \node[prem] (p2) at (0,1)   {Socrates is a man.};
  \node[conc] (c1) at (0,-0.1){Socrates is mortal.};
  \draw[black] (-2.75,0.5) -- (2.75,0.5);
  \node[font=\scriptsize, anchor=west] at (-2.6,-1.05) {premises above the line, conclusion below};
  % right: nonsense, same form
  \begin{scope}[xshift=6.6cm]
    \node[prem] (q1) at (0,2)   {All borogoves are mimsy.};
    \node[prem] (q2) at (0,1)   {This thing is a borogove.};
    \node[conc] (r1) at (0,-0.1){This thing is mimsy.};
    \draw[black] (-2.75,0.5) -- (2.75,0.5);
    \node[font=\scriptsize, anchor=west] at (-2.6,-1.05) {same shape, meaningless words};
  \end{scope}
\end{tikzpicture}
$$

We recognize that the conclusion follows from the premises. That recognition
does not draw on any fact about Socrates, and it does not need the meaning of
"mortal" — only the meaning of "all." Replace every content word with nonsense
and it remains valid: from "all borogoves are mimsy" and "this thing is a
borogove" it still follows that "this thing is mimsy." Correctness is due to form
and is independent of content.

> **Definition (Validity, informal).** A deduction is _logically correct_ when
> the conclusion follows from the premises by virtue of the **form** of the
> sentences alone, independent of the meaning of their non-logical vocabulary.
> Supplying a precise, mathematical version of this criterion is the first task
> of the subject.

The criterion is vague, and that vagueness is what forces a formal model.
Axiomatic mathematics is a long chain of such deductions laid end to end. When a
mathematician says a sentence follows from the axioms of set theory, the claim is
that the deduction can be translated into the model. Giving "follows from" and
"translated into the model" a mathematical meaning is the whole task.

## Two models, coarse and fine

The book presents two models, in order of increasing fidelity.

- **Sentential logic** is the coarse model. It resolves a compound sentence into
  atomic parts joined by connectives (_not_, _and_, _or_, _if–then_), and tracks
  how truth of the whole depends on truth of the parts. It preserves only crude
  properties of real deductions and is inadequate for interesting mathematics,
  but it is simple enough to analyze completely.
- **First-order logic** is the fine model. It adds quantifiers (_for all_,
  _there exists_), variables, predicates, and equality, and is well suited to the
  deductions that arise in mathematics. Most of the subject works in this model
  because of that expressive reach.

The first-order language reaches statements the sentential one cannot. The
set-theoretic principle of extensionality — "if the same things are members of
one object as of another, those objects are equal" — translates to

$$
\forall x\, \forall y\,\bigl( \forall z\, (z \in x \leftrightarrow z \in y) \to x = y \bigr),
$$

and the calculus definition of a limit — "for every positive $\varepsilon$ there
is a positive $\delta$ such that any $x$ within $\delta$ of $a$ has $f(x)$ within
$\varepsilon$ of $b$" — translates to

$$
\forall \varepsilon\,\bigl( \varepsilon > 0 \to \exists \delta\, ( \delta > 0 \land \forall x\, ( d\,x\,a < \delta \to d\,f\,x\,b < \varepsilon ) ) \bigr).
$$

Neither statement is expressible in the coarse sentential model; both are routine
in the fine one. The [language of sentential logic](/logic/sentential-logic/formal-languages-and-well-formed-formulas)
is where the coarse model is built; [first-order languages](/logic/first-order-languages/first-order-languages)
begin the fine one.

The difference between the two models shows in a single inference. The Socrates
syllogism is valid, yet the coarse model cannot see why.

> **Worked example.** Formalize "All men are mortal; Socrates is a man; therefore
> Socrates is mortal" in each model, and locate where the validity becomes
> visible.
>
> Sentential logic reads three unanalyzed atomic sentences:
> $$
> A: \text{all men are mortal}, \quad B: \text{Socrates is a man}, \quad C: \text{Socrates is mortal}.
> $$
> The argument is $\{A, B\}$ with conclusion $C$. Nothing ties the three atoms
> together, so the assignment making $A$ and $B$ true and $C$ false meets both
> premises while denying the conclusion. The coarse model therefore rates the
> inference invalid; it cannot look inside the sentences.
>
> First-order logic analyzes that internal structure. Take a one-place predicate
> $Mx$ for "$x$ is a man", $Hx$ for "$x$ is mortal", and a constant $s$ naming
> Socrates:
> $$
> \{\, \forall x\,(Mx \to Hx),\ \ Ms \,\} \models Hs .
> $$
> Every structure satisfying both premises satisfies $Hs$: instantiate the
> universal premise at $s$ to get $Ms \to Hs$, then detach using $Ms$. The fine
> model rates the inference valid, matching the informal judgment that the form
> alone forces the conclusion.

The detachment step — from $\varphi \to \psi$ and $\varphi$ infer $\psi$ —
already lives in the coarse model as a tautology, a schema true under every
assignment of truth values.

> **Worked example.** Verify that $((P \to Q) \land P) \to Q$ is a **tautology**
> by evaluating it on all four assignments to $P$ and $Q$.
>
> | $P$ | $Q$ | $P \to Q$ | $(P \to Q) \land P$ | $((P \to Q) \land P) \to Q$ |
> | :-: | :-: | :-: | :-: | :-: |
> | T | T | T | T | T |
> | T | F | F | F | T |
> | F | T | T | F | T |
> | F | F | T | F | T |
>
> The final column is constant $T$, so the schema holds under every assignment.
> Being a tautology depends only on the connectives, never on what $P$ and $Q$
> mean. This is the part of the syllogism the coarse model does capture; the
> quantifier step it misses.

The choice to model mathematical deduction, rather than reasoning in general,
fixes the scope. Many-valued, modal, and intuitionistic logics make different
selections of which properties of real deductions to keep, and none of them
appears here.

## The four questions

Once the model exists, four questions organize everything that follows.

1. **What does it mean for one sentence to follow logically from others?** This
   is the _semantic_ question: it is answered by defining truth in a structure
   and calling $\varphi$ a consequence of $\Gamma$ when every structure making
   all of $\Gamma$ true also makes $\varphi$ true.
2. **If a sentence does follow, what methods of proof establish it?** This is the
   _syntactic_ question: it is answered by a deductive calculus with axioms and
   rules, giving a notion of formal proof.
3. **Is there a gap between what an axiom system can prove and what is true?**
   For arithmetic, this asks whether provability and truth coincide.
4. **What is the connection between logic and computability?** This asks which
   logical questions can be settled by an algorithm.

$$
% caption: The four questions and the theorems that answer them, in the order the
% subject develops; questions 1 and 2 are tied together by soundness and
% completeness, questions 3 and 4 by the incompleteness and undecidability results.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  q/.style={draw, minimum width=40mm, minimum height=11mm, align=center},
  a/.style={draw, dashed, minimum width=40mm, minimum height=9mm, align=center, font=\scriptsize}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[q] (q1) at (0,3)    {1. logical consequence};
  \node[q] (q2) at (0,1.4)  {2. methods of proof};
  \node[q] (q3) at (0,-0.2) {3. provable versus true};
  \node[q] (q4) at (0,-1.8) {4. logic and computability};
  \node[a, draw=acc, text=acc] (a12) at (6.3,2.2)  {soundness and\\completeness};
  \node[a, draw=acc, text=acc] (a34) at (6.3,-1.0) {incompleteness,\\undecidability};
  \draw[->, acc, thick] (q1.east) -- (a12.west);
  \draw[->, acc, thick] (q2.east) -- (a12.west);
  \draw[->, acc, thick] (q3.east) -- (a34.west);
  \draw[->, acc, thick] (q4.east) -- (a34.west);
\end{tikzpicture}
$$

Questions 1 and 2 are linked. Semantics gives a relation
"$\Gamma$ semantically implies $\varphi$"; the deductive calculus gives a relation
"$\Gamma$ proves $\varphi$." The [soundness theorem](/logic/deductive-calculus/soundness)
shows every proof yields a genuine consequence, and the
[completeness theorem](/logic/deductive-calculus/completeness-and-consistency)
shows every consequence has a proof, so the two relations coincide. Questions 3
and 4 have a sharper edge: for arithmetic, provability and truth do _not_
coincide ([incompleteness](/logic/incompleteness/incompleteness-and-undecidability)),
and validity is not decidable by any algorithm, drawing the boundary the
[recursive functions](/logic/computability-and-representability/recursive-functions)
make precise.

Question 1 pins consequence to truth in a structure, and that truth is
computed one quantifier at a time. The same sentence can come out true on one
structure and false on another.

> **Worked example.** Evaluate $\forall x\,\exists y\ (x < y)$ — "every element
> has something strictly larger" — on two structures for the language with one
> binary relation symbol $<$.
>
> On $(\mathbb{N}, <)$ with the usual order, fix any $x = n$. The witness
> $y = n + 1$ satisfies $n < n + 1$, so $\exists y\ (x < y)$ holds for that $x$;
> since $n$ was arbitrary, the universal sentence is true:
> $$
> (\mathbb{N}, <) \models \forall x\,\exists y\ (x < y).
> $$
> On the three-element order $(\{0, 1, 2\}, <)$ the same sentence fails. Take
> $x = 2$: no member of the domain satisfies $2 < y$, so $\exists y\ (x < y)$ is
> false at $x = 2$, and one failing instance breaks the universal claim:
> $$
> (\{0, 1, 2\}, <) \not\models \forall x\,\exists y\ (x < y).
> $$
> One sentence with opposite truth values on two structures is why a consequence
> claim quantifies over all structures at once: $\Gamma \models \varphi$ demands
> that $\varphi$ hold in every structure where all of $\Gamma$ holds, not merely
> in one.

## The set-theoretic toolkit

The model is built inside ordinary mathematics, and its raw material is sets.[^ch0]
The notation below is standard and appears without further comment throughout.
Each piece is used where it is needed: Zorn's lemma in the completeness proof,
cardinals in the Löwenheim–Skolem theorems.

**Sets and extensionality.** A set is determined solely by its members. Formally,
if $A$ and $B$ have exactly the same elements, then $A = B$:

$$
\bigl(\forall t\; (t \in A \leftrightarrow t \in B)\bigr) \;\Longrightarrow\; A = B.
$$

Basic constructions follow: the empty set $\varnothing$, the singleton $\{x\}$,
the finite set $\{x_1, \dots, x_n\}$, union $A \cup B$, intersection $A \cap B$,
and the power set $\mathcal{P}A = \{ x \mid x \subseteq A \}$ of all subsets of
$A$. For a set $\mathcal{A}$ whose members are themselves sets, $\bigcup
\mathcal{A}$ collects everything belonging to some member, and $\bigcap
\mathcal{A}$ everything belonging to all members. Two sets are **disjoint** when
$A \cap B = \varnothing$, and a collection is **pairwise disjoint** when any two
of its members are disjoint.

**Ordered tuples and sequences.** An unordered pair satisfies $\{x, y\} = \{y,
x\}$, so it cannot record order. The **ordered pair** $\langle x, y \rangle$ is
defined so that it recovers both components in order:

$$
\langle x, y \rangle = \langle u, v \rangle \quad\text{iff}\quad x = u \ \text{and}\ y = v.
$$

Any construction with this property serves; the standard one is $\langle x, y
\rangle = \{ \{x\}, \{x, y\} \}$. Triples reduce to pairs by $\langle x, y, z
\rangle = \langle \langle x, y \rangle, z \rangle$, and $n$-tuples recursively by
$\langle x_1, \dots, x_{n+1} \rangle = \langle \langle x_1, \dots, x_n \rangle,
x_{n+1} \rangle$, with the convention $\langle x \rangle = x$. A **finite
sequence** (or **string**) over $A$ is an $n$-tuple $\langle x_1, \dots, x_n
\rangle$ with each $x_i \in A$; expressions in a formal language will be exactly
such strings.

The reduction of tuples to nested pairs carries one hazard, and unique
readability of formulas later depends on avoiding it.

> **Lemma (Decomposition of ordered tuples).** If $\langle x_1, \dots, x_m \rangle = \langle y_1, \dots, y_m,
> \dots, y_{m+k} \rangle$, then $x_1 = \langle y_1, \dots, y_{k+1} \rangle$.

The lemma says a shorter tuple can equal a longer one only when the first
component of the shorter is itself a sequence of the extra entries. The
consequence used repeatedly: if no member of $A$ is a finite sequence of other
members of $A$, then $\langle x_1, \dots, x_m \rangle = \langle y_1, \dots, y_n
\rangle$ with all entries in $A$ forces $m = n$ and $x_i = y_i$. A well-designed
alphabet has this "no symbol is a string of symbols" property, which is why the
parsing of formulas is unambiguous.

**Relations and functions.** The **Cartesian product** $A \times B$ is the set of
pairs $\langle x, y \rangle$ with $x \in A$ and $y \in B$, and $A^n$ is the set of
$n$-tuples over $A$. A **relation** is a set of ordered pairs; an **$n$-ary
relation on $A$** is a subset of $A^n$. Its **domain**, **range**, and **field**
are the sets of first components, second components, and both together. A
**function** $F$ is a single-valued relation: each $x \in \dom F$
has exactly one $y$ with $\langle x, y \rangle \in F$, written $y = F(x)$. We
write $F : A \to B$ when $\dom F = A$ and $\ran F
\subseteq B$; the map is **onto** when $\ran F = B$ and
**one-to-one** when each value comes from a single argument. An **$n$-ary
operation on $A$** is a function $A^n \to A$; a subset $B \subseteq A$ is
**closed** under $f$ when $f(b_1, \dots, b_n) \in B$ whenever every $b_i \in B$.
Every inductive definition in the subject, well-formed formulas included, is
built by closure under a family of operations.

**Properties of relations.** For a binary relation $R$ on $A$:

- **Reflexive on $A$**: $\langle x, x \rangle \in R$ for every $x \in A$.
- **Symmetric**: $\langle x, y \rangle \in R$ implies $\langle y, x \rangle \in R$.
- **Transitive**: $\langle x, y \rangle \in R$ and $\langle y, z \rangle \in R$
  imply $\langle x, z \rangle \in R$.
- **Trichotomy on $A$**: for all $x, y \in A$, exactly one of $\langle x, y
  \rangle \in R$, $x = y$, $\langle y, x \rangle \in R$ holds.

An **equivalence relation** on $A$ is reflexive on $A$, symmetric, and
transitive. An **ordering relation** on $A$ is transitive and satisfies
trichotomy.

### Equivalence relations and partitions

Equivalence relations recur throughout the subject: identifying provably equal
terms in the completeness proof, and identifying sentences with the same truth
conditions, both work by passing to equivalence classes.

> **Definition (Equivalence class, partition).** For an equivalence relation $R$
> on $A$ and $x \in A$, the **equivalence class** of $x$ is $[x] = \{ y \mid
> \langle x, y \rangle \in R \}$. The classes **partition** $A$: they are
> nonempty subsets, every element lies in exactly one, and
> $$
> [x] = [y] \quad\text{iff}\quad \langle x, y \rangle \in R.
> $$

The correspondence runs both ways. Every equivalence relation carves $A$ into
disjoint classes that cover it; every partition of $A$ into disjoint blocks
defines an equivalence relation, "$x$ and $y$ lie in the same block."

$$
% caption: An equivalence relation cuts a set into disjoint classes that together
% cover it; two elements are related exactly when they fall in the same class.
\begin{tikzpicture}[>=stealth, font=\footnotesize]
  \definecolor{acc}{HTML}{4A6FA5}
  \definecolor{grn}{HTML}{3C8C5A}
  % the set A as a rounded region carved into three classes
  \draw[black, thick] (0,0) rectangle (9,4);
  \node[anchor=south west, font=\scriptsize] at (0.1,4.05) {the set A};
  % dividing lines
  \draw[black] (3,0) -- (3,4);
  \draw[black] (6,0) -- (6,4);
  % class 1 points
  \fill[acc] (1.0,1.0) circle (2.4pt);
  \fill[acc] (2.0,2.4) circle (2.4pt);
  \fill[acc] (1.4,3.2) circle (2.4pt);
  \fill[acc] (2.3,0.8) circle (2.4pt);
  \node[acc, font=\scriptsize] at (1.5,0.35) {class one};
  % class 2 points
  \fill[grn] (4.0,1.4) circle (2.4pt);
  \fill[grn] (5.1,2.7) circle (2.4pt);
  \fill[grn] (4.6,0.9) circle (2.4pt);
  \node[grn, font=\scriptsize] at (4.5,0.35) {class two};
  % class 3 points
  \fill[black] (7.0,2.2) circle (2.4pt);
  \fill[black] (8.0,1.2) circle (2.4pt);
  \fill[black] (7.5,3.1) circle (2.4pt);
  \fill[black] (8.1,2.8) circle (2.4pt);
  \node[font=\scriptsize] at (7.5,0.35) {class three};
  % related pair inside a class
  \draw[acc, thick] (1.0,1.0) -- (2.0,2.4);
  \node[acc, font=\scriptsize, anchor=west] at (2.1,2.55) {related};
\end{tikzpicture}
$$

### Cardinality

Size is compared by matching, not counting. Sets $A$ and $B$ are
**equinumerous**, written $A \sim B$, when some one-to-one function maps $A$ onto
$B$. This is reflexive, symmetric, and transitive, and it agrees with ordinary
counting on finite sets while extending to infinite ones.

> **Definition (Finite, countable).** A set $A$ is **finite** when it is
> equinumerous with $\{0, 1, \dots, n-1\}$ for some natural number $n$. It is
> **countable** when some function maps it one-to-one into $\mathbb{N}$;
> equivalently, $A \preceq \mathbb{N}$. A countable set is either finite or
> equinumerous with $\mathbb{N}$ itself.

Two facts about countability are used constantly when the language is countable.

> **Theorem (Countability of finite sequences).** If $A$ is countable, then the set of all finite sequences of
> members of $A$ is countable.

The proof codes a sequence $\langle a_0, \dots, a_m \rangle$ by the number
$2^{f(a_0)+1} 3^{f(a_1)+1} \cdots p_m^{f(a_m)+1}$, a product of prime powers whose
exponents recover the entries. The same prime-power coding, scaled up, is the
mechanism behind the [arithmetization of syntax](/logic/incompleteness/incompleteness-and-undecidability)
in the incompleteness theorems. Since a formal language has countably many
expressions, its set of formulas and its set of finite proofs are both countable.

Not everything is countable. To be **dominated by** $B$, written $A \preceq B$, is to be
equinumerous with a subset of $B$; a set is countable exactly when
$A \preceq \mathbb{N}$. The cardinals are ordered: for any $\kappa$ and $\lambda$,
either $\kappa \le \lambda$ or $\lambda \le \kappa$, and any nonempty set of
cardinals has a least member. The finite cardinals $0, 1, 2, \dots$ are followed
by the least infinite cardinal $\aleph_0 = \card \mathbb{N}$, and
Cantor's theorem gives a strictly larger one:

$$
\aleph_0 \;<\; 2^{\aleph_0} \;=\; \card \mathbb{R}.
$$

The reals are uncountable. So is $\mathcal{P}(\mathbb{N})$, which has the same
size $2^{\aleph_0}$. The distinction between countable and uncountable is
why the [Löwenheim–Skolem
theorems](/logic/models-and-theories/compactness-and-lowenheim-skolem) have force:
a first-order theory cannot constrain its models to a single size across that gap.

$$
% caption: The size ladder used throughout: naturals, integers, and rationals all
% share the countable cardinality below Cantor's gap; the reals and the power set
% of the naturals sit at the uncountable size above it.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  s/.style={draw, minimum width=17mm, minimum height=9mm, align=center}]
  \definecolor{acc}{HTML}{4A6FA5}
  \definecolor{grn}{HTML}{3C8C5A}
  % lower shelf: countable
  \draw[black, thick] (-0.4,-0.4) rectangle (10.4,1.6);
  \node[s] (nn) at (1.2,0.6) {N};
  \node[s] (zz) at (3.6,0.6) {Z};
  \node[s] (qq) at (6.0,0.6) {Q};
  \node[align=left, font=\scriptsize, anchor=west] at (7.3,0.6) {countable\\one size};
  % gap
  \draw[->, acc, very thick] (5.0,1.8) -- (5.0,3.0);
  \node[acc, font=\scriptsize, anchor=west] at (5.2,2.4) {Cantor: strictly larger};
  % upper shelf: uncountable
  \draw[black, thick] (-0.4,3.2) rectangle (10.4,5.2);
  \node[s, draw=grn, text=grn] (rr) at (1.6,4.2) {R};
  \node[s, draw=grn, text=grn] (pn) at (4.4,4.2) {P(N)};
  \node[align=left, font=\scriptsize, anchor=west] at (5.9,4.2) {uncountable\\larger size};
\end{tikzpicture}
$$

### The axiom of choice and Zorn's lemma

A handful of arguments need a nonconstructive principle: given infinitely many
nonempty sets, a single function can select one member from each. This is the
**axiom of choice**. Its uses in this subject can usually be eliminated when the
language is restricted to be countable, but stating the general theorems cleanly
is easier with it. The form that appears in proofs is Zorn's lemma. Call a
collection $\mathcal{C}$ of sets a **chain** when any two of its members are
comparable under $\subseteq$.

> **Lemma (Zorn's lemma).** Let $\mathcal{A}$ be a set such that $\bigcup \mathcal{C} \in
> \mathcal{A}$ for every chain $\mathcal{C} \subseteq \mathcal{A}$. Then
> $\mathcal{A}$ has a **maximal** element — one that is a subset of no other
> member of $\mathcal{A}$.

The pattern is always the same. Order some family of "good" sets by inclusion;
check that unions of chains stay good; conclude a maximal good set exists. In the
[completeness theorem](/logic/deductive-calculus/completeness-and-consistency)
the good sets are the consistent sets of sentences, and the maximal one is a
maximal consistent set from which a model is read off.

[^intro]: Enderton, _Introduction_ — logic as a mathematical model of deductive thought, the airplane analogy for model-building, validity as form independent of content, and the four organizing questions.
[^ch0]: Enderton, Ch. 0 — Useful Facts about Sets: extensionality, ordered tuples and Lemma 0A, relations and functions, equivalence relations and partitions, countability (Theorem 0B), cardinal comparison and Cantor's theorem, the axiom of choice and Zorn's lemma.