# Proof package: lines too short

The proof package's \infer command automatically sizes the lines it draws.

However, it isn't always right (pdflatex output):

The line is too short on the left.

Is this a package bug/inaccuracy, or am I doing something wrong?

Here is the code (MWE made) that produced the document above:

\documentclass{article}
%
\usepackage{proof}
%
\begin{document}
$\infer{\bot}{ \infer{P}{ \infer{P \vee P}{ P \vee Q \quad P \vee \neg Q } } \qquad \infer{\neg P}{ \infer{\neg P \vee \neg P}{ \neg P \vee Q \quad \neg P \vee \neg Q } } }$
\end{document}

• After looking for some implementation code for \infer, and not finding anything; I suggest that the third line is space-sensitive. Since the right column is larger (added negative symbols) than the left, it is "read" as incomplete, thus is made shorter at the base connection. By intuition, my advice is to substitute in the left column code \quad with \qquad, this will add horizontal space and the line will cover the letter base. – TheVal Nov 18 '13 at 13:30
• You might have a look at bussproofs.sty of which you find a guide at logicmatters.net/latex-for-logicians/nd – egreg Nov 18 '13 at 14:58

You may have a look at bussproofs.sty; you find also an online guide

Here's a comparison (I added \qquad as suggested by Andrea L. for making the first line slightly wider)

\documentclass{article}
\usepackage{proof}
\usepackage{bussproofs}
\begin{document}
\begin{prooftree}
\AxiomC{$P\lor Q$} \AxiomC{$P\lor\lnot Q$}
\BinaryInfC{$P\lor P$}
\UnaryInfC{$P$}
\AxiomC{$\lnot P\lor Q$} \AxiomC{$\lnot P\lor \lnot Q$}
\BinaryInfC{$\lnot P\lor\lnot P$}
\UnaryInfC{$\lnot P$}
\BinaryInfC{$\bot$}
\end{prooftree}
$\infer{\bot}{ \infer{P}{ \infer{P \vee P}{ P \vee Q \qquad P \vee \neg Q } } \qquad \infer{\neg P}{ \infer{\neg P \vee \neg P}{ \neg P \vee Q \quad \neg P \vee \neg Q } } }$
\end{document}


• Glad to have left a useful suggestion posted inside an answer! – TheVal Nov 18 '13 at 16:35
• @AndreaL. You may add your answer based on proof – egreg Nov 18 '13 at 16:37
• The only thing that is stopping me to do that is the lack of documentation, since I do not know any buliding feature of \infer I don't want to leave tips that my cause errors with other situations. – TheVal Nov 18 '13 at 16:40