2

I'm using the package bussproofs to typeset sequent calculus proofs with LaTeX. Whilst I'm more than satisfied with the results, writing the code is cumbersome. Thus, I'd like to define a custom environment to make my life a little easier. Normally, I would write code like this:

\documentclass{article}
\usepackage{bussproofs}
\usepackage{amsmath}
\begin{document}
\begin{center}
    \begin{prooftree}
\def\fCenter{\mbox{\Large$\Rightarrow$}}
\Axiom$\alpha  \ \fCenter\ \alpha$
\Axiom$\beta   \ \fCenter\ \beta$
\RightLabel{FEA}
\BinaryInf$\alpha \to \beta, \alpha \ \fCenter\  \beta$
\RightLabel{UEA}
\UnaryInf$ (\alpha \to \beta) \land \alpha, \alpha \  \fCenter\ \beta$
\RightLabel{UEA}
\UnaryInf$ (\alpha \to \beta) \land \alpha, (\alpha \to \beta )\land \alpha \  \fCenter\ \beta$
\RightLabel{Contract}
\UnaryInf$ (\alpha \to \beta) \land \alpha \  \fCenter\ \beta$
\RightLabel{FES}
\UnaryInf$\  \fCenter\  (\alpha \to \beta) \land \alpha \to \beta$
\end{prooftree}
\end{center}
\end{document}

What I'd like to change now is this:

  • the environment is centered by default but the alignment can be changed by an optional argument
  • shorten the command names: \Axiom becomes \ax, \RightLabel becomes \rlab, \LeftLabel \llab, \UnaryInf, \BinaryInf, \TrinaryInf, \QuaternaryInf and \QuinaryInf become \inf1 to \inf5, respectively
  • \ax and the inference commands take the respective sequent as a mandatory argument; this argument is in math-mode by default so you don't need dollar signs
  • instead of \ \fCenter\, => is used to denote the alignment and automatically prints \Rightarrow (as defined in the very first line of the environment).

In the end, the proof displayed above should look something like this:

\documentclass{article}
\usepackage{bussproofs}
\usepackage{amsmath}
\begin{document}
\begin{scproof}
  \ax{\alpha => \alpha}
  \ax{\beta  => \beta}
  \rlab{FEA}
  \inf2{\alpha \to \beta, \alpha => \beta}
  \rlab{UEA}
  \inf1{(\alpha \to \beta) \land \alpha, \alpha => \beta}
  \rlab{UEA}
  \inf1{(\alpha \to \beta) \land \alpha, (\alpha \to \beta) \land \alpha => \beta}
  \rlab{Contract}
  \inf1{(\alpha \to \beta) \land \alpha => \beta}
  \rlab{FES}
  \inf1{=> (\alpha \to \beta) \land \alpha \to \beta}
\end{scproof}
\end{document}

I'm new to LaTeX and afraid this is too big of a project to handle on my own. Is there someone who can help me out?

1 Answer 1

1

Here's an implementation as you desire.

I'd never do \mbox{\Large$\Rightarrow$} with additional spaces around, so I used \implies.

\documentclass{article}
\usepackage{bussproofs}
\usepackage{amsmath}

\makeatletter
\newcommand{\vitus@ax}[1]{\vitus@@ax$#1$}
\def\vitus@@ax$#1=>#2${\Axiom$#1\fCenter#2$}
\newcommand\vitus@inf[2]{\vitus@@inf{#1}$#2$}
\def\vitus@@inf#1$#2=>#3${%
  \ifcase#1\or
  \expandafter\UnaryInf\or
  \expandafter\BinaryInf\or
  \expandafter\TernaryInf\or
  \expandafter\QuaternaryInf\or
  \expandafter\QuinaryInf\fi
  $#2\fCenter#3$%
}
\newenvironment{scproof}
 {% make the new user interface
  \let\ax\vitus@ax
  \let\inf\vitus@inf
  \let\rlab\RightLabel
  \def\fCenter{\implies}%
  % start the prooftree
  \prooftree
 }
 {\endprooftree}
\makeatother

\begin{document}

\begin{prooftree}
\def\fCenter{\implies}
\Axiom$\alpha  \fCenter\alpha$
\Axiom$\beta   \fCenter\beta$
\RightLabel{FEA}
\BinaryInf$\alpha \to \beta, \alpha \fCenter \beta$
\RightLabel{UEA}
\UnaryInf$ (\alpha \to \beta) \land \alpha, \alpha  \fCenter\beta$
\RightLabel{UEA}
\UnaryInf$ (\alpha \to \beta) \land \alpha, (\alpha \to \beta )\land \alpha  \fCenter\beta$
\RightLabel{Contract}
\UnaryInf$ (\alpha \to \beta) \land \alpha  \fCenter\beta$
\RightLabel{FES}
\UnaryInf$ \fCenter (\alpha \to \beta) \land \alpha \to \beta$
\end{prooftree}

\begin{scproof}
  \ax{\alpha => \alpha}
  \ax{\beta  => \beta}
  \rlab{FEA}
  \inf2{\alpha \to \beta, \alpha => \beta}
  \rlab{UEA}
  \inf1{(\alpha \to \beta) \land \alpha, \alpha => \beta}
  \rlab{UEA}
  \inf1{(\alpha \to \beta) \land \alpha, (\alpha \to \beta) \land \alpha => \beta}
  \rlab{Contract}
  \inf1{(\alpha \to \beta) \land \alpha => \beta}
  \rlab{FES}
  \inf1{=> (\alpha \to \beta) \land \alpha \to \beta}
\end{scproof}

\end{document}

enter image description here

2
  • Thank you so much! Do you also now a way of forcing the arrow to always be in the middle of a line? In lines where there is only α, the arrow is way too high. Try \ax{\alpha => \alpha}, \inf1{\lnot\alpha , \alpha =>} , \inf1{\lnot\alpha , \alpha \land \beta =>} and you'll see what I mean. Commented Jun 28, 2021 at 20:22
  • @VitusSchäfftlein I don't think the package provides for that.
    – egreg
    Commented Jun 28, 2021 at 20:31

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .