I have a rule for natural deduction that I'd like to typeset. It looks like this:

Universal quantifier introduction

How should I go about typesetting this with LaTeX? Should I use one of the packages (e.g. logicproof) - it seems a bit overkill given I'm not typesetting an actual proof, only one of the rules that can be used. I've also considered just using a \frac and maybe a tabular environment but this seems a bit messy.

  • I think it could be done using tikz: 5 text nodes for each text, 1 rectangle node, and one horizontal path underneath the rectangle
    – xtt
    May 11, 2017 at 13:24
  • The best approach is to start at the LaTeX for Logicians site and see if something there does what you need or can be adapted to do it. That generally gets you more intuitive and shorter code than manually laying stuff out.
    – cfr
    Feb 28, 2018 at 18:01
  • @Jason If logicproof is overkill, then surely tikz is :-).
    – cfr
    Mar 3, 2018 at 18:21

2 Answers 2


Similar to Tiuri's nice answer, but with stacks, instead of matrices.

  \tabbedLongstack{x_0 & \\ & \vdots \\ & \phi[x_0/x]}
  \forall x\,\phi
\forall x\,\mathrm{i}

enter image description here


I suggest to use \boxed around a matrix environment (or similar) in math mode to get the box, and then to just use a \frac. With this code:

        x_0 & \\
        & \vdots \\
        & \phi[x_0/x]
    \end{matrix}}_{\strut}}{\forall x\phi}\forall xi

I get this result:

enter image description here

Edit: The \strut from Steven's solution makes a lot of sense here, too.

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.