Paquete lplfitch: agregue numeración de líneas a la izquierda

Question

Estoy usando el paquete lplfitchpara componer pruebas de deducción natural en estilo Fitch. ¿Me gustaría numerar las líneas en el lado izquierdo de la barra vertical en lugar de en el lado izquierdo de la fórmula?

Esquemáticamente, esto es lo que me gustaría obtener:

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

Aquí hay un ejemplo práctico:

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

Produce algo como esto:

| 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 respuesta demuestra cómo usarfitchcomponer la prueba en la pregunta, que coloca los números de línea a la izquierda de la línea, y cómo modificar el ndentorno para que las reglas de inferencia definidas utilicen los símbolos apropiados para los conectivos lógicos.

De forma predeterminada, el paquete codifica estos símbolos y utiliza, por ejemplo, \wedgeen lugar de la semántica \land. Para el condicional, usa \Rightarrow. En este caso, no existe ninguna alternativa semántica. En lugar de codificar la herradura con \supset, agregamos una macro semántica adicional \lify la usamos.

La única parte complicada de esto tiene que ver con los cambios en el código cat y eso sólo es difícil porque no sé lo que estoy haciendo. Sin embargo, copiar y pegar las .styobras es una maravilla.

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