# Labeling parts of proofs

I'm using bussproofs to layout sequent-calculus proofs. I would like to label the parts of some of my inferences. For example, given the following proof:

\begin{prooftree}
\AxiomC{$X\vdash\phi\rightarrow\psi$}
\AxiomC{$Y\vdash\phi$}
\BinaryInfC{$X;Y\vdash\psi$}
\end{prooftree}


I would like to label the hypotheses as hypotheses and the conclusion as the conclusion. Ideally, I'd like to do this using overbraces and underbraces. So, for example, I'd like an overbrace spanning the hypotheses and, above the overbrace, the word hypotheses''.

Now, being greedy, there's something else I'd like, too: I'd like to put arrows labeling pieces of the inference as well, e.g. an arrow pointing to the $\vdash$ with the word "turnstile" at the bottom of the arrow, or an arrow pointing to the ";" with the word "punctuation" at the bottom.

Partial solutions are warmly welcomed, I'm asking for a lot here.

• For those who don't regularly immerse themselves in proof nomenclature, it would be helpful to provide even a hand drawn image of what you want. Also, providing a full MWE is better than a snippet. Aug 19 '15 at 20:41

Here's a method which uses the tikzmark library for TikZ:

\documentclass{article}
\usepackage{tikz}
\usetikzlibrary{tikzmark,decorations.pathreplacing,calc}
\usepackage{bussproofs}
\begin{document}
\begin{prooftree}
\AxiomC{\tikzmark{a}$X\vdash\phi\rightarrow\psi$\tikzmark{b}}
\AxiomC{\tikzmark{c}$Y\vdash\phi$\tikzmark{d}}
\BinaryInfC{\tikzmark{e}$X\tikzmark{e1};\tikzmark{f1}Y\tikzmark{e2}\vdash\tikzmark{f2}\psi$\tikzmark{f}}
\end{prooftree}
\begin{tikzpicture}[remember picture, overlay]
\draw [decorate, decoration={brace, amplitude=7.5pt}] ({pic cs:a}) +(0,\baselineskip) coordinate (g) -- (g -| {pic cs:d}) node [midway, above, anchor=south, yshift=5pt] {Hypotheses};
\draw [decorate, decoration={brace, amplitude=7.5pt}] ({pic cs:f}) +(0,-.5\baselineskip) coordinate (h) -- (h -| {pic cs:e}) node [midway, below, anchor=north, yshift=-7.5pt] {Conclusion};
\draw [<-] ($({pic cs:e2})!1/2!({pic cs:f2})$) coordinate (i) -- ([yshift=-1.25\baselineskip]{{pic cs:d} |- i}) node (j) [right] {Turnstile};
\draw [<-] ({pic cs:e1})  +(0,-1.5pt) -- (j -| {pic cs:a}) node [left] {Punctuation};
\end{tikzpicture}
\end{document}


• Glorious! This has everything I asked for all in one place. Thanks cfr.
– Shay
Aug 20 '15 at 1:51
• @Shay You're welcome. I like logic questions ;). But an MWE does make it easier, so please provide one next time you ask a question.
– cfr
Aug 20 '15 at 2:01

Not being a proof guy, and without an image, I'm sort of guessing at how to interpret the OP's request. Here is my guess.

I introduce \pointupat[<alignment>]{math content}{text description} as well as \ltxtoverbrace{<length>}{text description}. Obviously, a \pointdownat macro could be similarly composed.

Here is the MWE.

\documentclass{article}
\usepackage{bussproofs,amsmath,stackengine}
\newcommand\pointupat[3][c]{\def\useanchorwidth{T}\def\stackalignment{c}%
\def\stacktype{L}\setstackgap{L}{.8\baselineskip}%
\ensurestackMath{\stackunder{{}#2{}}{\def\stackalignment{#1}%
\stackunder{\uparrow}{\scriptstyle\text{#3}}}}}
\newcommand\ltxtoverbrace[2]{%
\rlap{$\overbrace{\strut\rule{#1}{0pt}}^{\text{#2}}$}
}
\begin{document}
\begin{prooftree}
\AxiomC{$\ltxtoverbrace{23ex}{hypotheses}X\vdash\phi\rightarrow\psi$}
\AxiomC{$Y\vdash\phi$}
\BinaryInfC{$\underbrace{X;Y\vdash\psi}_{\text{conclusion}}$}
\end{prooftree}
\begin{prooftree}
\AxiomC{$\overbrace{X\vdash\phi\rightarrow\psi}^{\text{hypothesis}}$}
\AxiomC{$Y\vdash\phi$}
\BinaryInfC{$X\pointupat[r]{;}{punctuation}Y\pointupat[l]{\vdash}{turnstile}\psi$}
\end{prooftree}
\end{document}