\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}