\begin{frame}[t]{Precisely One}
  There are different possibilities to express: \sentence{precisely one}.
  \pause\medskip
 
  \begin{block}{}
    Each of the following sentences expresses that 
    \begin{scenter}
      \sentence{There is precisely one $P$-value.}      
    \end{scenter}
    \pause\medskip
    
    \sentence{There is at least one, and at most one $P$-value:}
    \pause
    \begin{talign}
      \formula{\existsst{x}{\,
        \unpred{\mediumblue{P}}{x} 
        \logandinf \forallst{x}{\forallst{y}{
          (\unpred{\mediumblue{P}}{x} \logandinf \unpred{\mediumblue{P}}{y} \logimpinf \equalto{x}{y})
        }}
      }}     
    \end{talign}
    \pause
    \sentence{(Equivalently: there is a $P$-value, and all $P$-values are equal)}
    \pause\bigskip
    
    \sentence{There is a $P$-value $x$, and all $P$-values are equal to $x$:}
    \pause
    \begin{talign}
      \formula{\existsst{x}{(\,
        \unpred{\mediumblue{P}}{x} 
        \logandinf \forallst{y}{( \unpred{\mediumblue{P}}{y} \logimpinf \equalto{x}{y} )} 
      )}}
    \end{talign}
    \pause
    \sentence{There is a value $x$ such that} \\
    \quad\sentence{an arbitrary value is a $P$-value if and only if it is $x$:}
    \pause
    \begin{talign}
      \formula{\existsst{x}{\forallst{y}{(\unpred{\mediumblue{P}}{y} \logbiimpinf \equalto{x}{y})}}}
    \end{talign} 
  \end{block}
\end{frame}

\theme{Translation into Predicate Logic with Equality}