Rules of inference are (usually) used to infer (deduce) something new from something old, such that if the old is true then so is the new. Our purpose is just the opposite: to reduce something we hope is true to some new thing(s), such that if the new are true, then so is the old. Hence, what we call an "elimination rule" corresponds to what is usually called an "introduction rule," but applied

To illustrate this, let's consider the traditional rule for conjunction ("and") introduction:

P Q ----------- (P and Q)This says that if we have proved P and Q separately, then we are entitled to say we have proved their conjunction P and Q. A better formulation is

A |- P A |- Q ------------------- A |- (P and Q)where A is a set of axioms, and |- indicates first order proof. In our context, we have a

The rule that is usually called conjunction elimination is completely different: it says that if we have proved P and Q, then we are entitled to say we have proved P. This may be written:

A |- (P and Q) ---------------- A |- PUsing such traditional rules in the forward direction gives a

A |= P A |= Q ------------------- A |= (P and Q)where |= indicates semantic entailment, which is defined by satisfaction.

To emphasize the importance of soundness, and to indicate our backwards use of the rule, we will write our conjunction elimination in the form

A |= (P and Q) ----> A |= P and A |= QHowever, "real" proofs (e.g., from textbooks, research papers, lectures and blackboards) in general are neither top down nor bottom up! And reading a proof written in either of these styles can be pretty tedious; a proof is fun (or at least, relatively easier) to read if it is organized to tell a

The rules below are commonly used by our tatami system; they all involve
first order logic, with which we assume some familiarity - see Chapter 8 of the
forthcoming book, *Theorem Proving and Algebra* for a systematic
algebraic exposition of first order logic.

The following rules are treated in the tutorial on universal algebra: