141/160
\begin{frame}[t]{Reachability is Undefinable (Proof)}
   
  \begin{block}{}
    There is \alert{no} sentence\/ $\bap{\cform}{\const{c}}{\const{d}}$ such that for all $\model{\amodel}$:
    \begin{talign}\tag{$\star$}\label{eq:defines:reacable}
       \model{\amodel} \satisfies \bap{\cform}{\const{c}}{\const{d}}
       \;\Longleftrightarrow\;
       \text{$\intin{\const{d}}{\model{\amodel}}$ reachable from $\intin{\const{c}}{\model{\amodel}}$
             by $\intin{\sbinpred{R}}{\model{\amodel}}$-steps}
    \end{talign}     
  \end{block}
  \pause\medskip
  
  \begin{enumerate}[(1)]\setlength{\itemsep}{0.4ex}
     \item{}\label{item:assumption:express:reachability}
       Suppose that there exists $\bap{\cform}{\const{c}}{\const{d}}$ with \eqref{eq:defines:reacable}.
   \pause
      \item Then we consider the set $\bsetforms$ of formulas:    
        \begin{talign}
          \bsetforms & \;\; = \;\;
            \setexp{ \formula{\bap{\cform}{\const{c}}{\const{d}}} } \:\cup\:
            \setexp{ \formula{\lognot{\bap{\cformi{0}}{\const{c}}{\const{d}}}},\,
                     \formula{\lognot{\bap{\cformi{1}}{\const{c}}{\const{d}}}},\,
                     \formula{\lognot{\bap{\cformi{2}}{\const{c}}{\const{d}}}},\, \ldots }  
        \end{talign}
    \pause\vspace{-2.5ex}
      \item{}\label{item:set:inconsistent}
        The set $\bsetforms$ is \emph{inconsistent}\malt[7]{:
          \begin{itemize}
          \pause
            \item 
              If $\model{\amodel} \satisfies \bap{\cform}{\const{c}}{\const{d}}$,
              \pause
              there are $\sbinpred{R}$-steps from $\intin{\const{c}}{\model{\amodel}}$ to $\intin{\const{d}}{\model{\amodel}}$,
              \pause 
              say $\forestgreen{m}$.
          \pause
            \item 
              Hence $\model{\amodel} \satisfies \formula{\bap{\cformi{\forestgreen{m}}}{\const{c}}{\const{d}}}$, \pause
              and so $\model{\amodel} \satisfiesnot \formula{\lognot{\bap{\cformi{\forestgreen{m}}}{\const{c}}{\const{d}}}}$.
          \pause
            \item Consequently $\model{\amodel} \satisfiesnot \bsetforms$.
          \end{itemize}
        }{.}
      \updatepause
        \item \label{item:finite:subsets:consistent}
          Yet every finite $\bsetformsi{0}\subseteq\bsetforms$ is \emph{consistent}\malt[8]{:
          \begin{itemize}
          \pause
            \item 
              Let $\bsetformsi{0}\subseteq\bsetforms$ be finite.
          \pause
            \item 
              Then $\formula{\lognot{\bap{\cformi{\forestgreen{n_0}}}{\const{c}}{\const{d}}}} \notin \bsetformsi{0}$ 
              for some $\forestgreen{n_0}$.
          \pause
            \item 
              Let $\model{\amodel}$ a model 
              with exactly $\forestgreen{n_0}$ $\intin{\sbinpred{R}}{\model{\amodel}}$-steps
              from $\intin{\const{c}}{\model{\amodel}}$ to $\intin{\const{d}}{\model{\amodel}}$.
          \pause
            \item 
              Then 
              $\model{\amodel} \satisfies \formula{\bap{\cform}{\const{c}}{\const{d}}}\,$
              \pause and
              $\model{\amodel} \satisfies \formula{\lognot{\bap{\cformi{\black{n}}}{\const{c}}{\const{d}}}}$
              for all $n\neq\forestgreen{n_0}$.
          \pause
            \item 
              Hence $\model{\amodel} \satisfies \bsetformsi{0}$, \pause
              and we conclude that $\bsetformsi{0}$ is consistent. 
          \end{itemize}
          }{.}
      \updatepause
        \item
          A set $\bsetforms$ of formulas with 
          \mediumblue{\eqref{item:set:inconsistent}} and \mediumblue{\eqref{item:finite:subsets:consistent}}
          \alert{contradicts} the \alert{compactness theorem}.
      \pause
        \item   
          The problem must be \alert{assumption~\mediumblue{\eqref{item:assumption:express:reachability}}}.  
          \medskip
           
          So we conclude that \alert{there cannot be such a formula $\cform$}.
  \end{enumerate}  
  \vspace{10cm}
\end{frame}