\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}