\documentclass[12pt]{article}
\usepackage{amsfonts,amssymb}
\usepackage{amsmath}
%\documentstyle[12pt,amsfonts]{article}
%\documentstyle{article}

\setlength{\topmargin}{-.5in}
\setlength{\oddsidemargin}{0 in}
\setlength{\evensidemargin}{0 in}
\setlength{\textwidth}{6.5truein}
\setlength{\textheight}{8.5truein}
%\input ../basicmath/basicmathmac.tex
%
%\input ../adgeomcs/lamacb.tex
\input {"./mac.tex"}
\input {"./mathmac.tex"}
\input {"./prooftree.tex"}

\def\qleq{\sqsubseteq}
\def\impl{\Rightarrow}
\def\falsum{\perp}

%
\begin{document}

\begin{flushright}
Alina Chin \& Di Mu\\[10pt]
\end{flushright}

\begin{center}
\fbox{{\Large\bf Fall 2010 \hspace*{0.4cm} CIS 160}}\\
\vspace{1cm}
{\Large\bf Mathematical Foundations of Computer Science\\
Jean Gallier \\
\vspace{0.5cm}
Homework 2}\\[10pt]
September 28, 2010; Due October 5, 2010\\
Beginning of class
\end{center}


\vspace {0.5cm}\noindent
{\bf Problem 1.}
(a) Prove the ``de Morgan'' laws in classical logic:
\begin{align*}
\neg(P \land Q) & \equiv \neg P \lor \neg Q \\
\neg(P \lor Q) & \equiv \neg P \land \neg Q.
\end{align*} 



\settree1{
	\starttree{$\neg (\neg P\lor \neg Q)^z$}
	}

\settree2{
	\starttree{$\neg P^\alpha $}
	\step{$\neg P\lor \neg Q$}
	}
	
\settree1{
	\vnjointrees{1}{2}
	\step{$\perp $}
	\jstep{$P$}{$\scriptstyle \alpha$(by-contra)}
	}
	
\settree3{
	\starttree{$\neg (\neg P\lor \neg Q)^z$}
}
	
\settree4{
	\starttree{$\neg Q^\beta$}
	\step{$\neg P\lor \neg Q$}
}


\settree3{
	\vnjointrees{3}{4}
	\step{$\perp$}
	\jstep{$Q$}{$\scriptstyle \beta$(by-contra)}
}

\settree1{
	\njointrees{1}{3}
	\step{$P\land Q$}
	}
	
\settree5{
	\starttree{$\neg (P\land Q)^w$}}

\settree1{
	\vnjointrees{5}{1}
	\step{$\falsum$}
	\jstep{$\neg P\lor \neg Q$}{$\scriptstyle z$(by-contra)}
	\jstep{$\neg(P \land Q) \impl \neg P \lor \neg Q$}{$\scriptstyle w$}
	}
	
\bigskip
\ligne{\hfill\box1\hfill}	




\settree1{
  \starttree{$(P \land Q)^x$}
  \step{$P$}
}

\settree3{
  \starttree{$(P\land Q)^x$}
  \step{$Q$}
}

\settree2{
  \starttree{$(\neg Q)^w$}
}

\settree2{
  \snjointrees{2}{3}
  \step{$\falsum$}
  \step{$\neg P$}
}

\settree3{
  \starttree{$(\neg P \lor \neg Q)^y$}
}

\settree4{
  \starttree{$(\neg P)^v$}
  \step{$\neg P$}
}

\settree2{
  \tnjointrees{3}{4}{2}
  \jstep{$\neg P$}{$\scriptstyle v,w$}
}

\settree1{
  \njointrees{1}{2}
  \step{$\falsum$}
  \jstep{$\neg (P \land Q)$}{$\scriptstyle x$}
  \jstep{$(\neg P \lor \neg Q) \impl \neg (P \land Q)$}{$\scriptstyle y$}
}


\bigskip
\ligne{\hfill\box1\hfill}
\bigskip

\settree1{
  \starttree{$(\neg (P \lor Q))^z$}
}

\settree2{
  \starttree{$P^x$}
  \step{$P \lor Q$}
}

\settree1{
  \njointrees{1}{2}
  \step{$\falsum$}
  \jstep{$\neg P$}{$\scriptstyle x$}
}

\settree2{
  \starttree{$(\neg (P \lor Q))^z$}
}

\settree3{
  \starttree{$Q^x$}
  \step{$P \lor Q$}
}

\settree2{
  \njointrees{2}{3}
  \step{$\falsum$}
  \jstep{$\neg Q$}{$\scriptstyle y$}
}

