☰

析取-消除子证明盒 LaTeX

tag-icon • tag-icon boxes logic logicproof
析取-消除子证明盒 LaTeX

如何在 LaTeX 中的 logicproof 环境中并排编写子证明（如图所示）？在命题逻辑中使用析取消除定律时会用到这种类型的证明。 在此处输入图片描述

已编辑：为了证明析取，需要采取以下步骤： 在此处输入图片描述

意思是$\chi$从得到$\phi \lor \psi$，你需要找到$\phi$给出$\chi$和$\psi$的证明$\chi$。由于这是同时完成的，我们使用两个彼此相邻的子证明盒。

答案1

{NiceArray}这是使用（和 TikZ）的解决方案nicematrix。

\documentclass{article}
\usepackage{nicematrix,tikz}

\begin{document}

\[\renewcommand{\arraystretch}{1.5}
\setlength{\arraycolsep}{10pt}
\begin{NiceArray}{lllll@{\enskip}}
1 & \neg p \lor q & \text{premise} \\
2 & \Block[tikz={draw,offset=1pt}]{5-2}{}
    \neg p  & \text{premise}      & \Block[tikz={draw,offset=1pt}]{5-2}{}
                                    q       & \text{premise} \\
3 & \Block[tikz={draw,offset=3pt}]{3-2}{}
    p       & \text{assumption}   & \Block[tikz={draw,offset=3pt}]{2-2}{}
                                    p       & \text{assumption} \\
4 & \bot    & \neg\text{e}\; 3,2  & q       & \text{copy } 2 \\
5 & q       & \bot\text{e}\; 4    & p \to q & \mathord{\to}\text{i} \; 3-4 \\
6 & p \to q & \mathord{\to}\text{i}\; 3-5 \\
7 & p \to q &                     &         & \lor\text{e}\; 1,2-6
\end{NiceArray}\]

\end{document}

上述代码的输出

答案2

除了学习逻辑之外，我不建议尝试使用它。我假设你可以手写这些，并鼓励你这样做。

将其视为概念验证而非解决方案。至少存在两个问题。

  1. 使用子校样时，对齐明显错误。也就是说，wff 和对齐方式与子校样内相应的行号没有正确对齐。子校样中行的内容相对于相应的行号向下漂移（或行号相对于行的内容向上漂移）。
  2. 坦白说，其语法很糟糕。

我怀疑 (1) 可以使用 提供的功能来解决tabularray。我对这个包一点也不熟悉 --- 我认为我以前没有用过它；如果我用过，那也只是为了在 SE 上得到一个答案或类似的东西 --- 并且它的文档没有索引，我无法完全理解它如何、是否或在何处指定命令的语法。

(2) 需要一种具有自定义界面的适当方法，就像各种自然演绎证明包所提供的那样。如果这种证明方式流行起来，可能就会有人写一个。（我试图看看书籍在线资源是否提供了任何内容，但我甚至找不到页面。）

买者自负

并列子证明

\documentclass{article}
% ateb: https://tex.stackexchange.com/a/702389/
\usepackage{tabularray}
\newcommand*{\lfalse}{\ensuremath{\mathord{\bot}}}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\newcommand*{\liff}{\ensuremath{\mathbin{\leftrightarrow}}}
\NewExpandableDocumentCommand \lcsno {} {\arabic{rownum}.}
\begin{document}
\begin{tblr}{%
    colspec={Q[l]Q[l,mode=math]Q[l]Q[l,mode=math]Q[l]},
  }
  \lcsno & \lnot p \lor q & premise &  &  \\
  \lcsno & \SetCell[r=5,c=2]{l}{%
    \begin{tblr}{baseline=T,colspec={|Q[l,mode=math]Q[l,mode=text]|}}
      \hline
      \lnot p & assumption \\
      \SetCell[r=3,c=2]{l}{%
        \begin{tblr}{baseline=T,colspec={|Q[l,mode=math]Q[l,mode=text]|}}
          \hline
          p & assumption \\
          \lfalse & excl.~middle 2,3 \\
          q & $\lnot$\,e 4   \\
          \hline
        \end{tblr}%
      } & \\
      & \\
      & \\
      p \lif q & \lif\, i 3--5 \\
      \hline
    \end{tblr}%
  } & & \SetCell[r=5,c=2]{l}{%
    \begin{tblr}{baseline=T,colspec={|Q[l,mode=math]Q[l,mode=text]|}}
      \hline
      q & assumption \\
      \SetCell[r=2,c=2]{l}{%
        \begin{tblr}{baseline=T,colspec={|Q[l,mode=math]Q[l,mode=text]|}}
          \hline
          p & assumption \\
          q & repeat 2 \\
          \hline
        \end{tblr}%
      } & \\
      & \\
      p \lif q & \lif\, i 3--4  \\
      & \\
      \hline
    \end{tblr}%
  } & \\
  \lcsno &  & &  & \\
  \lcsno &  & &  & \\
  \lcsno &  & &  & \\
  \lcsno &  & &  & \\
  \lcsno & p \lif q & $\lor$\,e 1--6 & & \\
\end{tblr}
\end{document}

如果您发现子证明消失了，请注意，它tabularray非常挑剔，通常只是忽略一些东西而不是警告您。每个被替换的单元格都\SetCell必须明确创建为空单元格。仅仅留下空间是不够的。例如，我们无法替换

  \lcsno &  & &  & \\
  \lcsno &  & &  & \\
  \lcsno &  & &  & \\
  \lcsno &  & &  & \\

和

  \lcsno  \\
  \lcsno  \\
  \lcsno  \\
  \lcsno  \\

否则我们的子证明就会消失。与 不同\multicolumn，\SetCell有时会从它替换的第一列中获取上下文。因此，mode=text子证明中需要显式，否则理由会被排版为数学。

相关内容