# Natural deduction like proof

I'm not sure what the right word is for this kind of proof (in the picture):

It is some kind of combination of natural deduction and normal math proofs. I'm wondering how I could do this in LaTeX. I doesn't really need to look exactly like this. In the picture, I've put statement 6-11 to the right for example, but this is not really necessary. More generally I would like something as:

Given
1. statement
2. statement
Ⅰ   Statement to prove
3. hypothese
4. statement (justification)
5. statement (justification)
II   Other statement to prove
etc. etc.

Any suggestion for doing something like this in LaTeX, maybe some packages that I could use ?

• take a look at tex.stackexchange.com/questions/147063/… Commented Jan 12, 2014 at 15:54
• Commented Jan 12, 2014 at 16:15
• @cmhughes Interesting ! Commented Jan 12, 2014 at 16:43
• You might find logicmatters.net/latex-for-logicians/nd helpful (scroll down to Fitch-style layouts which are formatted in the way I think you have in mind for natural deduction). There might be something helpful there even though you are not doing exactly the same thing.
– cfr
Commented Jan 12, 2014 at 17:10
• unfortunately, the visual isn't really intelligible to me. but you may be looking for something like what is described in this tugboat article: ProofCheck: Writing and checking complete proofs in LaTeX by Bob Neveln and Bob Alps. Commented Jan 12, 2014 at 18:10

## 1 Answer

I'm having a lot of problems accessing the site right now but perhaps this will be useful. It does not look quite like the image you posted but it does maintain the basic structure. It supplements lplfitch with two new commands, \given and \toprove{}, to help keep the formatting of your variation consistent. Note that the commands beginning \l... are from the package. You need not use them if you prefer to type the full mathematical symbols directly or if their names are counter-intuitive from a mathematical perspective. Anyway, I hope it may be useful in some way:

\documentclass{article}

