Aligning proof rules in tables

Question

I would like to display the following rules in a table:

\documentclass[10pt]{beamer}
% Proofs
\usepackage{bussproofs}

\begin{document}

\begin{frame}{$\mathcal{M}$}
\textbf{Inference rules}
\begin{columns}
\begin{column}{0.5\textwidth}
\begin{prooftree}
\AxiomC{[$\phi$]}
\noLine
\UnaryInfC{$\psi$}
\LeftLabel{$\Rightarrow$-intro}
\UnaryInfC{$\phi \Rightarrow \psi$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$\phi \Rightarrow \psi$}
    \AxiomC{$\phi$}
    \LeftLabel{$\Rightarrow$-elim}
    \BinaryInfC{$\phi \Rightarrow \psi$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$\phi$ \; $x \notin fv(\text{assumps})$}
    \LeftLabel{$\bigwedge$-intro}
    \UnaryInfC{$\bigwedge x. \phi$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$\bigwedge x. \phi$}
    \LeftLabel{$\bigwedge$-elim}
    \UnaryInfC{$\phi[b/x]$}
\end{prooftree}
\end{column}

\begin{column}{0.5\textwidth}
\begin{prooftree}
    \AxiomC{}
    \LeftLabel{Refl}
    \UnaryInfC{$a \equiv a$}
\end{prooftree}
    
\begin{prooftree}
    \AxiomC{$a \equiv b$}
    \LeftLabel{Symmetry}
    \UnaryInfC{$b \equiv a$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$a \equiv b$}
    \AxiomC{$b \equiv c$}
    \LeftLabel{Transitivity}
    \BinaryInfC{$a \equiv c$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$y \notin fv(a)$}
    \LeftLabel{$\alpha$-conversion}
    \UnaryInfC{$(\lambda x. a) \equiv (\lambda y. a[y/x])$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{}
    \LeftLabel{$\beta$-conversion}
    \UnaryInfC{$(\lambda x. a)b \equiv a[b/x]$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$x \notin fv(f)$}
    \LeftLabel{$\eta$-conversion}
    \UnaryInfC{$(\lambda x. f(x)) \equiv f$}
\end{prooftree}

\note{
\begin{itemize}
\item $\eta$-conversion is equivalent to extensionality:

\begin{prooftree}
    \AxiomC{$f(x) \equiv g(x)$}
    \UnaryInfC{$f \equiv g$}
\end{prooftree}

\item It holds when $x \notin fv(f,g, \text{assumps})$.
\end{itemize}

\begin{itemize}
\item The side condition in $\bigwedge$-intro is better understood with a more verbose rule:

\begin{prooftree}
    \AxiomC{$\Gamma \vdash \varphi(y)$}
    \RightLabel{$y \notin fv(\Gamma) \land x \notin fv(\varphi)$}
    \UnaryInfC{$\Gamma \vdash \forall x. \varphi(x)$}
\end{prooftree}

\item Recall that $\bigwedge x. \varphi$ is an abbreviation of $\bigwedge (\lambda x. \varphi)$. So both formulations are equal. 
\end{itemize}
}
\end{column}
\end{columns}
\end{frame}

\end{document}

Right now it looks a bit messy. But I don't know how to insert proof environments into tables!

Answer 1

You can place proof trees in tabular provided you use \DisplayProof rather than the full prooftree environment.

The construction \begin{prooftree}<statements>\end{prooftree} is essentially equivalent to

\[
<statements>
\DisplayProof
\]

Here's the code I propose (I didn't touch the code in the \note).

\documentclass[10pt]{beamer}
% Proofs
\usepackage{bussproofs}
% tables
\usepackage{booktabs}

\begin{document}

\begin{frame}{$\mathcal{M}$}
\textbf{Inference rules}

\medskip

