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:

proof of P ∨ ¬P

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



\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


enter image description here

  • 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*:


  \csname flalign*\endcsname
  \theformalproofline.\quad & #1 &\qquad& \text{#2}%


\begin{formalproof}{\vdash P\lor\lnot P}
\step{\lnot(P\land\lnot 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}


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

enter image description here

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.