# Typesetting predicate natural deduction rules

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

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

\documentclass{article}
\usepackage{tabstackengine}
\TABstackMath
\setstacktabbedgap{1ex}
\setstackgap{L}{1.2\baselineskip}
\begin{document}
$\frac{ \,\fbox{ \tabbedLongstack{x_0 & \\ & \vdots \\ & \phi[x_0/x]} }_{\strut}\, }{ \forall x\,\phi } \forall x\,\mathrm{i}$
\end{document}


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:

\documentclass{article}
\usepackage{amsmath}
\begin{document}
\begin{align}
\frac{\boxed{\begin{matrix}
x_0 & \\
& \vdots \\
& \phi[x_0/x]
\end{matrix}}_{\strut}}{\forall x\phi}\forall xi
\end{align}
\end{document}


I get this result:

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