\begin{columns}
\begin{column}[t]{0.5\textwidth}
\centering
\begin{tabular}[t]{@{}l@{}}
\toprule[0pt] % set the anchor
  \AxiomC{[$\phi$]}
  \noLine
  \UnaryInfC{$\psi$}
  \LeftLabel{$\Rightarrow$-intro}
  \UnaryInfC{$\phi \Rightarrow \psi$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$\phi \Rightarrow \psi$}
  \AxiomC{$\phi$}
  \LeftLabel{$\Rightarrow$-elim}
  \BinaryInfC{$\phi \Rightarrow \psi$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$\phi$ \; $x \notin fv(\text{assumps})$}
  \LeftLabel{$\bigwedge$-intro}
  \UnaryInfC{$\bigwedge x. \phi$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$\bigwedge x. \phi$}
  \LeftLabel{$\bigwedge$-elim}
  \UnaryInfC{$\phi[b/x]$}
  \DisplayProof
\end{tabular}
\end{column}

\begin{column}[t]{0.5\textwidth}
\begin{tabular}[t]{@{}l@{}}
\toprule[0pt] % set the anchor
  \AxiomC{}
  \LeftLabel{Refl}
  \UnaryInfC{$a \equiv a$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$a \equiv b$}
  \LeftLabel{Symmetry}
  \UnaryInfC{$b \equiv a$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$a \equiv b$}
  \AxiomC{$b \equiv c$}
  \LeftLabel{Transitivity}
  \BinaryInfC{$a \equiv c$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$y \notin fv(a)$}
  \LeftLabel{$\alpha$-conversion}
  \UnaryInfC{$(\lambda x. a) \equiv (\lambda y. a[y/x])$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{\vphantom{X}}
  \LeftLabel{$\beta$-conversion}
  \UnaryInfC{$(\lambda x. a)b \equiv a[b/x]$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$x \notin fv(f)$}
  \LeftLabel{$\eta$-conversion}
  \UnaryInfC{$(\lambda x. f(x)) \equiv f$}
  \DisplayProof
\end{tabular}

\note{
\begin{itemize}
\item $\eta$-conversion is equivalent to extensionality:

\begin{prooftree}
    \AxiomC{$f(x) \equiv g(x)$}
    \UnaryInfC{$f \equiv g$}
\end{prooftree}

\item It holds when $x \notin fv(f,g, \text{assumps})$.
\end{itemize}

\begin{itemize}
\item The side condition in $\bigwedge$-intro is better understood with a more verbose rule:

\begin{prooftree}
    \AxiomC{$\Gamma \vdash \varphi(y)$}
    \RightLabel{$y \notin fv(\Gamma) \land x \notin fv(\varphi)$}
    \UnaryInfC{$\Gamma \vdash \forall x. \varphi(x)$}
\end{prooftree}

\item Recall that $\bigwedge x. \varphi$ is an abbreviation of $\bigwedge (\lambda x. \varphi)$. So both formulations are equal. 
\end{itemize}
}
\end{column}
\end{columns}
\end{frame}

\end{document}

Answer 2

Structure the contents of a frame into blocks. Add e.g. the following definitions to your preamble.

\setbeamercolor{block title}{use=structure,fg=structure.fg,bg=structure.fg!30!bg}
\setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!60!bg}
\setbeamertemplate{blocks}[rounded][shadow]
\setbeamertemplate{navigation symbols}{} % removes the navigation symbols that nobody uses

Use the block environment as follows:

\begin{block}{Headline of block, may be empty}
  Part of the contents of the frame
\end{block}

Moreover, as described in section 2.1 of the documentation of bussproofs, you can use \DisplayProof (or \DP, if you activate the shortcuts) to typeset the proof, as an alternative to the prooftree environment. The advantage is that the proof resulting from \Displayproof can also be put into a tabular.

\documentclass[10pt]{beamer}
\setbeamercolor{block title}{use=structure,fg=structure.fg,bg=structure.fg!30!bg}
\setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!60!bg}
\setbeamertemplate{blocks}[rounded][shadow]
\setbeamertemplate{navigation symbols}{}
%Proofs
\usepackage{bussproofs}

