handouts/Advanced/Mock a Mockingbird/parts/01 tmam.tex

\section{To Mock a Mockingbird}

\problem{}
Mark tells you that any bird $A$ is fond of at least one other bird. \\
Complete his proof.
\begin{alltt}
	let A           \cmnt{Let A be any any bird.}
	let Cx = A(Mx)  \cmnt{Define C as the composition of A and M}

	\cmnt{The rest is up to you.}
	CC = ??
\end{alltt}


\begin{helpbox}
	\texttt{Law:} There exists a Mockingbird, $Mx := xx$ \\
	\texttt{Def:} $A$ is fond of $B$ if $AB = B$
\end{helpbox}


\begin{solution}
	\begin{alltt}
		\lineno{} let A           \cmnt{Let A be any any bird.}
		\lineno{} let Cx = A(Mx)  \cmnt{Define C as the composition of A and M}
		\lineno{} CC = A(MC)
		\lineno{}    = A(CC)  \qed{}
	\end{alltt}
\end{solution}

\vfill
\problem{}
We say a bird $A$ is \textit{egocentric} if it is fond of itself. \\
Show that the laws of the forest guarantee that at least one bird is egocentric.


\begin{helpbox}
	\texttt{Law:} There exists a Mockingbird, $Mx := xx$ \\
	\texttt{Def:} $A$ is fond of $B$ if $AB = B$ \\
	\texttt{Lem:} Any bird is fond of at least one bird.
\end{helpbox}

\begin{solution}
	\begin{alltt}
		\lineno{} \cmnt{We know M is fond of at least one bird.}
		\lineno{} let E so that ME = E
		\lineno{}
		\lineno{} ME = E     \cmnt{By definition of fondness}
		\lineno{} ME = EE    \cmnt{By definition of M}
		\lineno{} \thus{} EE = E  \qed{}
	\end{alltt}
\end{solution}

\vfill
\pagebreak


\definition{}
We say a bird $A$ is \textit{agreeable} if for all birds $B$, there is at least one bird $x$ on which $A$ and $B$ agree. \\
In other words, $A$ is agreeable if given any $B$, we can find a bird $x$ satisfying $Ax = Bx$.

\problem{}
Is the Mockingbird agreeable?

\begin{solution}
	We know that $Mx = xx$. \\

	From this definition, we see that $M$ agrees with any $x$ on $x$ itself.
\end{solution}

\vfill

\problem{}
Take two birds $A$ and $B$. Let $C$ be their composition. \\
Show that if $C$ is agreeable, $A$ is agreeable.
\begin{alltt}
	\cmnt{Given information}
	let A, B
	let Cx = A(Bx)

	let D            \cmnt{Arbitrary bird}
	let Ex = D(Bx)   \cmnt{Define E as the composition of D and B}
	Cy = ??
\end{alltt}

\begin{helpbox}[0.65]
	\texttt{Def:} $A$ is agreeable if $Ax = Bx$ for all $B$ with some $x$. \\
	\texttt{Law:} For any $A, B$, there is C defined by Cx = A(Bx)
\end{helpbox}


\begin{solution}
	\begin{alltt}
		\lineno{} \cmnt{Given information}
		\lineno{} let A, B
		\lineno{} let Cx = A(Bx)
		\lineno{}
		\lineno{} let D                  \cmnt{Arbitrary bird}
		\lineno{} let Ex = D(Bx)         \cmnt{Define E as the composition of D and B}
		\lineno{} let y so that Cy = Ey  \cmnt{Such a y must exist because C is agreeable}
		\lineno{}
		\lineno{} A(By) = Ey
		\lineno{}       = D(By)  \qed{}
	\end{alltt}
\end{solution}

\vfill
\pagebreak

\problem{}
Given three arbitrary birds $A$, $B$, and $C$, show that there exists a bird $D$ satisfying $Dx = A(B(Cx))$

\begin{solution}
	\begin{alltt}
		\lineno{} let A, B, C
		\lineno{}
		\lineno{} \cmnt{Invoke the Law of Composition:}
		\lineno{} let Qx = B(Cx)
		\lineno{} let Dx = A(Qx)
		\lineno{}
		\lineno{} Dx = A(Qx)
		\lineno{}   = A(B(Cx))  \qed{}
	\end{alltt}
\end{solution}

\vfill


\definition{}
We say two birds $A$ and $B$ are \textit{compatible} if there are birds $x$ and $y$ so that $Ax = y$ and $By = x$. \\
Note that $x$ and $y$ may be the same bird. \\

\problem{}
Show that any two birds in this forest are compatible. \\
\begin{alltt}
	let A, B
	let Cx = A(Bx)
\end{alltt}

\begin{helpbox}
	\texttt{Law:} Law of composition \\
	\texttt{Lem:} Any bird is fond of at least one bird.
\end{helpbox}

\begin{solution}
	\begin{alltt}
		\lineno{} let A, B
		\lineno{}
		\lineno{} let Cx = A(Bx)  \cmnt{Composition}
		\lineno{} let y = Cy      \cmnt{Let C be fond of y}
		\lineno{}
		\lineno{} Cy = y
		\lineno{}    = A(By)
		\lineno{}
		\lineno{} let x = By  \cmnt{Rename By to x}
		\lineno{} Ax = y  \qed{}
	\end{alltt}
\end{solution}

\vfill

\problem{}
Show that any bird that is fond of at least one bird is compatible with itself.

\begin{solution}
	\begin{alltt}
		\lineno{} let A
		\lineno{} let x so that Ax = x  \cmnt{A is fond of at least one other bird}
		\lineno{} Ax = x  \qed{}
	\end{alltt}

	That's it.
\end{solution}

\vfill
\pagebreak