
我正在使用該包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}