# Graphically closing hypothesis in formal logic

I am writing some notes for my students. I am facing a small problem. I want to write down some examples of formal logic in which open hypothesis are closed at some point, which is graphically represented by vertical lines. See the figure as reference. The example shows that, assuming the proposition in line 1, the proposition in line 7 can be proven, for which lines 1 to 7 are a proof. In the example, lines 1, 2 and 3 have a horizontal line in front, which means they are hypothesis that have been "opened" (introduced) at some moment. The later two have been "closed" with lines 6 and 5 respectively (first line 3 with line 5, and then line 2 with line 6). Note that lines are closed in a FILO manner, therefore they can't cross.

My problem: How to draw these lines? I would say pgf/tikz, but perhaps there is something simpler.

Thanks!

$\begin{array}{rll} 1&p\lthen q\\ 2&q\lthen r\\ 3&p\\ 4&q & \mathrm{E}{\lthen}\ 1,3\\ 5&r & \mathrm{E}{\lthen}\ 2,4\\ 6&p\lthen r & \mathrm{I}{\lthen}\ 3{-}5\\ 7&(q\lthen r)\lthen (p\lthen r) & \mathrm{I}{\lthen}\ 2{-}6 \end{array}$


Update: The package logicproof offers a nice classical environment for such proofs.

You can definitely do it with TikZ. Notice that you may (temporarily) need to download tikzmark from GitHub (or just hit return in the first run when there are error messages) until the updated library makes it to CTAN.

\documentclass{article}
\usepackage{amssymb}
\let\lthen\to
\usepackage{tikz}
\usetikzlibrary{tikzmark,calc}
\newcounter{lconnect}
\begin{document}
$\begin{array}{rll} \tikzmarknode{1}{1}&p\lthen q\\ \tikzmarknode{2}{2}&q\lthen r\\ \tikzmarknode{3}{3}&p\\ \tikzmarknode{4}{4}&q & \mathrm{E}{\lthen}\ 1,3\\ \tikzmarknode{5}{5}&r & \mathrm{E}{\lthen}\ 2,4\\ \tikzmarknode{6}{6}&p\lthen r & \mathrm{I}{\lthen}\ 3{-}5\\ \tikzmarknode{7}{7}&(q\lthen r)\lthen (p\lthen r) & \mathrm{I}{\lthen}\ 2{-}6 \end{array}$
\begin{tikzpicture}[overlay,remember picture,lconnect/.style args={#1 and #2}{%
/utils/exec=\stepcounter{lconnect},insert path={(#1.west)--
++(-1*\pgfkeysvalueof{/tikz/lconnect/offset}-1*\number\value{lconnect}*\pgfkeysvalueof{/tikz/lconnect/step},0) |- (#2.west)}},
self close/.style={insert path={(#1.north west) --
++(-1*\pgfkeysvalueof{/tikz/lconnect/offset}-1*\number\value{lconnect}*\pgfkeysvalueof{/tikz/lconnect/step},0) |-
(#1.south west) }}, lconnect/.cd,
offset/.initial=0.1em,step/.initial=0.4em]
\draw[lconnect/.list={3 and 5,2 and 6},self close/.list={1,7}];
\end{tikzpicture}
\end{document}


• Nice, it works! However, it is missing the opening in line 1. Adding "1 and 1" to the list seems to do the work. What would you suggest otherwise? Sometimes it is useful to close a line on itself. Thanks anyway for the great answer. – vitaminace33 Jun 17 at 18:47