Fitch-Style Predicate Logic Proof

Question

I've been attempting to typeset some predicate logic proofs in the style of Huth and Ryan, and I'm having trouble determining how to display declared variables in the same format. Below is an example of one of these proofs.

I've been using the logicproof package to typeset my proofs so far, and this is what I have presently when recreating the above proof.

Does anyone have any insight as to how to declare the variable to the left of the statement?

LaTeX source:

\documentclass{article}
\usepackage{logicproof}

\begin{document}
\begin{logicproof}{1}
    \forall x \, (P(x) \to Q(x)) & premise \\
    \forall x \, P(x) & premise \\
    \begin{subproof}
        P(x_0) \to Q(x_0) & $\forall x \, \mathrm{e}$ 1 \\
        P(x_0) & $\forall x \, \mathrm{e}$ 2 \\
        Q(x_0) & $\to \mathrm{e}$ 3, 4
    \end{subproof}
    \forall x \, Q(x) & $\forall x \, \mathrm{i}$ 3--5
\end{logicproof}
\end{document}

Answer 1

You can increase \subproofhorizspace (the extra pair of braces in my code keep the change local) and then use \llap for the variable:

\documentclass{article}
\usepackage{logicproof}

\begin{document}

{
\setlength\subproofhorizspace{2em}
\begin{logicproof}{1}
    \forall x \, (P(x) \to Q(x)) & premise \\
    \forall x \, P(x) & premise \\\hspace*{-30pt}
    \begin{subproof}
        \llap{$x_0\quad$} P(x_0) \to Q(x_0) & $\forall x \, \mathrm{e}$ 1 \\
        P(x_0) & $\forall x \, \mathrm{e}$ 2 \\
        Q(x_0) & $\to \mathrm{e}$ 3, 4
    \end{subproof}
    \forall x \, Q(x) & $\forall x \, \mathrm{i}$ 3--5
\end{logicproof}
}

\end{document}

The above solution will change the horizontal separation on both sides; if you want individual control, here's one possibility:

\documentclass{article}
\usepackage{logicproof}

\newlength\subproofhorizspaceright
\setlength\subproofhorizspaceright{\subproofhorizspace}
\makeatletter
\renewcommand{\lp@stop@proof@line}{%
  \whiledo{\value{lp@temp}>\value{lp@nested}}{%
    \addtocounter{lp@temp}{-1}%
    \lp@amper%
    \hspace*{\subproofhorizspaceright}%
  }%
  \whiledo{\value{lp@temp}>0}{%
    \addtocounter{lp@temp}{-1}%
    \lp@amper%
    \hspace*{\subproofhorizspaceright}%
    \vline%
  }%
}
\makeatother

\begin{document}

{
\setlength\subproofhorizspace{2em}
\begin{logicproof}{1}
    \forall x \, (P(x) \to Q(x)) & premise \\
    \forall x \, P(x) & premise \\\hspace*{-30pt}
    \begin{subproof}
        \llap{$x_0\quad$} P(x_0) \to Q(x_0) & $\forall x \, \mathrm{e}$ 1 \\
        P(x_0) & $\forall x \, \mathrm{e}$ 2 \\
        Q(x_0) & $\to \mathrm{e}$ 3, 4
    \end{subproof}
    \forall x \, Q(x) & $\forall x \, \mathrm{i}$ 3--5
\end{logicproof}
}

\end{document}

Now there's \subproofhorizspace controlling the space to the left and \subproofhorizspaceright for the space to the right.

Answer 2

The solution of Gonzalo Medina does not work particularly well for nested subproofs. By accident, I discovered that I could solve the problem by simply increasing the depth of nesting sufficiently:

\begin{logicproof}{4}
    \forall x \, (P(x) \to Q(x)) & premise \\
    \forall x \, P(x) & premise \\\hspace*{-30pt}
    \begin{subproof}
        \llap{$x_0\quad$} P(x_0) \to Q(x_0) & $\forall x \, \mathrm{e}$ 1 \\
        P(x_0) & $\forall x \, \mathrm{e}$ 2 \\
        Q(x_0) & $\to \mathrm{e}$ 3, 4
    \end{subproof}
    \forall x \, Q(x) & $\forall x \, \mathrm{i}$ 3--5
\end{logicproof}

I do not know whether this solution is stable or not.