% -----------------------acknowledge for overleaf and designer of this template-----------------------
\documentclass[12pt]{exam}
\usepackage{amsthm}
\usepackage{libertine}
\usepackage[utf8]{inputenc}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb}
\usepackage{multicol}
\usepackage[shortlabels]{enumitem}
\usepackage{siunitx}
\usepackage{cancel}
\usepackage{graphicx}
\usepackage{pgfplots}
\usepackage{listings}
\usepackage[all]{xy}


%command 
\newcommand{\code}[1]{\ulcorner #1 \urcorner}
%\newcommand{\CE}{$\mathsf{CE}$}
\newcommand{\Ce}{$\mathsf{CE}$~}
\newcommand{\II}{{\sf I \,}}
\newcommand{\ol}[1]{\overline{#1}}

\newcommand{\la}{\leftarrow}
\newcommand{\ra}{\rightarrow}
\newcommand{\lr}{\leftrightarrow}
\newcommand{\La}{\Leftarrow}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\LR}{\Leftrightarrow}

% automata
%\usepackage{tikz}
%\usetikzlibrary{automata, positioning, arrows}


\pgfplotsset{width=10cm,compat=1.9}
\usepgfplotslibrary{external}
\tikzexternalize

\newcommand{\class}{\Large Logic and Computation II, Spring 2023 } % This is the name of the course 
\newcommand{\examnum}{Homework No.11} % This is the index of the homework
\newcommand{\examdate}{} % This is the due date
\newcommand{\examname}{Name:    } % Your name here





\begin{document}
\pagestyle{plain}
\thispagestyle{empty}

\noindent
\begin{tabular*}{\textwidth}{l @{\extracolsep{\fill}} r @{\extracolsep{8pt}} l}
\textbf{\class} & & \textit{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\
&&\\
\textbf{\examnum} & &\textit{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\ 
\textbf{\examdate} &&\\
\textbf{\examname} &&\\
\end{tabular*}\\
\rule[2ex]{\textwidth}{2pt}
% ---

\noindent \textbf{Problem 1}\\
In a $\Sigma_1$ complete theory $T$, show that 1-consistency ($\Sigma_1$-soundness) of $T$ is equivalent to the following: for any $\Sigma_0$ formula $\varphi(x)$, if $\varphi(\overline{n})$ is provable in $T$ for all $n$, then $\exists x \neg \varphi(x)$ is not provable in $T$. 
\bigskip

\noindent\underline{\textsf{Solution:}}

\vspace{8cm}


\bigskip

\noindent \textbf{Problem 2}\\
Let $A, B$ be two disjoint \textsf{CE} sets.
Assume a theory $T$ is $\Sigma_1$-complete.
Show that there exists a $\Sigma_1$ formula $\psi(x)$ such that 
$$n \in A \Rightarrow T \vdash \psi(\overline{n}), \quad n \in B \Rightarrow T \vdash \neg \psi(\overline{n}).$$
From this, deduce that $\{ \ulcorner\sigma\urcorner : T \vdash \sigma \}$
and $\{ \ulcorner\sigma\urcorner : T \vdash \neg \sigma \}$ are computably inseparable.
(See Part 1-6, Slide p.25.) In particular,  $\{ \ulcorner\sigma\urcorner : T \vdash \sigma \}$
is not computable.
\bigskip

\noindent\underline{\textsf{Solution:}}


\bigskip
\newpage
\noindent \textbf{Problem 3}\\
Complete the proof of G\"odel-Rosser's theorem.


\begin{itemize}
\item Let $A= \{ \code\sigma : T \vdash \sigma \}$, $B= \{ \code\sigma : T \vdash \neg \sigma \}$.
If $T$ is consitent \textsf{CE} theory, then $A, B$ are disjoint \textsf{CE} sets.
\item Similarly to the proof of the strong representation theorem for computable sets, costruct a formula $\psi(x)$ such that $A \subset \{ n : T \vdash \psi(\ol{n}) \}$ and
  $B \subset \{ n : T \vdash \neg \psi(\ol{n}) \}$.
\item Considering the sentence $\sigma$ such that  $T \vdash (\sigma \lr \neg \psi(\code\sigma))$, 
prove that $\code\sigma \not\in A \cup B$.
\end{itemize}
Also, notice that if $A, B$ were computably separable,
we could construct a formula $\psi(x)$ such that 
$\{ n : T \vdash \psi(\ol{n}) \} \cup
\{ n : T \vdash \neg \psi(\ol{n}) \}
= {\mathbb N}$.
\bigskip

\noindent\underline{\textsf{Solution:}}



\vspace{8cm}


\bigskip

\noindent \textbf{Problem 4}\\
Show that there is a consistent theory $T$ that proves its own contradiction $\neg \mathrm{Con}(T)$.
\bigskip

\noindent\underline{\textsf{Solution:}}

\newpage 
\noindent \textbf{Problem 5}\\
Let $\mathrm{Bew}^\#_T(x) \equiv (\mathrm{Bew}_T(x) \land x \ne \overline{\code{0=1}})$. For any true proposition $\sigma$,  $$\mathrm{Bew}^\#_T(\overline{\code{\sigma}}) \lr \mathrm{Bew}_T(\overline{\code{\sigma}} )$$ and  $$T \vdash \neg \mathrm{Bew}^\#_T(\overline{\code{0=1}}).$$

Does it contradict with the second incompleteness theorem?
\bigskip

\noindent\underline{\textsf{Solution:}}

\end{document}




