• The commands
• Usage
• Chaining uses of the rules to build proofs
• Further tricks and tips
• Limitations/unwanted features

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)

Back to proofs page | Home