
私は、このパッケージを使用してlplfitch
、自然演繹の証明をフィッチ スタイルでタイプセットしています。式の左側ではなく、縦棒の左側に行番号を付けたいのですが。
図式的に言えば、私が得たいものは次のとおりです。
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
定義された推論規則が論理接続詞に適切な記号を使用するように環境を変更する方法。
デフォルトでは、パッケージはこれらのシンボルをハードコードし、\wedge
意味的な ではなくeg を使用します\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}