Cfrgtkky

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[.5linewidth][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[.5linewidth][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[.5linewidth][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}} \

                          &       \[-.8normalbaselineskip]

        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}