20/155
\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}