9

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.

enter image description here

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.

enter image description here

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}
Improve this question
2
  • 2
    Welcome to the site. It is far better to provide a complete Minimum Working Example (MWE), starting with \documentclass, including all necessary packages, etc., ending with \end{document}. It saves work for those wishing to help you, and provides additional [often necessary] information.
    – Steven B. Segletes
    Sep 17, 2015 at 15:51
  • You might look at natded. This seems to have facilities somewhat closer to what is needed here, even though designed for (two) different ways of laying out proofs.
    – cfr
    Sep 17, 2015 at 22:46

2 Answers 2

Reset to default
10

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}

enter image description here

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}

enter image description here

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

Improve this answer
1
  • 1
    It is curious that the package doesn't support this given that it claims to support precisely this style of proof in the predicate calculus. At least, it gives this book as an example in the documentation. (I've never seen a proof laid out this way before.) Strange.
    – cfr
    Sep 17, 2015 at 22:34
1

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.

Improve this answer

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .