lplfitch-Paket: Zeilennummerierung auf der linken Seite hinzufügen

Question

Ich verwende das Paket, lplfitchum Beweise für natürliche Deduktion im Fitch-Stil zu setzen. Ich möchte die Zeilen auf der linken Seite des vertikalen Balkens nummerieren, statt links von der Formel?

Hier ist schematisch das, was ich gerne hätte:

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

Hier ist ein funktionierendes Beispiel:

\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}

Das Ergebnis ist in etwa wie folgt:

| 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

Answer 1

Diese Antwort zeigt, wie manfitchden Beweis in der Frage zu setzen, wobei die Zeilennummern links von der Zeile stehen, und wie die ndUmgebung so geändert werden muss, dass die definierten Inferenzregeln die entsprechenden Symbole für die logischen Konnektoren verwenden.

Standardmäßig codiert das Paket diese Symbole fest und verwendet eg \wedgeanstelle des semantischen \land. Für den Bedingungssatz verwendet es \Rightarrow. In diesem Fall gibt es keine semantische Alternative. Anstatt das Hufeisen mit fest zu codieren \supset, fügen wir ein zusätzliches semantisches Makro hinzu \lifund verwenden dieses.

Der einzige knifflige Teil davon betrifft die Änderungen am Cat-Code und das ist nur deshalb schwierig, weil ich nicht weiß, was ich tue. Das Kopieren und Einfügen funktioniert jedoch .stywunderbar.

\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}