\documentclass{article}

\usepackage{amsmath}
\usepackage{amssymb}

\usepackage{bussproofs}

\newcommand{\con}{{\bigwedge \hspace{-2.5mm} \bigwedge}}
\newcommand{\dis}{\bigvee \hspace{-2.5mm} \bigvee}

\newcommand{\unsat}{unsatisfiable}
\newcommand{\sat}{satisfiable}


\title{History of Logic\\
Final Exam (Take Home)} 
\author{Joost J.\  Joosten}
\begin{document}
\maketitle

Please submit your answers by email to me before June 28, say, 18:00. 
Those taking this exam for level 3 are expected to give more formal proofs.
 
\begin{enumerate}

\item
In this exercise, $\sf PA$ stands for Peano Arithmetic as presented in the book.
\begin{enumerate}
\item
Let $\pi \in \Pi^0_1$ be such that ${\sf PA} \nvdash \neg \pi$. Prove that then necessarily, $\pi$ is true.
\item
Give a $\sf PA$ proof to the effect that
\[
\forall x\, \forall y\ (x+y =y+x).
\]


\end{enumerate}

\item
Prove that there is a model of true arithmetic, such that there are two non-standard elements $c$ and $d$ with $c<d$ such that $c+i\neq d$ for any standard number $i$.


\item
Let $f$ be a computable function and let $T$ be a theory containing the by now so familiar sufficient amount of arithmetic. Explain informally why it is the case that if 
\[
f(m) = n\mbox{, then } T \vdash f(\overline{m}) = \overline{n}.
\]

\item
Recall L\"ob's theorem:
\[
T\vdash {\sf Bew}_T(\ulcorner A \urcorner) \to A \ \ \Rightarrow \ \ T\vdash A.
\]
\begin{enumerate}
\item
Prove L\"ob's theorem using G\"odel's second incompleteness theorem as is sketched in the book.
\item
Prove G\"odel's second incompleteness theorem using L\"ob's theorem and a clever substitution.
\item
Use L\"ob's theorem to prove\footnote{Hint: take for $A$ the formalization of L\"ob and use the fact that $T \vdash {\sf Bew}_T(\ulcorner B\to C \urcorner)\wedge {\sf Bew}_T(\ulcorner B\urcorner) \to {\sf Bew}_T(\ulcorner C\urcorner)$.} the formalized version of L\"ob's theorem:
\[
T\vdash  {\sf Bew}_T(\ulcorner {\sf Bew}_T(\ulcorner A \urcorner) \to A\urcorner) \to {\sf Bew}_T(\ulcorner A \urcorner) .
\]
\end{enumerate}


\item
Consider the Rosser Sentence from the book. Let us call it $R_T$ for the moment. 
\begin{enumerate}
\item
Show that $R_T$ is a $\Pi_1^0$ sentence.

\item
Suppose $T$ is a theory such that it proves the \emph{minimal number principle} for decidable predicates. That is, if $\varphi$ is some decidable predicate, then 
\[
T\vdash \exists x\  \varphi (x) \to \exists y\ (\varphi (y) \wedge \forall \, z{<}y \ \neg \varphi(z)) .  
\]
In the rest of this exercise, we shall assume that $T$ is such a theory. Prove that, 
\[
T\vdash \varphi \Rightarrow 
T\vdash \exists y\ ({\sf Proof}_T(y, \ulcorner   \varphi \urcorner)
\wedge \forall \, z{<}y \neg {\sf Proof}_T(z, \ulcorner   \varphi  \urcorner))
\]

\item
Show that if a theory $T$ is consistent, then its Rosser sentence $R_T$ will be undecidable in $T$.

\end{enumerate}
\item
The so-called \emph{busy beaver} function $B$ is defined as follows.
\[
B(w) = \max \{ s \mid P_i(j) =s \ \& \ |\langle i,j\rangle|\leq w \}
\]
\begin{enumerate}
\item
Do you expect the busy beaver function to be a slow-growing or rather a fast growing function.

\item
Use Chaitin's incompleteness theorem to prove that $K(s)$ is not a computable function.

\item
Prove that the busy beaver function is not a computable function.

\end{enumerate}



\end{enumerate}

Choose one of the following two exercises.

\begin{enumerate}
\item[A]
Prove that for any $n$, we can find a sequence of computable enumerable sets $A_i$ such that 
\[
A_0 \subset A_1 \subset \ldots \subset A_n
\]
and also such that $A_{i+1}\setminus A_i$ is not computably enumerable for 
$0\leq i< n$.

\item[B]
Write a mini-essay of at most 4 A-4 on one of the following topics:
\begin{itemize}
\item 
The incompleteness theorems and physics.

\item
The incompleteness theorems and the theory of the mind.

\item
The incompleteness theorems and the foundations of mathemtics.

\item
The incompleteness theorems, epistemology and truth.

\end{itemize}



\end{enumerate}
\end{document}