\begin{document}

\begin{frame}{$\mathcal{M}$~-- Inference rules}
\begin{columns}
  \begin{column}{0.45\textwidth}
    \begin{block}{Implication}
      \begin{tabular}{@{}lc@{}}
        $\Rightarrow$-intro
      & \AxiomC{[$\phi$]} \noLine \UnaryInfC{$\psi$}
        \LeftLabel{}
        \UnaryInfC{$\phi \Rightarrow \psi$}
        \DisplayProof
      \\[5ex]
        $\Rightarrow$-elim
      & \AxiomC{$\phi \Rightarrow \psi$} \AxiomC{$\phi$}
        \LeftLabel{}
        \BinaryInfC{$\phi \Rightarrow \psi$}
        \DisplayProof           
      \end{tabular}
    \end{block}

    \begin{block}{Quantification}
      \begin{tabular}{@{}lc@{}}
        $\bigwedge$-intro
      & \AxiomC{$\phi$ \; $x \notin fv(\text{assumps})$}
        \UnaryInfC{$\bigwedge x. \phi$}
        \DisplayProof                    
      \\[5ex]
        $\bigwedge$-elim
      & \AxiomC{$\bigwedge x. \phi$}
        \UnaryInfC{$\phi[b/x]$}
        \DisplayProof                    
      \end{tabular}
    \end{block}
\end{column}

\begin{column}{0.54\textwidth}
  \begin{block}{Equivalence}
    \begin{tabular}{@{}lc@{}}
      reflexivity
    & \AxiomC{}
      \UnaryInfC{$a \equiv a$}
      \DisplayProof
    \\[3ex]
      symmetry
    & \AxiomC{$a \equiv b$}
      \UnaryInfC{$b \equiv a$}
      \DisplayProof
    \\[3ex]
      transitivity
    & \AxiomC{$a \equiv b$}
      \AxiomC{$b \equiv c$}
      \BinaryInfC{$a \equiv c$}
      \DisplayProof
    \end{tabular}
  \end{block}
  \begin{block}{$\lambda$ rules}
    \begin{tabular}{@{}lc@{}}
      $\alpha$-conversion
    & \AxiomC{$y \notin fv(a)$}
      \UnaryInfC{$(\lambda x. a) \equiv (\lambda y. a[y/x])$}
      \DisplayProof
    \\[4ex]
      $\beta$-conversion
    & \AxiomC{}
      \UnaryInfC{$(\lambda x. a)b \equiv a[b/x]$}
      \DisplayProof
    \\[3ex]
      $\eta$-conversion
    & \AxiomC{$x \notin fv(f)$}
      \UnaryInfC{$(\lambda x. f(x)) \equiv f$}
      \DisplayProof
    \end{tabular}
  \end{block}
  \note{
    \begin{itemize}
    \item $\eta$-conversion is equivalent to extensionality:

      \begin{prooftree}
        \AxiomC{$f(x) \equiv g(x)$} \UnaryInfC{$f \equiv g$}
      \end{prooftree}

    \item It holds when $x \notin fv(f,g, \text{assumps})$.
    \end{itemize}

    \begin{itemize}
    \item The side condition in $\bigwedge$-intro is better understood
      with a more verbose rule:

      \begin{prooftree}
        \AxiomC{$\Gamma \vdash \varphi(y)$}
        \RightLabel{$y \notin fv(\Gamma) \land x \notin fv(\varphi)$}
        \UnaryInfC{$\Gamma \vdash \forall x. \varphi(x)$}
      \end{prooftree}

    \item Recall that $\bigwedge x. \varphi$ is an abbreviation of
      $\bigwedge (\lambda x. \varphi)$. So both formulations are
      equal.
    \end{itemize}
  }
\end{column}
\end{columns}
\end{frame}

\end{document}