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)

Previous page of this mini-guide | Back to proofs page | Home