\documentclass[11pt]{article}

\usepackage[margin=1.6in]{geometry}
\usepackage{proof}
\usepackage{amsmath,amsthm,amssymb}

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

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

\newcommand\amp{\mathop{\&}}

\newcommand\pimp{\mathop{\supset}}
\newcommand\pand{\mathop{\wedge}}
\newcommand\por{\mathop{\vee}}
\newcommand\ptrue{\top}
\newcommand\pfalse{\bot}
\newcommand\peq{\Leftrightarrow}

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

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

\title{Constructive Logic (15-317), Fall 2012 \\
       Assignment 1: Natural Deduction}
\author{Carlo Angiuli \texttt{(cangiuli@cs)}}
\date{Out: Thursday, September 6, 2012 \\
      Due: Thursday, September 13, 2012 (before class)}

\begin{document}
\maketitle

Welcome to 15-317, Fall 2012 edition!  In this, your first homework
assignment, you will practice essential logic skills like carrying
out proofs in natural deduction and verifying the local soundness and
completeness of logical connectives.

The Tutch portion of your work (Section~\ref{sec:tutch}) should be
submitted electronically using the command
\begin{verbatim}
  $ /afs/andrew/course/15/317/bin/submit -r hw01 <files...>
\end{verbatim}
from any Andrew server.  You may check the status of your submission by
running the command
\begin{verbatim}
  $ /afs/andrew/course/15/317/bin/status hw01
\end{verbatim}
If you have trouble running either of these commands, email Carlo.

The written portion of your work (Sections \ref{sec:notutch} and
\ref{sec:harmony}) should be submitted at the beginning of class.  If you are
familiar with \LaTeX, you are encouraged to use this document as a template for
typesetting your solutions, but you may alternatively write your solutions
\textit{neatly} by hand.

\section{Tutch Proofs (15 points)}
\label{sec:tutch}

\begin{task}[15 points]
Prove the following theorems using Tutch:
\begin{verbatim}
absurdity : (A & ~A) => B
demorgan : ~(A | B) => ~A & ~B
sComb : (A => B => C) => (A => B) => (A => C)
orImpl : (A => C) => (B => C) => (A | B => C)
dnIntro : A => ~~A
\end{verbatim}
\end{task}

On Andrew machines, you can check your progress against the requirements
file \texttt{/afs/andrew/course/15/317/req/hw01.req} by running the command
\begin{verbatim}
  $ /afs/andrew/course/15/317/bin/tutch -r hw01 <files...>
\end{verbatim}

\section{Can't Tutch This (8 points)}
\label{sec:notutch}

\begin{task}[4 points]
Give a derivation of the following judgement in terms of the inference rule
notation given in lecture:
\[ (A \lor \neg A)\pimp (\neg\neg A \pimp A)\true \]
\end{task}

\begin{task}[4 points]
Give a derivation of the following judgement in terms of the inference rule
notation given in lecture:
\[ (A\lor\neg A)\pimp (((A\pimp B)\pimp A)\pimp A)\true \]
\end{task}

\section{Harmony (17 points)}
\label{sec:harmony}
Consider a new connective $A\amp B$, defined by the following introduction and
elimination rules.
\[
\infer[\amp I]
  {A\amp B\true}
  {A\true & B\true}
\qquad
\infer[\amp E_1]
  {C\true}
  {A\amp B\true & \deduce[\ddd]{C\true}{[A\true]}}
\qquad
\infer[\amp E_2]
  {C\true}
  {A\amp B\true & \deduce[\ddd]{C\true}{[B\true]}}
\]
As with the elimination rule for $\lor$, each $\amp$ elimination introduces a
hypothesis which can be used any number of times in order to prove $C\true$.

\begin{task}[7 points]
Decide which, if any, of the judgments below are true, and give a derivation of
each true judgment.
\[\begin{aligned}
(A\land B) &\pimp (A\amp B) \true \\
(A\amp B) &\pimp (A\land B) \true \\
(A\amp B) &\pimp (A\amp B) \true \\
\end{aligned}\]
\end{task}

\begin{task}[5 points]
Are these rules locally sound? Give all local reductions for these rules, and
use these to justify your claim.
\end{task}

\begin{task}[5 points]
Are these rules locally complete? Give all local expansions for these rules, and
use these to justify your claim.
\end{task}

\end{document}