\documentstyle[portrait,semcolor]{seminar}

\input{macros.tex}

\newrgbcolor{negcolor}{0.8 0 0}
\newrgbcolor{affirmcolor}{0 0.65 0.15}
\newrgbcolor{noisecolor}{0.8 0 0}
\newrgbcolor{noisecolorone}{0.825 0.3 0}
\newrgbcolor{noisecolortwo}{0.824 0 0.578}
\newrgbcolor{evcolor}{0 0.55 0.3}
\newrgbcolor{ptcolor}{0 0 0.8}
\newrgbcolor{conncolor}{0 0 0.8}

\slideframe{none}

\begin{document}

\begin{slide*}
\begin{center}
{\Large Intuitive Counterexamples for Constructive Fallacies}\\[5ex]
James Lipton\\
{\it Wesleyan University}\\[5ex]
Michael J.\ O'Donnell\\
{\it The University of Chicago}
\end{center}
\end{slide*}

\begin{slide*}
\begin{center}
{\LARGE\sf ADVERTISEMENT}\\[5ex]
{\it The Chicago Journal of}\\
{\it Theoretical Computer Science}
\end{center}
\begin{raggedright}
Published by MIT Press\\
in \LaTeX\ source format on Internet\\[3ex]
{\tt http://cs-www.uchicago.edu/publications/cjtcs}\\[3ex]
{\tt chicago-journal@cs.uchicago.edu}
\end{raggedright}
\end{slide*}

\begin{slide*}
\begin{center}
{\Large Intuitive Counterexamples for Constructive Fallacies}
\end{center}
\vspace{5ex}
\begin{raggedright}
``Intuitive'' means:\\[5ex]
{\em Not\/}\\
{\negcolor easy to do the metamathematics intuitively}\\[5ex]
{\em But rather,}\\
{\affirmcolor connected to nonmathematical intuitions}
\end{raggedright}
\end{slide*}

\begin{slide*}
\begin{raggedright}
Hand-drawn slide showing logic (looks like car) salesman.\\
Salesman: ``1930 Heyting Calculus, \ldots it's fully constructive,
dual algebraic units, \ldots''\\
Customer: ``But it won't prove $(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$!''\\
A countermodel is an {\em excuse\/} for not proving a given formula.
\end{raggedright}
\end{slide*}

\begin{slide*}
\begin{center}
\setlength{\arraycolsep}{2ex}
\renewcommand{\arraystretch}{2}
\begin{displaymath}
\begin{array}{|c|c|}
\hline
\alpha & F \\
\hline
\beta & T \\
\hline
\end{array}
\end{displaymath} \\[5ex]
{\sf Classical countermodel for} \\
$(\alpha\limplies\beta)\limplies(\beta\limplies\alpha)$\\[5ex]
$\alpha =$
``In the table above, the symbol `$\alpha$' appears in a row
with the symbol `$T$'.''\\[3ex]
$\beta =$
``In the table above, the symbol `$\beta$' appears in a row
with the symbol `$T$'.''
\end{center}
\end{slide*}

\begin{slide*}
\begin{center}
{\setlength{\unitlength}{.225cm}
  \begin{picture}(20,20)(-10,-6)
    \thicklines
    \put(1,1){        \vector(1,1){8}                         }
    \put(-1,1){       \vector(-1,1){8}                        }
    \put(0,0){        \circle*{1}                             }
    \put(0,-3){       \makebox(0,0)[t]{$\set{}$}              }
    \put(-10,10){     \circle*{1}                             }
    \put(-10,13){     \makebox(0,0)[b]{$\set{\alpha}$} }
    \put(10,10){      \circle*{1}                             }
    \put(10,13){      \makebox(0,0)[b]{$\set{\beta}$}  }
  \end{picture}
} \\[5ex]
{\sf Kripke countermodel for} \\
$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$
\end{center}
\end{slide*}

\begin{slide*}
\begin{center}
{\sf Temporal/epistemic interpretation of Kripke model}
\end{center}
\vspace{5ex}
\begin{raggedright}
{\it Now:\/}\\
Neither $\alpha$ nor $\beta$ is constructively knowable\\[5ex]
{\it Possibly tomorrow:}\\
$\alpha$ is knowable, but not $\beta$\\[5ex]
{\it But also possibly tomorrow:}\\
$\beta$ is knowable, but not $\alpha$
\end{raggedright}
\end{slide*}

\begin{slide*}
\begin{center}
Realizability [Kleene, L\"auchli]\\
Formulae as types [Howard, Tait]\\
Brouwer-Heyting-Kolmogorov interpretation
\end{center}
\vspace{5ex}
\begin{raggedright}
Evidence for\\
\begin{itemize}
\item $\alpha{\conncolor\land}\beta$---%
  $\alpha$ evidence {\conncolor\em paired with\/} $\beta$ evidence
\item $\alpha{\conncolor\lor}\beta$---%
  $\alpha$ evidence {\conncolor\em or\/} $\beta$ evidence,\\
  \hspace{8ex}{\conncolor\em marked as such}
\item $\alpha{\conncolor\limplies}\beta$---%
  {\conncolor\em maps\/} $\alpha$ evidence {\conncolor\em to} $\beta$ evidence
\item ${\conncolor\forall x}\sepdot\alpha$---%
  {\conncolor\em maps individuals\/} $d$ {\conncolor\em to}
  $\subst{d}{x}{\alpha}$ evidence
\item ${\conncolor\exists x}\sepdot\alpha$---%
  {\conncolor\em individual\/} $d$ {\conncolor\em paired with}\\
  \hspace{9ex}$\subst{d}{x}{\alpha}$ evidence
\end{itemize}
\end{raggedright}
\end{slide*}

\begin{slide*}
\begin{center}
Which evidence for $\alpha$ {\em realizes/verifies\/} $\alpha$?
\end{center}
\vspace{5ex}
\begin{raggedright}
\begin{itemize}
\item {\negcolor\em All evidence\/} yields classical logic
\item {\negcolor\em Computable evidence\/} [Kleene]\\
   yields too much (no completness) [Rose]
\item {\affirmcolor\em Permutation invariant evidence\/} [L\"auchli]\\
  is just right
  (soundness and completeness,\\
  but nonconstructive metamathematics)
\item {\affirmcolor\em Reliably typed evidence\/} [Lipton, O'Donnell]\\
  improves intuition,\\
  constructive metamathematics
  \begin{itemize}
    \item {\affirmcolor Constructive proof of soundness}
    \item {\negcolor Conjecture constructive completeness}
  \end{itemize}
\end{itemize}
\end{raggedright}
\end{slide*}

\begin{slide*}
\begin{center}
{\em (Propositional) L\"auchli realizability model}\\
$\model{M}=\tuple{\universe{U},\evidence{P},\noise{N}}$
\end{center}
\vspace{3ex}
\begin{raggedright}
\begin{itemize}
\item $\universe{U}$ (domain of evidence)
\item $\evidence{P}$ maps
  atomic propositions to subsets of \mbox{$\universe{U}$}
\item $\noise{N}$ is a group of permutations of $\universe{U}$\\
  (noise in $\universe{U}$)
\end{itemize}
Permutations in $\noise{N}$ pull up naturally\\
to higher types\\
(same as {\em logical relations\/} from $\lambda$-calculus)
\end{raggedright}
\begin{center}
$\evidence{a}\in\evidence{P}(\alpha)$ is a {\em realizer\/}\\
iff\\
$f_{\alpha}(\evidence{a})=\evidence{a}$ for all $f\in\noise{N}$
\end{center}
\end{slide*}

\begin{slide*}
\begin{center}
\setlength{\unitlength}{0.025cm}
\begin{picture}(145,177)(55,635)
\thicklines
\put(100,760){\ptcolor\vector( 1, 0){ 83}}
\put(100,640){\ptcolor\vector( 1, 0){ 83}}
\put( 80,740){\noisecolor\vector( 0,-1){ 80}}
\put(200,740){\noisecolor\vector( 0,-1){ 80}}
\put( 80,755){\makebox(0,0)[b]{\ptcolor$\evidence{a}_1$}}
\put(200,755){\makebox(0,0)[b]{\ptcolor$\evidence{b}_1$}}
\put( 80,635){\makebox(0,0)[b]{\ptcolor$\evidence{a}_2$}}
\put(200,635){\makebox(0,0)[b]{\ptcolor$\evidence{b}_2$}}
\put( 80,800){\makebox(0,0)[b]{\evcolor$\evidence{P}(\alpha)$}}
\put(200,800){\makebox(0,0)[b]{\evcolor$\evidence{P}(\beta)$}}
\put(140,770){\makebox(0,0)[b]{\ptcolor$\evidence{c}$}}
\put(140,650){\makebox(0,0)[b]{\ptcolor$f_{\alpha\limplies\beta}(\evidence{c})$}}
\put( 70,705){\makebox(0,0)[r]{\noisecolor$f_{\alpha}$}}
\put(50,620){\evcolor\dashbox{5}(60,160){}}
\put(190,705){\makebox(0,0)[r]{\noisecolor$f_{\beta}$}}
\put(170,620){\evcolor\dashbox{5}(60,160){}}
\end{picture} \\[5ex]
{\sf Diagram of the permuted function} \\
$f_{\alpha\limplies\beta}(\evidence{c})$
\end{center}
\end{slide*}

\begin{slide*}
\begin{raggedright}
Handwritten slide illustrating noise in language using\\
English {\em moose\/} and French {\em mousse}
\end{raggedright}
\end{slide*}

\begin{slide*}
\begin{center}
{\LARGE Permutation invariance\\
$=$ \\
Communicability\\
in spite of noise}\\[8ex]
Necessary, but {\em not\/} sufficient,\\
condition for constructibility\\[3ex]
Necessity is enough for countermodels
\end{center}
\end{slide*}

\begin{slide*}
\begin{center}
\setlength{\unitlength}{0.025cm}
\begin{picture}(270,252)(40,600)
\thicklines
\put(100,640){\noisecolortwo\vector(-4, -1){0}}
\put(100,700){\noisecolortwo\oval( 40,120)[r]}
\put(260,640){\noisecolorone\vector(-4, -1){0}}
\put(260,700){\noisecolorone\oval( 40,120)[r]}
\put( 60,760){\noisecolortwo\vector( 4, 1){0}}
\put( 60,700){\noisecolortwo\oval( 40,120)[l]}
\put(220,760){\noisecolorone\vector( 4, 1){0}}
\put(220,700){\noisecolorone\oval( 40,120)[l]}
\put( 70,617){\noisecolorone\oval( 14, 26)[tl]}
\put( 80,617){\noisecolorone\oval( 34, 34)[b]}
\put( 90,617){\noisecolorone\oval( 14, 26)[tr]}
\put( 90,630){\noisecolorone\vector(-4, 1){0}}
\put(230,617){\noisecolortwo\oval( 14, 26)[tl]}
\put(240,617){\noisecolortwo\oval( 34, 34)[bl]}
\put(240,617){\noisecolortwo\oval( 34, 34)[br]}
\put(250,617){\noisecolortwo\oval( 14, 26)[tr]}
\put(250,630){\noisecolortwo\vector(-4, 1){0}}
\put( 90,783){\noisecolorone\oval( 14, 26)[br]}
\put( 80,783){\noisecolorone\oval( 34, 34)[tr]}
\put( 80,783){\noisecolorone\oval( 34, 34)[tl]}
\put( 70,783){\noisecolorone\oval( 14, 26)[bl]}
\put( 70,770){\noisecolorone\vector( 4, -1){0}}
\put(250,783){\noisecolortwo\oval( 14, 26)[br]}
\put(240,783){\noisecolortwo\oval( 34, 34)[tr]}
\put(240,783){\noisecolortwo\oval( 34, 34)[tl]}
\put(230,783){\noisecolortwo\oval( 14, 26)[bl]}
\put(230,770){\noisecolortwo\vector( 4, -1){0}}
\put( 80,755){\makebox(0,0)[b]{\ptcolor$a_1$}}
\put(240,755){\makebox(0,0)[b]{\ptcolor$b_1$}}
\put( 80,635){\makebox(0,0)[b]{\ptcolor$a_2$}}
\put(240,635){\makebox(0,0)[b]{\ptcolor$b_2$}}
\put( 80,840){\makebox(0,0)[b]{\evcolor$\evidence{P}(\alpha)$}}
\put(240,840){\makebox(0,0)[b]{\evcolor$\evidence{P}(\beta)$}}
\put( 30,700){\makebox(0,0)[r]{\noisecolortwo$f_{2}$}}
\put(110,700){\makebox(0,0)[r]{\noisecolortwo$f_{2}$}}
\put(190,700){\makebox(0,0)[r]{\noisecolorone$f_{1}$}}
\put(270,700){\makebox(0,0)[r]{\noisecolorone$f_{1}$}}
\put(80,810){\makebox(0,0)[b]{\noisecolorone$f_{1}$}}
\put(80,590){\makebox(0,0)[t]{\noisecolorone$f_{1}$}}
\put(240,810){\makebox(0,0)[b]{\noisecolortwo$f_{2}$}}
\put(240,590){\makebox(0,0)[t]{\noisecolortwo$f_{2}$}}
\end{picture} \\[5ex]
{\sf L\"auchli realizability countermodel for} \\
$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$
\end{center}
\end{slide*}

\begin{slide*}
\begin{center}
  {\sf Interpretation of L\"auchli countermodel}
\end{center}
\vspace{5ex}
\begin{raggedright}
$\alpha$ has two pieces of evidence\\
$\beta$ has two pieces of evidence\\[5ex]
{\noisecolorone\em Jane Doe:}\\
agrees with our names for $\alpha$ evidence,\\
reverses our names for $\beta$ evidence\\
won't accept $\alpha\limplies\beta$\\[5ex]
{\noisecolortwo\em Richard Roe:}\\
agrees with our names for $\beta$ evidence\\
reverses our names for $\alpha$ evidence\\
won't accept $\beta\limplies\alpha$
\end{raggedright}
\end{slide*}

\begin{slide*}
\begin{center}
{\LARGE\sf What more do we want?}
\end{center}
\begin{raggedright}
\begin{itemize}
\item {\em Constructive\/} metamathematics\\
  (L\"auchli requires {\em Axiom of Choice}\\
  to produce evidence functions)
\item No dependence on {\em identification\/} of evidence,\\
  only require {\em reliability}
\item Allow nondeterminism in proof of implication
\end{itemize}
\end{raggedright}
\end{slide*}

\begin{slide*}
\begin{center}
{\em (Propositional) relational realizability model}\\
$\model{M}=\tuple{\universe{U},\evidence{P},\noise{N}}$
\end{center}
\vspace{3ex}
\begin{raggedright}
\begin{itemize}
\item $\universe{U}$ (domain of evidence)
\item $\evidence{P}$ maps
  atomic propositions to subsets of \mbox{$\universe{U}$}
\item $\noise{N}$ is a set of permutations of $\universe{U}$\\
  (noise in $\universe{U}$)
\end{itemize}
\end{raggedright}
Same as L\"auchli model so far\\
(except $\noise{N}$ not a group),\\
but we need a {\em different\/} type hierarchy
\end{slide*}

\begin{slide*}
\begin{center}
{\sf Differences in relational type hierarchy}
\end{center}
\vspace{5ex}
\begin{raggedright}
\begin{itemize}
\item Evidence for $\alpha\limplies\beta$ is\\
  {\conncolor\em reliable nondeterministic mapping}\\
  instead of {\em function}
\item Expand each individual evidence to\\
  {\conncolor finite sets of evidence (nondeterministic)}
  \begin{itemize}
  \item {\conncolor Only {\em one\/} member of a set\\
    needs to be correct}
  \end{itemize}
\end{itemize}
Permutations still pull up to higher types\\
as {\em logical relations\/} from $\lambda$-calculus\\[3ex]
BUT (the final, key, difference):
\end{raggedright}
\begin{center}
$\evidence{A}\in{\conncolor\hat{\universe{U}}_{\alpha}}$
  is a {\em realizer\/}\\
iff\\
$\hat{f}_{\alpha}(\evidence{A}){\conncolor\intersect\evidence{P}(\alpha)}$
  {\conncolor is inhabited} for all $f\in\noise{N}$
\end{center}
\end{slide*}

\begin{slide*}
\begin{center}
{\sf Examples of formal definitions}
\end{center}
\begin{raggedright}
\begin{itemize}
\item Let $S\subseteq S'$,\hspace{3ex} $T\subseteq T'$,\hspace{3ex} $r\subseteq S'\times T'$
  \begin{itemize}
  \item $r$ is $S$--$T$ {\em entire\/}
    from $S'$ to $T'$\\
    iff $\forall s\in S\sepdot\exists t\in T\sepdot s\relation{r}t$
  \item $r$ is $S$--$T$ {\em reliable\/} from $S'$ to $T'$\\
     iff $r[S]\subseteq T$
  \item $r:S',S\hookrightarrow T,T'$ {\em (reliable mapping)}\\
     iff $r$ is entire and reliable
  \end{itemize}
\item $\hat{\evidence{P}}(\alpha)=$
  finite subsets of $\hat{\universe{U}}_{\alpha}$\\
  \hspace{7ex}inhabited by member of $\evidence{P}(\alpha)$
\item $\evidence{P}(\alpha\limplies\beta)=
  \hat{\universe{U}}_{\alpha},\hat{\evidence{P}}(\alpha)\hookrightarrow
  \hat{\evidence{P}}(\beta),\hat{\universe{U}}_{\beta}$\\
  (reliable mappings from $\hat{\evidence{P}}(\beta)$ to 
  $\hat{\universe{U}}_{\beta}$)
\item $f_{\alpha\limplies\beta}(r)=
  \setof{\tuple{\hat{f}_{\alpha}(A),\hat{f}_{\beta}(B)}}
  {A\relation{r}B}$
\end{itemize}
\end{raggedright}
\end{slide*}

\begin{slide*}
\begin{center}
\setlength{\unitlength}{0.025cm}
\begin{picture}(260,230)(30,540)
\thicklines
\put( 90,685){\noisecolorone\vector(-4, -1){0}}
\put( 90,698){\noisecolorone\oval( 14, 26)[br]}
\put( 80,698){\noisecolorone\oval( 34, 34)[tr]}
\put( 80,698){\noisecolorone\oval( 34, 34)[tl]}
\put( 70,698){\noisecolorone\oval( 14, 26)[bl]}
\put(250,685){\noisecolortwo\vector(-4, -1){0}}
\put(250,698){\noisecolortwo\oval( 14, 26)[br]}
\put(240,698){\noisecolortwo\oval( 34, 34)[tr]}
\put(240,698){\noisecolortwo\oval( 34, 34)[tl]}
\put(230,698){\noisecolortwo\oval( 14, 26)[bl]}
\put(150,585){\noisecolor\vector( 4, 1){0}}
\put(150,572){\noisecolor\oval( 14, 26)[tl]}
\put(160,572){\noisecolor\oval( 34, 34)[bl]}
\put(160,572){\noisecolor\oval( 34, 34)[br]}
\put(170,572){\noisecolor\oval( 14, 26)[tr]}
\put( 90,665){\noisecolortwo\vector( 1,-1){ 60}}
\put(230,665){\noisecolorone\vector(-1,-1){ 60}}
\put( 80,670){\makebox(0,0)[b]{\ptcolor$a$}}
\put(240,670){\makebox(0,0)[b]{\ptcolor$b$}}
\put( 80,720){\makebox(0,0)[b]{\noisecolorone\noisecolorone$f_1$}}
\put(160,590){\makebox(0,0)[b]{\ptcolor$c$}}
\put(240,720){\makebox(0,0)[b]{\noisecolortwo$f_2$}}
\put(105,630){\makebox(0,0)[r]{\noisecolortwo$f_2$}}
\put(180,630){\makebox(0,0)[r]{\noisecolorone\noisecolorone$f_1$}}
\put(160,545){\makebox(0,0)[t]{${\noisecolorone f_1}{\noisecolor ,}{\noisecolortwo f_2}$}}
\put(190,650){\evcolor\dashbox{5}(100,120){}}
\put( 30,650){\evcolor\dashbox{5}(100,120){}}
\put( 80,745){\makebox(0,0)[b]{\evcolor$\evidence{P}(\alpha)$}}
\put(240,745){\makebox(0,0)[b]{\evcolor$\evidence{P}(\beta)$}}
\end{picture} \\[5ex]
{\sf Relational realizability countermodel for} \\
$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$ \\
{\it erroneous version}
\end{center}
\end{slide*}

\begin{slide*}
\begin{center}
\setlength{\unitlength}{0.02cm}
\begin{picture}(260,230)(30,540)
\thicklines
\put(  0,685){\noisecolorone\vector(-4, -1){0}}
\put(  0,698){\noisecolorone\oval( 14, 26)[br]}
\put(-10,698){\noisecolorone\oval( 34, 34)[tr]}
\put(-10,698){\noisecolorone\oval( 34, 34)[tl]}
\put(-20,698){\noisecolorone\oval( 14, 26)[bl]}
\put( 85,685){\noisecolorone\vector(-4, -1){0}}
\put( 85,698){\noisecolorone\oval( 14, 26)[br]}
\put( 75,698){\noisecolorone\oval( 34, 34)[tr]}
\put( 75,698){\noisecolorone\oval( 34, 34)[tl]}
\put( 65,698){\noisecolorone\oval( 14, 26)[bl]}
\put(170,685){\noisecolorone\vector(-4, -1){0}}
\put(170,698){\noisecolorone\oval( 14, 26)[br]}
\put(160,698){\noisecolorone\oval( 34, 34)[tr]}
\put(160,698){\noisecolorone\oval( 34, 34)[tl]}
\put(150,698){\noisecolorone\oval( 14, 26)[bl]}
\put(255,685){\noisecolorone\vector(-4, -1){0}}
\put(255,698){\noisecolorone\oval( 14, 26)[br]}
\put(245,698){\noisecolorone\oval( 34, 34)[tr]}
\put(245,698){\noisecolorone\oval( 34, 34)[tl]}
\put(235,698){\noisecolorone\oval( 14, 26)[bl]}
\put(340,685){\noisecolorone\vector(-4, -1){0}}
\put(340,698){\noisecolorone\oval( 14, 26)[br]}
\put(330,698){\noisecolorone\oval( 34, 34)[tr]}
\put(330,698){\noisecolorone\oval( 34, 34)[tl]}
\put(320,698){\noisecolorone\oval( 14, 26)[bl]}
\put(  0,570){\noisecolortwo\vector(-4, -1){0}}
\put(  0,583){\noisecolortwo\oval( 14, 26)[br]}
\put(-10,583){\noisecolortwo\oval( 34, 34)[tr]}
\put(-10,583){\noisecolortwo\oval( 34, 34)[tl]}
\put(-20,583){\noisecolortwo\oval( 14, 26)[bl]}
\put( 85,570){\noisecolortwo\vector(-4, -1){0}}
\put( 85,583){\noisecolortwo\oval( 14, 26)[br]}
\put( 75,583){\noisecolortwo\oval( 34, 34)[tr]}
\put( 75,583){\noisecolortwo\oval( 34, 34)[tl]}
\put( 65,583){\noisecolortwo\oval( 14, 26)[bl]}
\put(170,570){\noisecolortwo\vector(-4, -1){0}}
\put(170,583){\noisecolortwo\oval( 14, 26)[br]}
\put(160,583){\noisecolortwo\oval( 34, 34)[tr]}
\put(160,583){\noisecolortwo\oval( 34, 34)[tl]}
\put(150,583){\noisecolortwo\oval( 14, 26)[bl]}
\put(255,570){\noisecolortwo\vector(-4, -1){0}}
\put(255,583){\noisecolortwo\oval( 14, 26)[br]}
\put(245,583){\noisecolortwo\oval( 34, 34)[tr]}
\put(245,583){\noisecolortwo\oval( 34, 34)[tl]}
\put(235,583){\noisecolortwo\oval( 14, 26)[bl]}
\put(340,570){\noisecolortwo\vector(-4, -1){0}}
\put(340,583){\noisecolortwo\oval( 14, 26)[br]}
\put(330,583){\noisecolortwo\oval( 34, 34)[tr]}
\put(330,583){\noisecolortwo\oval( 34, 34)[tl]}
\put(320,583){\noisecolortwo\oval( 14, 26)[bl]}
\put(160,670){\makebox(0,0)[b]{\ptcolor$a_0$}}
\put(160,555){\makebox(0,0)[b]{\ptcolor$b_0$}}
\put(-10,720){\makebox(0,0)[b]{\noisecolorone$f_1$}}
\put( 75,720){\makebox(0,0)[b]{\noisecolorone$f_1$}}
\put(160,720){\makebox(0,0)[b]{\noisecolorone$f_1$}}
\put(245,720){\makebox(0,0)[b]{\noisecolorone$f_1$}}
\put(330,720){\makebox(0,0)[b]{\noisecolorone$f_1$}}
\put(-10,605){\makebox(0,0)[b]{\noisecolortwo$f_2$}}
\put( 75,605){\makebox(0,0)[b]{\noisecolortwo$f_2$}}
\put(160,605){\makebox(0,0)[b]{\noisecolortwo$f_2$}}
\put(245,605){\makebox(0,0)[b]{\noisecolortwo$f_2$}}
\put(330,605){\makebox(0,0)[b]{\noisecolortwo$f_2$}}
\put(110,545){\evcolor\dashbox{5}(100,105){}}
\put(110,660){\evcolor\dashbox{5}(100,105){}}
\put(160,745){\makebox(0,0)[b]{\evcolor$\evidence{P}(\alpha)$}}
\put(160,630){\makebox(0,0)[b]{\evcolor$\evidence{P}(\beta)$}}
\put(175,670){\noisecolortwo\vector(1,0){55}}
\put(200,675){\makebox(0,0)[b]{\noisecolortwo$f_2$}}
\put(245,670){\makebox(0,0)[b]{\ptcolor$a_1$}}
\put(260,670){\noisecolortwo\vector(1,0){55}}
\put(285,675){\makebox(0,0)[b]{\noisecolortwo$f_2$}}
\put(330,670){\makebox(0,0)[b]{\ptcolor$a_2$}}
\put(370,670){\makebox(0,0)[b]{\noisecolortwo$\cdots$}}
\put( 90,670){\noisecolortwo\vector(1,0){55}}
\put(120,675){\makebox(0,0)[b]{\noisecolortwo$f_2$}}
\put( 75,670){\makebox(0,0)[b]{\ptcolor$a_{-1}$}}
\put(  5,670){\noisecolortwo\vector(1,0){55}}
\put( 30,675){\makebox(0,0)[b]{\noisecolortwo$f_2$}}
\put(-10,670){\makebox(0,0)[b]{\ptcolor$a_{-2}$}}
\put(-50,670){\makebox(0,0)[b]{\noisecolortwo$\cdots$}}
\put(175,555){\noisecolorone\vector(1,0){55}}
\put(200,560){\makebox(0,0)[b]{\noisecolorone$f_1$}}
\put(245,555){\makebox(0,0)[b]{\ptcolor$b_1$}}
\put(260,555){\noisecolorone\vector(1,0){55}}
\put(285,560){\makebox(0,0)[b]{\noisecolorone$f_1$}}
\put(330,555){\makebox(0,0)[b]{\ptcolor$b_2$}}
\put(370,555){\makebox(0,0)[b]{\noisecolorone$\cdots$}}
\put( 90,555){\noisecolorone\vector(1,0){55}}
\put(120,560){\makebox(0,0)[b]{\noisecolorone$f_1$}}
\put( 75,555){\makebox(0,0)[b]{\ptcolor$b_{-1}$}}
\put(  5,555){\noisecolorone\vector(1,0){55}}
\put( 30,560){\makebox(0,0)[b]{\noisecolorone$f_1$}}
\put(-10,555){\makebox(0,0)[b]{\ptcolor$b_{-2}$}}
\put(-50,555){\makebox(0,0)[b]{\noisecolorone$\cdots$}}
\end{picture} \\[5ex]
{\sf Relational realizability countermodel for} \\
$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$ \\
{\it correct version}
\end{center}
\end{slide*}

\begin{slide*}
\begin{center}
  {\sf Interpretation of relational countermodel}
\end{center}
\vspace{5ex}
\begin{raggedright}
$\alpha$ has countable pieces of evidence\\
$\beta$ has countable pieces of evidence\\[5ex]
{\noisecolorone\em Jane Doe:}\\
agrees with our names for $\alpha$ evidence,\\
shifts our names for $\beta$ evidence\\
won't accept $\alpha\limplies\beta$\\[5ex]
{\noisecolortwo\em Richard Roe:}\\
agrees with our names for $\beta$ evidence\\
shifts our names for $\alpha$ evidence\\
won't accept $\beta\limplies\alpha$
\end{raggedright}
\end{slide*}

\begin{slide*}
\begin{center}
{\sf Further questions for research}
\end{center}
\begin{raggedright}
\begin{itemize}
\item Extend realizability to higher-order logic\\
  Do we need closer approximation to constructibility?
\item Develop relational analogue of $\lambda$-calculus\\
  Are there advantages to relational proofs?
\item Define modal logics by restrictions on evidence
  (e.g., $\evidence{P}(\invar\alpha)=$ invariants in $\evidence{P}(\alpha)$)
\item Define relevant implications by\\
  restrictions on mappings,\\
  (e.g., permutation orbit isomorphisms)
\item Characterize Kripke models that are natural
  translations of L\"auchli realizability models\\
  This relates to open problems in group/lattice theory
\end{itemize}

\end{raggedright}
\end{slide*}

\end{document}