\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{compactness theorem}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{model_theory}{}\paragraph*{{Model theory}}\label{model_theory}

[[!include model theory - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{theorem}{Theorem}\dotfill \pageref*{theorem} \linebreak
\noindent\hyperlink{remark}{Remark}\dotfill \pageref*{remark} \linebreak
\noindent\hyperlink{compactness_for_propositional_logic}{Compactness for propositional logic}\dotfill \pageref*{compactness_for_propositional_logic} \linebreak
\noindent\hyperlink{illustrations}{Illustrations}\dotfill \pageref*{illustrations} \linebreak
\noindent\hyperlink{totalorder}{Total orders}\dotfill \pageref*{totalorder} \linebreak
\noindent\hyperlink{choicelike_consequences}{Choice-like consequences}\dotfill \pageref*{choicelike_consequences} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

The \textbf{compactness theorem} is a fundamental result of \emph{[[model theory]]} on the existence of [[models]] of [[first-order theories]].

Historically it goes back to work of [[Gödel]] and Mal'cev in the 1930s.

[[Lindström's theorem]] uses the compactness and the [[Löwenheim-Skolem theorem]] to characterize classical first-order logic. The validity or non-validity of the compactness theorem in logical systems other than first-order logic plays under the name of \emph{compactness property} an important role in [[abstract model theory]].

\hypertarget{theorem}{}\subsection*{{Theorem}}\label{theorem}

Briefly, the compactness theorem states that a set of first-order formulas $\Phi$ has a model precisely iff every finite subset of $\Phi$ has a model.

\hypertarget{remark}{}\subsubsection*{{Remark}}\label{remark}

There are different proofs for the compactness theorem e.g. an entirely `semantic' one using [[ultraproduct|ultraproducts]]. A particularly transparent one relies on the completeness theorem for first-order logic and the essential finitude of the notion of formal proof\footnote{In the German literature the compactness theorem is therefore also called `Endlichkeitssatz'.} : Suppose $\Phi$ has no model, due to completeness this implies that there is a contradiction $\varphi$ with $\Phi\vdash\varphi$ but such a deduction of $\varphi$ can involve only a finite subset $\Phi_0\subset \Phi$ hence $\Phi_0\vdash\varphi$ and $\Phi_0$ would have no model as well.

Despite the intuitive appeal, this approach obliges one to establish the completeness theorem, which depends on fiddly details of formal proofs and deductive systems to make rigorous.

\hypertarget{compactness_for_propositional_logic}{}\subsubsection*{{Compactness for propositional logic}}\label{compactness_for_propositional_logic}

The motivation for the terminology stems from the observation that the compactness theorem literally expresses the compactness of a suitable topology on first-order structures.

\hypertarget{illustrations}{}\subsection*{{Illustrations}}\label{illustrations}

As the compactness theorem is arguably the most fundamental result of model theory, there are too many examples of its use for us to do it much justice here. But perhaps a few examples here will help illustrate some typical uses.

\hypertarget{totalorder}{}\subsubsection*{{Total orders}}\label{totalorder}

\begin{prop}
\label{total}\hypertarget{total}{}
Every set $X$ can be totally ordered.

\end{prop}
Of course this trivially follows from the stronger result that every set can be [[well-ordered set|well-ordered]], if we permit the [[axiom of choice]]. But part of our point here is that we don't need the full strength of the axiom of choice: the result can be derived from the weaker ``choice principle'' called the [[ultrafilter theorem]], on which the compactness theorem depends.

\begin{proof}
Introduce a [[language]] (i.e., [[signature (in logic)|signature]]) with a constant symbol $c_p$ for each $p \in X$ and a binary relation symbol $L$, and for a [[theory]] take axioms $\neg (c_p = c_q)$ whenever $p \neq q$ in $X$ and the usual axioms to make $L$ a [[total order]] (reflexivity, transitivity, antisymmetry, and connectedness). This theory is finitely satisfiable: any finite subset $\Sigma$ of the axioms has a model, by interpreting each $c_x$ occurring in an inequality axiom belonging to $\Sigma$ simply as $x$, and totally ordering those finitely many $x$ in some way to interpret $L$; the remaining $c_x$ can be interpreted as the bottom element of that total order without any harm. By the compactness theorem, this theory has a model $Y$, and the restriction of the total order on $Y$ to the set of all constants $c_x$ in $Y$ is used to totally order all the $x \in X$.

\end{proof}
With slightly more effort, a similar argument can be given to show that every [[partial order]] can be extended to a total order. We just proved the case where the partial order is discrete.

\hypertarget{choicelike_consequences}{}\paragraph*{{Choice-like consequences}}\label{choicelike_consequences}

Again, we assume the ultrafilter principle but do not assume the [[axiom of choice]].

\begin{cor}
\label{surj}\hypertarget{surj}{}
If $p: F \to X$ is [[surjection|surjective]] and every [[fiber]] is finite, then $p$ has a section $s$.

\end{cor}
\begin{proof}
Using Proposition \ref{total} to totally order $F$, each fiber inherits a total order that is a [[well-ordered set|well-order]] by finiteness, and we can choose $s(x)$ for $x \in X$ to be the least element in the fiber $F_x$ by nonemptiness.

\end{proof}
\begin{prop}
\label{countable}\hypertarget{countable}{}
A countable disjoint union of finite sets is again countable.

\end{prop}
\begin{proof}
Let $F_n$ be the countable family and let $F$ be the union; again we have a fibering $F \to \mathbb{N}$ with fiber $F_n$ over $n$. Using Proposition \ref{total}, totally order $F$; each $F_n$ inherits an order from $F$, and since total orders on finite sets are well-orders, we have chosen a countable family of well-orders. Now put the [[lexicographic order]] on the set of pairs $F' = \{(n, x): n \in \mathbb{N}, x \in F_n\}$. This is a well-ordering, and clearly the projection $F' \to F$ is a bijection, so we obtain a well-ordering of $F$ by transport of structure (differing, probably, from the original total ordering of $F$ which has done its job but is of no further use). Then we can define a partial map $\phi: \mathbb{N} \to F$ by induction: $\phi(0)$ is the bottom of $F$, and $\phi(n+1)$ is (if it exists) the bottom of the complement of $\phi([0, n])$. This defines a bijection from an initial segment of $\mathbb{N}$ onto $F$, which is what we wanted.

\end{proof}
\begin{cor}
\label{wkl}\hypertarget{wkl}{}
\textbf{(Weak K\"o{}nig's lemma)} Every infinite [[tree]] for which there is finite branching at each node has an infinite branch.

\end{cor}
\begin{proof}
A tree is by definition the [[category of elements]] $e = (n, x \in F(n))$ of a [[presheaf]] $F: \mathbb{N}^{op} \to Set$ where $\mathbb{N}$ has its usual order and $F(0)$ is terminal. A \emph{descendant} of an element $e = (n, x \in F(n))$ is an element that maps to $e$, i.e., an element $(m, y \in F(m))$ with $m \geq n$ and $F(m \geq n)(y) = x$. A \emph{child} of $e$ is such a descendant with $m = n+1$.

By the branching hypothesis, the set $E_n$ of elements $e = (n, x)$ is finite. By Proposition \ref{countable}, the set of nodes or elements $E = \sum_n E_n$ is countable, i.e., is enumerated by some bijection $\mathbb{N} \to E$. Then an infinite branch (a [[global section]] $s$ of $F$) is given by recursion as follows: $s(0)$ is the root (the unique element of $E_0$). The root has infinitely many descendants since the tree is infinite. Given that $s(n) \in F(n)$ has infinitely many descendants, let $s(n+1)$ be the first of its children in the enumeration that also has infinitely many descendants (such children exist since $s(n)$ has only finitely many children by the branching hypothesis).

\end{proof}
Weak K\"o{}nig's lemma lends its name to one the so-called Big Five systems of [[reverse mathematics]], namely $WKL_0$, and (over a certain weak fragment of second-order arithmetic) is equivalent to many results in classical elementary analysis.

\begin{remark}
\label{weak}\hypertarget{weak}{}
Actually, the WKL as stated above is stronger than another result that goes by that name, namely that an infinite subtree of the infinite binary tree $2^{\lt \omega}$ (consisting of finite 0-1 sequences or words, where the root is the empty word and the parent of a nonempty word is obtained by leaving off the last binary digit) has an infinite branch. This is provable in ZF without choice or other choice-free forms of set theory; the key point is that $2^{\lt \omega}$, and subtrees thereof, already have enumerations ready to hand; we don't need an argument like Proposition \ref{countable} to construct one. From there, the recursive construction of a branch in the proof of Corollary \ref{wkl} can be performed without making choices.

\end{remark}
\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[Löwenheim-Skolem theorem]]


\item [[Skolem's paradox]]


\item [[Lindström's theorem]]


\item [[Deligne completeness theorem]]


\item [[Stone duality]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item Wikipedia, \emph{\href{https://en.wikipedia.org/wiki/Compactness_theorem}{compactness theorem}}

\end{itemize}
[[!redirects compactness theorems]]



\end{document}