3

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.

1
  • 1
    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. – Steven B. Segletes Aug 19 '15 at 20:41
4

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}

annotated proof

2
  • 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
4

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}

enter image description here

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.