\section{The Curious Kestrel}

\definition{}
Recall that a bird is \textit{egocenteric} if it is fond of itself. \\
A bird is \textit{hopelessly egocentric} if $Bx = B$ for all birds $x$.

\definition{}
More generally, we say that a bird $A$ is \textit{fixated} on a bird $B$ if $Ax = B$ for all $x$. \\
Convince yourself that a hopelessly egocentric bird is fixated on itself.



\problem{}
Say $A$ is fixated on $B$. Is $A$ fond of $B$?

\begin{solution}
	Yes! See the following proof.
	\begin{alltt}
		\lineno{} let B
		\lineno{} let B
		\lineno{} let A so that Ax = B
		\lineno{} \thus{} AB = B \qed{}
	\end{alltt}
\end{solution}
\vfill



\definition{}
The \textit{Kestrel} $K$ is defined by the following relationship:
$$
	(Kx)y = x
$$
In other words, this means that for every bird $x$, the bird $Kx$ is fixated on $x$.

\problem{}
Show that an egocenteric Kestrel is hopelessly egocentric

\begin{solution}
	\begin{alltt}
		\lineno{} KK = K
		\lineno{} \thus{} (KK)y = K
		\lineno{} \thus{} Ky = K \qed{}
	\end{alltt}
\end{solution}

\vfill
\pagebreak


\problem{}
Assume the forest contains a Kestrel. \\
Given $L_1$ and $L_2$, show that at least one bird is hopelessly egocentric.

\begin{helpbox}[0.75]
	\texttt{Def:} $K$ is defined by $(Kx)y = x$ \\
	\texttt{Def:} $A$ is fond of $B$ if $AB = B$ \\
	\texttt{???:} You'll need one more result from the previous section. Good luck!
\end{helpbox}

\begin{solution}
	The final piece is a lemma we proved earler: \\
	Any bird is fond of at least one bird

	\begin{alltt}
		\lineno{} let A so that KA = A   \cmnt{Any bird is fond of at least one bird}
		\lineno{} (KA)y = y              \cmnt{By definition of the kestrel}
		\lineno{} \thus{} Ay = A \qed{}  \cmnt{By 01}
	\end{alltt}
\end{solution}

\vfill

\problem{Kestrel Left-Cancellation}<leftcancel>
In general, $Ax = Ay$ does not imply $x = y$. However, this is true if $A$ is $K$. \\
Show that $Kx = Ky \implies x = y$.

\begin{alltt}
	\cmnt{This is a hint.}
	let x, y so that Kx = Ky
\end{alltt}

\begin{solution}
	\begin{alltt}
		\lineno{} let x, y so that Kx = Ky
		\lineno{} let z
		\lineno{}
		\lineno{} (Kx)z = (Ky)z  \cmnt{By 01}
		\lineno{}
		\lineno{} \cmnt{By the definition of K}
		\lineno{} (Kx)z = x
		\lineno{} (Ky)z = y
		\lineno{}
		\lineno{} \thus{} x = (Kx)z = (Ky)z = y \qed{}
	\end{alltt}
\end{solution}

\vfill
\pagebreak

\problem{}
Show that if $K$ is fond of $Kx$, $K$ is fond of $x$.

\begin{solution}
	\begin{alltt}
		\lineno{} let x so that K(Kx) = Kx
		\lineno{} (K(Kx))y = (Kx)y
		\lineno{}          = Kx  \cmnt{By definition of K}
		\lineno{} x = Kx  \cmnt{By 03 and definition of K}
	\end{alltt}
\end{solution}

\vfill

\problem{}
An egocentric Kestrel must be extremely lonely. Why is this?

\begin{solution}
	If a Kestrel is egocenteric, it must be the only bird in the forest:

	\begin{alltt}
		\lineno{} \cmnt{Given}
		\lineno{} Kx = K for some x
		\lineno{} \cmnt{We have shown that an egocentric kestrel is hopelessly egocentric}
		\lineno{} Kx = K for all x
		\lineno{}
		\lineno{} let x, y
		\lineno{} Kx = K
		\lineno{} Ky = K
		\lineno{} Kx = Ky
		\lineno{} x = y for all x, y  \cmnt{By \ref{leftcancel}}
		\lineno{} x = y = K \qed{}  \cmnt{By 10, and since K exists}
	\end{alltt}
\end{solution}

\vfill
\pagebreak