# Logicproof dashed boxes for Natural Deduction

I have been using the Logicproof package to write proofs in Fitch style. It creates environments using tabular to make writing proofs less bothersome.

I can't seem to figure out how to create a dashed box in a subproof as in this example: This is what I have so far. The second subproof should however use a dashed box.

\documentclass{article}
\usepackage{logicproof}
\usepackage{amssymb}

\begin{document}

\begin{logicproof}{2}
\begin{subproof}
\square p \land \square q & assumption\\
\square p & $\land \mathrm{e}_1$ 1\\
\square q & $\land \mathrm{e}_2$ 1\\
\begin{subproof} %This should have a dashed box
p & $\square \mathrm{e}$ 2\\
q & $\square \mathrm{e}$ 3\\
p \land q & $\land \mathrm{i}$ 4, 5
\end{subproof}
\square (p \land q) & $\square \mathrm{i}$ 4--6
\end{subproof}
\square p \land \square q \to \square (p \land q) & $\to \mathrm{i}$ 1--7
\end{logicproof}

\end{document}


Does anyone know if it is possible to create a dashed subproof using logicproof?

If that is not possible how would one go about creating an environment similar to the subproof environment?

Since nobody has answered this in almost a month, I'm going to post my partial solution in the hope that somebody else will take up the challenge.

The package is using a tabular environment, basically, to construct the proof. It uses \cline to draw the horizontal lines. So, if we can substitute dashed lines, we could get half of the problem done.

arydshln supports dashed horizontal and vertical rules in tabular and array environments. So we can substitute its \cdashline{} for the standard \cline{}.

We do this by making a modified copy of logicproof's command \lp@cr@clines, which we call \lp@cr@cdashlines, and a modified copy of logicproof's environment subproof, which we call subproofd. subproofd uses \lp@cr@cdashlines where subproof uses \lp@cr@clines, and \lp@cr@cdashlines uses \cdashline{} where \lp@cr@clines uses cline{}.

The upshot of this is that we can use subproofd in place of subproof to typeset a sub-proof whose box's horizontal lines are dashed rather than continuous. Obviously, the remaining problem is to make the vertical lines of the box dashed. The problem is that arydshln supports vertical dashed rules by providing an alternative to | for tabular/array specifications.

But logicproof does not use this mechanism to draw the vertical lines of its boxes as its standard column specification shows:

 {{r@{~~~}*{#1}{l}@{~}>{$}l<{$}@{~~~~}l@{~}*{#1}{r}}}


Instead, it uses \vline and I'm not sure how to make these dashed in the subproofd environment.

\documentclass{article}
\usepackage{logicproof}
\usepackage{arydshln}
\usepackage{amssymb}
\newcommand*{\nec}{\ensuremath{\mathord{\square}}}
\makeatletter
\newcommand{\lp@cr@cdashlines}{% modified copy of lp@cr@clines
\lp@set@clines%
\lp@orig@arraycr%
\cdashline{\value{lp@cline@1}-\value{lp@cline@2}}%
}
\newenvironment{subproofd}{% modified copy of subproof
\ifthenelse{%
\value{lp@total@nests}>\value{lp@nested}%
}{% All is well; don't do anything.
}{%
\PackageError{logicproof}{Too many nested subproofs!}{%
Increase the maximum number of nested subproofs allowed
in the current logicproof environment.%
}%
}%
\endgroup%
\lp@stop@proof@line%
\lp@orig@arraycr%
\lp@go@up@a@line%
\stepcounter{lp@nested}%
\lp@cr@cdashlines%
&%
\lp@continue@proof@line%
}{%
\ifthenelse{%
0<\value{lp@nested}%
}{% All is well; don't do anything.
}{%
\PackageError{logicproof}{Cannot end a subproof before it begins}{%
You must have a \protect\begin{subproof} before you can use %
\protect\end{subproof}.%
}%
}%
\lp@stop@proof@line%
\lp@cr@cdashlines%
\lp@extend@space%
\lp@start@proof@line%
\begingroup%
\def\@currenvir{subproofd}%
}
\makeatother
\begin{document}

\begin{logicproof}{2}
\begin{subproof}
\nec p \land \nec q & assumption\\
\nec p & $\land \mathrm{e}_1$ 1\\
\nec q & $\land \mathrm{e}_2$ 1\\
\begin{subproofd} %This should have a dashed box
p & $\nec \mathrm{e}$ 2\\
q & $\nec \mathrm{e}$ 3\\
p \land q & $\land \mathrm{i}$ 4, 5
\end{subproofd}
\nec (p \land q) & $\nec \mathrm{i}$ 4--6
\end{subproof}
\nec p \land \nec q \to \nec (p \land q) & $\to \mathrm{i}$ 1--7
\end{logicproof}

\end{document}

• Actually, the problem is even more that the verticals are also being drawn using loops and you'd need to distinguish which level of the loop should get which kind of line, I think. I don't really understand what it is doing, exactly. – cfr Mar 20 '16 at 0:37