3

I'm trying to do something similar to the proof in picture where there is a gap in the steps of the proof. I tried bussproofs-extra package, but it doesn't let me make the dots from two inferences to converge towards one inference (i.e., similar to BinaryInf but dots leading to it from two UnaryInfs). Any help would be highly appreciated!

For example, a sample without the dots would look like this:

\documentclass{article}
\usepackage{bussproofs}
\usepackage{tikz}
\usepackage{bussproofs-extra}
\usepackage{amssymb,amsmath}


\begin{document} 
\begin{prooftree}
\def\fCenter{\mbox{\ $\vdash$\ }}
\AxiomC{} 
\UnaryInf$\Gamma, \varphi \fCenter \Delta$
\AxiomC{}
\UnaryInf$\Gamma\fCenter \varphi, \Delta$\RightLabel{\scriptsize Cut}
\BinaryInf$ \Gamma \fCenter \Delta$ 
\end{prooftree}   


\end{document}  

fill in gaps in proofs. Image was taken from "Generalized Revenge" by Murzi & Rossi

9
  • 3
    Welcome to TeX.se. Can you post a sample document that gives most of the proof here but without the dots. This will make it a lot easier for people to help you.
    – Alan Munn
    Nov 16, 2020 at 4:45
  • 2
    Thanks but can you edit your question instead of using a comment and make the code fragment a complete compilable document.
    – Alan Munn
    Nov 16, 2020 at 16:11
  • 1
    No worries, we all have to learn. :) But it's really helpful to post complete documents beginning with \documentclass{...} and ending with \end{document} containing the code you're asking about instead of just a fragment of code as you have done. This way people can see the actual package you're using, and they don't have to spend their time constructing a document on their own to help you solve your problem.
    – Alan Munn
    Nov 16, 2020 at 16:19
  • 1
    Thanks! A bit more than is needed, so I've trimmed your code to show what I had in mind. This is a good model for future questions. And responding to comments as you've done is also really helpful!
    – Alan Munn
    Nov 16, 2020 at 16:43
  • 2
    Great if you have an answer it’s perfectly fine to add an answer yourself. I would use the sample document modified with the solution and a line or two of explanation along with a screenshot of the result. Don’t do this in the comments or in your question but add it as a proper answer.
    – Alan Munn
    Nov 16, 2020 at 23:12

1 Answer 1

2

I have received an answer via twitter–thanks to Shawn Standefer! Here is how it's done:

    \documentclass{article}
    \usepackage{bussproofs}
    \usepackage{tikz}
    \usepackage{bussproofs-extra}
    \usepackage{amssymb,amsmath}
    
    
\begin{document}

\begin{prooftree}
        \def\fCenter{\mbox{\ $\vdash$\ }}
        \AxiomC{}\LeftLabel{\scriptsize $\square$}\RightLabel{\scriptsize $n$}
        \UnaryInfC{$\Gamma \fCenter \varphi$}
        \AxiomC{}\LeftLabel{\scriptsize $\square$}\RightLabel{\scriptsize $n$}
        \UnaryInfC{$\Delta, \varphi \fCenter \psi$}
        \noLine
        \BinaryInfC{$\ddots\ \ \ \reflectbox{$\ddots$}$}
        \noLine
        \UnaryInfC{$\vdots$}
        \noLine
        \UnaryInfC{$\Gamma, \Delta \fCenter \psi$}\RightLabel{\scriptsize Cut-Un-I, $n$}
        \UnaryInfC{$\Gamma, \Delta \fCenter Un(\ulcorner \varphi \urcorner)$}
\end{prooftree}

\end{document}

It requires reflectbox and use that as a binary inference. The noLine just removes the horizontal line of an inference.

enter image description here

You must log in to answer this question.

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