菲奇式自然演绎证明的阴影部分

Question

我正在使用 fitch 包（由 Selinger 教授编写，我相信现在由 Richard Zach 维护）用于教学目的 - - 我猜很多人都这样做。

如果能够用阴影突出显示部分校样，那将非常有帮助。恐怕我真的不知道该怎么做。我知道如何将整个校样放在阴影环境中，例如使用 mdframed 包。

我已经添加了一个用于简单防伪的 MWE，以及一个我希望能够用手绘的框进行遮蔽的图像。

\documentclass{article}

\usepackage{fitch}
\begin{document}

\begin{displaymath}
\begin{nd}
  \hypo {1} {P \lor Q} \by{}{}%
  \hypo {2} {P \rightarrow R} \by{}{}%
  \hypo {3} {Q \rightarrow R} \by{}{}%
  \open%
  \hypo {4} {P} \by{}{}%
  \have {5} {R} \by{}{}%
  \close%
  \open%
  \hypo {6} {Q} \by{}{}%
  \have {7} {R} \by{}{}%
  \close%
  \have {8} {R} \by{}{}%
\end{nd}
\end{displaymath}

\end{document}

Answer 1

tikzmark通过适当放置 s 并在之后绘制 a ，您可以轻松使用框突出显示证明的相关部分tikzpicture。

例如，

\documentclass{article}
% ateb: https://tex.stackexchange.com/a/700683/  i gwestiwn Bernhard: https://tex.stackexchange.com/q/700671/    
\usepackage{fitch}
\usepackage{tikz}
\usetikzlibrary{tikzmark}
\usetikzlibrary{fit}
\usetikzlibrary{calc}
\begin{document}

\begin{displaymath}
  \begin{nd}
    \hypo {1} {P \lor Q} \by{}{}%
    \hypo {2} {P \rightarrow R} \by{}{}%
    \hypo {3} {Q\tikzmark{a} \rightarrow R} \by{}{}%
    \open 
    \hypo {4} {\tikzmarknode{b}{P}} \by{}{}
    \have {5} {\tikzmarknode{c}{R}} \by{\tikzmarknode{d}{\strut}}{}
    \close
    \open
    \hypo {6} {Q} \by{}{}%
    \have {7} {R} \by{}{}%
    \close
    \have {8} {R} \by{}{}%
  \end{nd}
\end{displaymath}
\begin{tikzpicture}[remember picture,overlay]
  \node [fit=({pic cs:a} |- b) (b) (c) ($(d.south)!.75!(c |- d.south)$),draw=red] {};
\end{tikzpicture}

\end{document}

如果你真的想给证明的那部分涂上阴影，而不是在它周围画，事情就会变得相当棘手。在证明构造出来之前，你不知道在哪里涂上阴影；在证明构造出来之后，你无法轻松地在它下面涂上阴影。

一种方法是将证明放在 中tikzpicture。然后我们可以backgrounds在构造证明后使用该库来遮蔽相关的子证明。例如，

\documentclass{article}
% ateb: https://tex.stackexchange.com/a/700683/  i gwestiwn Bernhard: https://tex.stackexchange.com/q/700671/
\usepackage{fitch}
\usepackage{tikz}
\usetikzlibrary{tikzmark}
\usetikzlibrary{fit}
\usetikzlibrary{calc}
\usetikzlibrary{backgrounds}
\begin{document}
\begin{tikzpicture}[remember picture]
  \node [align=center] {%
    $\begin{nd}
      \hypo {1} {P \lor Q} \by{}{}%
      \hypo {2} {P \rightarrow R} \by{}{}%
      \hypo {3} {Q\tikzmark{e} \rightarrow R} \by{}{}%
      \open 
      \hypo {4} {\subnode{f}{P}} \by{}{}
      \have {5} {\subnode{g}{R}} \by{\subnode{h}{\strut}}{}
      \close
      \open
      \hypo {6} {Q} \by{}{}%
      \have {7} {R} \by{}{}%
      \close
      \have {8} {R} \by{}{}%
    \end{nd}$
  };
  \scoped[on background layer]
  {
    \node [fit=({pic cs:e} |- f) (f) (g) ($(h.south)!.75!(g |- h.south)$),fill=cyan!25] {};
  }
\end{tikzpicture}
\end{document}