\documentclass[11pt]{article}
\usepackage{fullpage}
\usepackage{times}
\usepackage{amsmath,amsfonts,amssymb,amsthm}
\usepackage{shadow}
\usepackage{enumerate}
\usepackage{fitch}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}
\newtheorem{claim}{Claim}
\newtheorem{definition}{Definition}
\newcommand{\imp}{\rightarrow}
\newcommand{\mc}[1]{\mathcal{#1}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\mfr}[1]{\mathfrak{#1}}
\newcommand{\mcal}[1]{\mathcal{#1}}

\newcommand{\ignore}[1]{}
\newcommand{\mybox}{\shabox}

\newcommand{\bzero}{\mathbf{0}}
\newcommand{\bone}{\mathbf{1}}
\newcommand{\vpi}{\varphi}
\DeclareMathOperator{\Cons}{Cons}
\DeclareMathOperator{\Free}{Free}

\begin{document}

\par\noindent{\bf CS81 HW\#5 Spring 2012} {\em Out: 02/15/2012. Due: 02/22/2012 (before class)}
\paragraph{Policy on homeworks}
\begin{enumerate}
\item {\em Collaboration}:
        You may discuss a question with any other student currently taking CS81 provided:
        (i) both of you contribute equally;
        (ii) you come away from any discussion with an understanding in your mind (and no archived solution of any form is retained);
        (iii) your submission is your own work prepared by yourself on a separate occassion.

\item {\em Reference materials}:
        You should only refer to materials from this semester of CS81
        (class notes, handouts, textbooks, grutors, instructor, etc).

\item {\em Submission}:
        Your submission should be legible or is prepared using TeX.
\end{enumerate}

\vspace{.2in}

\par\noindent{\bf G\"{o}del's peak via Henkin's trail\footnote{Map by Ebbinghaus, Flum and Thomas.}}

\vspace{.1in}

\par\noindent
Fix a first-order language $L_{S}$ over a {\bf countable} alphabet $S$.
Let $\Phi$ be a collection of formulas of $L_{S}$. 
Assume the {\bf Soundness} Theorem for $ND$ holds: if $\Phi \vdash \vpi$, then $\Phi \models \vpi$, 
for any formula $\vpi$.
Let $\Free(\Phi)$ denote the set of free (unbound) variables which appear in $\Phi$. \\

\par\noindent{\sc Prove carefully all the claims in the shadowed boxes.}

\begin{enumerate}[I.]
%1
\item \label{stmt1}
	\begin{enumerate}[(a)]
	\item We say $\Phi$ is {\bf consistent} ({\em notation}: $\Cons(\Phi)$) iff
		there is no formula $\phi$ so that $\Phi \vdash \phi$ and $\Phi \vdash \lnot\phi$. 
	\item We say $\Phi$ is {\bf satisfiable} iff there is a model $\mfr{M}$ for which
		$\mfr{M} \models \Phi$.
	\end{enumerate}

%2
\item \label{stmt2}
	\fbox{$\Phi$ is not consistent iff $\Phi \vdash \vpi$, for any formula $\vpi$.}
        \begin{proof}
        ($\Rightarrow$) If $\Phi$ is not consistent, then there is a formula $\psi$ for which $\Phi \vdash \psi$
        and $\Phi \vdash \lnot\psi$. From this we obtain $\Phi \vdash \bot$ and thus $\Phi \vdash \vpi$,
        for any formula $\vpi$.\\
        ($\Leftarrow$) If $\Phi \vdash \psi$, for any formula $\psi$, then $\Phi \vdash \vpi$ and
        $\Phi \vdash \lnot\vpi$, for any formula $\vpi$. Thus, $\Phi$ is not consistent.
        \end{proof}

%4
\item \label{stmt4}
	\fbox{If $\Phi$ is satisfiable, then $\Phi$ is consistent.}
        \begin{proof}
        If $\Phi$ is not consistent, then for some formula $\vpi$ we have $\Phi \vdash \vpi$ and
        $\Phi \vdash \lnot\vpi$. By the Soundness Theorem, $\Phi \models \vpi$ and $\Phi \models \lnot\vpi$.
        So, $\Phi$ is not satisfiable since no model can satisfy both $\vpi$ and $\lnot\vpi$.
        \end{proof}

	The {\em structure} of the above proof (in Natural Deduction {\em itself}) is:
	\[
	\begin{nd}
		\hypo {2} {\Phi \mbox{ is not consistent}}	\by{assumption}{}
		\have {3} {(\exists \vpi)[(\Phi \vdash \vpi) \wedge (\Phi \vdash \lnot\vpi)]}
			\by{definition of inconsistent}{2}
		\have {4} {(\Phi \vdash \hat{\vpi}) \wedge (\Phi \vdash \lnot\hat{\vpi})}
			\Ee{3}
		\have {5} {\Phi \vdash \hat{\vpi}}
			\ae{4}
		\have {6} {\Phi \models \hat{\vpi}}
			\by{by Soundness Theorem}{5}
	\end{nd}
	\]
	\[
	\begin{ndresume}
		\have {7} {\Phi \vdash \lnot\hat{\vpi}}
			\ae{4}
		\have {8} {\Phi \models \lnot\hat{\vpi}}
			\by{by Soundness Theorem}{7}
		\have {9} {\Phi \models (\hat{\vpi} \wedge \lnot\hat{\vpi})}
			\by{by property of semantic entailment}{}
		\have {10} {\Phi \models \bot}
			\by{identity for $\bot$}{}
		\have {11} {\Phi \mbox{ is not satisfiable}}
			\by{since no model can satisfy $\bot$}{}
	\end{ndresume}
	\]

%5
\item \label{stmt5}
	For each formula $\vpi$, we have:
	\begin{enumerate}[(a)]
	%5a
	\item \label{stmt5a}
	\fbox{If $\Phi \not\vdash \vpi$, then $\Cons(\Phi \cup \{\lnot\vpi\})$.}
        \begin{proof}
        Suppose that $\Phi \cup \{\lnot\vpi\}$ is not consistent. Then, for some formula $\psi$, we have
        $\Phi \cup \{\lnot\vpi\} \vdash \psi$ and $\Phi \cup \{\lnot\vpi\} \vdash \lnot\psi$.
        Thus, we may deduce $\Phi \vdash \vpi$ as follows:
        \begin{small}
        \[
        \begin{nd}
        \hypo {1} {\Phi}        \by{premise}{}
        \open
                \hypo {2} {\lnot\vpi}   \by{assumption}{}
                \have {3} {\psi}        \by{since $\Phi,\lnot\vpi \vdash \psi$}{}
                \have {4} {\lnot\psi}   \by{since $\Phi,\lnot\vpi \vdash \lnot\psi$}{}
                \have {5} {\bot}        \ni{3,4}
        \close
        \have {6} {\lnot\lnot\vpi}      \ni{2-5}
        \have {7} {\vpi}                \nne{6}
        \end{nd}
        \]
        \end{small}
        \end{proof}


	%5b
	\item \label{stmt5b}
	\mybox{If $\Cons(\Phi)$ and $\Phi \vdash \vpi$, then $\Cons(\Phi \cup \{\vpi\})$.}

	%5c
	\item \label{stmt5c}
	\mybox{If $\Cons(\Phi)$, then $\Cons(\Phi \cup \{\vpi\})$ or $\Cons(\Phi \cup \{\lnot\vpi\})$.}

	\end{enumerate}

%6
\item \label{stmt6}
	\fbox{$\Phi$ is consistent iff any finite subset of $\Phi$ is consistent.}

%7
\item \label{stmt7}
	\begin{enumerate}[(a)]
	\item We say $\Phi$ is {\bf maximally consistent} iff $\Cons(\Phi)$ and $\forall\vpi$
		if $\Cons(\Phi \cup \{\vpi\})$ then $\vpi \in \Phi$.
	\item We say $\Phi$ has {\bf witnesses}  iff $\forall\vpi = (\exists x)\psi$, 
		there is a term $t$ where $((\exists x)\psi \to \psi[t/x]) \in \Phi$.
	\end{enumerate}

%8
\item \label{stmt8}
	Let $\Phi$ be maximally consistent and has witnesses. Then, for any formulas $\vpi$ and $\psi$:
	\begin{enumerate}[(a)]
	\item \label{stmt8a}
	\mybox{If $\Phi \vdash \vpi$ then $\vpi \in \Phi$.}

	\item \label{stmt8b}
	\mybox{Either $\vpi \in \Phi$ or $\lnot\vpi \in \Phi$.}

	\item \label{stmt8c}
	\mybox{$(\vpi \vee \psi) \in \Phi$ iff $\vpi \in \Phi$ or $\psi \in \Phi$.}

	\item \label{stmt8d}
	\mybox{If $(\vpi \to \psi) \in \Phi$ and $\vpi \in \Phi$, then $\psi \in \Phi$.}

	\item \label{stmt8e}
	\mybox{$(\exists x)\psi \in \Phi$ iff there is a term $t$ with $\psi[t/x] \in \Phi$.}
	\end{enumerate}

\item \label{stmt9}
	Let $T_{S}$ be the set of all $S$-terms in $L_{S}$. 
	We define an \shabox{\bf equivalence relation} $\sim$ on $T_{S}$ as:
	\[
		t_{0} \sim t_{1} \ \ \ \mbox{ iff } \ \ \ (t_{0} = t_{1}) \in \Phi.
	\]
	For a term $t$, let $[t]$ be the equivalence class of $t$ which is the set of terms equivalent to $t$:
	\[
		[t] = \{t' \in T_{S} : t \sim t'\}.
	\]
	Let $T_{\Phi}$ be the set of equivalence classes:
	\[
		T_{\Phi} = \{[t] : t \in T_{S}\}.
	\]

\item \label{stmt10}
	Let $\mfr{A}_{\Phi} = (T_{\Phi},\mfr{a})$ be an {\bf $S$-structure} defined as follows:
	\begin{enumerate}[(a)]
	\item \label{stmt10a}
	For each constant $c \in S$, we have $\mfr{a}(c) = [c]$.

	\item \label{stmt10b}
	For each $n$-ary function symbol $f \in S$, we have
	$\mfr{a}(f)([t_{0}],\ldots,[t_{n-1}]) = [f(t_{0},\ldots,t_{n-1})]$.

	\item \label{stmt10c}
	For each $n$-ary relation symbol $R \in S$:
	\[
		([t_{0}],\ldots,[t_{n-1}]) \in \mfr{a}(R) 
		\ \ \ \mbox{ iff } \ \ \ 
		R(t_{0},\ldots,t_{n-1}) \in \Phi.
	\]
	\end{enumerate}
	Let $\sigma_{\Phi}$ be a valuation of the variables where for each variable $x \in S$,
	we have $\sigma_{\Phi}(x) = [x]$.

	This defines a {\bf model} $\mfr{M}_{\Phi} = (\mfr{A}_{\Phi},\sigma_{\Phi})$ 
	over the language $L_{S}$.


\item \label{stmt11}
	\begin{enumerate}[(a)]
	\item \label{stmt11a}
	\fbox{For all terms $t$, we have $\mfr{M}_{\Phi}(t) = [t]$.}

	\item \label{stmt11b}
	\fbox{For all {\em atomic} formulas $\vpi$, we have $\mfr{M}_{\Phi} \models \vpi$ iff $\vpi \in \Phi$.}

	\end{enumerate}

\item \label{stmt12}
	\fbox{Let $\Phi$ be maximally consistent and has witnesses. Then, for each formula $\vpi$,
	$\mfr{M}_{\Phi} \models \vpi \mbox{ iff } \vpi \in \Phi$.}

\item \label{stmt13}
	\fbox{Let $\Phi$ be consistent and $\Free(\Phi)$ is {\bf finite}.
	Then, there is a consistent $\Psi \supseteq \Phi$ which has {\em witnesses}.}

\item \label{stmt14}
	\fbox{Let $\Psi$ be consistent. Then, there is a {\em maximally consistent} $\Theta \supseteq \Psi$.}

\item \label{stmt15}
	\fbox{%Let $\Phi \subseteq L_{S}$, where $S$ is at most {\bf countable}.
	If $\Phi$ is consistent, then $\Phi$ satisfiable.}

\item \label{peak}
	\mybox{If $\Phi \models \vpi$, then $\Phi \vdash \vpi$.}

\end{enumerate}

\end{document}


