1

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:

enter image description here

  • 2
    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
  • 1
    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
4

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

enter image description here

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

enter image description here

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

enter image description here

\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

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.