\settree1{
  \njointrees{1}{2}
  \step{$\neg P \land \neg Q$}
  \jstep{$\neg (P \lor Q) \impl (\neg P \land \neg Q)$}{$\scriptstyle z$}
}

\bigskip
\ligne{\hfill\box1\hfill}
\bigskip

\settree1{
  \starttree{$(\neg P \land \neg Q)^w$}
  \step{$\neg Q$}
}
\settree2{
  \starttree{$Q^y$}
}
\settree3{
  \snjointrees{2}{1}
  \step{$\falsum$}
  \step{$P$}
}

\settree2{
  \starttree{$P^x$}
  \step{$P$}
}

\settree1{
  \starttree{$(P \lor Q)^z$}
}

\settree1{
  \tnjointrees{1}{2}{3}
  \jstep{$P$}{$\scriptstyle x, y$}
}
\settree2{
  \starttree{$(\neg P \land \neg Q)^w$}
  \step{$\neg P$}
}
\settree1{
  \njointrees{2}{1}
  \jstep{$\falsum$}{$\scriptstyle z$ ($\neg$-intro)}
  \step{$\neg (P \lor Q)$}
  \jstep{$(\neg P \land \neg Q) \impl \neg (P \lor Q)$}{$\scriptstyle w$}
}

\bigskip
\ligne{\hfill\box1\hfill}

\medskip
(b)
Prove that  $\neg(P \lor Q)  \equiv \neg P \land \neg Q$ is also provable
in intuitionistic logic.

We proved $\neg(P \lor Q)  \equiv \neg P \land \neg Q$ without RAA in part a, so it can be seen as intuitionistic logic too.


\medskip
(c)
Prove that the proposition $(P \land \neg Q) \impl \neg(P \impl Q)$ is provable
in intuitionistic logic and 
$\neg(P \impl Q) \impl (P \land \neg Q)$ is provable in 
classical logic.

\settree1{
  \starttree{$(P \land \neg Q)^x$}
  \step{$P$}
}
\settree2{
  \starttree{$(P \impl Q)^y$}
}
\settree2{
  \njointrees{1}{2}
  \step{$Q$}
}

\settree1{
  \starttree{$(P \land \neg Q)^x$}
  \step{$\neg Q$}
}

\settree1{
  \njointrees{1}{2}
  \step{$\falsum$}
  \jstep{$\neg (P \impl Q)$}{$\scriptstyle y$ ($\neg$-intro)}
  \jstep{$(P \land \neg Q) \impl \neg (P \impl Q)$}{$\scriptstyle x$}
}

\bigskip
\ligne{\hfill\box1\hfill}







\settree1{
	\starttree{$\neg (P\impl Q)^x$}
	}
	
\settree2{
	\starttree{$Q^z$,$P^\alpha$}
	\step{$Q$}
	\jstep{$P \impl Q$}{$\scriptstyle \alpha$}
	}
	
\settree1{
	\vnjointrees{1}{2}
	\step{$\perp$}
	\step{$P$}
	}
	
\settree3{
	\starttree{$\neg (P\impl Q)^x$}
}

\settree4{
	\starttree{$Q^z$,$P^\beta$}
	\step{$Q$}
	\jstep{$P\impl Q$}{$\scriptstyle \beta$}
}


\settree3{
	\vnjointrees{3}{4}
	\step{$\perp$}
	\step{$\neg Q$}
}


\settree1{
	\vnjointrees{1}{3}
	\step{$P\land \neg Q$}
	\jstep{$\neg(P \impl Q) \impl (P \land \neg Q)$}{$\scriptstyle x$}
}
\bigskip
\ligne{\hfill\box1\hfill}

\medskip	
	
	
	

\vspace {0.5cm}\noindent
{\bf Problem 2.}
(a) Prove that $P \impl \neg\neg P$ is provable in intuitionistic logic.

\settree1{
  \starttree{$P^x$, $(P\impl \perp)^y$}
  \step{$\falsum$}
  \jstep{$(P\impl \perp)\impl \perp$}{$\scriptstyle y$}
  \jstep{$P\impl ((P\impl \perp)\impl \perp)$}{$\scriptstyle x$}
    }
  
\bigskip
\ligne{\hfill\box1\hfill}

\medskip
(b)
Prove that $\neg\neg\neg P$ and $\neg P$ are
equivalent in intuitionistic logic.


\settree1{
	\starttree{$\neg ((P\impl \perp)\impl \perp)^y$}
  }
