bussproofs

The bussproofs extension implements the bussproofs style package from LaTeX. See the CTAN page for more information and documentation of bussproofs.

Note that there are a couple of important differences between the use of the package in MathJax compared to actual LaTeX. First, proofs always have to be in a prooftree environment, i.e., inference macros are only recognised if they are enclosed in \begin{prooftree} and \end{prooftree}. Consequently the \DisplayProof command is not necessary.

Second, unlike in the LaTeX package, options for abbreviated inference rule macros do not have to be manually set. All abbreviated macros are directly available. Thus commands like \BinaryInfC and \BIC can be used immediately and interchangeably.

For example:

\begin{prooftree}
\AxiomC{}
\RightLabel{Hyp$^{1}$}
\UnaryInfC{$P$}
\AXC{$P\to Q$}
\RL{$\to_E$}
\BIC{$Q^2$}
\AXC{$Q\to R$}
\RL{$\to_E$}
\BIC{$R$}
\AXC{$Q$}
\RL{Rit$^2$}
\UIC{$Q$}
\RL{$\wedge_I$}
\BIC{$Q\wedge R$}
\RL{$\to_I$$^1$}
\UIC{$P\to Q\wedge R$}
\end{prooftree}

Also note that the bussproofs commands for sequent calculus derivations are not yet fully implemented.

This extension is loaded automatically when the autoload extension is used. To load the bussproofs extension explicitly, add '[tex]/bussproofs' to the load array of the loader block of your MathJax configuration, and add 'bussproofs' to the packages array of the tex block.

window.MathJax = {
  loader: {load: ['[tex]/bussproofs']},
  tex: {packages: {'[+]': ['bussproofs']}}
};

Alternatively, use \require{bussproofs} in a TeX expression to load it dynamically from within the math on the page, if the require extension is loaded.

---