\begin{frame}{Everybody Votes for At Most One Person} We translate in a few steps. \pause\medskip \begin{block}{\sentence{Jan votes for at most one person}} \pause $\formula{\forallst{x}{\forallst{y}{( \binpred{V}{\const{j}}{x} \logandinf \binpred{V}{\const{j}}{y} \logimpinf \equalto{x}{y} )}}}$ \end{block} \pause\medskip Now a property: \begin{block}{\sentence{$\freevar{z}$ votes for at most one person:}} \pause $\formula{\forallst{x}{\forallst{y}{( \binpred{V}{\freevar{z}}{x} \logandinf \binpred{V}{\freevar{z}}{y} \logimpinf \equalto{x}{y} )}}}$ \end{block} \pause\medskip The sentence `\sentence{Everybody votes for at most one person.}' states that this property is shared by everyone ($\formula{\forall \freevar{z}}$):\pause{} \begin{block}{\sentence{Everybody votes for at most one person:}} \pause $\formula{\forallst{\chocolate{z}}{\forallst{x}{\forallst{y}{( \binpred{V}{\chocolate{z}}{x} \logandinf \binpred{V}{\chocolate{z}}{y} \logimpinf \equalto{x}{y} )}}}}$ \end{block} \end{frame}