2.6.5: Lindenbaum’s Lemma

Last updated
Save as PDF

Page ID: 121714

$ \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } $

$ \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} $

$ \newcommand{\dsum}{\displaystyle\sum\limits} $

$ \newcommand{\dint}{\displaystyle\int\limits} $

$ \newcommand{\dlim}{\displaystyle\lim\limits} $

$ \newcommand{\id}{\mathrm{id}}$ $ \newcommand{\Span}{\mathrm{span}}$

( \newcommand{\kernel}{\mathrm{null}\,}\) $ \newcommand{\range}{\mathrm{range}\,}$

$ \newcommand{\RealPart}{\mathrm{Re}}$ $ \newcommand{\ImaginaryPart}{\mathrm{Im}}$

$ \newcommand{\Argument}{\mathrm{Arg}}$ $ \newcommand{\norm}[1]{\| #1 \|}$

$ \newcommand{\inner}[2]{\langle #1, #2 \rangle}$

$ \newcommand{\Span}{\mathrm{span}}$

$ \newcommand{\id}{\mathrm{id}}$

$ \newcommand{\Span}{\mathrm{span}}$

$ \newcommand{\kernel}{\mathrm{null}\,}$

$ \newcommand{\range}{\mathrm{range}\,}$

$ \newcommand{\RealPart}{\mathrm{Re}}$

$ \newcommand{\ImaginaryPart}{\mathrm{Im}}$

$ \newcommand{\Argument}{\mathrm{Arg}}$

$ \newcommand{\norm}[1]{\| #1 \|}$

$ \newcommand{\inner}[2]{\langle #1, #2 \rangle}$

$ \newcommand{\Span}{\mathrm{span}}$ $ \newcommand{\AA}{\unicode[.8,0]{x212B}}$

$ \newcommand{\vectorA}[1]{\vec{#1}} % arrow$

$ \newcommand{\vectorAt}[1]{\vec{\text{#1}}} % arrow$

$ \newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } $

$ \newcommand{\vectorC}[1]{\textbf{#1}} $

$ \newcommand{\vectorD}[1]{\overrightarrow{#1}} $

$ \newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}} $

$ \newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}} $

$ \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } $

$\newcommand{\longvect}{\overrightarrow}$

$ \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} $

$\newcommand{\avec}{\mathbf a}$ $\newcommand{\bvec}{\mathbf b}$ $\newcommand{\cvec}{\mathbf c}$ $\newcommand{\dvec}{\mathbf d}$ $\newcommand{\dtil}{\widetilde{\mathbf d}}$ $\newcommand{\evec}{\mathbf e}$ $\newcommand{\fvec}{\mathbf f}$ $\newcommand{\nvec}{\mathbf n}$ $\newcommand{\pvec}{\mathbf p}$ $\newcommand{\qvec}{\mathbf q}$ $\newcommand{\svec}{\mathbf s}$ $\newcommand{\tvec}{\mathbf t}$ $\newcommand{\uvec}{\mathbf u}$ $\newcommand{\vvec}{\mathbf v}$ $\newcommand{\wvec}{\mathbf w}$ $\newcommand{\xvec}{\mathbf x}$ $\newcommand{\yvec}{\mathbf y}$ $\newcommand{\zvec}{\mathbf z}$ $\newcommand{\rvec}{\mathbf r}$ $\newcommand{\mvec}{\mathbf m}$ $\newcommand{\zerovec}{\mathbf 0}$ $\newcommand{\onevec}{\mathbf 1}$ $\newcommand{\real}{\mathbb R}$ $\newcommand{\twovec}[2]{\left[\begin{array}{r}#1 \\ #2 \end{array}\right]}$ $\newcommand{\ctwovec}[2]{\left[\begin{array}{c}#1 \\ #2 \end{array}\right]}$ $\newcommand{\threevec}[3]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \end{array}\right]}$ $\newcommand{\cthreevec}[3]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \end{array}\right]}$ $\newcommand{\fourvec}[4]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}$ $\newcommand{\cfourvec}[4]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}$ $\newcommand{\fivevec}[5]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}$ $\newcommand{\cfivevec}[5]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}$ $\newcommand{\mattwo}[4]{\left[\begin{array}{rr}#1 \amp #2 \\ #3 \amp #4 \\ \end{array}\right]}$ $\newcommand{\laspan}[1]{\text{Span}\{#1\}}$ $\newcommand{\bcal}{\cal B}$ $\newcommand{\ccal}{\cal C}$ $\newcommand{\scal}{\cal S}$ $\newcommand{\wcal}{\cal W}$ $\newcommand{\ecal}{\cal E}$ $\newcommand{\coords}[2]{\left\{#1\right\}_{#2}}$ $\newcommand{\gray}[1]{\color{gray}{#1}}$ $\newcommand{\lgray}[1]{\color{lightgray}{#1}}$ $\newcommand{\rank}{\operatorname{rank}}$ $\newcommand{\row}{\text{Row}}$ $\newcommand{\col}{\text{Col}}$ $\renewcommand{\row}{\text{Row}}$ $\newcommand{\nul}{\text{Nul}}$ $\newcommand{\var}{\text{Var}}$ $\newcommand{\corr}{\text{corr}}$ $\newcommand{\len}[1]{\left|#1\right|}$ $\newcommand{\bbar}{\overline{\bvec}}$ $\newcommand{\bhat}{\widehat{\bvec}}$ $\newcommand{\bperp}{\bvec^\perp}$ $\newcommand{\xhat}{\widehat{\xvec}}$ $\newcommand{\vhat}{\widehat{\vvec}}$ $\newcommand{\uhat}{\widehat{\uvec}}$ $\newcommand{\what}{\widehat{\wvec}}$ $\newcommand{\Sighat}{\widehat{\Sigma}}$ $\newcommand{\lt}{<}$ $\newcommand{\gt}{>}$ $\newcommand{\amp}{&}$ $\definecolor{fillinmathshade}{gray}{0.9}$

$\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} } }$

We now prove a lemma that shows that any consistent set of sentences is contained in some set of sentences which is not just consistent, but also complete. The proof works by adding one sentence at a time, guaranteeing at each step that the set remains consistent. We do this so that for every $A$, either $A$ or $\lnot A$ gets added at some stage. The union of all stages in that construction then contains either $A$ or its negation $\lnot A$ and is thus complete. It is also consistent, since we made sure at each stage not to introduce an inconsistency.

Lemma $\PageIndex{1}$: Lindenbaum’s Lemma

Every consistent set $\Gamma$ in a language $\Lang{L}$ can be extended to a complete and consistent set $\Gamma^*$.

Proof. Let $\Gamma$ be consistent. Let $A_0$, $A_1$, … be an enumeration of all the sentences of $\Lang L$. Define $\Gamma_0 = \Gamma$, and \[\Gamma_{n+1} = \begin{cases} \Gamma_n \cup \{ A_n \} & \textrm{if $\Gamma_n \cup \{A_n\}$ is consistent;} \\ \Gamma_n \cup \{ \lnot A_n \} & \textrm{otherwise.} \end{cases}\nonumber\] Let $\Gamma^* = \bigcup_{n \geq 0} \Gamma_n$.

Each $\Gamma_n$ is consistent: $\Gamma_0$ is consistent by definition. If $\Gamma_{n+1} = \Gamma_n \cup \{A_n\}$, this is because the latter is consistent. If it isn’t, $\Gamma_{n+1} = \Gamma_n \cup \{\lnot A_n\}$. We have to verify that $\Gamma_n \cup \{\lnot A_n\}$ is consistent. Suppose it’s not. Then both $\Gamma_n \cup \{A_n\}$ and $\Gamma_n \cup \{\lnot A_n\}$ are inconsistent. This means that $\Gamma_n$ would be inconsistent by Propositions 8.9.3 and 9.8.3, contrary to the induction hypothesis.

For every $n$ and every $i < n$, $\Gamma_i \subseteq \Gamma_n$. This follows by a simple induction on $n$. For $n=0$, there are no $i < 0$, so the claim holds automatically. For the inductive step, suppose it is true for $n$. We have $\Gamma_{n+1} = \Gamma_n \cup \{A_n\}$ or $= \Gamma_n \cup \{\lnot A_n\}$ by construction. So $\Gamma_n \subseteq \Gamma_{n+1}$. If $i < n$, then $\Gamma_i \subseteq \Gamma_n$ by inductive hypothesis, and so $\subseteq \Gamma_{n+1}$ by transitivity of $\subseteq$.

From this it follows that every finite subset of $\Gamma^*$ is a subset of $\Gamma_n$ for some $n$, since each $B \in \Gamma^*$ not already in $\Gamma_0$ is added at some stage $i$. If $n$ is the last one of these, then all $B$ in the finite subset are in $\Gamma_n$. So, every finite subset of $\Gamma^*$ is consistent. By Propositions 8.8.5 and 9.7.5, $\Gamma^*$ is consistent.

Every sentence of $\Frm[L]$ appears on the list used to define $\Gamma^*$. If $A_n \notin \Gamma^*$, then that is because $\Gamma_n \cup \{A_n\}$ was inconsistent. But then $\lnot A_n \in \Gamma^*$, so $\Gamma^*$ is complete. ◻

Search

Text Color

Text Size

Margin Size

Font Type