\documentclass[t]{beamer}
\usepackage{pgf,amssymb}

\iftrue

\useinnertheme{rounded}

\definecolor{grayblue}{rgb}{.92,.92,.94}
%\definecolor{grayblue}{rgb}{1,1,1}
\definecolor{grayred}{rgb}{1,.9,.9}
%\definecolor{grayred}{rgb}{1,1,1}

\setbeamercolor{palette primary}{use=structure,fg=black,bg=grayblue}
\setbeamercolor*{titlelike}{parent=palette primary}

\let\realtitlepage=\titlepage
\let\realframe=\frame
\let\realframetitle=\frametitle
\let\realinsertframenumber=\insertframenumber
\let\realauthor=\author
\let\realitemize=\itemize
\def\othertitlepage{\vbox to 0pt{\vspace{5.05em}\realtitlepage\vss}}
\def\titlepage{\addtocounter{framenumber}{-1}\subpdfbookmark{\inserttitle}{Title}\global\let\titlepage=\othertitlepage\titlepage}
\def\otherframe{\global\def\itemize{\vspace{-.2em}\realitemize\parskip=.4em\itemsep=.7em}\global\def\frametitle##1{\belowpdfbookmark{\theframenumber. \ifx\linktitle\nolinktitle ##1\else\linktitle\fi}{Frame\theframenumber}\global\let\frametitle=\realframetitle\frametitle{##1}}\realframe}
\def\bookmarksoff{\let\frame=\realframe\let\insertframenumber=\relax}
\def\bookmarkson{\let\frame=\otherframe\let\insertframenumber=\realinsertframenumber}
\bookmarksoff

\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{items}{{\footnotesize $\gray{\blacktriangleright}$}}
\setbeamertemplate{frametitle}[default][center]
\setbeamerfont{frametitle}{size=\normalsize}
%\setbeamercolor{block body}{bg=blue!16.9}
\setbeamercolor{block body}{bg=grayred}
\AtBeginSection[]{\global\parskip=.8em\bookmarksoff\addtocounter{framenumber}{-1}\setbeamercolor{frametitle}{bg=grayred}\begin{frame}{\hfill\normalsize\textcolor{black!35}{\uppercase\expandafter{\romannumeral\thesection}}}\vspace{2.7em}\begin{block}{}\vspace{5pt}\centerline{{\scriptsize\strut}\textcolor[rgb]{.75,0,0}{\insertsectionhead}}\vspace{5.2pt}\end{block}\end{frame}\color{black}\setbeamercolor{frametitle}{bg=grayblue}\bookmarkson}
\let\Tiny=\tiny

\makeatletter
\def\author#1{\let\KV@Hyp@pdfauthor=\relax\realauthor{#1}}
\newdimen\leftmargin
\newdimen\rightmargin
\setlength{\leftmargin}{\beamer@leftmargin}
\setlength{\rightmargin}{\beamer@rightmargin}
\setbeamertemplate{frametitle}{\nointerlineskip
\@tempdima=\textwidth \advance\@tempdima by\beamer@leftmargin\advance\@tempdima by\beamer@rightmargin
\begin{beamercolorbox}[wd=\@tempdima]{frametitle}\vbox to 3.5em{\vbox to 0pt{\vskip .25em
\strut\hfill\llap{\footnotesize\textcolor{black!35}{\insertframenumber}}\hskip .55em\strut\par\vss}\vss
\strut\hskip 2.6em\blue{\insertframetitle}\hfill\hskip 2.6em\strut\par\vskip .2em\vss}%
\end{beamercolorbox}\vspace{.1em}}
\makeatother

\fi

\def\datetimeevent#1#2#3{\date{\vspace{.5em}\par#1$\,$, #2\\\vspace{.5em}{\footnotesize{#3}}}}

\def\toolong{$\hspace{-100cm}$}

\def\red{\textcolor[rgb]{1,0,0}}
\def\green{\textcolor[rgb]{0,.5,0}}
\def\blue{\textcolor[rgb]{0,0,.7}}
\def\gray{\textcolor[rgb]{.5,.5,.5}}
\def\darkgray{\textcolor[rgb]{.4,.4,.4}}
\def\lightgray{\textcolor[rgb]{.8,.8,.8}}
\def\black{\textcolor[rgb]{0,0,0}}
\def\white{\textcolor[rgb]{1,1,1}}

\begin{document}

\title{Pollack-inconsistency}
\author{\only<2>{\red}{Freek} Wiedijk}
\institute{Radboud University Nijmegen}
\datetimeevent{2010 07 15}{12$\,$:$\,$00}{\scriptsize{UITP} 2010}

\begin{frame}
\titlepage
\end{frame}

\section{when can one trust a proof assistant?}

\pgfdeclareimage[height=27em]{believing}{pics/believing}

\begin{frame}
\frametitle{Randy Pollack and how to believe a machine-checked proof}
\vbox to 0pt{%
\vspace{-4.5em}
\hbox to 0pt{\hspace{1.5em}\hspace{-\leftmargin}\lightgray{{\black{\pgfuseimage{believing}}}}\hss}%
\vss
}%
\pause
\vbox to 0pt{%
\vss
\hbox to 0pt{\hss\pgfimage[width=16em]{pics/randy}\hspace{-\textwidth}\hspace{-\rightmargin}}%
\vspace{-19em}%
}

\end{frame}

\begin{frame}
\frametitle{formal proof versus correctness}

\green{the computer has checked a formalization without finding errors} \\
\pause
is it now \red{certain} that there are no errors?
\pause

\global\tracingmacros=1
\begin{itemize}
\item
\global\tracingmacros=0
\textbf{philosophical issues}

`certainty without any doubt is impossible'
\pause

\item
\textbf{software issues}

`all programs have bugs'
\pause

\item
\textbf{the real problem}

\green{certain} that the \green{proofs} are correct \\
\green{\textbf{not} certain} that the \red{definitions} are `correct'

\end{itemize}

\end{frame}

\begin{frame}
\frametitle{the de Bruijn criterion}
\vspace{-.8em}
\begin{center}
\begingroup
\footnotesize
\setlength{\unitlength}{1.75pt}
\def\arraystretch{1}
\begin{picture}(102.5,110)(0,-7.5)
\only<6>{\put(0,65){\color{red!15}{\rule{55\unitlength}{35\unitlength}}}}
\only<5->{\thicklines}
\only<3->{\put(0,0){\only<5->{\lightgray}{\framebox(102.5,100){}}}}
\thinlines
\only<1-2>{\put(0,0){\framebox(102.5,50){proof assistant}}}
\only<3->{\put(0,0){\makebox(102.5,50){\only<3-4>{proof assistant}}}}
\only<5->{\put(102.5,-2){\makebox(0,0)[rt]{\strut\emph{proof assistant}}}}
\only<2->{\put(5,70){\framebox(45,25){\begin{tabular}{c}\only<2-3>{independent\\proof \emph{checker}}\only<4->{proof checking\\\emph{kernel}}\end{tabular}}}}
\only<5->{\put(5,5){\framebox(92.5,45){\begin{tabular}{c}\emph{remainder of the system:} \\ {theorem database}, {basic reasoning}, \\ {rewriting}, {back-chaining}, \\ {proof search}, {decision procedures}, \\ {etc.}\end{tabular}}}}
\only<5->{\put(27.5,50){\vector(0,1){20}}
\put(27.5,70){\vector(0,-1){20}}}
\only<2>{\put(27.5,50){\vector(0,1){20}}
\put(30,60){\makebox(0,0)[l]{\strut\emph{proof object}}}}
\end{picture}
\endgroup
\end{center}

\end{frame}

\section{a student's remark}

\begin{frame}
\frametitle{a proof assistant for propositional logic}
course \textbf{proof assistants} at Radboud University Nijmegen
\pause

\begin{itemize}
\item
\green{implement small proof assistant}

LCF-style proof assistant \\
minimal propositional logic (= only implication)

$$\gray{\only<-2>{\hspace{-.5em}\frac{\strut}{\Gamma \cup \{A\} \vdash A}\quad\frac{\Gamma \cup \{A\} \vdash B}{\Gamma \vdash A \to B}\quad\frac{\Gamma \vdash A \to B\quad \Gamma \vdash A}{\Gamma \vdash B}}
\only<3->{\hspace{-1em}\frac{\strut}{\{A\} \vdash A}\quad\frac{\Gamma \vdash B}{\Gamma - \{A\} \vdash A \to B}\quad\frac{\Gamma \vdash A \to B\quad \Delta \vdash A}{\Gamma \cup \Delta \vdash B}\hspace{-1em}}}$$

\end{itemize}
\pause
\pause

student \textbf{Marc Schoolderman}:

\begin{itemize}
\item
\green{let's add the other propositional connectives} \pause\dots \\
\textsl{\dots\ in the parser and pretty-printer!}
\pause

\red{parser and pretty-printer have to know about logic}

\end{itemize}

\end{frame}

\section{the digits of hundred factorial}

\begin{frame}[fragile]
\frametitle{the kernel of HOL Light}
\green{proof assistant that best satisfies the de Bruijn criterion:}

\red{HOL Light}, John Harrison, 1998--\emph{today}
\pause

\green{proof checking kernel} = \red{\texttt{fusion.ml}}

671 lines $\approx$ 10 printed pages $\approx$ $0.2\,\%$ of the system \\
only 395 lines of actual code
\medskip
\pause

\blue{self-verification of HOL Light}: John Harrison, 2006\pause

\vspace{-.8em}
\begin{semiverbatim}\footnotesize
\gray{\only<4>{let rec type_of tm =}\only<5>{let typeof = define}
\only<4>{  match tm with}\only<5>{ `(typeof (Var n ty) = ty) /\\}
\only<4>{    Var(_,ty) -> ty}\only<5>{  (typeof (Equal ty) = Fun ty (Fun ty Bool)) /\\}
\only<4>{  | Const(_,ty) -> ty}\only<5>{  (typeof (Select ty) = Fun (Fun ty Bool) ty) /\\}
\only<4>{  | Comb(s,_) -> hd(tl(snd(dest_type(type_of s))))}\only<5>{  (typeof (Comb s t) = codomain (typeof s)) /\\}
\only<4>{  | Abs(Var(_,ty),t) -> Tyapp("fun",[ty;type_of t])}\only<5>{  (typeof (Abs n ty t) = Fun ty (typeof t))`;;}}
\end{semiverbatim}

\end{frame}

\begin{frame}[fragile]
\frametitle{numerical calculations in HOL Light}
\vspace{-.8em}
\begin{semiverbatim}\footnotesize
\green{# \pause\black{\only<8>{\red}{`{1 + 1}`};;}\pause
val it : term = `1 + 1`
# \pause\black{NUM_REDUCE_CONV it;;}
val it : thm = |- {1 + 1 = 2}
# \pause\black{rhs (concl it);;}
val it : term = \only<-6,8>{\red}{`2`}
# \pause\black{#remove_printer print_qterm;;}
# \black{it;;}
val it : term =
  \only<-7>{\red}{Comb (Const ("NUMERAL", `:num->num`),
   Comb (Const ("BIT0", `:num->num`),
    Comb (Const ("BIT1", `:num->num`), Const ("_0", `:num`))))}
# \pause\black{#install_printer print_qterm;;}
# \black{\only<7>{\red}{`NUMERAL (BIT0 (BIT1 _0))`};;}
val it : term = \only<7>{\red}{`2`}
\uncover<7>{# }\pause\vspace{-.4em}
# \black{rhs (concl (NUM_REDUCE_CONV \red{`FACT 100`}))};;
val it : term =
  \red{`93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000`}\toolong
# }
\end{semiverbatim}
\vspace{-.5em}

\end{frame}

\section{Pollack-inconsistency}

\begin{frame}<2->
\frametitle{the structure of a proof assistant}
\vspace{-1em}
\begin{center}
\begingroup
\footnotesize
\setlength{\unitlength}{1.75pt}
\def\arraystretch{1}
\begin{picture}(145,122.5)(0,-7.5)
\only<2-5>{\put(0,55){\color{red!15}{\rule{35\unitlength}{45\unitlength}}}}
\only<6->{\put(0,55){\color{red!15}{\rule{90\unitlength}{45\unitlength}}}}
\thicklines
\put(0,0){\lightgray{\framebox(102.5,100){}}}%
\only<3->{\put(40,50){\lightgray{\framebox(100,57.5){}}}%
\put(140,108.5){\makebox(0,0)[rb]{\strut\emph{interface}}}}
\only<3->{\put(95,23.75){\lightgray{\vector(0,1){26.25}}}
\put(95,23.75){\lightgray{\vector(-1,0){7.5}}}}
\only<3>{\put(30,77.5){\lightgray{\vector(1,0){10}}}
\put(40,77.5){\lightgray{\vector(-1,0){10}}}}
\thinlines
\put(102.5,-2){\makebox(0,0)[rt]{\strut\emph{proof assistant}}}
{\put(5,62.5){\framebox(25,30){\begin{tabular}{c}{proof}\\{checking}\\\emph{kernel}\end{tabular}}}
\put(5,5){\framebox(82.5,37.5){\begin{tabular}{c}\emph{remainder of the system:} \\ {theorem database}, {basic reasoning}, \\ {rewriting}, {back-chaining}, \\ {proof search}, {decision procedures}, \\ {etc.}\end{tabular}}}
\put(17.5,42.5){\vector(0,1){20}}
\put(17.5,62.5){\vector(0,-1){20}}}
\only<4->{\put(45,80){{\framebox(40,15){\strut{{\only<5->{formula }parser}}}}}
\put(45,60){{\framebox(40,15){\strut{{\only<5->{formula }printer}}}}}
\put(110,80){\framebox(25,15){\strut {editor}}}
\put(45,87.5){\vector(-1,0){15}}
\put(145,87.5){\vector(-1,0){10}}
\put(110,87.5){\vector(-1,0){25}}
\put(30,67.5){\vector(1,0){15}}
\put(85,67.5){\vector(1,0){60}}}
\end{picture}
\endgroup
\end{center}

\end{frame}

\begin{frame}
\frametitle{is parsing the left inverse of pretty-printing?}
formula parser and pretty-printer:
\begin{eqnarray*}
\red{{\sf parse}_{\sf f}} &:& {\sf string} \to {\sf formula} \\
\red{{\sf print}_{\sf f}} &:& {\sf formula} \to {\sf string}
\end{eqnarray*}
\pause
generally $\red{{\sf print}_{\sf f}}$ is total while $\red{{\sf parse}_{\sf f}}$ is not
\bigskip
\pause

\strut\rlap{`\blue{well-behaved}':}\hfill$\green{{\sf parse}_{\sf f}({\sf print}_{\sf f}(\phi)) = \phi}$\hfill\strut
\pause

in practice well-behavedness occasionally breaks
\pause

$$\green{{\sf print}_{\sf f}({\sf parse}_{\sf f}(s)) \ne s}$$
$$\hspace{-1em}\gray{{\sf parse}_{\sf f}(\mbox{\tt "1 + 1 = 2"}) = {\sf parse}_{\sf f}(\mbox{\tt "1+1=2"}) = {\sf parse}_{\sf f}(\mbox{\tt "(1 + 1) = 2"})}\hspace{-1em}$$

\end{frame}

\begin{frame}
\frametitle{Pollack-axioms and Pollack-inconsistency}
\red{Pollack-inconsistency:}

\strut\hfill`\green{$\bot$ is provable from Pollack-axioms}'\hfill\strut
\pause

\red{Pollack-axioms:}
$$
\begin{array}{ccc}
\mbox{`$\green{\phi_1 \Leftrightarrow \phi_2}$'} &\mbox{when}& {{\sf print}_{\sf f}(\phi_1) = {\sf print}_{\sf f}(\phi_2)} \\
\pause
\mbox{`$\green{t_1 = t_2}$'} &\mbox{when}& {{\sf print}_{\sf t}(t_1) = {\sf print}_{\sf t}(t_2)}
\pause
\end{array}
$$

\begin{itemize}
\item
default printer with default settings

\item
default equality

\gray{Coq: `Leibniz equality'}

\item
only $t_1$ and $t_2$ for which $t_1 = t_2$ is well-typed

\end{itemize}

\end{frame}

\begin{frame}
\frametitle{weak versus strong Pollack-inconsistency}
\red{strong} Pollack-inconsistency = \\
\hfill\green{\dots\ without adding definitions}\hspace{3em}\strut

\red{weak} Pollack-inconsistency = \\
\hfill\green{\dots\ extra definitions allowed}\hspace{3em}\strut
\bigskip

\begin{itemize}
\item
\dots\ on top of the standard library of the system

\item
only \textbf{conservative} definitions

{same provable formulas not involving the new definition}

\item
notations considered a form of definition

\gray{Coq: coercions}

\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Pollack-super-inconsistency}
Pollack-\red{super}-inconsistency =
\begin{eqnarray*}
\green{\mbox{$\phi$ is provable}} &\mbox{with}& \green{{\sf print}_{\sf f}(\phi) = {\sf print}_{\sf f}(\red{\bot})}
\end{eqnarray*}
where
$$\red{\bot} =
\lightgray{\left\{\gray{\begin{array}{ll}
\red{\tt F} & \mbox{HOL} \\
\red{\tt False} & \mbox{Isabelle} \\
\red{\tt False} & \mbox{Coq} \\
\red{\tt contradiction} & \mbox{Mizar}
\end{array}}\right\}}
\medskip
\pause
$$

not only does the system appear inconsistent \\
\green{it even looks like one has proved a trivial \red{false} in the system}

\end{frame}

\section{some of the best proof assistants are Pollack-inconsistent}

\begin{frame}[fragile]
\def\linktitle{HOL Light (and Isabelle)}
\frametitle{HOL Light\only<2->{ (and Isabelle)}}
\vspace{-.8em}
\begin{semiverbatim}\footnotesize
\green{# \pause\pause\black{\only<.(1)-.(3)>{\red}{`?!x:1. T`};;}\pause
val it : term = `?!x. T`
# \pause\black{\only<.(1)>{\red}{`?!x:bool. T`};;}
val it : term = `?!x. T`
\only<.(1)>{# }\pause\vspace{-.4em}
# \black{\only<.(1)-.(3)>{\red}{mk_eq(mk_var("0",`:1`),mk_var("1",`:1`))};;}\pause
val it : term = `0 = 1`
# \pause\black{prove(it, ONCE_REWRITE_TAC[one] THEN REFL_TAC);;}
val it : thm = \only<.(1),11>{\red}{|- 0 = 1}
\only<.(1)>{# }\pause\vspace{-.4em}
# \black{override_interface("F",\only<.(1)>{\red}{`T`});;}
val it : unit = ()
# \pause\black{\only<.(1)>{\red}{mk_const("F",[])};;}
val it : term = `F`
# \black{\only<.(1)>{\red}{`T`};;}
val it : term = `F`
# \pause\black{prove(`F`, ACCEPT_TAC TRUTH);;}
val it : thm = \red{|- F}
# }
\end{semiverbatim}

\end{frame}

\begin{frame}[fragile]
\frametitle{Coq}
\vspace{-.8em}
\begin{semiverbatim}\footnotesize
\green{Coq < \pause\black{\only<5>{\red}{Coercion S : nat >-> nat.}}
S is now a coercion\medskip
Coq < \pause\black{Check 0.}
\only<3-4>{\red}{0}
     : nat\medskip
Coq < \pause\black{Check 1.}
\only<4>{\red}{0}
     : nat\medskip
Coq < \pause\black{Definition _Prop := Prop.}
_Prop is defined\medskip
Coq < \black{Definition _not : _Prop -> Prop := not.}
_not is defined\medskip
Coq < \black{\only<.(1)>{\red}{Coercion _not : _Prop >-> Sortclass.}}
_not is now a coercion\medskip
Coq < }
\end{semiverbatim}

\end{frame}

\begin{frame}[fragile]
\frametitle{Coq (continued)}
\vspace{-.8em}
\begin{semiverbatim}\footnotesize
\green{\gray{Coq < Coercion _not : _Prop >-> Sortclass.
_not is now a coercion}\medskip
Coq < \black{Lemma _I : \only<1>{\red}{_not False}.}
1 subgoal\medskip
  ============================
   \only<1>{\red}{False}\medskip
_I < \pause\black{exact (fun x => x).}
Proof completed.\medskip
_I < \black{Qed.}
exact (fun x => x).\medskip
_I is defined\medskip
Coq < \pause\black{Check _I.}
_I
     : \red{False}\medskip
Coq < }
\end{semiverbatim}
\vspace{-1em}

\end{frame}

\pgfdeclareimage[height=22em]{mizar}{pics/mizar}

\begin{frame}[fragile]
\frametitle{Mizar}
\vspace{-.8em}
\begin{semiverbatim}\footnotesize
{definition let \only<2>{\red}{x be real number};
  func \only<2>{\red}{[x] equals 1}; coherence;
end;\medskip
definition let \only<3>{\red}{x be natural number};
  func \only<3>{\red}{[x] equals 0}; coherence;
end;\medskip
theorem \only<4,7>{\red}{[0] <> [0 qua real number]};}
\end{semiverbatim}

\vbox to 0pt{
\vspace{3em}
\def\shiftbf#1{\strut\rlap{#1}\hspace{.3pt}#1}
\begin{semiverbatim}\footnotesize
\uncover<6->{\shiftbf{theorem} \textsl{:: POLLACK:1}
  \blue{\only<7>{\red}{[0 ] <> [0 ]}} ;}
\end{semiverbatim}
\vspace{-3.8em}
\uncover<6->{\begin{picture}(0,0)\put(105,0){\gray{\vector(1,0){70}}}\end{picture}}
\vspace{-16.2em}

\hbox to 0pt{\hspace{16em}\only<5->{\pgfuseimage{mizar}}\hss}
\vss
}

\end{frame}

\section{Pollack-consistency on the cheap}

\begin{frame}
\frametitle{checking the pretty-printer at runtime}
`hack' for making it easier to \blue{prove} Pollack-consistency\pause

\begin{itemize}
\item
\red{${\sf print}_{\sf normal}$}

good, complicated

\item
\red{${\sf print}_{\sf failsafe}$}

failsafe, trivial

\end{itemize}
\medskip
\pause

combine into \red{${\sf print}_{\sf combined}$}:
\vbox to -1.5em{\footnotesize
\vspace{-14.6em}
\hspace{20em}%
\begin{picture}(110,150)
\put(40,157.5){\vector(0,-1){17.5}}
\put(0,120){\framebox(80,20){$s := \red{{\sf print}_{\sf normal}}(\phi)$}}
\put(40,120){\vector(0,-1){17.5}}
\put(0,80){\makebox(80,20){\green{${\sf parse}(s) = \phi$}?}}
\put(-10,90){\line(4,1){50}}
\put(90,90){\line(-4,1){50}}
\put(-10,90){\line(4,-1){50}}
\put(90,90){\line(-4,-1){50}}
\put(100,92){\makebox(0,0)[b]{\strut\emph{no}}}
\put(90,90){\line(1,0){10}}
\put(100,90){\vector(0,-1){22.5}}
\put(-20,92){\makebox(0,0)[b]{\strut\emph{yes}}}
\put(-10,90){\line(-1,0){10}}
\put(-20,90){\vector(0,-1){22.5}}
\put(-42.5,47.5){\framebox(45,20){\darkgray{\textbf{return}} $s$}}
\put(55,47.5){\framebox(90,20){\darkgray{\textbf{return}} $\red{{\sf print}_{\sf failsafe}}(\phi)$}}
\end{picture}
\vss}
\vspace{-2em}
\pause

$$\green{\begin{array}{c}
{\sf parse}({\sf print}_{\sf failsafe}(\phi)) = \phi \\
\Downarrow \\
{\sf parse}({\sf print}_{\sf combined}(\phi)) = \phi 
\end{array}}$$

\end{frame}

\section{does Pollack-inconsistency matter?}

\begin{frame}[fragile]
\frametitle{the attitude of the proof assistants community}
\textbf{computer algebra users}

\textsl{a little inconsistency does not matter much \dots}
\vspace{.5em}
\pause

{\footnotesize\green{\texttt{> \only<2>{1/(1-x) = simplify(1/(1-x))}\only<3->{int(1/(1-x),x) = int(simplify(1/(1-x)),x)}}
$$\only<2>{\frac{1}{1-x} = -\frac{1}{-1 + x}}\only<3->{\phantom{\rlap{$\displaystyle\frac{1}{1}$}}-\ln(1 - x) = -\ln(-1 + x)}$$
\texttt{\pause\pause> evalf(subs(x=-1, \%));}
$$-0.6931471806 = -0.6931471806 - 3.141592654 i$$}}
\vspace{-1.5em}
\pause

\textbf{proof assistant users}
\only<.(3)>{\\\gray{apart from principled people like Randy Pollack and Mark Adams}}

\textsl{consistency is very important!\\\pause
a little \red{Pollack}-inconsistency does not matter much \dots}


\end{frame}

\end{document}