\documentclass{amsart}

\usepackage{amssymb} 

\title{21-300 F15 HW 4}

\begin{document}

\maketitle


   Since it's harder to word-process proofs, you may submit hand-written solutions 
   to this homework subject to the following conditions: your homework is written
   in black ink on alternating lines, and is submitted as a legible 600dpi scan in
   PDF form. 

   Note: When I say ``prove'' in this homework I mean produce a formal proof using
   the proof rules from class. Unless I specify hypotheses, your proof should 
   have no hypotheses. Letters from the Greek alphabet ($\alpha$, $\beta$, $\gamma$, $\delta$)
   stand for arbitrary formulae. Your proofs should be labelled so that it is clear which proof rule was used at
   which stage. 

   IMPORTANT: PLEASE EMAIL COMPLETED HOMEWORKS TO:
\begin{verbatim}
   lserafin.algebra@gmail.com
\end{verbatim}

\begin{enumerate}


\item   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]$.

\item  Prove the formulae:
   

\begin{enumerate}

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

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

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

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


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

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


\end{enumerate}



\item  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$. 


\end{enumerate}

\end{document} 



