겐첸 시스템을 MathJax로! bussproofs

bussproofs 패키지를 통해 다음과 같은 증명들을 (MathJax를 비롯한) \(\TeX\) 환경에서 표현할 수 있다.

A User Guide[링크]

$$
\begin{prooftree}
 \AxiomC{$P$}
 \AxiomC{$\neg P$}
  \BinaryInfC{$Q$}
\end{prooftree}
\tag{EFQ}
$$

코드:

$$
\begin{prooftree}
    \AxiomC{$P$}
    \AxiomC{$\neg P$}
        \BinaryInfC{$Q$}
\end{prooftree}
\tag{EFQ}
$$

$$
\begin{prooftree}
\def\fCenter{\mbox{ $\vdash$ }}
 \Axiom$A, B, C\fCenter D$
 \UnaryInf$A, B\fCenter C \supset D$
\end{prooftree}
\tag{RD}
$$

코드:

$$
\begin{prooftree}
    \def\fCenter{\mbox{ $\vdash$ }}
    \Axiom$A, B, C\fCenter D$
    \UnaryInf$A, B\fCenter C \supset D$
\end{prooftree}
\tag{RD}
$$

$$
\begin{prooftree}
 \AxiomC{$P$}
\AxiomC{}
 \RightLabel{$\scriptsize{\text{AxPr}_1}$}
 \UnaryInfC{$P \supset (Q\supset P)$}
  \RightLabel{MP}
  \BinaryInfC{$(Q\supset P)$}
\end{prooftree}
$$

코드:

$$
\begin{prooftree}
    \AxiomC{$P$}
\AxiomC{}
    \RightLabel{$\scriptsize{\text{AxPr}_1}$}
    \UnaryInfC{$P \supset (Q\supset P)$}
        \RightLabel{MP}
        \BinaryInfC{$(Q\supset P)$}
\end{prooftree}$$