\settree2{
	\starttree{$P^y$,$(P \impl \perp)^z$}
	\step{$\perp$}
	\step{$((P\impl \perp)\impl \perp)^z$}
  }
  
\settree1{
  \vnjointrees{1}{2}
  \step{$\perp$}
  \jstep{$P\impl \perp$}{$\scriptstyle y$}
  \jstep{$((P\impl \perp)\impl \perp)\impl (P\impl \perp)$}{$\scriptstyle x$}
  }


\bigskip
\ligne{\hfill\box1\hfill}

\settree1{
  \starttree{$((P\impl \perp)\impl \perp)^y$, $(P\impl \perp)^x$}
  \step{$\perp$}
  \jstep{$((P\impl \perp)\impl \perp)\impl \perp$}{$\scriptstyle y$}
  \jstep{$(P\impl \perp)\impl (((P\impl \perp)\impl \perp)\impl \perp)$}{$\scriptstyle x$}
    }
  
\bigskip
\ligne{\hfill\box1\hfill}




\vspace {0.5cm}\noindent
{\bf Problem 3}
(a)
Prove that the proposition
\[
(P \lor \neg P) \impl (((P \impl Q) \impl P) \impl P)
\]
is provable in intuitionistic logic.


\settree1{
	\starttree{$((P\impl Q)\impl P)^\alpha $}
  }
\settree2{
	\starttree{$\neg P^y$, $P^y$}
	\step{$\perp$}
	\step{$Q$}
	\jstep{$P\impl Q$}{$\scriptstyle x$}
  }
  
\settree1{
  \vnjointrees{1}{2}
  \step{$P$}
  \jstep{$((P\impl Q)\impl P)\impl P$}{$\scriptstyle \alpha$}
  }
  
\settree3{
	\starttree{$((P\impl Q)\impl P)^\beta$, $P^x$}
	\step{$P$}
	\jstep{$((P\impl Q)\impl P)\impl P$}{$\scriptstyle \beta $}
	}
	
\settree4{
	\starttree{$(P\lor \neg P)^t$}
	}
	
\settree1{
	\tjointrees{1}{3}{4}
	\jstep{$((P\impl Q)\impl P)\impl P$}{$\scriptstyle x,y$}
	\jstep{$(P \lor \neg P) \impl (((P \impl Q) \impl P) \impl P)$}{$\scriptstyle t$}
}

\bigskip
\ligne{\hfill\box1\hfill}




\medskip
(b)
Prove that the proposition 
$((P \impl Q) \impl P) \impl P$ is classically provable.


\settree1{
	\starttree{$((P\impl Q)\impl P)^x$}
  }
\settree2{
	\starttree{$(\neg P^)y$, $P^y$}
	\step{$\falsum$}
	\step{$Q$}
	\jstep{$P\impl Q$}{$\scriptstyle x$}
  }
  
\settree1{
  \vnjointrees{1}{2}
  \step{P}
  }

\settree3{
  \starttree{$(\neg P)^y$}
  }
  
\settree1{
	\jointrees{1}{3}
	\step{$\falsum$}
	\jstep{$P$}{$\scriptstyle y (RAA)$}
	\jstep{$((P \impl Q) \impl P) \impl P$}{$\scriptstyle x$}
}

\bigskip
\ligne{\hfill\box1\hfill}

\vspace {0.5cm}\noindent
{\bf Problem 4}
(a)
Prove that the proposition
\[
\neg\neg (((P \impl Q) \impl P) \impl P)
\]
is provable in intuitionistic logic.

\medskip
(b)
Use (a) to prove that the proposition 
$((P \impl Q) \impl P) \impl P$ is classically provable.

\vspace {0.5cm}\noindent
{\bf Problem 5.}
Prove that the rule

\settree1{
     \starttree{$\Gamma$}
     \istep{$\s{D}_1$}
     \istep{$P\impl Q$}
}
\settree2{
     \starttree{$\Delta$}
     \istep{$\s{D}_2$}
     \istep{$\neg Q$}
}
\settree1{
     \njointrees{1}{2}
     \step{$\neg P$}
}

\bigskip
\ligne{\hfill\box1\hfill}

\bigskip\noindent
can be derived from the other rules of intuitionistic logic.
This means that you have to describe how a deduction tree $\s{D}_1$ for
$P \impl Q$ from $\Gamma$ and a deduction tree $\s{D}_2$ for
$\neg Q$ from $\Delta$ can be combined to obtain a deduction
of $\neg P$ from $\Gamma\cup \Delta$.







\end{document}