我正在使用该包lplfitch
以 Fitch 样式排版自然演绎证明。我想在竖线左侧而不是公式左侧对行进行编号?
示意图中,以下是我想要得到的:
1. | hypothesis_1
2. | hypothesis_2
3. |_ hypothesis_3
3. | deduction_1 rule_1
4. | deduction_2 rule_2
5. | deduction_3 rule_3
6. | deduction_4 rule_4
7. | deduction_5 rule_5
这是一个有效的例子:
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{lplfitch}
\begin{document}
\fitchprf{
\pline[1.]{\forall x (Fx\supset Axf)}[H]\\
\pline[2.]{\forall x(Fx\supset Afx)}[H]\\
\pline[3.]{Fi}[H]}{
\pline[4.]{Fi\supset Aif}[\lalle{1, i}]\\
\pline[5.]{Aif}[\life{3}{4}]\\
\pline[6.]{Fi\supset Afi}[\lalle{2, i}]\\
\pline[7.]{Afi}[\life{5}{6}]\\
\pline[8.]{Aif\land Afi}[\landi{5}{7}]
}
\end{document}
它会产生类似这样的结果:
| 1. hypothesis_1
| 2. hypothesis_2
|_3. hypothesis_3
| 4. deduction_1 rule_1
| 5. deduction_2 rule_2
| 6. deduction_3 rule_3
| 7. deduction_7 rule_4
| 8. deduction_8 rule_5
答案1
这个答案演示了如何使用惠誉对问题中的证明进行排版,将行号放在行的左边,以及如何修改环境nd
以便定义的推理规则使用适当的逻辑连接词符号。
默认情况下,该包会对这些符号进行硬编码,并使用 eg\wedge
而不是语义\land
。对于条件,它使用\Rightarrow
。在这种情况下,没有语义替代方案。\supset
我们不是使用 硬编码马蹄铁,而是添加一个额外的语义宏\lif
并使用它。
唯一棘手的部分涉及 cat 代码更改,这很困难,因为我不知道自己在做什么。但是,从中复制粘贴效果.sty
很好。
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{fitch}
% modified from fitch.sty
{\chardef\x=\catcode`\*
\catcode`\*=11
\global\let\nd*astcode\x}
\catcode`\*=11
\def\nd*init{%
\let\open\nd*open%
\let\close\nd*close%
\let\hypo\nd*hypo%
\let\have\nd*have%
\let\hypocont\nd*hypocont%
\let\havecont\nd*havecont%
\let\by\nd*by%
\let\guard\nd*guard%
\def\ii{\by{$\lif$I}}%
\def\ie{\by{$\lif$E}}%
\def\Ai{\by{$\forall$I}}%
\def\Ae{\by{$\forall$E}}%
\def\Ei{\by{$\exists$I}}%
\def\Ee{\by{$\exists$E}}%
\def\ai{\by{$\land$I}}%
\def\ae{\by{$\land$E}}%
\def\ai{\by{$\land$I}}%
\def\ae{\by{$\land$E}}%
\def\oi{\by{$\lor$I}}%
\def\oe{\by{$\lor$E}}%
\def\ni{\by{$\lnot$I}}%
\def\ne{\by{$\lnot$E}}%
\def\be{\by{$\bot$E}}%
\def\nne{\by{$\lnot\lnot$E}}%
\def\r{\by{R}}%
}
\catcode`\*=\nd*astcode
\let\lif\supset
\begin{document}
\[
\begin{nd}
\hypo {1} {\forall x (Fx\lif Axf)}
\hypo {2} {\forall x(Fx\lif Afx)}
\hypo {3} {Fi}
\have {4} {Fi\lif Aif} \Ae{1}
\have {5} {Aif} \ie{3,4}
\have {6} {Fi\lif Afi} \Ae{2}
\have {7} {Afi} \ie{3,6}
\have {8} {Aif\land Afi} \ai{5,7}
\end{nd}
\]
\end{document}