形式逻辑中的图形化关闭假设

Question

我正在为我的学生写一些笔记。我遇到了一个小问题。我想写下一些形式逻辑的例子，其中开放的假设在某个点被关闭，这在图形上用垂直线表示。请参阅该图作为参考。 该示例表明，假设第 1 行中的命题，则可以证明第 7 行中的命题，第 1 行至第 7 行是该命题的证明。在该示例中，第 1、2 和 3 行前面有一条水平线，这意味着它们是在某一时刻被“打开”（引入）的假设。后两行分别与第 6 行和第 5 行“闭合”（首先是第 3 行与第 5 行闭合，然后是第 2 行与第 6 行闭合）。请注意，这些线以 FILO 方式闭合，因此它们不能交叉。

我的问题：如何绘制这些线条？我会说 pgf/tikz，但也许有更简单的东西。

谢谢！

\[ \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} \]

更新：软件包逻辑证明为此类证明提供了良好的经典环境。

Answer 1

你绝对可以用 Ti 来做到这一点钾Z. 请注意，您可能（暂时）需要tikzmark从GitHub（或者在第一次运行出现错误消息时直接按回车键）直到更新后的库到达 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}