Multi-column spacing of many equation-like environments

Question

I suppose I have a pretty simple question. I want to write down a logic inference system. A good example can be found on page 9 in this document:

What environment would you advise me to use to get a similar effect? In particular I would like to get nice multicolumn alignment (like in a table) and some standard spacing around every element. I don't care particularly about the border around the whole thing.

I tried using tabular however it produces too little spacing. This probably could be fixed, but feels like a hack.

EDIT: I think I might have been misunderstood. I don not ask how to write down inference rules themselves. I already know how to do it and I use bussproofs package for that. What I need is a way to put all those rules that I have in one table with nice spacing in it. Therefore I ask about an environment that would be suitable for something like that.

EDIT(2): Ok, If someone thinks that tabular is the right approach, could you please tell me how to add some padding (margin) to all of the cells - both horizontal and vertical. I realize this might be a trivial question, however I have just spent half an hour looking for an answer.

Answer 1

Skipping over minor details, this may be accomplished with a tabular:

\usepackage{array}
\newcolumntype{C}{>{$\displaystyle}c<{$}}
\newcommand{\onecol}[1]{\multicolumn{2}{C}{#1}}

The above code should go in the preamble. Then the big thing can be set by

\begin{figure}
\centering
\renewcommand{\arraystretch}{2} % adjust here for interrow spacing
\begin{tabular}{CC}
\onecol{Formula for first line} \\
\onecol{Formula for second line} \\
\onecol{Formula for third line} \\
Left formula & right formula (row 4)\\
Left formula & right formula (row 5)\\
...
\end{tabular}
\caption{Sequent calculus formulation}\label{fig:seqcalc}
\end{figure}

Instead of setting \arraystretch you can define

\newcommand\mystrut{\vrule width 0pt height 24pt depth 24pt}

and insert \mystrut in a cell in each row but the first and the last. Adjust the dimensions to suit.

Answer 2

It actually seems to me that you should use some of the amsmath environments : gather, aligned, and gathered. I am typing from my phone right now so an example is difficult (I will update later) but you probably want something like this :

\begin{gather*}
  \begin{aligned}
   \begin{gathered} Left formula \\ Left formula … \end{gathered} &&
   \begin{gathered} Right formula \\ Right formula … \end{gathered}
  \end{aligned}
  \\
  \begin{gathered}
   Formula \\
   Formula \\
   …
  \end{gathered}
  …
\end{gather*}

When you want a two-column set of formulas (with.each column centered) use an aligned with a gathered for each column. For a single column just use gathered. Put the whole thing in a gather so that the sets are collectively centered and you should get what the example shows.

Answer 3

Here's a minor mock-up using @egreg's tabular and @percusse's \frac suggestion:

\documentclass{article}
\usepackage{amsmath}% http://ctan.org/pkg/amsmath
\usepackage{array}% http://ctan.org/pkg/array
\usepackage{MnSymbol}% http://ctan.org/pkg/mnsymbol
\newcolumntype{C}{>{$\displaystyle}c<{$}}
\newcommand{\onecol}[1]{\multicolumn{2}{C}{#1}}
\newcommand{\seq}[2]{\frac{\strut#1}{\strut#2}}
\begin{document}
\begin{figure}[ht]
  \centering
  \renewcommand{\arraystretch}{2.5} % adjust here for interrow spacing
  \begin{tabular}{C@{\quad}C}
    \onecol{\seq{}{A \vdash A}\ \textit{Identity}} \\
    \onecol{\seq{\Gamma,A,B,\Delta \vdash C}{\Gamma,B,A,\Delta \vdash C}\ \textit{Exchange}} \\
    \onecol{\seq{\Gamma \vdash B \qquad B,\Delta \vdash C}{\Gamma,\Delta \vdash C}\ \textit{Cut}} \\
    \seq{}{\Gamma \vdash \mathbf{t}}\ (\mathbf{t}_\mathcal{R}) &
      \seq{}{\Gamma, \mathbf{f} \vdash A}\ (\mathbf{f}_\mathcal{L}) \\
    \seq{\Gamma \vdash A}{\Gamma,I \vdash A}\ (I_\mathcal{L}) &
      \seq{}{{}\vdash I}\ (I_\mathcal{R}) \\
    \seq{\Gamma,A,B \vdash C}{\Gamma, A \otimes B \vdash C}\ (\otimes_\mathcal{L}) &
      \seq{\Gamma \vdash A \qquad \Delta \vdash B}{\Gamma,\Delta \vdash A \otimes B}\ (\otimes_\mathcal{R}) \\
    \seq{\Gamma \vdash A \qquad \Delta,B \vdash C}{\Gamma,\Delta,A \multimap B \vdash C}\ (\multimap_\mathcal{L}) &
      \seq{\Gamma,A \vdash B}{\Gamma \vdash A \multimap B}\ (\multimap_\mathcal{R}) \\
    \seq{\Gamma,A \vdash C}{\Gamma,A \mathbin{\&} B \vdash C}\ (\&_{\mathcal{L}-1}) &
      \seq{\Gamma,B \vdash C}{\Gamma,A \mathbin{\&} B \vdash C}\ (\&_{\mathcal{L}-2}) \\
    \onecol{\vdots}
  \end{tabular}
  \caption{Sequent Calculus Formulation of \textbf{ILL}}
\end{figure}
\end{document}

Some things to note:

• You tabular column specification will determine the space between the two-column entries:

  \begin{tabular}{C@{\quad}C}
  

  will insert \quad between the widest elements in either column. To visualize the gap , you could use C@{}|@{\quad}|@{}C:

  

• An \arraystretch of 2.5 seems sufficient to spread out the expressions within the tabular.

• \frac centres its contents with respect to the math axis, so there's no need to fiddle around with vertical adjustment in placing contents on the right.
• \frac is also supplied with a \strut in the numerator and denominator for spacing considerations. Alternatively, use \mystrut as defined in @egreg's answer. For convenience, everything is used in a macro \seq that takes, as arguments, the same configuration as \frac.