\documentclass[8pt]{amsart}



\usepackage{amssymb} 


\usepackage{proof}

\usepackage[makeroom]{cancel}



\title{21-300 F15 HW 1-4 solutions}

\begin{document}

\maketitle

\section*{Homework 1} 


\begin{enumerate}

\item (25  points total)  Recall that we defined an inductive structure to generate the wff's of propositional logic as follows:
 The wffs are finite strings of symbols from the alphabet
\[
    \{ A_n : n \in {\mathbb N} \} \cup \{ (, ) \} \cup \{ \vee, \wedge, \neg, \rightarrow \}
\]
     $B$ is the set of all strings
   of length $1$ of form $A_n$, and $K = \{ F_\vee, F_\neg, F_\wedge, F_\rightarrow \}$
   is  a family of functions for generating strings: $F_\vee(s, t) = (s \vee t)$,
   $F_\wedge(s, t) = (s \wedge t)$, $F_\rightarrow(s, t) = (s \rightarrow t)$, $F_\neg(s) = (\neg s)$.
  We showed in class that this has unique readability. The set $C$ of wffs is the closure of $B$ under $K$.

\begin{enumerate}

\item (10 points)  Define a function $G: C \rightarrow {\mathbb N}$ by the following recursion:
   $G(A_n) = 1$ for all $n$, $G( (s \vee t) ) = G(s) + G(t)$,
   $G( (s \wedge t) ) = G(s) + G(t)$, $G( (s \rightarrow t) ) = G(s) + G(t)$,
   $G( (\neg s) ) = G(s)$.

   What is $G$? For full credit your answer should include an inductive proof that
   your description of $G$ is correct.

   $G$ is the function that returns for each $s \in C$ the number of entries in $s$ that are
   {\em propositional letters}, that is symbols of the form $A_n$ for some $n$. 
   To see this we do a proof by induction on the inductive structure, where the
   property $P(s)$ we are proving is
   ``$G(s)$ is the the number of entries in $s$ that are propositional letters''.

   Base case:  Since  $G(A_n) = 1$ for all $n$, the property $P(s)$ for all $s \in B$.

   Successor step(s): Officially we need four steps, one for each function, but 
   we just check $F_\wedge$.  Suppose that $P(s)$ and $P(t)$ hold, that
   that is $s$ has $G(s)$ propositional letters and $t$ has $G(t)$ propositional letters.
   Then $(s \wedge t)$ has $G(s) + G(t)$ propositional letters, and
   by definition $G( (s \wedge t) ) = G(s) + G(t)$, so that $P( (s \wedge t) )$ holds.   



\item (10 points)  Give a recursive definition for each of the following functions on $C$. For full credit each answer should
   include an inductive proof that the definition is correct.

   Note: I just give the inductive definitions, the proofs are similar to the one I just gave. 

\begin{enumerate} 

\item  The function which returns the length of the string $s$ for each $s \in C$.
     $G(A_n) = 1$ for all $n$, $G( (s \vee t) ) = G(s) + G(t) + 3$,
   $G( (s \wedge t) ) = G(s) + G(t) + 3$, $G( (s \rightarrow t) ) = G(s) + G(t) + 3$,
   $G( (\neg s) ) = G(s) +3$.


\item  The function which returns the set of propositional letters appearing in $s$ for each
   $s \in C$.

     $G(A_n) = \{ A_n \}$ for all $n$, $G( (s \vee t) ) = G(s) \cup G(t)$,
   $G( (s \wedge t) ) = G(s) \cup G(t)$, $G( (s \rightarrow t) ) = G(s) \cup G(t)$,
   $G( (\neg s) ) = G(s)$.


\end{enumerate} 




\item (5 points)  Is it possible to give a recursive definition for the function from $C$ to $\mathbb N$ which returns 
   the number of distinct propositional letters appearing in $s$? 

   This one is a bit tricky. The official definition of recursion says
   that we can define $G(F(a_0, \ldots a_{k-1}))$ as  $H_F(a_0, \ldots a_{k-1}, G(a_0), \ldots G(a_{k-1}))$
   for any function $H_F$ of the right type, that is the value of $G$ at $F(a_0, \ldots a_{k-1})$ 
   is allowed to depend on the $a_i$'s as well as the values of $G$ on the $a_i$'s. 
  
   So we can write a recursive definition that goes like this:
   $G(A_n) = 1$, $G ( (s \wedge t) )$ is the the number of distinct propositional letters appearing in $(s \wedge t)$,
   and similarly for the other connectives. It's a reasonable complaint that this is cheating, and not really recursive
   since we ignore the values of $G(s)$ and $G(t)$ completely, but it is a legal recursive definition.

   Suppose we say that a recursive definition is {\em pure} if the value of $G(F(a_0, \ldots a_{k-1}))$ 
   only depends on the values of $G(a_0)$, \ldots $G(a_{k-1})$. The earlier examples in this question are all
   pure recursive definitions, and it's easy to see that the  number of distinct propositional letters appearing in $s$
   can't be computed by a pure recursive definition; for example $A_1 \wedge A_1$ and $A_1 \wedge A_2$ should get
   different values even though $A_1$ and $A_2$ get the same value!



