\documentclass[12pt]{article}

%%%%%%%%%%%%%%%%%%
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{txfonts}
\usepackage{enumerate}
\usepackage{fancyhdr}

%%%custom definitions
\renewcommand{\qedsymbol}{\nobreak
\fbox{\tiny \textsc{q.e.d.}}
}

%%%semantic definitions
\newcommand{\intersect}{\cap}
\newcommand{\union}{\cup}
\newcommand{\nonnegative}{\mathbb{N}}
\newcommand{\integer}{\mathbb{Z}}
\newcommand{\rational}{\mathbb{Q}}
\newcommand{\real}{\mathbb{R}}
\newcommand{\complex}{\mathbb{C}}
\renewcommand{\implies}{\Rightarrow}
\newcommand{\assign}{\leftarrow}
\DeclareMathOperator*{\lcm}{lcm}
%%%

%%%local definitions
\newcommand{\symnot}{\neg}
\newcommand{\symand}{\wedge}
\newcommand{\symor}{\vee}
\newcommand{\symimply}{\rightarrow}
\DeclareMathOperator{\symxor}{XOR}
\DeclareMathOperator{\symnand}{NAND}
\DeclareMathOperator{\setSent}{Sent}
%%%

%%%Theorem environment
\newtheorem{alg}{Algorithm}
\newtheorem{conj}{Conjecture}
\newtheorem{cor}{Corollary}
\newtheorem*{cor*}{Corollary}
\newtheorem{claim}{Claim}
\newtheorem*{claim*}{Claim}
\newtheorem{dfn}{Definition}
\newtheorem{ex}{Example}
\newtheorem{lem}{Lemma}
\newtheorem{prob}{Problem}
\newtheorem{prop}{Proposition}
\newtheorem{soln}{Solution}
\newtheorem{thm}{Theorem}
\newtheorem*{thm*}{Theorem}

\begin{document}
%%% Title boilerplate
\title{Logic Homework 4}
\author{\textsc{D. Dakota Blair}}
\baselineskip=4ex
\maketitle
%%%

\begin{abstract}
A presentation of solutions to the fourth homework.
\end{abstract}

\section*{Problem 4.1}
\begin{thm*}[Compactness of Propositional Logic]
A set of sentences has a model if and only if every finite subset has a model.
\end{thm*}

\begin{cor*}[Consequence is finitary]
A statement that follows from a set of sentences in prepositional logic
follows from a finite subset of them.
\end{cor*}

\begin{cor*}
The four-color problem is finitary.
That is, only finite maps need be considered.
\end{cor*}

\begin{proof}
Note that a given (possibly infinite) colored map $a$ may be checked for
the four-color property by a (possibly infinite) set $M_a$ of sentences.
Define $C$, the set of colors used in a colored map $a$ as
\[
C = \{x | x \mbox{ is a color used in colored map } a\}.
\]
Then for a state $S_\alpha \in a$ define a map
$\mbox{Color}:a \rightarrow C$ mapping the state
$S_\alpha$ to its color in $a$.
The sentence
\[
\phi(S_\alpha, S_\beta) =
(S_\alpha \neq S_\beta) \symand
\left(\mbox{Color}(S_\alpha) \neq \mbox{Color}(S_\beta) \right) \symand
(|C| \leq 4)
\]
may be constructed for each pair of neighboring states
$S_\alpha, S_\beta \in a$.
Then 
\[
M_a = \bigcup_{\substack{
S_\alpha \in a\\
S_\beta \in a\\
S_\alpha \mbox{ \tiny neighbors \normalsize } S_\beta}}
\phi(S_\alpha, S_\beta)
\]
is a set of sentences which must all be true if the four-color property holds
for the map $a$. If any one is false, the property does not hold for that map.
By the compactness theorem there exists a finite subset $m_a$ of this
set which sufficies to prove the theorem on this map.
Let
\[
M = \bigcup_a m_a.
\]
This is a (possibly infinite) set of sentences. Therefore by the compactness
theorem there exists a finite set $M_0$ that models $\phi$.

Then the set $M_0$ corresponds to a finite portion of the map $a$.
Since this portion is all that is needed to prove the four-color
property of this map, it may be considered independently as a finite map.
Because this can be done for any colored map, only finite maps need be
considered for the four-color theorem.
\end{proof}
\end{document}
