Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!shelby!msi.umn.edu!cs.umn.edu!ub.d.umn.edu!kpierce
From: kpierce@ub.d.umn.edu (Keith Pierce)
Newsgroups: comp.text.tex
Subject: Typesetting Proofs from Formal Logic
Message-ID: <874@ub.d.umn.edu>
Date: 8 Feb 91 22:12:46 GMT
Sender: kpierce@ub.d.umn.edu
Organization: University of Minnesota, Duluth. Computer Science
Lines: 56

I would like to typeset logical deductions in a format similar to that
displayed in the text SYMBOLIC LOGIC, by R. H. Thomason.  The deductions
look something like this approximation using ASCII text:

Problem: Derive (p => t) from 
	     (p => ((q and r) or (s and t))
         and (r => t)
Proof:

 1  | (p => ((q and r) or (s and t))     hypothesis
 2  | (r => t)                           hypothesis
    |-------
 3  |  | p                               hypothesis
    |  |------
 4  |  | (p => ((q and r) or (s and t))  1, reiteration
 5  |  | ((q and r) or (s and t))        3,4 modus ponens
 6  |  |  | (q and r)                    hypothesis
    |  |  |------
 7  |  |  | r                            6, conj elim
 8  |  |  | (r => t)                     2, reiteration
 9  |  |  | t                            7,8, modus ponens
    |  |
10  |  |  | (s and t)                    hypothesis
    |  |  |-----
11  |  |  | t                            10, conjunction elimination
12  |  | t                               5,6-9,10-11, disj. elimination
13  | (p => t)                           3-12, implication introduction

For those not familiar with the notation: the vertical lines represent
deductions, the horizontal line separates hypotheses for the deduction
from derivations that use the hypotheses.  One can nest subsidiary
deductions, in which temporary hypotheses are made and then dispatched
using the usual Gentzen-type natural deduction rules.

How would you typeset this easily in LaTeX?  I can figure out how to
typeset a deduction that has no subsidiary deductions using LaTeX's
tabular environment, and probably figure out how to write a macro that
generates a line number and automatically increments it.  But how about
the subsidiary deductions?  The format seems to beg for a nested tabular
environment, but then (a) how do you generate the proper line numbers in
the outermost environment, and (b) how do you get the rightmost column
of proof justifications to line up correctly across all deductions?

OK, I'm willing to consider a TeX solution, but would prefer to stay
in LaTeX, or at least use TeX commands that work correctly using
lplain.tex.

Keith Pierce

Keith Pierce, Professor
Department of Computer Science 
University of Minnesota, Duluth
Duluth, MN 55812-2496

internet: kpierce@d.umn.edu
bellnet:  218-726-7194