\end{enumerate}

\item  (10 points total)  (This exercise is intended to motivate our restriction to finitary functions) Let 
   $X$ be the set of all subsets of $\mathbb N$, let $X^{\mathbb N}$ be the set of
   all infinite sequences $(x_n : n \in {\mathbb N})$ from $X$, and let
   $F: X^{\mathbb N} \rightarrow X$ be the function that returns $\{ n : n \notin x_n \}$ 
   on the argument $(x_n : n \in {\mathbb N})$. 

   Given $Y \subseteq X$ we will say that $Y$ is {\em closed under $F$} if 
   $F( (y_n : n \in {\mathbb N} ) ) \in Y$ for all sequences such that $y_n \in Y$ for all $n$.

\begin{enumerate}

\item (3 points) Prove that $F( (x_n : n \in {\mathbb N}) ) \neq x_n$.  

    Two sets are equal if they have the same members. By construction
    $n \in F( (x_n : n \in {\mathbb N}) ) \iff n \notin x_n$, so it is
    not possible that  $F( (x_n : n \in {\mathbb N}) ) = x_n$. 


\item (2 points)  Prove that no countable set $Y \subseteq X$ is closed under $F$.

    If $Y$ is countable and closed under $F$ then let $(x_n : n \in {\mathbb N})$ enumerate $Y$,
   and use the previous result to get a contradiction. 


\item (5 points)  Let $B = \{ \emptyset \}$ and let $Y$ be such that $B \subseteq Y \subseteq X$ and
    $Y$ is closed under $F$. Prove that $Y = X$.

    We claim first that ${\mathbb N} \in Y$. To see this consider the sequence which is
   constant with value $\emptyset$ at each entry, clearly $F$ returns $\mathbb N$ on this sequence.
   Now we claim that every $A \subseteq {\mathbb N}$ is in $Y$; to see this
   define a sequence by $x_n = \emptyset$ for $n \in A$, $x_n = {\mathbb N}$ for $n \notin A$.
   Now $n \notin x_n \iff x_n = \emptyset \iff n \in A$, so $F$ returns $A$ on this sequence.



\end{enumerate}
  
