☰

自然演绎法类似证明

tag-icon • tag-icon theorems
自然演绎法类似证明

我不知道该用什么词来形容这种证明（如图）：

在此处输入图片描述

它是自然演绎和正常数学证明的某种组合。我想知道如何在 LaTeX 中做到这一点。我实际上不需要看起来完全像这样。在图片中，我将语句 6-11 放在右侧，但这并不是必需的。更一般地说，我想要这样的东西：

鉴于
1. 声明
2. 声明
一   待证明的陈述
3. 假设
   4. 陈述（论证）
5. 陈述（论证）
二   其他可证明的陈述
等等。

对于在 LaTeX 中做这样的事情有什么建议吗，也许我可以使用一些软件包？

答案1

我现在访问该网站时遇到了很多问题，但也许这会很有用。它看起来不太像您发布的图片但它确实保留了基本结构。它补充lplfitch了两个新命令\given和\toprove{}，以帮助保持变体格式一致。请注意，开头的命令\l...来自包。如果您更喜欢直接输入完整的数学符号，或者它们的名称从数学角度来看是违反直觉的，则无需使用它们。无论如何，我希望它在某种程度上可能有用：

\documentclass{article}

\usepackage[T1]{fontenc}
\usepackage{textcomp}
\usepackage{lmodern}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{lplfitch}
\renewcommand{\formula}[1]{\ensuremath{#1}}
\newcommand*{\fitchline}{\cline{1-1}\\[-2ex]}
\newcounter{thingstoprove}
\newcommand*{\given}{%
  \setcounter{thingstoprove}{0}%
   & {\bfseries Given}\\\fitchline}
\newcommand*{\toprove}[1]{%
  \stepcounter{thingstoprove}%
  \\[-2ex] & {\bfseries \Roman{thingstoprove}}\formula{\; #1} & To show\\\fitchline}
\setlength{\fitchprfwidth}{.7\textwidth}

\begin{document}

\noindent\fitchprf{%
  \given
  \pline[1.]{\lall a,b \in \mathcal{Z}\ ( a|b \liff \lis c \in \mathcal{Z}\ ac = b )}[Pr.]\\
  \pline[2.]{\lall a,b \in \mathcal{Z}, p \in \mathcal{P}\ ( p|ab \lif p|a \lor p|b )}[Pr.]\\
  \pline[3.]{\lall x \in \mathcal{Q}\ ( \lis m,n \in \mathcal{Z},  n \neq 0 : x = \frac{m}{n}, gcd(m,n) = 1 )}[Pr.]}{%
  \toprove{\sqrt{2} \notin \mathcal{Q}}
  \subproof{\pline[4.]{\sqrt{2} \in \mathcal{Q}}[Ass.\ for \emph{reductio}]}{%
    \pline[5.]{\sqrt{2} = \frac{m}{n} \text{ for some } m, n \in \mathcal{Z}, gcd (m,n) = 1}[3,4]\\
    \pline[6.]{2n^2 = m^2}[multiply by 2; square]\\
    \pline[7.]{2|m^2}[1,6]\\
    \pline[8.]{2|m}[2,7]\\
    \pline[9.]{m = 2c \text{ for some } c \in \mathcal{Z}}[1,8]\\
    \pline[10.]{2n^2 = 4c^2}[6,9]\\
    \pline[11.]{n^2 = 2c^2}[divide by 2]\\
    \pline[12.]{2|n^2}[1,11]\\
    \pline[13.]{2|n}[2,12]\\
    \pline[14.]{gcd(m,n) \geq 2}[8,13]\\
    \pline[15.]{\lfalse}[\lfalsei{5}{14}]
    }
  \pline[16.]{\sqrt{2} \notin \mathcal{Q}}[\lnoti{4--15}]
}\bigskip

\noindent\fitchprf{%
  \given
  \pline[1.]{statement}\\
  \pline[2.]{statement}}
  {%
    \toprove{\text{Statement to prove}}
    \subproof{\pline[3.]{hypothesis}[Hyp.]}{%
      \pline[4.]{statement}[justification]
      }
    \pline[5.]{statement}[justification]\\
    \toprove{\text{Other statement to prove}}
    \ellipsesline
}

\end{document}

使用 lplfitch 进行 fitch 风格证明

如果您喜欢冒险，以下内容应提供完全相同的输出，并自动管理证明行的行号：

\documentclass{article}

\usepackage[T1]{fontenc}
\usepackage{textcomp}
\usepackage{lmodern}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{lplfitch}
\usepackage{etoolbox}
\renewcommand{\formula}[1]{\ensuremath{#1}}
\newcommand*{\fitchline}{\cline{1-1}\\[-2ex]}
\newcounter{thingstoprove}
\newcommand*{\given}{%
  \setcounter{thingstoprove}{0}%
   & {\bfseries Given}\\\fitchline}
\newcommand*{\toprove}[1]{%
  \stepcounter{thingstoprove}%
  \\[-2ex] & {\bfseries \Roman{thingstoprove}}\formula{\; #1} & To show\\\fitchline}
\setlength{\fitchprfwidth}{.7\textwidth}
\newcounter{plineno}
\newcommand*{\reallyresetplineno}{\setcounter{plineno}{0}}
\let\resetplineno\reallyresetplineno
\pretocmd{\fitchprf}{\resetplineno}{\GenericWarning{Hackery}{Successfully prepended code to fitchprf.}}{\GenericWarning{Hackery}{Failed to patch fitchprf. Sorry, you will need to manage line numbering yourself.}}
\apptocmd{\fitchprf}{\global\let\resetplineno\reallyresetplineno}{\GenericWarning{Hackery}{Successfully appended code to fitchprf.}}{\GenericWarning{Hackery}{Failed to patch fitchprf. Sorry, you will need to manage line numbering yourself.}}
\pretocmd{\subproof}{\global\let\resetplineno\relax}{\GenericWarning{Hackery}{Successfully prepended code to subproof.}}{\GenericWarning{Hackery}{Failed to patch subproof. Sorry, you will need to manage line numbering yourself.}}
\makeatletter
  \patchcmd{\pline}{\@empty}{\stepcounter{plineno}\arabic{plineno}.}{\GenericWarning{Hackery}{Successfully patched pline.}}{\GenericWarning{Hackery}{Failed to patch pline. Sorry, you will need to manage line numbering yourself.}}
\makeatother

\begin{document}

\noindent\fitchprf{%
  \given
  \pline{\lall a,b \in \mathcal{Z}\ ( a|b \liff \lis c \in \mathcal{Z}\ ac = b )}[Pr.]\\
  \pline{\lall a,b \in \mathcal{Z}, p \in \mathcal{P}\ ( p|ab \lif p|a \lor p|b )}[Pr.]\\
  \pline{\lall x \in \mathcal{Q}\ ( \lis m,n \in \mathcal{Z},  n \neq 0 : x = \frac{m}{n}, gcd(m,n) = 1 )}[Pr.]}{%
  \toprove{\sqrt{2} \notin \mathcal{Q}}
  \subproof{\pline{\sqrt{2} \in \mathcal{Q}}[Ass.\ for \emph{reductio}]}{%
    \pline{\sqrt{2} = \frac{m}{n} \text{ for some } m, n \in \mathcal{Z}, gcd (m,n) = 1}[3,4]\\
    \pline{2n^2 = m^2}[multiply by 2; square]\\
    \pline{2|m^2}[1,6]\\
    \pline{2|m}[2,7]\\
    \pline{m = 2c \text{ for some } c \in \mathcal{Z}}[1,8]\\
    \pline{2n^2 = 4c^2}[6,9]\\
    \pline{n^2 = 2c^2}[divide by 2]\\
    \pline{2|n^2}[1,11]\\
    \pline{2|n}[2,12]\\
    \pline{gcd(m,n) \geq 2}[8,13]\\
    \pline{\lfalse}[\lfalsei{5}{14}]
    }
  \pline{\sqrt{2} \notin \mathcal{Q}}[\lnoti{4--15}]
}\bigskip

\noindent\fitchprf{%
  \given
  \pline{statement}\\
  \pline{statement}}
  {%
    \toprove{\text{Statement to prove}}
    \subproof{\pline{hypothesis}[Hyp.]}{%
      \pline{statement}[justification]
      }
    \pline{statement}[justification]\\
    \toprove{\text{Other statement to prove}}
    \ellipsesline
}

\end{document}

相关内容