# Writing a natural deduction proof in Latex

I have checked the other questions, before anyone asks, but the style of proof appears to be subtly different and I would be expected to stick to the convention that I am using.

My question is how to create a proof in Latex like the one in the image attached:

(Apologies for the lighting, it is late for me)

This is not a Fitch-style proof, as no indentation is present, or those bars. I could use ordered lists, but I am wondering if there is a package that allows me to auto-indent lines and the side-notes/operations as that can be fiddly with raw lists (although if anyone has any pointers on this I would be happy to hear them).

Any ideas? I am quite surprised I wasn't able to find any packages that use this kind of proof, it is the style used in Mendelson's Introduction to Mathematical Logic, so perhaps it is old-school. Appreciate any guidance people can provide.

Another solution, based on listliketab:

\documentclass{article}
\usepackage[showframe]{geometry}
\usepackage{listliketab}

\begin{document}

\storestyleof{enumerate}
\begin{listliketab}%
\newcounter{tabenum}\setcounter{tabenum}{0}
\newcommand{\step}{\refstepcounter{tabenum}\thetabenum.}
\noindent \begin{tabular}{L >{$}l <{$}@{\hskip4em}l}
\multicolumn{2}{c}{$\vdash P\lor\lnot P$} \\
\step & \lnot(P\land\lnot P) & Hyp \\
\step & P & {Hyp}\\
\step & P\lor\lnot P & 2, $\lor$-introduction \\
\step & \bot & 1, 3, contradiction \\
\step & \lnot P & 2, 4, negation-introduction \\
\step & P\lor\lnot P & 5, $\lor$-introduction \\
\step & \bot & 1, 6, contradiction \\
\step & \lnot\lnot(P\lor\lnot P) & 1, 7, negation-introduction \\
\step & P\lor\lnot P & 8, double negation elimination
\end{tabular}
\end{listliketab}

\end{document}


• ShareLatex seems to complain about the sign in the \noindent line, but this works quite well. Thanks! – Daniel Soutar Apr 27 '18 at 14:55 • Did you load array? – Bernard Apr 27 '18 at 15:23 • I had not, and that helped, thanks. One other thing - regarding overflow onto another line - how do I handle formulas that can span more than a few cm? Do the notes on the right shift? Can they handle multiple lines? – Daniel Soutar Apr 28 '18 at 18:28 • You can use one of the aligned, alignedat, gathered or multlined environment (the latter requires loading mathtools in the place of amsmath). – Bernard Apr 28 '18 at 19:41 You can build an environment based on flalign*: \documentclass{article} \usepackage{amsmath} \usepackage{showframe} \newcounter{formalproofline} \newenvironment{formalproof}[1] {% \setcounter{formalproofline}{0}% \csname flalign*\endcsname &\makebox[0pt][l]{\displaystyle#1} } {\endflalign} \newcommand{\step}[2]{% \\ \stepcounter{formalproofline}% \theformalproofline.\quad & #1 &\qquad& \text{#2}% } \begin{document} \begin{formalproof}{\vdash P\lor\lnot P} \step{\lnot(P\land\lnot P)}{Hyp} \step{P}{Hyp} \step{P\lor\lnot P}{2,\lor$-introduction} \step{\bot}{1, 3, contradiction} \step{\lnot P}{2, 4, negation-introduction} \step{P\lor\lnot P}{5,$\lor\$-introduction}

The showframe` package just draws the page borders, for checking the alignment.