\documentclass[12pt]{cas-handout}
\usepackage{amsmath,amsfonts,multicol}
\usepackage{paralist}
\usepackage{pdfpages}

\newtheorem{theorem}{Theorem}

\anumber{5}
\title{Beyond Natural Deduction}
\duedate{11:00am, Wednesday, October 5}

\begin{document}
\maketitle 

\begin{itemize}
  \item Emails about this assignment should be directed to
    \helpalias.
 \item The usual collaboration rules apply. You may \emph{discuss} an
    exercise with any other student(s) currently taking CS 81 as long as:
    \begin{compactitem}
      \item You contribute equally;
      \item You come away from this discussion only with
        \emph{understanding in your head} --- no written materials or
        computer notes may be retained;
      \item Your submission is authored solely by you, on a separate
        occasion.
   \end{compactitem}
  \item You should refer only to materials from this semester of CS 81 (lecture
   notes, handouts, textbooks, grutors, profs, etc.).
 \item Bring a writeup/printout to class on the due date. Illegible answers
    will get no credit.
\item Make sure your submission includes your name!
\end{itemize}

\hrule

\bigskip\bigskip
\noindent

\section{Tableau Proofs}
For each of the following, give a tableau proof.
\begin{enumerate}
\item $\vdash \quad (p \to q) \lor (q \to r)$
\item $(p \land q)\to r,\ r\to s, q \land \lnot s \quad \vdash \quad \lnot p$
\item $(\exists x.\ P(x)) \to (\exists y. Q(y))\quad \vdash\quad \exists z.\
  (P(z) \to Q(z))$
\item $\forall x.\ \bigl((P(x) \to Q(x)) \land (Q(x)\to
P(x))\bigr) \quad \vdash\quad (\forall x.\ P(x)) \to (\forall x.\ Q(x))$
\end{enumerate}

\section{Sequent Calculus}
\begin{enumerate}
\item For each of the following, give a sequent-calculus proof. If you wish, you
  can treat the sequences of formulas as sets, and leave uses of
  the structural (exchange, weakening, and contraction) rules implicit
  except where they help for clarity.  (For example, you might treat
  $p,q,r \vdash p$ as an axiom, rather than taking $p\vdash p$ and
  weakening twice on the left.)
  \begin{enumerate}
  \item $\vdash p \lor \lnot p$
  \item $\lnot (p\land q) \vdash \lnot p \lor \lnot q$
  \item $\vdash ((p\to q)\to p)\to p$
  \item $\bot \vdash A$
  \end{enumerate}

\item
Gentzen developed the sequent calculus as a method of proving results
about natural deduction. He proved the following key facts (by
induction and proof trees!):
\begin{itemize}
\item For every natural deduction proof, there is a corresponding
  sequent-calculus proof with the same conclusion (possibly using the
  Cut rule) and vice-versa.  Hence, both systems have the same
  theorems.
\item For every sequent-calculus proof using the Cut rule, there is a
  (possibly much longer) sequent-calculus proof of the same result
  that does not use the Cut rule. (This property of sequent calculus is called ``Cut
  Elimination.'')
\end{itemize}

A logical system is said to be \emph{consistent} if it
is impossible to prove $\bot$ from no assumptions.
Relying on Cut Elimination and the fact that sequent calculus proofs
are (inductively generated) trees, prove that
sequent calculus (and hence natural deduction!) is consistent.\footnote{There's a completely different proof of
consistency that relies on via soundness and completeness of natural
deduction. The goal here is a ``purely syntactic'' proof of
consistency that doesn't involve
models at all, just proof trees.} That is, prove that $\vdash \bot$ is not a theorem
of sequent calculus.

\end{enumerate}

\section{Resolution}

Convert each of the following to clausal form, and show the
resolution proofs:

\begin{enumerate}
\item $\vdash \quad (p \to q) \lor (q \to r)$
\item $(p \land q)\to r,\ r\to s, q \land \lnot s \quad \vdash \quad \lnot p$
\end{enumerate}


\end{document}
