Math & Science ⇒ Sequent calculus

[drbob]

I'm trying to typeset a proof using sequent calculus. I'm using an align* environment, but I can't figure out a way to do lines over each line of the proof, as shown here: http://en.wikipedia.org/wiki/Sequent_ca ... derivation. Does anyone have any ideas about how to achieve this?

This is the code I've got so far, which typesets the proof nicely, apart from the lack of lines.

Code: Select all

\begin{align*}
	P(a) \lseq P(a)			&\qquad	P(b) \lseq P(b)			& \mbox{$\forall{}l$} \\
	\forall x.\, P(x) \lseq P(a)	&\qquad	\forall x.\, P(x) \lseq P(b)	& \mbox{$\land{}r$} \\
	\forall x.\, P(x) &\lseq P(a) \land P(b)				& \mbox{$\limpl{}r$} \\
	&\lseq \forall x.\, P(x) \limpl P(a) \land P(b)
\end{align*}

I've considered \frac, but it would make the LaTeX completely unreadable, which I'd rather avoid. \overline doesn't want to work, and gives the following errors:

! Missing } inserted.
<inserted text>
}
l.250 \end{align*}

! Missing { inserted.
<inserted text>
{
l.250 \end{align*}

! Missing } inserted.
<inserted text>
}
l.250 \end{align*}

! Missing \endgroup inserted.
<inserted text>
\endgroup
l.250 \end{align*}

! Undefined control sequence.
\reserved@b ->\sf@subref

l.250 \end{align*}

! Misplaced \omit.
<recently read> \omit

l.250 \end{align*}

! Missing { inserted.
<inserted text>
{
l.250 \end{align*}

[frabjous]

I recommend doing this with the bussproofs package instead. Some other options are discussed on this page of the LaTeX for Logicians site.

[drbob]

Wow, the bussproofs package is perfect. Thanks!

[localghost]

Now that the problem is solved, please be so kind and mark the topic accordingly as clearly written in Section 3 of the Board Rules (to be read before posting). Please keep that in mind for the future so that further reminders will not be necessary.


Best regards and welcome to the board
Thorsten

[drbob]

Now that the problem is solved, please be so kind and mark the topic accordingly as clearly written in Section 3 of the Board Rules (to be read before posting). Please keep that in mind for the future so that further reminders will not be necessary.

Sorry, done!