\item (10 points total)  An absent-minded professor messes up the definition of the wff's of propositional logic by 
   leaving out all the right parentheses, that is by writing
     ``$B$ is the set of all strings
   of length $1$ of form $A_n$, and $K = \{ F_\vee, F_\neg, F_\wedge, F_\rightarrow \}$
   is  a family of functions for generating strings: $F_\vee(s, t) = (s \vee t$,
   $F_\wedge(s, t) = (s \wedge t$, $F_\rightarrow(s, t) = (s \rightarrow t$, $F_\neg(s) = (\neg s$.''

   Is the resulting inductive structure uniquely readable?

   Yes. We will proceed much as we did in class for the inductive structure that generates the
   wff's of propositional logic. Recall that the main point there was that an initial segment of
   a wff is not a wff; once we had this it was easy to get unqiue readability, and the same argument will
   work here.

   For the purposes of this question, let us say that a bff (Bogusly Formed Formula) is a string generated
   by the professor's inductive structure. Given a string $s$ from the language, let $f(s)$ be the
   quantity (number of entries in s which are propositional letters) + (number of entries which are
   $\neg$) - (number which are left parentheses). 

   Claim one: If $s$ is a bff then $f(s) = 1$. We prove it by induction as usual. Clearly
   it holds for propositional letters. Applying $F_\neg$ adds one left parenthesis and one
   $\neg$, so if $f(s) = 1$ then $f( (\neg s ) = 1$. Finally applying any of 
   $F_\wedge$, $F_\vee$, $F_\rightarrow$ adds one left parenthesis and no $\neg$'s, so
   (eg) if $f(s) = f(t) = 1$ then $f( (s \wedge t ) = f(s) + f(t) -1 = 1$.
 
   Claim two: If $s$ is an initial segment of a bff then $f(s) \le 0$. Again we prove it by
   induction on bffs. Clearly it holds for propositional letters. The initial segments 
   of $( \neg s$ have the form empty string, $($, or $( \neg s'$ for $s'$ an initial segment
   of $s$ so the induction easily goes through. The initial segments of (eg)
   $(s \wedge t$ have one of the forms empty string, $($,  $(s'$ for $s'$ initial in $s$,
   $(s \wedge$ or $(s \wedge t'$ for $t'$ initial in $t$. Again the induction goes through.
   
   [THERE ARE VARIOUS ``INVARIANTS'' YOU CAN USE. THIS ONE IS SAM ZBARSKY'S AND IS 
    MUCH SLICKER THAN ONE I HAD IN MIND]

\end{enumerate}

\section*{Homework 2}


\begin{enumerate}

\item  (40 points total, 10 for each proof) Prove the formulae:

\begin{enumerate}

\item  $(\alpha \rightarrow \beta) \rightarrow ( (\neg \alpha) \vee \beta)$.

This one is quite tricky. Start by building a proof of $(\alpha \vee (\neg \alpha))$.
We proceed by contradiction, so we assume the negation $\neg(\alpha \vee (\neg \alpha))$
 and derive contradictory conclusions. 

\medskip

\infer[(\neg I)]{(\neg\alpha)}{\infer[(\vee I)]{(\alpha \vee (\neg \alpha))}{\cancel{\alpha}} & (\neg(\alpha \vee (\neg \alpha)))}

\smallskip

\infer[(\neg I)]{(\neg(\neg\alpha))}{\infer[(\vee I)]{(\alpha \vee (\neg \alpha))}{\cancel{\neg\alpha}} & (\neg(\alpha \vee (\neg \alpha)))}

\medskip 

Now we combine and use the not-introduction and contradiction rules.

\medskip

\infer[(RAA)]
{(\alpha \vee (\neg\alpha))}
{
\infer[(\neg I)]
{ (\neg(\neg(\alpha \vee (\neg \alpha))))}
{
\infer[(\neg I)]{(\neg\alpha)}{\infer[(\vee I)]{(\alpha \vee (\neg \alpha))}{\cancel{\alpha}} & \cancel{(\neg(\alpha \vee (\neg \alpha)))}}
&
\infer[(\neg I)]{(\neg(\neg\alpha))}{\infer[(\vee I)]{(\alpha \vee (\neg \alpha))}{\cancel{\neg\alpha}} & \cancel{(\neg(\alpha \vee (\neg \alpha)))}}
}
}

\medskip

   It is now straightforward to do a ``case analysis'' in which we derive the conclusion with the help
       of $\alpha$ and then with the help of $(\neg \alpha)$. 
   Explicitly we build proofs

\medskip 

\infer[(\vee I)]{((\neg \alpha) \vee \beta)}{\infer[(\rightarrow E)]{\beta}{\alpha & (\alpha \rightarrow \beta)}}

and

\infer[(\vee I)]{((\neg \alpha) \vee \beta)}{(\neg \alpha)}

\medskip 

  Then we combine everything together using the or-elimination rule.


\infer[(\vee E)]
{( (\neg \alpha) \vee \beta) }
{
\infer[(RAA)]
{(\alpha \vee (\neg\alpha))}
{
\infer[(\neg I)]
{ (\neg(\neg(\alpha \vee (\neg \alpha))))}
{
\infer[(\neg I)]{(\neg\alpha)}{\infer[(\vee I)]{(\alpha \vee (\neg \alpha))}{\cancel{\alpha}} & \cancel{(\neg(\alpha \vee (\neg \alpha)))}}
&
\infer[(\neg I)]{(\neg(\neg\alpha))}{\infer[(\vee I)]{(\alpha \vee (\neg \alpha))}{\cancel{\neg\alpha}} & \cancel{(\neg(\alpha \vee (\neg \alpha)))}}
}
}
&
\infer[(\vee I)]{((\neg \alpha) \vee \beta)}{\infer[(\rightarrow E)]{\beta}{\cancel{\alpha} & (\alpha \rightarrow \beta)}}
&
\infer[(\vee I)]{((\neg \alpha) \vee \beta)}{\cancel{(\neg \alpha)}}
}

   Finally we do an implication-introduction
\[
\infer[(\rightarrow I)]
{(\alpha \rightarrow \beta) \rightarrow ( (\neg \alpha) \vee \beta)}
{
\infer[(\vee E)]
{( (\neg \alpha) \vee \beta) }
{
\infer[(RAA)]
{(\alpha \vee (\neg\alpha))}
{
\infer[(\neg I)]
{ (\neg(\neg(\alpha \vee (\neg \alpha))))}
{
\infer[(\neg I)]{(\neg\alpha)}{\infer[(\vee I)]{(\alpha \vee (\neg \alpha))}{\cancel{\alpha}} & \cancel{(\neg(\alpha \vee (\neg \alpha)))}}
&
\infer[(\neg I)]{(\neg(\neg\alpha))}{\infer[(\vee I)]{(\alpha \vee (\neg \alpha))}{\cancel{\neg\alpha}} & \cancel{(\neg(\alpha \vee (\neg \alpha)))}}
}
}
&
\infer[(\vee I)]{((\neg \alpha) \vee \beta)}{\infer[(\rightarrow E)]{\beta}{\cancel{\alpha} & \cancel{(\alpha \rightarrow \beta)}}}
&
\infer[(\vee I)]{((\neg \alpha) \vee \beta)}{\cancel{(\neg \alpha)}}
}
}
\]


\item  $( (\neg \alpha) \vee \beta) \rightarrow (\alpha \rightarrow \beta)$. 


   First we prove $\beta$ from $\alpha$ and $( (\neg \alpha) \vee \beta)$.

\medskip

\infer[\vee E]{\beta}{( (\neg \alpha) \vee \beta) & \infer[(\neg E)]{\beta}{\alpha & \cancel{(\neg \alpha)}} & \cancel{\beta}}   

\medskip

   Then we use the implication-introduction rule twice.

\medskip

\infer[(\rightarrow I)]
{( (\neg \alpha) \vee \beta) \rightarrow (\alpha \rightarrow \beta)}
{
\infer[(\rightarrow I)]
{\alpha \rightarrow \beta}
{
\infer[\vee E]{\beta}{\cancel{( (\neg \alpha) \vee \beta)} & \infer[(\neg E)]{\beta}{\cancel{\alpha} & \cancel{(\neg \alpha)}} & \cancel{\beta}}   
}
}

\medskip

\item  $(\alpha \rightarrow \beta) \rightarrow ( (\neg \beta) \rightarrow (\neg\alpha))$. 


\medskip

\infer[(\rightarrow I)]
{(\alpha \rightarrow \beta) \rightarrow ( (\neg \beta) \rightarrow (\neg\alpha))}
{
\infer[(\rightarrow I)]
{ ( (\neg \beta) \rightarrow (\neg\alpha))}
{
\infer[(\neg I)]
{(\neg \alpha)}
{
\infer[(\rightarrow E)]{\beta}{\cancel{\alpha} & \cancel{(\alpha \rightarrow \beta)}}
&
\cancel{(\neg \beta)}
}
}
}



\item  $((\neg \beta) \rightarrow (\neg\alpha)) \rightarrow  (\alpha \rightarrow \beta)$ 

\medskip

\infer[(\rightarrow I)]
{
((\neg \beta) \rightarrow (\neg\alpha)) \rightarrow  (\alpha \rightarrow \beta)
}
{ 
\infer[(\rightarrow I)]
{\alpha \rightarrow \beta}
{
\infer[(RAA)]
{\beta}
{
\infer[(\neg I)]
{(\neg(\neg \beta))}
{
\cancel{\alpha} 
&
\infer[(\rightarrow I)]{(\neg \alpha)}{\cancel{(\neg \beta)} & \cancel{((\neg \beta) \rightarrow (\neg\alpha))}}
}
}
}
}

\end{enumerate} 

\item  (20 points, 10 for each) Prove the following formulae without using the Contradiction rule (that is the last rule from class, that lets
    you take a proof with conclusion $\neg \neg \beta$ and make a proof with the same hypotheses and conclusion $\beta$).

\begin{enumerate}

\item $\neg \beta \rightarrow \neg \neg \neg \beta$.

\medskip

\infer[(\rightarrow I)]
{\neg\beta \rightarrow \neg\neg\neg\beta}
{
\infer[(\neg I)]{\neg\neg\neg\beta}{\cancel{\neg\beta} & \cancel{\neg\neg\beta}}
}


\item $\neg \neg \neg \beta \rightarrow \neg \beta$. 


\infer[(\rightarrow I)]
{\neg \neg \neg \beta \rightarrow \neg \beta}
{
\infer[(\neg I)]
{\neg \beta}
{
\infer[(\neg I)]
{\neg\neg\beta}
{\cancel{\beta} & \cancel{\neg\beta}}
&
\cancel{\neg\neg\neg\beta}
}
}




\end{enumerate} 


\item  (10 points) Prove the formula $\beta \vee \gamma$ from the hypotheses $\alpha \vee \beta$, $\neg \alpha \vee \gamma$.
 
  We use the proof of $\alpha \vee \neg \alpha$ from earlier. 

\infer[(\vee E)]
{\beta \vee \gamma}
{
\infer[(RAA)]
{(\alpha \vee (\neg\alpha))}
{
\infer[(\neg I)]
{ (\neg(\neg(\alpha \vee (\neg \alpha))))}
{
\infer[(\neg I)]{(\neg\alpha)}{\infer[(\vee I)]{(\alpha \vee (\neg \alpha))}{\cancel{\alpha}} & \cancel{(\neg(\alpha \vee (\neg \alpha)))}}
&
\infer[(\neg I)]{(\neg(\neg\alpha))}{\infer[(\vee I)]{(\alpha \vee (\neg \alpha))}{\cancel{\neg\alpha}} & \cancel{(\neg(\alpha \vee (\neg \alpha)))}}
}
}
&
\infer[(\vee I)]
{\beta \vee \gamma}
{
\infer[\vee E]{\gamma}{( (\neg \alpha) \vee \gamma) & \infer[(\neg E)]{\gamma}{\cancel{\alpha} & \cancel{(\neg \alpha)}} & \cancel{\gamma}}   
}
&
\infer[(\vee I)]
{\beta \vee \gamma}
{
\infer[\vee E]{\beta}{( \alpha \vee \beta) & \infer[(\neg E)]{\beta}{\cancel{\alpha} & \cancel{(\neg \alpha)}} & \cancel{\beta}}   
}
}


\item (10 points)  A consistent theory $\Gamma$ is said to be {\em maximally consistent} if there no consistent
   $\Delta$ with $\Gamma \subsetneq \Delta$. Prove that a maximally consistent theory is deductively closed.   
   Hint: Suppose it isn't, what would be a natural thing to try adding? 

    Let $\Gamma \vdash \delta$. We claim that
    $\Gamma \cup \{ \delta \}$ is consistent; if not then 
    easily (apply not-introduction) $\Gamma \vdash \neg \delta$, contradicting the consistency of $\Gamma$.
    Now maximality implies that $\delta \in \Gamma$.  


\end{enumerate}

\section*{Homework 3} 

\begin{enumerate}

\item (10 points total)  Recall that the {\em deductive closure} of a set $\Gamma$ of propositional formulae
     is $\{ \delta: \Gamma \vdash \delta \}$. A set is {\em deductively closed} if and only
     if it is equal to its own deductive closure.  Use the Soundness and Completeness
     theorems to give a short proof that for any $\Gamma$ the deductive closure 
     of $\Gamma$ is deductively closed (if your proof uses induction or is more than ten
     lines long then it is probably too long)

     Let $\delta$ be in the deductive closure of the deductive closure of $\Gamma$, and fix
     a proof $P$ of $\delta$ from hypotheses in the deductive closure of $\Gamma$. By 
      Soundness any truth assignment that satisfies $\Gamma$ satisfies the hypotheses of $P$, and
     hence by Soundness satisfies $\delta$. So $\Gamma \models \delta$ and thus by Completeness
     $\Gamma \vdash \delta$. 


\item (10 points total) Prove that no finite consistent set of propositional formulae is complete.

   Let $F$ be  a finite consistent set and let $n$ be largest such that $A_n$ appears in $F$.
   Since $F$ is consistent, by Completeness there is some truth assignment $f$ that satisfies $F$. Changing the
   value of $f(A_{n+1})$ we obtain another assignment satisfying $F$, so by Soundness
   $F$ can neither prove $A_n$ nor prove $\neg A_n$.


\item (10 points total) Let $\Gamma$ be a set of propositional formulae. Prove that if every finite
    subset of $\Gamma$ is consistent, then $\Gamma$ is consistent.

   Proofs are finite, so if $\Gamma$ is inconsistent then a finite subset must be inconsistent.





\item (20 points total) Two formulae of propositional logic are {\em equivalent} if they are satisfied by exactly the
   same truth assignments. 

\begin{enumerate}
\item (10 points)  Prove that every propositional formula is equivalent to one which only uses $\neg$ and $\wedge$.
\item (10 points) Prove that not every propositional formula is equivalent to one which only uses $\rightarrow$.
\end{enumerate}

  It will suffice to express the other connectives, then an easy induction on propositional formulae will prove
   the result. $\alpha \vee \beta$ is equivalent to $\neg(\neg \alpha \wedge \neg \beta)$,
   and $\alpha \rightarrow \beta$ is equivalent to $\neg \alpha \vee \beta$, which is equivalent to
   $\neg(\alpha \wedge \neg \beta)$.

   If a formula contains only $\rightarrow$ connectives then it is always true when every variable is set to true. 



\item (15 points total)  Consider a signature for a first order language which has only three symbols, a binary function
    symbol $\circ$, a constant symbol $e$, and a binary relation symbol $\equiv$ (whose intended 
   interpretation is the equality relation).  Write down sentences which express:
\begin{enumerate}
\item  (5 points) $\circ$ is commutative. 
\item  (5 points) $\circ$ is associative.
\item  (5 points) $e$ is a two-sided identity element for $\circ$.
\end{enumerate}

$\forall x \; \forall y \;  x \circ y \equiv y \circ x$, or to be really picky

$(\forall x_0 \; ( \forall x_1 \; \equiv(\circ(x_0, x_1), \circ(x_1,x_0)) ) )$.

$\forall x \; \forall y \;  \forall z \;  (x \circ y) \circ z \equiv x \circ( y \circ z)$.

$\forall x \; (x \circ e \equiv x) \wedge (e \circ x \equiv x)$.


\end{enumerate}



\section*{Homework 4} 


\begin{enumerate}


\item (10 points)   Prove by induction on the term $\rho$ that if $x$ and $y$ are distinct variables
    and $\sigma$ and $\tau$ are closed terms, then
   $\rho[x/\sigma][y/\tau] = \rho[y/\tau][x/\sigma]$.

Base case(s): If $\rho$ is a constant $c$ then $c[x/\sigma][y/\tau] = c = c[y/\tau][x/\sigma]$.

  If $\rho$ is $x$ then $x[x/\sigma][y/\tau]=\sigma[y/\tau] = \sigma$ as $\sigma$ is closed.
   Now $x[y/\tau][x/\sigma] = x[x/\sigma] = \sigma$, using that $x$ and $y$ are distinct in the first step. 

  A similar argument works if $\rho$ is $y$.

  Finally if $\rho$ is a variable symbol $z$ which is not $x$ or $y$, then
  $z[x/\sigma][y/\tau] = z = z[y/\tau][x/\sigma]$.

 Induction step(s): Easy using the recursive definition of substitution.  


\item  (30 pts, 5 per proof) Since we are using the quantifier rules which have tricky restrictions, we will
 build proofs in stages making sure we obey the restrictions at each step. 
   

\begin{enumerate}

\item $\exists x \;  \phi \rightarrow \neg \forall  x \; \neg \phi$.

  Start with
\[
  \infer[(\forall E)]{\neg \phi}{\forall x \; \neg \phi}
\]
 Then build
\[
  \infer[(\neg I)]{\neg \forall x \; \neg \phi}{\phi &  \infer[(\forall E)]{\neg \phi}{\cancel{\forall x \; \neg \phi}}}
\]

   Since $x$ only appears free in the hypothesis $\phi$ and not in the conclusion, we may
  use the $\exists E$ rule to get
\[
  \infer[(\exists E)]{\neg \forall x \; \neg \phi}{\exists x \; \phi &   \infer[(\neg I)]{\neg \forall x \; \neg \phi}{\cancel{\phi} &  \infer[(\forall E)]{\neg \phi}{\cancel{\forall x \; \neg \phi}}} }
\]
  and then do $\rightarrow I$ to finish
\[
\infer[(\rightarrow I)]
{
  \exists x \;  \phi \rightarrow \neg \forall  x \; \neg \phi
}
{
 \infer[(\exists E)]{\neg \forall x \; \neg \phi}{\cancel{\exists x \; \phi} &   \infer[(\neg I)]{\neg \forall x \; \neg \phi}{\cancel{\phi} &  \infer[(\forall E)]{\neg \phi}{\cancel{\forall x \; \neg \phi}}} }
}
\]

\item $\neg \forall x \;  \neg \phi \rightarrow \exists  x \; \phi$.

Start with 
\[
   \infer[(\exists I)]{\exists x \; \phi}{\phi}
\]

Then
\[
\infer[(\neg I)]{\neg \phi}{\infer[(\exists I)]{\exists x \; \phi}{\cancel{\phi}} & \neg \exists x \; \phi}
\]
 
Since there are no free $x$'s in the hypotheses,
\[
\infer[(\forall I)]{\forall x \; \neg \phi}{
\infer[(\neg I)]{\neg \phi}{\infer[(\exists I)]{\exists x \; \phi}{\cancel{\phi}} & \neg \exists x \; \phi}
}
\]

 Now we just use a couple of propositional rules:
\[
\infer[(\rightarrow I)]
{
\neg \forall x \;  \neg \phi \rightarrow \exists  x \; \phi
}
{
\infer[(RAA)]
{\exists x \; \phi}
{
\infer[(\neg I)]{\neg \neg \exists x \; \phi}
{
\infer[(\forall I)]{\forall x \; \neg \phi}{
\infer[(\neg I)]{\neg \phi}{\infer[(\exists I)]{\exists x \; \phi}{\cancel{\phi}} & \cancel{\neg \exists x \; \phi}}
}
&
\cancel{\neg \forall x \; \neg \phi}
}
}
}
\]






\item $\forall x \; \phi \rightarrow \neg \exists x \; \neg \phi$.

   Start with an easy application of $\forall E$,
\[
   \infer[(\forall E)]{\phi}{\forall x \; \phi}
\]
   Then do $\neg I$ to get
\[
  \infer[(\neg I)]{\neg \forall x \; \phi}{\infer[(\forall E)]{\phi}{\cancel{\forall x \; \phi}} & \neg \phi}
\]

   At this point we can make an application of $\exists E$ with $\exists x \; \neg \phi$, 
\[
   \infer[(\exists E)]{\neg \forall x \; \phi}{\exists x \; \neg \phi &
\infer[(\neg I)]{\neg \forall x \; \phi}{\infer[(\forall E)]{\phi}{\cancel{\forall x \; \phi}} & \cancel{\neg \phi}}}
\]
  This was legal because $x$ was not free in the conclusion and only appeared in $\neg \phi$ among the hypotheses.

Now we just use the propositional rules $\neg I$ and $\rightarrow I$ to finish
\[
\infer[(\rightarrow I)]
{\forall x \; \phi \rightarrow \neg \exists x \; \neg \phi}
{
\infer[(\neg I)]{\neg \exists x \; \neg \phi}
{
\cancel{\forall x \; \phi}  &
   \infer[(\exists E)]{\neg \forall x \; \phi}{\cancel{\exists x \; \neg \phi} &
\infer[(\neg I)]{\neg \forall x \; \phi}{\infer[(\forall E)]{\phi}{\cancel{\forall x \; \phi}} & \cancel{\neg \phi}}} 
}
}
\]
   



\item $\neg \exists x \; \neg \phi \rightarrow \forall  x \; \phi$.

   Start with an easy application of $\exists I$,
\[
   \infer[(\exists I)]{\exists x \; \neg \phi}{\neg \phi}
\]
  then do a $\neg I$ followed by a $RAA$ to get 
\[
\infer[(RAA)]{\phi}{\infer[(\neg I)]{\neg \neg \phi}{\neg \exists x \; \neg \phi &
  \infer[(\exists I)]{\exists x \; \neg \phi}{\cancel{\neg \phi}}}}
\]

  At this point $x$ is not free in the hypotheses so we may do $\forall I$ to get
\[
\infer[(\forall I)]{\forall x \; \phi}
{
\infer[(RAA)]{\phi}{\infer[(\neg I)]{\neg \neg \phi}{\neg \exists x \; \neg \phi &
  \infer[(\exists I)]{\exists x \; \neg \phi}{\cancel{\neg \phi}}}}
}
\]
 and then finish with a $\rightarrow I$ to get 
\[
\infer[(\rightarrow I)]{\neg \exists x \; \neg \phi \rightarrow \forall  x \; \phi}
{
\infer[(\forall I)]{\forall x \; \phi}
{
\infer[(RAA)]{\phi}{\infer[(\neg I)]{\neg \neg \phi}{\cancel{\neg \exists x \; \neg \phi} &
  \infer[(\exists I)]{\exists x \; \neg \phi}{\cancel{\neg \phi}}}}
}
}
\]






\item $\exists x \; (\phi \vee \psi) \rightarrow ( \exists x \; \phi \vee \exists x \; \psi )$ 


  Build (easy) the proofs
\[
   \infer[(\vee I)]{\exists x \; \phi \vee \exists x \; \psi}{\infer[(\exists I)]{\exists x \; \phi}{\phi}}
\]
and
\[
   \infer[(\vee I)]{\exists x \; \phi \vee \exists x \; \psi}{\infer[(\exists I)]{\exists x \; \psi}{\psi}}
\]

Then use the propositional $\vee E$ rule to get
\[
   \infer[(\vee E)]{\exists x \; \phi \vee \exists x \; \psi}{\phi \vee \psi & 
 \infer[(\vee I)]{\exists x \; \phi \vee \exists x \; \psi}{\infer[(\exists I)]{\exists x \; \phi}{\cancel{\phi}}} &
   \infer[(\vee I)]{\exists x \; \phi \vee \exists x \; \psi}{\infer[(\exists I)]{\exists x \; \psi}{\cancel{\psi}}}
}
\]

 Now we can apply the $\exists E$ rule:
\[
\infer[(\exists E)]{\exists x \; \phi \vee \exists x \; \psi}
{\exists x \; (\phi \vee \psi) &
   \infer[(\vee E)]{\exists x \; \phi \vee \exists x \; \psi}{\cancel{\phi \vee \psi} & 
 \infer[(\vee I)]{\exists x \; \phi \vee \exists x \; \psi}{\infer[(\exists I)]{\exists x \; \phi}{\cancel{\phi}}} &
   \infer[(\vee I)]{\exists x \; \phi \vee \exists x \; \psi}{\infer[(\exists I)]{\exists x \; \psi}{\cancel{\psi}}}
}}
\]
   and finish with the $\rightarrow I$ rule
\[
\infer[(\rightarrow I)]{\exists x \; (\phi \vee \psi) \rightarrow ( \exists x \; \phi \vee \exists x \; \psi )}
{
 \infer[(\exists E)]{\exists x \; \phi \vee \exists x \; \psi}
{\cancel{\exists x \; (\phi \vee \psi)} &
   \infer[(\vee E)]{\exists x \; \phi \vee \exists x \; \psi}{\cancel{\phi \vee \psi} & 
 \infer[(\vee I)]{\exists x \; \phi \vee \exists x \; \psi}{\infer[(\exists I)]{\exists x \; \phi}{\cancel{\phi}}} &
   \infer[(\vee I)]{\exists x \; \phi \vee \exists x \; \psi}{\infer[(\exists I)]{\exists x \; \psi}{\cancel{\psi}}}
}}}
\]

\item $(\exists x \; \phi \vee \exists x \; \psi) \rightarrow  \exists x \; (\phi \vee \psi)$

   Start with the trivial propositional proofs
\[
   \infer[(\vee I)]{\phi \vee \psi}{\phi}, \infer[(\vee I)]{\phi \vee \psi}{\psi} 
\]
   Since $x$ is always permitted for $x$ we may use $\exists I$ to build 
\[
   \infer[(\exists I)]{\exists x \; (\phi \vee \psi)}{\infer[(\vee I)]{\phi \vee \psi}{\phi}}, 
   \infer[(\exists I)]{\exists x \; (\phi \vee \psi)}{\infer[(\vee I)]{\phi \vee \psi}{\psi}} 
\]
   Since the only free appearance of $x$ in the hypotheses of the first proof is in $\phi$,
   and $x$ is not free in the conclusion we may use $\exists E$ and build a proof
\[
\infer[(\exists E)]{\exists x \; (\phi \vee \psi)}{\exists x \; \phi &   \infer[(\exists I)]{\exists x \; (\phi \vee \psi)}{\infer[(\vee I)]{\phi \vee \psi}{\cancel{\phi}}}},
\]
and similarly
\[
\infer[(\exists E)]{\exists x \; (\phi \vee \psi)}{\exists x \; \psi &   \infer[(\exists I)]{\exists x \; (\phi \vee \psi)}{\infer[(\vee I)]{\phi \vee \psi}{\cancel{\psi}}}}
\]

  Now we use the propositional $\vee E$ and $\rightarrow I$ rules to finish.
\[
\infer[(\rightarrow I)]{(\exists x \; \phi \vee \exists x \; \psi) \rightarrow  \exists x \; (\phi \vee \psi)}
{
   \infer[(\vee E)]{\exists x \; (\phi \vee \psi)}
{
   \cancel{\exists x \; \phi \vee \exists x \; \psi} & 
   \infer[(\exists E)]{\exists x \; (\phi \vee \psi)}{\cancel{\exists x \; \phi} &   \infer[(\exists I)]{\exists x \; (\phi \vee \psi)}{\infer[(\vee I)]{\phi \vee \psi}{\cancel{\phi}}}} &
   \infer[(\exists E)]{\exists x \; (\phi \vee \psi)}{\cancel{\exists x \; \psi} &   \infer[(\exists I)]{\exists x \; (\phi \vee \psi)}{\infer[(\vee I)]{\phi \vee \psi}{\cancel{\psi}}}}
}
}   
\]


\end{enumerate}




\item  (10 points) Let $\phi$ be a formula in some first order language, and suppose that $\phi$ has exactly two
    free variables $x$ and $y$. Let $\mathcal M$ be a structure for the language. Prove that
 ${\mathcal M} \models \forall x \; \forall y \; \phi$ if and only if 
 ${\mathcal M} \models \forall y \; \forall x \; \phi$. 



 ${\mathcal M} \models \forall x \; \forall y \; \phi$ if and only if 
  for all $a$ in $M$ ${\mathcal M} \models \forall y \; \phi[x/c_a]$ if and only if 
  for all $a, b \in M$ ${\mathcal M} \models \; \phi[x/c_a][y/c_b]$.
  Similarly ${\mathcal M} \models \forall y \; \forall x \; \phi$ if and only if 
   for all $a, b \in M$ ${\mathcal M} \models \; \phi[y/c_b][x/c_a]$.

  So we will be done once we can prove that $\phi[x/c_a][y/c_b] = \phi[y/c_b][x/c_a]$.
  In fact we may as well prove a version of Q1 for formulae, which is a straightforward
  induction whose base case (atomic formulae) is handled by Q1.  




\end{enumerate} 

\end{document} 






\end{document} 



