# Natural Deduction with Latex

I am new to Latex and I would like to do natural deduction. I know there are many resources on internet and it has been mentioned here a lot too, but I have not been able to find a convenient, easy-to-use package or any other method for doing natural deduction with Latex. I want to have only vertical lines for my proofs (no horizontal lines) and add my own justifications, not a set of predefined justifications. To better illustrate my question, here is a picture:

• Did you type "natural deduction" or "proof tree" in the search box at the top of this page and investigate the results of such a search? – Mico Feb 3 at 5:41
• Yes, the ones I found do not have the structure I am looking for. – Rob Feb 3 at 5:46
• Do you have a web link that explains this way of recording natural deductions in detail to give? – AndréC Feb 3 at 6:22
• Unfortunately not. That is the way I learnt. – Rob Feb 3 at 9:14

This provides a sufficient start; setting the construction inside an array (with possible nesting):

\documentclass{article}

\usepackage{xparse,amsmath}

\makeatletter
\NewDocumentCommand{\logicstep}{ o }{%
\refstepcounter{enumi}(\theenumi)%
\IfValueT{#1}{\ltx@label{#1}}%
}
\makeatother

\newcommand{\logictitle}[1]{%
\setcounter{enumi}{0}% Restart "logic" counter
\makebox[.5\linewidth][l]{$#1$}%
}

\begin{document}

$\begin{array}{c} \logictitle{A / B \rightarrow A} \\[\jot] \begin{array}{c | l | l @{\qquad} l } \logicstep[first] & \multicolumn{3}{l}{A} \\ \logicstep[second] & & B & \text{Supp /~\rightarrow Int} \\ \logicstep[third] & & A & \text{reit \eqref{first}} \\ \logicstep & \multicolumn{1}{l}{B \rightarrow A} & & \text{\rightarrow Int \eqref{second} - \eqref{third}} \end{array} \end{array}$

\end{document}


\logicstep[<label>] sets the numbering in the first column. The optional <label> allows you to \reference it (using \eqref or otherwise).

Here's another visual:

\documentclass{article}

\usepackage{xparse,amsmath}

\makeatletter
\NewDocumentCommand{\logicstep}{ o }{%
\refstepcounter{enumi}(\theenumi)%
\IfValueT{#1}{\ltx@label{#1}}%
}
\makeatother

\newcommand{\logictitle}[1]{%
\setcounter{enumi}{0}% Restart "logic" counter
\makebox[.5\linewidth][l]{$#1$}%
}

\begin{document}

$\begin{array}{c} \logictitle{A / C \rightarrow (B \rightarrow A)} \\[\jot] \begin{array}{c | l | l | l @{\qquad} l } \logicstep[first] & \multicolumn{3}{l}{A} & \multicolumn{1}{@{}l}{\text{premise}} \\ \logicstep[second] & \quad & \multicolumn{1}{|l}{C} & \multicolumn{1}{l}{} & \text{Supp, \rightarrow Int} \\ \logicstep[third] & & & B & \text{Supp, \rightarrow Int} \\ \logicstep[fourth] & & & A & \text{Reit \eqref{first}} \\ \logicstep[fifth] & & \multicolumn{1}{|l}{B} & \multicolumn{1}{l}{} & \text{\rightarrow Int, \eqref{third}--\eqref{fourth}} \\ \logicstep & \multicolumn{3}{l}{C \rightarrow (B \rightarrow A)} & \text{\rightarrow Int, \eqref{second}--\eqref{fifth}} \end{array} \end{array}$

\end{document}


Now with a line-break:

\documentclass{article}

\usepackage{xparse,amsmath}

\makeatletter
\NewDocumentCommand{\logicstep}{ o }{%
\refstepcounter{enumi}(\theenumi)%
\IfValueT{#1}{\ltx@label{#1}}%
}
\makeatother

\newcommand{\logictitle}[1]{%
\setcounter{enumi}{0}% Restart "logic" counter
\makebox[.5\linewidth][l]{$#1$}%
}

\begin{document}

$\begin{array}{c} \logictitle{A / C \rightarrow (B \rightarrow A)} \\[\jot] \begin{array}{c | l | l | l @{\qquad} l } \logicstep[first] & \multicolumn{3}{l}{A} & \multicolumn{1}{@{}l}{\text{premise}} \\ \logicstep[second] & \quad & \multicolumn{1}{|l}{C} & \multicolumn{1}{l}{} & \text{Supp, \rightarrow Int} \\ \logicstep[third] & & & B & \text{Supp, \rightarrow Int} \\ \logicstep[fourth] & & & A & \text{Reit \eqref{first}} \\ & \\[-.8\normalbaselineskip] \logicstep[fifth] & & & B & \text{Example 1} \\ \logicstep[sixth] & & & A & \text{Example 2} \\ \logicstep[seventh] & & \multicolumn{1}{|l}{B} & \multicolumn{1}{l}{} & \text{\rightarrow Int, \eqref{third}--\eqref{fourth}} \\ \logicstep & \multicolumn{3}{l}{C \rightarrow (B \rightarrow A)} & \text{\rightarrow Int, \eqref{second}--\eqref{fifth}} \end{array} \end{array}$

\end{document}

• That is more or less what I was looking for. I am wondering how would I be able to do more nested suppositions, say 3 for example. I could not figure it out. – Rob Feb 3 at 8:09
• @RobG.: I am completely unfamiliar with logical proofs and merely replicated the output. If you can provide a 3-supposition proof (through an image, say), I'm sure one can figure out how to nest these... – Werner Feb 3 at 8:19
• my apologies, I uploaded a new image with 3 suppositions. A proof like this can require even more suppositions at times. – Rob Feb 3 at 8:33
• @RobG.: See the end of my updated answer. – Werner Feb 3 at 17:17
• That works! I encountered another problem. Sorry, I did not see it coming first. How can I separate these vertical lines? I uploaded a new image. Also, when I compiled your code on my device, I saw the second vertical line appearing a little thicker than the other two. Do you know what might have caused the issue? Thanks – Rob Feb 3 at 19:23