Пакет lplfitch: Добавить нумерацию строк слева

Question

Я использую пакет 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

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