\begin{frame}{Russell's Barber Paradox} \paradox \medskip What does the law require of the barber? \alert{He has no option!} \pause\smallskip \hspace*{\fill}\rule{0.7\textwidth}{0.75pt}\hspace*{\fill}\mbox{} \medskip Is the following formula satisfiable? \begin{align*} \formula{\existsst{x}{\big( \unpred{man}{x} \logandinf \forallst{y}{\big(\unpred{man}{y} \logimpinf (\binpred{shaves}{x}{y} \logbiimpinf \lognot{\binpred{shaves}{y}{y}}) \big)} \big)}} \end{align*} \pause Or the following simplified version? \begin{align*} \formula{\existsst{x}{ \forallst{y}{(\binpred{shaves}{x}{y} \logbiimpinf \lognot{\binpred{shaves}{y}{y}})}}} \end{align*} \pause Actually this formula is \alert{unsatisfiable} (not satisfiable). \vspace{10cm} \end{frame} \theme{Predicate Logic with Equality}