proof.sty: A User Guide

3. Chaining uses of the rules to build proofs

Suppose we want to set this derivation of one of De Morgan's Laws:

Proceed from the bottom up. So we start

 \infer[^{(2)}] {\neg(\phi \land \psi} {\bot}

Note the use of superscript to generate a small label. Now replace '\bot' with the inference of which it is the conclusion:

 \infer[^{(2)}] {\neg(\phi \land \psi)} {\infer[^{(1)}] {\bot} {(\neg\phi \lor \neg\psi) & \bot & \bot} }

Don't worry about the spacing of the top premiss list. It will automatically adjust as the proof-tree is extended upward. Now again replace the first '\bot' in the premiss-list with the inference of which it is the conclusion:

 \infer[^{(2)}] {\neg(\phi \land \psi)} {\infer[^{(1)}] {\bot} {(\neg\phi \lor \neg\psi) & \infer {\bot} {\phi & \neg\phi} & \bot} }

To put a 'premiss discharge' rule over the negated phi, treat that as an inference from the null list of premisses:

 \infer[^{(2)}] {\neg(\phi \land \psi)} {\infer[^{(1)}] {\bot} {(\neg\phi \lor \neg\psi) & \infer {\bot} {\phi & \infer[^{(1)}] {\neg\phi}{} } & \bot} }

And keep on going in the same way!

Obvious tip: It goes without saying that it is only too easy to lose a vital bracket. So set proofs incrementally as just illustrated, and LaTeX them to check the output every couple of steps (and put the proof initially in a short separate file so you can check the output speedily).

4. Further tricks and tips (next page)