\documentclass[11pt]{article}

\usepackage[margin=1.6in]{geometry}
\usepackage{proof}
\usepackage{amsmath,amsthm,amssymb}
\usepackage[colorlinks=true,linkcolor=black,urlcolor=black]{hyperref}

% font{
\usepackage{pxfonts}
%% fix sans serif
\renewcommand\sfdefault{cmss}
\DeclareMathAlphabet{\mathsf}{OT1}{cmss}{m}{n}
\SetMathAlphabet{\mathsf}{bold}{OT1}{cmss}{b}{n}
% }font

\newtheorem{theorem}{Theorem}
\theoremstyle{definition}
\newtheorem{task}{Task}

\newcommand\pimp{\mathop{\supset}}
\newcommand\pand{\mathop{\wedge}}
\newcommand\por{\mathop{\vee}}
\newcommand\ptrue{\top}
\newcommand\pfalse{\bot}
\newcommand\pforall[3]{\forall #1{:}#2.\, #3}
\newcommand\pexists[3]{\exists #1{:}#2.\, #3}

\newcommand\tabort[1]{\mathsf{abort}\;#1}
\newcommand\tlam[3]{\lambda #1{:}#2.\,#3}
\newcommand\tinl[1]{\mathsf{in_1}\;M}
\newcommand\tinr[1]{\mathsf{in_2}\;M}
\newcommand\tcase[5]{\mathsf{case}(#1, #2.#3, #4.#5)}
\newcommand\tunit{\langle\rangle}
\newcommand\tpair[2]{\langle #1, #2 \rangle}
\newcommand\tfst[1]{\pi_1 #1}
\newcommand\tsnd[1]{\pi_2 #1}

\newcommand\true{\;\textit{true}}
\newcommand\false{\;\textit{false}}
\newcommand\ddd{\raisebox{0.2em}[1.3em]{$\vdots$}}
\newcommand\com{\raisebox{0.3em}{$\ ,\ \ $}}
\newcommand\hyp[2]{\infer[#1]{#2}{}}

\newcommand{\lred}{\mathrel{\raisebox{0.5em}{$\Longrightarrow_R$}}}
\newcommand{\lexp}{\mathrel{\raisebox{0.5em}{$\Longrightarrow_E$}}}

\newcommand{\jsub}[3]{[#1/#2]\;#3}

\newcommand{\DD}{\mathcal{D}}
\newcommand{\EE}{\mathcal{E}}
\newcommand{\FF}{\mathcal{F}}

\newcommand{\G}{\Gamma}
\newcommand{\D}{\Delta}
\newtheorem{lemma}{Lemma}
\newcommand{\seq}{\longrightarrow}
\newcommand{\nat}{\textsf{nat}}
\newcommand{\even}{\textsf{even}}
\newcommand{\odd}{\textsf{odd}}
\newcommand{\s}{\textsf{s}}

\newcommand{\cl}{\mathrel{\ensuremath{\vdash_C}}}
\newcommand{\PBC}{\textsf{PBC}}
\newcommand{\throw}[2]{\langle #1\rhd #2\rangle}

\title{Constructive Logic (15-317), Fall 2012 \\
       Assignment 5: Classical Logic}
\author{Carlo Angiuli \texttt{(cangiuli@cs)}}
\date{Out: Friday, October 12, 2012 \\
      Due: Thursday, October 18, 2012 (before class)}

\begin{document}
\maketitle

In this assignment, you will investigate the relationship between constructive
and classical logic.

\section{Double-Negation Translation (12 points)}

Unlike in constructive logic, which has only a judgment for truth, classical
logic has judgments for truth, falsity, and contradiction. Classical logic also
has a primitive notion of negation ($\lnot A$), whereas constructive logic
simply defines $\lnot A$ to be $A\pimp\bot$.

The G\"odel--Gentzen double--negation translation takes a classical proposition
$A$ to a constructive proposition $A^*$, and is defined inductively on the
structure of $A$ as follows:
\[\begin{aligned}
\top^* &= \top \\
\bot^* &= \bot \\
(A\land B)^* &= A^* \land B^* \\
(A\pimp B)^* &= A^* \pimp B^* \\
(A\lor B)^* &= \lnot\lnot(A^* \lor B^*) \\
(\lnot A)^* &= \lnot A^*\\
P^* &= \lnot\lnot P \text{ where $P$ atomic}
\end{aligned}\]
(\emph{Note:} On the left, $\lnot$ is the primitive classical notion of
negation; on the right, $\lnot$ is an abbreviation for $-\pimp\bot$.)

\begin{task}[12 points]\label{task:stable}
Prove that, for any classical proposition $A$,
\[ \cdot\vdash \lnot\lnot A^*\pimp A^*\true \]
is derivable (constructively). You need only show the cases for:
\begin{itemize}
\item $\top$
\item atomic propositions
\item $\pimp$
\item $\lor$
\end{itemize}
\end{task}

\section{Embedding Classical Logic (28 points)}

The G\"odel--Gentzen double--negation translation allows us to \emph{embed}
classical logic into constructive logic in the following sense:

\begin{theorem}\label{thm:dnt}
\noindent
\begin{enumerate}
\item If $\G\cl A\true$, then $\G^*\vdash A^*\true$.
\item If $\G\cl A\false$, then $\G^*\vdash \lnot A^*\true$.
\item If $\G\cl \#$, then $\G^*\vdash \bot\true$.
\end{enumerate}
\end{theorem}

In the above theorem, $\G^*$ is the result of applying the double--negation
translation to each proposition in the context; $\cl$ indicates a classical
derivation, using the rules listed at the end of this assignment; and $\vdash$
indicates a constructive derivation. In other words, this theorem states that
any classically--derivable proposition has a constructively--derivable
counterpart, given by the translation.

\begin{task}[28 points]
Prove Theorem \ref{thm:dnt}, showing the following cases:
\begin{itemize}
\item $\pimp T$
\item $\lor T1$
\item $\pimp F$
\item $\lor F$
\item $\lnot F$
\item $\#$
\item $\PBC T$
\end{itemize}
You may use the result stated in Task \ref{task:stable}. (\emph{Hint:} You will
also need weakening.)
\end{task}

\pagebreak
\appendix
\advance\hsize by 2cm
\advance\hoffset by -1cm

\section{Classical rules}

\[
\infer[\pimp T]
  {\G\cl \lambda x:A.M:A\pimp B\true}
  {\G,x:A\true\cl M:B\true}
\qquad
\infer[\land T]
  {\G\cl \tpair MN:A\land B\true}
  {\G\cl M:A\true & \G\cl N:B\true}
\qquad
\infer[\top T]
  {\G\cl \star:\top\true}
  {}
\]

\[
\infer[\lor T1]
  {\G\cl \tinl M:A\lor B\true}
  {\G\cl M:A\true}
\qquad
\infer[\lor T2]
  {\G\cl \tinr M:A\lor B\true}
  {\G\cl M:B\true}
\qquad
\infer[\lnot T]
  {\G\cl \lnot K:\lnot A\true}
  {\G\cl K:A\false}
\]

\[
\infer[\pimp F]
  {\G\cl M;K:A\pimp B\false}
  {\G\cl M:A\true & \G\cl K:B\false}
\qquad
\infer[\lor F]
  {\G\cl [K,L]:A\lor B\false}
  {\G\cl K:A\false & \G\cl L:B\false}
\qquad
\infer[\bot F]
  {\G\cl \bullet:\bot\false}
  {}
\]

\[
\infer[\land F1]
  {\G\cl \pi_1\cdot K:A\land B\false}
  {\G\cl K:A\false}
\qquad
\infer[\land F2]
  {\G\cl \pi_2\cdot K:A\land B\false}
  {\G\cl K:B\false}
\qquad
\infer[\lnot F]
  {\G\cl \lnot M:\lnot A\false}
  {\G\cl M:A\true}
\]

\[
\infer[\#]
  {\G\cl \throw MK:\#}
  {\G\cl M:A\true & \G\cl K:A\false}
\qquad
\infer[\textsf{hyp} T]
  {\G,x:A\true\cl x:A\true}
  {}
\qquad
\infer[\textsf{hyp} F]
  {\G,x:A\false\cl x:A\false}
  {}
\]

\[
\infer[\PBC T]
  {\G\cl u:A\false.E:A\true}
  {\G,u:A\false\cl E:\#}
\qquad
\infer[\PBC F]
  {\G\cl u:A\true.E:A\false}
  {\G,u:A\true\cl E:\#}
\]

\end{document}