Pacote lplfitch: Adicione numeração de linha à esquerda

Question

Estou usando o pacote lplfitchpara compor provas de dedução natural no estilo Fitch. Gostaria de numerar as linhas no lado esquerdo da barra vertical em vez de no lado esquerdo da fórmula?

Esquematicamente, aqui está o que eu gostaria de obter:

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

Aqui está um exemplo prático:

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

Produz algo assim:

| 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

Esta resposta demonstra como usarfitchpara compor a prova na questão, que coloca os números das linhas à esquerda da linha, e como modificar o ndambiente para que as regras de inferência definidas usem os símbolos apropriados para os conectivos lógicos.

Por padrão, o pacote codifica esses símbolos e usa, por exemplo, \wedgeem vez da semântica \land. Para o condicional, ele usa \Rightarrow. Neste caso, não há alternativa semântica. Em vez de codificar a ferradura com \supset, adicionamos uma macro semântica adicional \life a usamos.

A única parte complicada disso envolve as alterações no código do gato e isso só é difícil porque não sei o que estou fazendo. No entanto, copiar e colar das .stymaravilhas funciona.

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