Someone know a package that permit to write natural deduction in this linear form with this kind of strokes? Thank you! P.S. The example of ND is from Jan von Plato's book, Elements of logical reasoning.
-
Welcome to TeX.SX! This book is written in LaTeX. You could kindly write the author and ask for the code of that image.– LaRiFaRiSep 9, 2015 at 12:32
-
2Welcome to TeX.SX! Maybe the nice survey of LaTeX for logicians can help you.– moeweSep 9, 2015 at 12:34
-
If none of the packages in the link do what you want, you could try building your own (maybe using a table How to enumerate the rows of a table, Automatic table row numbers, the lines can probably be drawn with TikZ (?)). In that case it would be nice to see some code of what you have tried so far.– moeweSep 9, 2015 at 16:46
1 Answer
A bit late, but here is a solution with pstricks
. The idea is to add empty nodes (\pnodes
) at suitable places in a tabular
environment, then connect them with \ncbar
node connections. You can look at the pst-node
package documentation for details.
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{fourier}
\usepackage{array}
\usepackage{pstricks-add}
\usepackage{auto-pst-pdf}
\newcommand\lAnd{\mathrel{\&}}
\begin{document}
\begin{postscript}
\psset{angle=180, linewidth=0.6pt}
\renewcommand\arraystretch{1.25}
\newcounter{tabenum}\setcounter{tabenum}{0}
\newcommand{\tabitem}{\refstepcounter{tabenum} \thetabenum.}
\begin{tabular}{r@{\enspace}>{$}l<{$}@{\qquad}l}
\pnode(-0.4em,0.6ex){H1}\tabitem & A\lAnd B & hypothesis: goal $\neg\neg A\lAnd\neg\neg B$ \\
\tabitem & A & $1,\lAnd E$ \\
\tabitem & B & $1, \lAnd E$ \\
\pnode(-0.4em,0.6ex){H2}\tabitem & \neg A & hypothesis: goal $\bot$ \\
\tabitem & \bot & $4, 1, \subset E$ \\
\tabitem & \neg\neg A \pnode(0, 2.25ex){G2} & $4{-}5, \subset I$ \\
\pnode(-0.4em,0.6ex){H3}\tabitem & \neg B & hypothesis: goal $\bot$ \\
\tabitem & \bot & $7, 3, \subset E$ \\
\tabitem & \neg\neg B \pnode(0, 2.25ex){G3} & $7{-}8, \subset I$ \\
\tabitem & \neg\neg A\lAnd\neg\neg B & $6, 9, \lAnd I$ \\
\tabitem & A\lAnd B \supset \neg\neg A\lAnd\neg\neg B \pnode(0, 2.3ex){G1}
\end{tabular}%\end{listliketab}
\ncbar[armA=20pt]{H1}{G1}
\ncbar{H2}{G2}
\ncbar{H3}{G3}
\end{postscript}
\end{document}