proof.sty: A User Guide

1. The commands

The proof.sty package by Makoto Tatsuta offers four new commands for proof-building:

infer[optional_label]{conclusion}{premiss-list}

infer=[optional_label]{conclusion}{premiss-list}

infer*[optional_label]{conclusion}{premiss-list}

deduce[optional_label]{conclusion}{premiss-list}

Notes:

• The optional label, conclusion and premiss-list are all set in math mode.
• Two or more items in a premiss-list are separated by '&'.
• The conclusion or the premiss-list is allowed to be empty -- so '{}' is allowed as an argument.

2. Usage

Here's a simple use of the basic '\infer' command and its output:

 \infer{B}{A & (A \rightarrow B)}

We can spread out the premiss-list by adding spacing, and can add a (full-size, roman) label as follows:

 \infer[\mathrm{MP}] {B}{A & \quad (A \rightarrow B)}

The '\infer=' command works just the same, but delivers a double rule: hence

 \infer={B \land A}{A \land B)}

The '\infer*' produces four vertical dots rather than a rule: thus

 \infer*{B}{A & (A \rightarrow B)}

Finally, '\deduce' basically behaves like '\infer' except that it doesn't produce any sort of rule. However, if the optional label is present, the label -- or whatever -- appears vertically between the premiss(es) and conclusion: so this might be useful for inserting symbols, thus:

 \deduce[\updownarrow]{B}{A}

3. Chaining uses of the rules to build proofs (next page)