\usepackage[T1]{fontenc}
\usepackage{textcomp}
\usepackage{lmodern}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{lplfitch}
\renewcommand{\formula}[1]{\ensuremath{#1}}
\newcommand*{\fitchline}{\cline{1-1}\\[-2ex]}
\newcounter{thingstoprove}
\newcommand*{\given}{%
\setcounter{thingstoprove}{0}%
& {\bfseries Given}\\\fitchline}
\newcommand*{\toprove}[1]{%
\stepcounter{thingstoprove}%
\\[-2ex] & {\bfseries \Roman{thingstoprove}}\formula{\; #1} & To show\\\fitchline}
\setlength{\fitchprfwidth}{.7\textwidth}

\begin{document}

\noindent\fitchprf{%
\given
\pline[1.]{\lall a,b \in \mathcal{Z}\ ( a|b \liff \lis c \in \mathcal{Z}\ ac = b )}[Pr.]\\
\pline[2.]{\lall a,b \in \mathcal{Z}, p \in \mathcal{P}\ ( p|ab \lif p|a \lor p|b )}[Pr.]\\
\pline[3.]{\lall x \in \mathcal{Q}\ ( \lis m,n \in \mathcal{Z},  n \neq 0 : x = \frac{m}{n}, gcd(m,n) = 1 )}[Pr.]}{%
\toprove{\sqrt{2} \notin \mathcal{Q}}
\subproof{\pline[4.]{\sqrt{2} \in \mathcal{Q}}[Ass.\ for \emph{reductio}]}{%
\pline[5.]{\sqrt{2} = \frac{m}{n} \text{ for some } m, n \in \mathcal{Z}, gcd (m,n) = 1}[3,4]\\
\pline[6.]{2n^2 = m^2}[multiply by 2; square]\\
\pline[7.]{2|m^2}[1,6]\\
\pline[8.]{2|m}[2,7]\\
\pline[9.]{m = 2c \text{ for some } c \in \mathcal{Z}}[1,8]\\
\pline[10.]{2n^2 = 4c^2}[6,9]\\
\pline[11.]{n^2 = 2c^2}[divide by 2]\\
\pline[12.]{2|n^2}[1,11]\\
\pline[13.]{2|n}[2,12]\\
\pline[14.]{gcd(m,n) \geq 2}[8,13]\\
\pline[15.]{\lfalse}[\lfalsei{5}{14}]
}
\pline[16.]{\sqrt{2} \notin \mathcal{Q}}[\lnoti{4--15}]
}\bigskip

\noindent\fitchprf{%
\given
\pline[1.]{statement}\\
\pline[2.]{statement}}
{%
\toprove{\text{Statement to prove}}
\subproof{\pline[3.]{hypothesis}[Hyp.]}{%
\pline[4.]{statement}[justification]
}
\pline[5.]{statement}[justification]\\
\toprove{\text{Other statement to prove}}
\ellipsesline
}

\end{document}


If you like to live dangerously, the following should give precisely the same output with automatic management of line numbering for proof lines:

\documentclass{article}

\usepackage[T1]{fontenc}
\usepackage{textcomp}
\usepackage{lmodern}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{lplfitch}
\usepackage{etoolbox}
\renewcommand{\formula}[1]{\ensuremath{#1}}
\newcommand*{\fitchline}{\cline{1-1}\\[-2ex]}
\newcounter{thingstoprove}
\newcommand*{\given}{%
\setcounter{thingstoprove}{0}%
& {\bfseries Given}\\\fitchline}
\newcommand*{\toprove}[1]{%
\stepcounter{thingstoprove}%
\\[-2ex] & {\bfseries \Roman{thingstoprove}}\formula{\; #1} & To show\\\fitchline}
\setlength{\fitchprfwidth}{.7\textwidth}
\newcounter{plineno}
\newcommand*{\reallyresetplineno}{\setcounter{plineno}{0}}
\let\resetplineno\reallyresetplineno
\pretocmd{\fitchprf}{\resetplineno}{\GenericWarning{Hackery}{Successfully prepended code to fitchprf.}}{\GenericWarning{Hackery}{Failed to patch fitchprf. Sorry, you will need to manage line numbering yourself.}}
\apptocmd{\fitchprf}{\global\let\resetplineno\reallyresetplineno}{\GenericWarning{Hackery}{Successfully appended code to fitchprf.}}{\GenericWarning{Hackery}{Failed to patch fitchprf. Sorry, you will need to manage line numbering yourself.}}
\pretocmd{\subproof}{\global\let\resetplineno\relax}{\GenericWarning{Hackery}{Successfully prepended code to subproof.}}{\GenericWarning{Hackery}{Failed to patch subproof. Sorry, you will need to manage line numbering yourself.}}
\makeatletter
\patchcmd{\pline}{\@empty}{\stepcounter{plineno}\arabic{plineno}.}{\GenericWarning{Hackery}{Successfully patched pline.}}{\GenericWarning{Hackery}{Failed to patch pline. Sorry, you will need to manage line numbering yourself.}}
\makeatother

\begin{document}

\noindent\fitchprf{%
\given
\pline{\lall a,b \in \mathcal{Z}\ ( a|b \liff \lis c \in \mathcal{Z}\ ac = b )}[Pr.]\\
\pline{\lall a,b \in \mathcal{Z}, p \in \mathcal{P}\ ( p|ab \lif p|a \lor p|b )}[Pr.]\\
\pline{\lall x \in \mathcal{Q}\ ( \lis m,n \in \mathcal{Z},  n \neq 0 : x = \frac{m}{n}, gcd(m,n) = 1 )}[Pr.]}{%
\toprove{\sqrt{2} \notin \mathcal{Q}}
\subproof{\pline{\sqrt{2} \in \mathcal{Q}}[Ass.\ for \emph{reductio}]}{%
\pline{\sqrt{2} = \frac{m}{n} \text{ for some } m, n \in \mathcal{Z}, gcd (m,n) = 1}[3,4]\\
\pline{2n^2 = m^2}[multiply by 2; square]\\
\pline{2|m^2}[1,6]\\
\pline{2|m}[2,7]\\
\pline{m = 2c \text{ for some } c \in \mathcal{Z}}[1,8]\\
\pline{2n^2 = 4c^2}[6,9]\\
\pline{n^2 = 2c^2}[divide by 2]\\
\pline{2|n^2}[1,11]\\
\pline{2|n}[2,12]\\
\pline{gcd(m,n) \geq 2}[8,13]\\
\pline{\lfalse}[\lfalsei{5}{14}]
}
\pline{\sqrt{2} \notin \mathcal{Q}}[\lnoti{4--15}]
}\bigskip

\noindent\fitchprf{%
\given
\pline{statement}\\
\pline{statement}}
{%
\toprove{\text{Statement to prove}}
\subproof{\pline{hypothesis}[Hyp.]}{%
\pline{statement}[justification]
}
\pline{statement}[justification]\\
\toprove{\text{Other statement to prove}}
\ellipsesline
}

\end{document}

• Is it possible to define a counter for \pline? Is seems that typing line numbers manually is not a very efficient (nor robust) thing to do. Commented Jan 15, 2014 at 21:42
• @KevinC See the addition to my answer. This gives just the same output but manages number of proof lines automagically. Since this patches the commands of lplfitch rather more seriously than the original code (it uses the facilities of etoolbox), this is likely to be more fragile. But it does seem to work with the examples I used, at least.
– cfr
Commented Jan 15, 2014 at 23:00
• Wow, thank you so much !! This is awesome :) Commented Jan 16, 2014 at 10:24
• @Kasper No problem. It was interesting - I've never used this package or the etoolbox patching commands before. But I've wanted an excuse to play with the latter!
– cfr
Commented Jan 16, 2014 at 14:55