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:
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}
