3

I'd like every derivation in my document to meet these two requirements:

  1. The distance between two consecutive inference lines should always be the same (the red arrows in the figure should have equal length).
  2. The thesis symbol should be vertically centered with respect to the superior and inferior inference lines (the blue lines in the figure should have equal length).

MWE:

\documentclass{article}

\usepackage{amsmath}
\usepackage{tikz}
\usepackage{bussproofs}
\usepackage{bussproofs-extra}

\begin{document}
 \begin{center}
  \AxiomC{}
  \UnaryInfC{$B \vdash B$}
  \UnaryInfC{$\vdash A,B$}
  \UnaryInfC{$\neg A \vdash B$}
  \AxiomC{}
  \RightLabel{$\pi_0$}
  \DeduceC{$B \vdash \lVert A\rVert$}
  \RightLabel{\scriptsize$(\mathit{cut})$}
  \BinaryInfC{$\neg A \vdash \lVert A\rVert$}
  \DisplayProof
 \end{center}
\end{document}

2 Answers 2

3

Without knowing the bussproofs package, I'd suggest that you switch off the standard interlineskip and include a "strut" in every inference.

In plain TeX, you can use \offinterlineskip in tables if you want to control the line height via struts. Is there something analogous in bussproofs?

The strut is defined and used as follows:

\def\infcstrut{\vrule width 0pt height Xpt depth Ypt} % once at the beginning
...
\UnaryInfC{$\infcstrut B \vdash B$}

Here Y is a number large enough to accomodate the \lVert that goes below the baseline in the third row, and X = Y + height of thesis symbol.

Addendum: After looking briefly at the bussproof source code, I am sorry to say that this package seems to have its own detailed rules for calculating the distance between lines, which should not be so easy to override.

2nd addendum: Here's what I meant, done in plain TeX. (But that isn't easily generalizable, I'm afraid.)

\hsize 12em
\def\mystrut{\vrule width0pt height10.444pt depth3.5pt}
\def\label{\leaders\vbox to.75ex{\hsize=.25\hsize\line{\hss.}}\vfil}
\def\infc#1{\mystrut\hss$#1$\hss}
\offinterlineskip
\leftline{\valign{&\hrule #&\hbox to.5\hsize{\infc{#}}\cr
&B\vdash B&&\vdash A,B&height.75pt&\neg A \vdash B\cr
\multispan5{\label}&B \vdash \Vert A\Vert\cr
\multispan5{\vss\hbox to0pt{\hskip -.25\hsize$\;\pi_0$\hss}\vss}\cr
}}
\vbox to0pt{\vss\line{\hss\rlap{$\;(cut)$}}\vss}
\hrule
\line{\infc{\neg A \vdash \Vert A\Vert}}
\bye

plain TeX

3
  • Thank you! But what is the height of the thesis symbol? And is there a smart way to determine the smallest Y that works?
    – Lele99_DD
    Nov 2, 2021 at 19:10
  • According to the Computer Modern source files, the height of the thesis symbol at 10pt font size is 250/36pt. How small you make Y depends on how much clearance you want between the \lVert and the horizontal rule. Try it out. Nov 2, 2021 at 20:17
  • In plain TeX, the depth of the strut at 10pt font size is Y = 3.5pt. Together with X = Y + 250/36pt, this makes baselines X + Y = 13.944pt apart. In plain TeX, they are 12pt apart, but a larger baseline distance seems appropriate for such formulas. Nov 3, 2021 at 6:55
1

(Not a solution, simply an attempt.)

I don't think this is realistically achievable, but I feel that if a solution exists, you would have better chances of finding it with ebproof.

\documentclass{article}
\usepackage{amsmath}
\usepackage{ebproof}
\begin{document}
\begin{center}
    \begin{prooftree}[
        rule margin=0pt,     % Spacing above and below inference lines set to 0.
        rule code={          % This code replaces the code for the inference line with…
            \vspace{.2em}    % … a space above the line…
            \hrule           % … the line itself …
            \vspace{.3em}    % … a space below the line.
        }
        ]  
        \hypo{}
        \infer1{B \vdash B}
        \infer1{\vdash A,B}
        \infer1{\neg A \vdash B}
        \hypo{}
        \ellipsis{\(\pi_0\)}{B \vdash \lVert A\rVert}
        \infer2[\((\mathit{cut})\)]{\neg A \vdash \lVert A\rVert}
    \end{prooftree}
\end{center}
\end{document}

gives:

enter image description here

It looks a bit nicer (both in the code and in the appearance, if you ask me) than what you have right now.

(The idea of using a struct, now abandoned, comes from https://tex.stackexchange.com/a/614725/34551 but does not seem to achieve what I wanted, i.e. a fixed line height)

2
  • This example still seems to have the standard interlineskip, so the strut increased the clearance above and below, and the thesis symbol is not vertically centered. Nov 3, 2021 at 7:12
  • @HeikoTheißen I have tried to improve, and still believe that this is an approach that would be likely to succeed, but can't make it work.
    – Clément
    Nov 3, 2021 at 13:48

You must log in to answer this question.

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